5
$\begingroup$

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?

Improve this question
$\endgroup$
3
  • $\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$
    – Noam Zeilberger
    Commented 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
    Commented 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$
    – Noam Zeilberger
    Commented Aug 22, 2016 at 19:43

1 Answer 1

Reset to default
6
$\begingroup$

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.

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