# Enumerating all simply typed lambda terms of a given type

How can I enumerate all simply typed lambda terms which have a specified type?

More precisely, suppose we have the simply typed lambda calculus augmented with numerals and iteration, as described in this answer. How can I enumerate all lambda terms of type N (natural number)?

For example, the first few lambda terms of type N are

zero
succ zero
succ (succ zero), K zero zero
succ (succ (succ zero)), K zero (suc zero), K (suc zero) zero, iter zero suc zero


and so on. How can I systematically continue this pattern, while ensuring that only well-typed terms are generated?

• Perhaps you could add a bit more explanation about what exactly are your motivations/which problem are you trying to solve? There can be infinitely many terms of a given simple type (as in your example): are you trying to get a bound on the number of ($\alpha$-equivalence classes of) terms of a given size, or just trying to list them...or something else? Aug 22, 2016 at 14:02
• @NoamZeilberger I am trying to find the smallest simply typed function that returns a natural number or a sequence of natural numbers. Aug 22, 2016 at 19:07
• So you mean something like an analogue of Kolmogorov complexity relative to simply typed lambda calculus/System T? That's an interesting question, but I suspect it's going to be very hard to compute even restricted to STLC without iteration, since normalization has non-elementary complexity. Aug 22, 2016 at 19:43

This question has been considered several times in the academic community, from the practical:

Yakushev & Jeuring, Enumerating Well-Typed Terms Generically

to the more theoretical

Grygiel & Lescanne, Counting and generating lambda terms

Implementations can pretty easily be found online. I didn't find any that addressed a system with iterators per se, but it shouldn't be a stretch from what already exists.

• Is the Fetsher et al algorithm complete? It's a random generator. Aug 22, 2016 at 13:08
• there was another recent paper on this from Paul Tarau: arxiv.org/abs/1608.03912 Aug 22, 2016 at 13:54
• The Fetsher & al paper does not say anything about the completeness of their approach, though a quick overview tends to suggest that every term is generated with probability 1.
– cody
Aug 22, 2016 at 21:46