3
$\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?

$\endgroup$
  • $\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 Aug 22 '16 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 '16 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 Aug 22 '16 at 19:43
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.

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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