# lambda-calculus

## 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 ↠_{β} u_{1} and t ↠_{β} u_{2},
there exists such v that: u_{1} ↠_{β} v and u_{2} ↠_{β} 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 -
〈t_{1}, t_{2}〉, π_{1} and π_{2} and two
β-reduction rules - π_{i}〈t_{1}, t_{2}〉→_{β} t_{i}.

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 t_{1}t_{2}) ↠_{β}t_{i}) - 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.