Untyped Lambda Calculus (Topic 15)

Implementation of untyped lambda calculus with de Bruijn indices in Lean and proof of Omega and Y combinator properties.

Logic.lean contains the full implementation and proofs.

Representation

Untyped lambda calculus terms are represented using an inductive type Term, with variables, abstractions, and applications.

Single-step beta reduction, many-step beta reduction, and beta equivalence (beta, beta_star, beta_eq) are defined as inductive relations, which are represented in the type system as functions from terms to propositions.

Some syntax sugar is defined to simplify writing terms. For example, the Y combinator is defined as λ ((λ (1 @ (0 @ 0))) @ (λ (1 @ (0 @ 0)))).

This uses:

• the custom notation λ for the lambda abstraction constructor
• the infix operator @ for application
• an instance of the OfNat typeclass to implicitly convert number constants to variable terms without explicitly writing var

de Bruijn Indices

Variables are represented using de Bruijn indices, which specify the number of lambda abstractions to skip to find the binder of the variable. This simplifies substitution and removes the need for variable names.

Ω Combinator Ω = (λx.xx)(λx.xx) | Ω = (λ (0 @ 0)) @ (λ (0 @ 0))

Omega reduces to itself in a single beta reduction step, as shown in Omega_proof. It serves as a simple proof that untyped lambda calculus computations are not guaranteed to terminate.

A many-step version Omega_proof_star is then derived using the trivial to_star helper, although it could also be proven with reflexivity (but that is not the point of the exercise).

Y Combinator Y = λf.(λx.f(xx))(λx.f(xx)) | Y = λ ((λ (1 @ (0 @ 0))) @ (λ (1 @ (0 @ 0))))

The Y combinator is used for defining recursive functions in pure lambda calculus, and is commonly used to prove that untyped lambda calculus can express all Turing-computable functions.

In simply typed lambda calculus, which forbids the Y-combinator, only primitive recursive functions can be expressed.

I was unable to prove the Y combinator beta reduction theorem as stated in the requirements, and it doesn't actually seem possible. The proof would require reversing a reduction step, which is not valid for many-step beta reduction.

An alternate combinator that would satisfy the original many-step reduction requirement is the Θ Turing fixed-point combinator Θ = (λx.λf.f(xxf))(λx.λf.f(xxf)), where Θ f ↠β f (Θ f), instead of only Y f =β f (Y f).

Instead I proved beta equivalence of (Y f) and (f (Y f)), as shown in Y_fixed_point; they both reduce to the same term (f T), which then reduces to (f (f T)), (f (f (f T))), and so on.

Several sub-proofs are involved which are combined to obtain the final result.

A lemma is proven to show that (subst k s (lift k t)) = t (i.e. lifting prevents t from being affected by substitution), which is used to cancel out substitution and lifting around f during the sub-proof that T reduces to (f T).