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

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?

  • $\begingroup$ 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? $\endgroup$ Aug 22, 2016 at 14:02
  • $\begingroup$ @NoamZeilberger I am trying to find the smallest simply typed function that returns a natural number or a sequence of natural numbers. $\endgroup$
    – user76284
    Aug 22, 2016 at 19:07
  • $\begingroup$ 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. $\endgroup$ Aug 22, 2016 at 19:43

1 Answer 1


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

Yakushev & Jeuring, Enumerating Well-Typed Terms Generically

Fetsher & al, Making Random Judgments: Automatically Generating Well-Typed Terms from the Definition of a Type-System

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.

  • $\begingroup$ Is the Fetsher et al algorithm complete? It's a random generator. $\endgroup$ Aug 22, 2016 at 13:08
  • 1
    $\begingroup$ there was another recent paper on this from Paul Tarau: arxiv.org/abs/1608.03912 $\endgroup$ Aug 22, 2016 at 13:54
  • $\begingroup$ 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. $\endgroup$
    – cody
    Aug 22, 2016 at 21:46

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.