The untyped lambda calculus

Reading: TAPL Chapter 5.1.

Syntax

The syntax of the λ-calculus is simple:

t ::= x       variable
      λx. t   abstraction
      t t     application

Two rules to remember about the concrete syntax:

• The body of an abstraction extends as far right as possible: λx. t1 t2 ≡ λx. (t1 t2).

• Application is left-associative: t1 t2 t3 ≡ (t1 t2) t3.

If a variable occurrence x sits outside any abstractions λx. t, it is free; otherwise, it is bound. A bound variable occurrence x is bound by the smallest enclosing λx, which is called its binder. (In computer programming, we would say that the inner λx shadows the outer λx.) For example, in (λx. x (λx. x)) (u r) (p. 56), the two occurrences of x have different binders; we can draw lines to make it clear which variable occurrences are bound by which binders (known as a Stoy diagram):

(λx. x (λx. x)) (u r)
  └──┘   └──┘

Renaming a λx, and all the occurrences of x that it binds, to a fresh (= not already used) variable name is called α-conversion, and if two terms that can be α-converted to the same term (that is, they are α-equivalent), we consider them just to be the same term (Convention 5.3.4). So, for example,

(λx. x (λx. x)) (u r) ≡ (λy. y (λz. z)) (u r)

Semantics (informal)

Lambda terms are functions and behave roughly like you’d expect functions to behave. To evaluate a closed λ-term (that is, a λ-term with no free variables),

• To evaluate an abstraction λx. t, do nothing.

• To evaluate an application t1 t2:

  1. Evaluate t1 to get a value λx. t12.
  2. Evaluate t2 to get a value t2.
  3. Finally, β-reduce (λx. t12) t2.

This is called call-by-value evaluation. Other evaluation strategies are discussed in More about evaluation.

To β-reduce (λx. t12) t2 means to substitute t2 into every occurrence of x that is bound by the λx. In the example above, the operand (u r) should only be substituted into the occurrences of x that are bound by the first λx:

(λx. x (λx. x)) (u r)
  └──┘   └──┘
⟶ u r (λx. x)
          └──┘

Capture-avoiding substitution

Here’s another example of β-reduction that has a pitfall:

  ┌──────┐
(λx. λy. x y) (y z)
      └────┘ 
⟶ λy. y z y         bad!
     └──────┘

This last term is bad because the line and the variable names do not agree: there’s an occurrence of y that is not connected by a line to the nearest enclosing λy.

This problem is called variable capture. Avoiding it is treated in Section 5.3, but the short story is that you should first α-convert y to a new name, say, w.

(λx. λy. x y) (y z)
= [x↦y z](λy. x y)   problem: y occurs free in (y z)
= [x↦y z](λw. x w)   first α-convert
= λw. y z w           then apply substitution to body

Equivalence

We’ve seen α-equivalence already, but sometimes we will want to know whether two terms, even if they aren’t α-equivalent, are “behaviorally equivalent” (p. 64), a.k.a. observationally equivalent. For example, λx. (λy. y) x and λx. (λy. x) z aren’t identical, but behave the same in the sense that they evaluate to the same thing when applied to an argument. For a proper definition of behavioral equivalence, see More about equality. For our purposes, it probably suffices to say that, in order to show that two terms are behaviorally equivalent, we are allowed to perform β-reductions inside abstractions. We call this βᵥ-reduction and write t ⟶v t' if t βᵥ-reduces to t'. For example, λx. (λy. y) x and λx. (λy. x) z are behaviorally equivalent, because they βᵥ-reduce to the same thing:

λx. (λy. y) x ⟶v λx. x
λx. (λy. x) z ⟶v λx. x