Untyped lambda-calculus

Assuming infinite (countable) set Variable of variables (x, y, …), Term (t, u, …) is:

  • Variable or
  • λ Variable . Term (abstraction) or
  • Term Term (application)

Conventions:

  • application associates to the left: tuv means (tu)v;
  • application binds stronger than the abstraction: λx.xy means λx.(xy);
  • abstractions can be grouped: λxyz.xz(yz) means λx.λy.λz.xz(yz).

Variable x in λx.t is bound; variable than is not bound is free; term with no free variables is closed.

χ-reduction is the least binary relation on terms such that when t →χ t’ then also:

  • λx.t →χ λx.t’ (ξ-reduction);
  • tu →χ t’u (congruence);
  • ut →χ ut’ (congruence)

and:

  • α-reduction: λx.t →α λy.t’, where t’ is t with all free occurrences of x renamed to y;
  • β-reduction: (λx.t)u →β t’, where t’ is t with all free occurrences of x replaced by u (substitution, t[u/x]);
  • η-reduction (extensionality): λx.t →η t.

if t →χ u, t is a χ-redex; χ-expansion is a relation opposite to →χ; ↠χ (multi-step reduction; reduction path) is the reflexive and transitive closure of →χ; ＝χ (χ-equivalence, χ-convertability) is the symmetric closure of ↠χ.

Term that can not be reduced is in normal form (a value). Term t is weekly normalizing if there exist a normal form u such that t ↠β u. Term is strongly normalizing when every sequence of reductions will eventually produce a normal form. Not all terms a strongly normalizing (for example, Ω = (λx.xx)(λx.xx) reduces to itself), but (confluence, Church-Rosser property): if t ↠β u1 and t ↠β u2, there exists such v that: u1 ↠β v and u2 ↠β v.

When substituting a term for a bound variable, care needs to be taken not to accidentally “capture” a variable that is free in that term. This is a great pain for the implementers (who can’t just say that terms are equivalence classes by ＝α), and various tricks were developed to ease it (de-Brujin indices, Barendregt convention); we will say no more about it, and just assume that before substitution all variables that need to be distinct are given fresh names :)

Encodings

We can (and eventually will) extend the calculus by adding new term forms together with the corresponding reduction rules. For example, for products, we can add three forms of terms - 〈t1, t2〉, π1 and π2 and two β-reduction rules - πi〈t1, t2〉→β ti.

It is also possible to just encode common types and data structures in the untyped lambda calculus:

  • identity: I = λx.x
  • booleans: T = λxy.x; F = λxy.y
  • if-then-else: if = λbxy.bxy (if T t u ↠β t; if F t u ↠β u)
  • logical operations: and = λxy.xyF; or = λxy.xTy; nor = λx.xFT;
  • product and projections: pair = λxyb. if b x y; π1 = λp.pT; π2 = λp.pF (πi(pair t1 t2) ↠β ti)
  • Church numerals: n = λfx.f(f(…(fx))) where f is applied n times; 0 = λnfx.x
  • succ = λnfx.f(nfx)
  • add = λmnfx.m succ n; mul = λmnfx.m (add n) 0; exp = λmn.n (mul m) 1
  • iszero = λnxy.n(λz.y)x
  • pred = λnfx.n(λgh.h(gf))(λy.x)(λy.y)
  • sub = λmn.n pred m
  • leq = λmn.iszero (sub m n)

Fixed points

u is a fixed point of term u if t u ↠β u; in lambda-calculus, every term has a fixed point, and there is a term Y (fixed point combinator) such that Yt is a fixed point of t! For example:

  • Curry fixed point combinator: Y = λf.(λx.f(xx))(λx.f(xx))
  • Turing fixed point combinator: ϴ = (λfx.x(ffx))(λfx.x(ffx))

(Fixed point combinator is the Russel paradox in disguise when terms are read as predicates, λx.t is read as {x | t}, and tu is read as u ∈ t.)

Functions definable in lambda-calculus are precisely the recursive ones (Kleene theorem).

Reduction strategies

Orders on redexes:

  • all the redexes of t and u are inside the redex (λx.t)u;
  • all the redexes of t are to the left of all the redexes of u in tu.

Reduction strategy determines the order in which the redexes in a term get reduced:

  • innermost (=call by value) (outermost (=call by name)) strategy selects the most inside (outside) redexes;
  • left (right) strategy selects the the most left (right) redexes.
  • week strategy never reduces abstractions λx.t, even if there are redexes in t;
  • left strategy is head if it never reduces variable applications x t1 … tn even if some ti has redexes.
  • normal order strategy is leftmost outermost; it is normalizing: if the term has a normal form, this strategy will find it (standardization theorem).

Combinatory logic

All λ-terms can be built (up to β-equivalence) from just three combinators, thus avoiding variables, α-conversion and all that, and formulating β-reduction directly on the combinators:

  • I = λx.x (using a variable);
  • S = λxyz.(xz)(yz) (duplicating a variable);
  • K = λxy.x (erasing a variable).

Actually, just S and K suffice as the “basis” of the λ-calculus, since I = S K K.

Indeed, one combinator is sufficient: ι = λx.xSK; we can then define: I = ιι; K = ι(ι(ιι)); S = ι(ι(ι(ιι))). So, every λ-term can be encoded as a binary word ;)

Besides being cute, nameless (combinator-based) representations of λ-terms are used in implementation of functional programming languages. But people normally do not program in it.

Models

Setting aside combinatory algebra models, classic model of the untyped lambda calculus uses domains, where the conundrum of D≅D⇒D resulting from the fact that in untyped lambda calculus everything is a function and anything can be applied to anything gets resolved by considering monotone/continuous functions.

Problems

Encoding everything is not an approach suitable for human programmers.

Some properties of the untyped lambda-calculus contradict intuitions about functions:

  • everything can be applied to everything (including itself);
  • everything has a fixed point;
  • a term is not guaranteed to have a normal form (some calculations get stuck).

The main problem is that since there is only one type, and propositions are types, it is impossible to express any properties of the functions being defined. We need to introduce types - starting with the simple ones.

Simply typed lambda-calculus

TODO

Bibliography

[Mim20] “Program ＝ Proof”, Mimram, 2020.

[SU06] “Lectures on the Curry-Howard Isomorphism”, Sorensen & Urzyczyn, 2006.

[Sel13] “Lecture notes on the lambda calculus”, Selinger, 2013.

[Bar84] “The Lambda Calculus: Its Syntax and Semantics”, Barendregd, 1984.

[ML20] “How did ‘judgement’ come to be a term of logic?”, Per Martin Löf, 2020.

[NG14] “Type Theory and Formal Proof”, Nederpelt & Geuvers, 2014.

[Sch24] “Uber die Bausteine der mathematischen Logik”, Schonfinkel, 1924.

[SS71] “Toward a Mathematical Semantics for Computer Languages”, Scott & Strachey, 1971.