Examine individual changes

'<blockquote> A ''combinator'' is a closed λ-term. ~ J. Fokker, 1992<ref name="fokker">Jeroen Fokker. 1992. The systematic construction of a one-combinator basis for Lambda-Terms. Form. Asp. Comput. 4, Suppl 1 (Nov 1992), 776–780. https://doi.org/10.1007/BF03180572</ref> </blockquote> 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 == {{stub}} == 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)<ref name="statman">Rick Statman. 2005. Two variables are not enough. In Proceedings of the 9th Italian conference on Theoretical Computer Science (ICTCS'05). Springer-Verlag, Berlin, Heidelberg, 406–409. https://doi.org/10.1007/11560586_32</ref> == 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)<ref>A. Church, “Carew A. Meredith. Single axioms for the systems (C, N), (C, O) and (A, N) of the two-valued propositional calculus. The journal of computing systems, vol. 1 no. 3 (1953), pp. 155–164.,” Journal of Symbolic Logic, vol. 19, no. 2, pp. 143–144, 1954. doi:10.2307/2268913</ref><ref name="fokker" /> '''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. ([[Chris Barker|Barker]], 2001) λf.f(λx.λy.λz.xz(yz))(λx.λy.x) '''Construction (Alpha).''' There is a complete closed λ-term of Fokker size seven. ([[John Tromp|Tromp]] & [[User:mtve|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) == References == <references />'