Notes:Lambda calculus

This is a NOTES page, so it isn't an actual page in the wiki yet!

Lambda terms

We define $\lambda$-terms as follows:
Let the following be given:

• Variables: an infinite sequence of expressions, $v_1,\ldots,v_n\ldots$
• Atomic constants: a sequence of expressions again, that may also be finite or empty

The set of expressions called $\lambda$-terms is defined inductively as follows:

1. All variables and atomic constants are $\lambda$-terms
   • These are known as atoms
2. If $M$ and $N$ are $\lambda$-terms then $(MN)$ is a $\lambda$-term
   • Known as applications
   • this is a short hand for $M(N)$ in our modern terminology
3. If $M$ is any $\lambda$-term and $x$ any variable then $(\lambda x.M)$ is a $\lambda$-term
   • Any such expression is called an abstraction

Examples

• $(\lambda v_0.(v_0v_{00}))$ - a function that $x\mapsto x(v_{00})$ I think

Here $x$, $y$ and $z$ are distinct variables:

• $(\lambda x.(xy))$ - a function that $x\mapsto x(y)$ I think
• $((\lambda y.y)(\lambda x.(xy)))$ - This is difficult to put into words, but simply results in the function that $x\mapsto x(y)$
• $(x(\lambda x.(\lambda x.x)))$ - This is nasty, it looks like $x(x)$
• $(\lambda x.(yz))$ 'constant' function that $x\mapsto y(z)$

Notations

• Capital letters denote arbitrary $\lambda$- terms
• $x,y,z,u,v,w$ will denote variables
• Brackets will be skipped where it is understood that things are left associative, that is:
  • $MNPQ$ is understood to mean $(((MN)P)Q)$ (which to us means: $((M(N))(P))(Q)$ - you can see why this notation is dropped!)
• $(\lambda x.(PQ))$ will become $\lambda x.PQ$
• $(\lambda x_1.(\lambda x_2.(\ldots(\lambda x_n.M)\ldots))).$ becomes $\lambda x_1x_2\ldots x_n.M$
• Syntatic identity will be denoted by $\equiv$, so $M\equiv N$ will mean that $M$ is exactly the same term as $N$

Length of a term

The length of a term $M$ is denoted $\text{lng}(M)$ and is the total number of occurrences of atoms in $M$

Occurs in

See page 6 of

Scope

(This is similar to scopes in programming languages)
For a particular occurrence of $\lambda x.M$ in a $\lambda$-term $P$, the occurrence of $M$ is called the scope of the occurrence of $\lambda x$ immediately to the left.

Free and bound variables

An occurrence of a variable $x$ in a term $P$ is called:

• Bound if it is in the scope of a $\lambda x$ in $P$
• Bound and binding if and only if it is the $x$ in $\lambda x$
• Free otherwise.

In addition:

• If $x$ has at least one binding occurrence in $P$ we call it a bound variable of $P$
  • This requires thought but once it clicks it should be obvious, any variable that is a parameter of a function is a bound variable (at some point, even if unused)
• If $x$ has at least one free occurrence in $P$ we call it a free variable of $P$
• We denote the set of free variables of $P$ as: $\text{FV}(P)$

Substitution

For any $M$, $N$ and $x$ define:

• $[N/x]M$ as the result of substituting $N$ for every free occurrence of $x$ in M, and changing the bound variables to avoid name clashes.

The exact definition is given inductively as follows

1. $[N/x]x \equiv N$
2. $[N/x]a \equiv a$ for all atoms $a\not\equiv x$
3. $[N/x](PQ)\equiv ([N/x]P[N/x]Q)$
4. $[N/x](\lambda x.P)\equiv \lambda x.P$
   • This demonstrates scoping well, even if $x$ occurs in $P$ it's bound already, and not free.
5. $[N/x](\lambda y.P)\equiv \lambda y.P$ if $x\not\in\text{FV}(P)$
6. $[N/x](\lambda y.P)\equiv \lambda y.[N/x]P$ if $x\in\text{FV}(P)$ and $y\not\in\text{FV}(N)$
7. $[N/x](\lambda y.P)\equiv \lambda z.[N/x][z/y]P$ if $x\in\text{FV}(P)$ and $x\in\text{FV}(N)$ where $z$ is the first variable $\not\in\text{FV}(NP)$

Note:

• For the last 3 we assume that $x\not\equiv y$