Closed lambda term

A combinator is a closed λ-term. ~ J. Fokker, 1992

In lambda calculus, a closed lambda-term, closed λ-term, or generalized combinator is a term with at least one abstraction and no free variables or constants. Closed terms represent self-contained computations and have many useful purposes throughout computer science.

Via lambda calculus

A term of lambda calculus is closed when it does not have any free variables or constants. In a certain sense, this is one condition, not two. For example, consider the following non-closed term:

λx.c

This term has a constant c, or equivalently has a free variable c. In either case, this term must be interpreted within a context or environment which provides the value of c. Put another way, closed λ-terms are precisely the λ-terms which do not change when the context changes around them.

A closed term may discard bound variables. For example, the following common term, which expresses the K combinator, binds x and y but only uses x:

λx.λy.x

A closed term may also use variables more than once. For example, Turing's term uses one argument twice:

λx.xx

A lambda term is closed if and only if it has a De Bruijn indexing; any free variables or constants cannot be assigned De Bruijn indices.

Via combinators

Closed lambda terms generalize combinatory logic.

Theorem. Every combinator can be written as a closed lambda term in normal form.

To do this, merely write the combinator out at full rank and then transform its parameters into λ-abstractions. For example, considering the S combinator:

S x y z = x z (y z);

The corresponding closed lambda term is:

λx.λy.λz.xz(yz)

Size

The Fokker size of a closed term is the number of abstractions and applications it contains when written in normal form. For example, the normal form of K is:

λx.λy.x

So the Fokker size of K is two.

Every closed term can be simplified to have a minimal Fokker size. In particular, the number of abstractions is bounded when written this way.

Theorem. Every closed λ-term is beta-convertible to a closed λ-term with at most three bound variables. (Statman, 2005)

Completeness

A basis set of closed terms is complete if its closure under composition includes every closed term. In the common case where one term will suffice, a closed term is complete if every other closed term can be built from it using composition alone.

Construction (Meredith's basis). There is a complete closed λ-term of Fokker size 74. (Meredith, 1963)

Construction. There is a complete closed λ-term of Fokker size 23. (Böhm)

Construction. There is a complete closed λ-term of Fokker size 18. (Barendregt, 1971)

Construction. There is a complete closed λ-term of Fokker size 14. (Rosser)

Construction. There is a complete closed λ-term of Fokker size 12. (Fokker, 1992)

λf.f(λx.λy.λz.xz(yz))(λx.λy.λz.x)

Construction (Iota). There is a complete closed λ-term of Fokker size 11. (Barker, 2001)

λf.f(λx.λy.λz.xz(yz))(λx.λy.x)

Construction (Alpha). There is a complete closed λ-term of Fokker size seven. (Tromp & mtve)

λx.λy.λz.xz(y(λw.z))

One obstruction to completeness is the above theorem of Statman, which shows that some closed terms cannot be built without a certain number of abstractions.

Corollary. A complete basis must have at least one closed λ-term with at least three bound variables; there is no complete closed λ-term of Fokker size two. (Statman, 2005)