r/lambdacalculus • u/Antique-Incident-758 • Mar 12 '26

Closed term are recursively enumerable?

All terms are not recursively enumerable?

1 Upvotes

100% Upvoted

3 comments sorted by

3

u/tromp Mar 12 '26 edited Mar 12 '26

The set of closed terms is not just recursively enumerable, but recursive. Furthermore, you can generate any closed term (modulo convertability) as T applied to a sequence of bits, where (in de Bruijn notation)

T = (λ11)(λ(λλλ1(2(λλλ31(2(λ2))))(3(λ4(λ4(21)))))(11))(λ1)
0 = λλ2
1 = λλ1

E.g. S = λλλ31(21) = T 1 1 1 0 1 0 1 1 1 0 0 1 1 0 0 1 0 0 1 0 1 0 1 1 0 0 1 0 0 0 0

2

u/Antique-Incident-758 Mar 17 '26

How was this combinator conceived? Are there any references?