Notes:Lambda calculus

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

Lambda terms

We define [ilmath]\lambda[/ilmath]-terms as follows:
Let the following be given:

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

The set of expressions called [ilmath]\lambda[/ilmath]-terms is defined inductively as follows:

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

Examples

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

Here [ilmath]x[/ilmath], [ilmath]y[/ilmath] and [ilmath]z[/ilmath] are distinct variables:

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

Notations

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

Length of a term

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

Occurs in

See page 6 of

Scope

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

Free and bound variables

An occurrence of a variable [ilmath]x[/ilmath] in a term [ilmath]P[/ilmath] is called:

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

In addition:

• If [ilmath]x[/ilmath] has at least one binding occurrence in [ilmath]P[/ilmath] we call it a bound variable of [ilmath]P[/ilmath]
  • 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 [ilmath]x[/ilmath] has at least one free occurrence in [ilmath]P[/ilmath] we call it a free variable of [ilmath]P[/ilmath]
• We denote the set of free variables of [ilmath]P[/ilmath] as: [ilmath]\text{FV}(P)[/ilmath]

Substitution

For any [ilmath]M[/ilmath], [ilmath]N[/ilmath] and [ilmath]x[/ilmath] define:

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

The exact definition is given inductively as follows

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

Note:

• For the last 3 we assume that [ilmath]x\not\equiv y[/ilmath]