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)

The record is currently split across three related terms, known as Alpha, Beta, and Gamma, which all have Fokker size seven. It is not known how Alpha was constructed, but Beta and Gamma were discovered via brute-force search.

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

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

K = A(AA)(A(AA)AAAAA)
B = A(A(A(A(AA)A))(AA)A)(A(A(AA)))
C = A(A(A(AA)(AA)(A(AA)A))A)AA
W = AA(A(A(AA)A))
S = A(A(AA(AA(AA))(A(A(AA(AA))))))AA

Construction (Beta). There is a complete closed λ-term of Fokker size seven. (User:Blashyrkh, 2026)

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

K = β(β(β(β(βββ))β)β)ββ
B = ββ(β(β(ββββ)ββ))(β(β(β(βββ))β))β
C = β(β(ββ(β(β(βββ))))ββ)β(β(β(ββ)β)ββ)
W = ββ(β(ββ)(β(β(ββ)β)β)ββ)
S = β(β(β(βββ))(ββ))β(β(β(β(β(βββ)))(β(βββ)β)β)β)

Construction (Gamma). There is a complete closed λ-term of Fokker size seven. (Blashyrkh, 2026)

γ = λx.λy.λz.yz(x(λw.z))

K = γ(γ(γ(γγ)(γγ)γ)(γγγ(γγ))γ)γ
S = γγγ(γγ(γγ)γ)γ(γ(γ(γγ(γ(γ(γγ)(γγ))))))

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)

Open question. What is the smallest complete closed λ-term in terms of Fokker size? It is at least three and at most seven.