<p>This question has been considered several times in the academic community, from the practical:</p>

<p>Yakushev &amp; Jeuring, <a href="http://www.cogsys.wiai.uni-bamberg.de/aaip09/aaip09_submissions/enumerating.pdf"><em>Enumerating Well-Typed Terms Generically</em></a></p>

<p>Fetsher &amp; <em>al</em>, <a href="http://users.eecs.northwestern.edu/~baf111/random-judgments/random-judgments-esop15.pdf"><em>Making Random Judgments: Automatically Generating
Well-Typed Terms from the Definition of a Type-System</em></a></p>

<p>to the more theoretical</p>

<p>Grygiel &amp; Lescanne, <a href="https://hal.inria.fr/ensl-00740034v1/document"><em>Counting and generating lambda terms</em></a></p>

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

CC BY-SA 3.0
2016-08-22T13:08:25.640Z
Is the Fetsher et al algorithm complete? It's a random generator.
Martin Berger
CC BY-SA 3.0
2016-08-22T13:54:08.800Z
there was another recent paper on this from Paul Tarau: http://arxiv.org/abs/1608.03912
Noam Zeilberger
CC BY-SA 3.0
2016-08-22T21:46:13.410Z
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
CC BY-SA 3.0
2016-08-22T11:54:01.960Z
2016-08-22T11:54:01.960Z
cody
<p>How can I enumerate all <a href="https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus" rel="nofollow noreferrer">simply typed lambda terms</a> which have a specified type?</p>

<p>More precisely, suppose we have the simply typed lambda calculus augmented with numerals and iteration, as described in <a href="https://cstheory.stackexchange.com/questions/15038/combinators-for-the-primitive-recursive-functions/15041#15041">this answer</a>. How can I enumerate all lambda terms of type N (natural number)?</p>

<p>For example, the first few lambda terms of type N are</p>

<pre><code>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
</code></pre>

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

CC BY-SA 3.0
2016-08-22T14:02:03.530Z
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?
Noam Zeilberger
CC BY-SA 3.0
2016-08-22T19:07:01.440Z
@NoamZeilberger I am trying to find the smallest simply typed function that returns a natural number or a sequence of natural numbers.
user76284
CC BY-SA 3.0
2016-08-22T19:43:26.077Z
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.
Noam Zeilberger
<ds.algorithms><co.combinatorics><lambda-calculus><combinatorics><typed-lambda-calculus>
Enumerating all simply typed lambda terms of a given type
user76284
# Enumerating all simply typed lambda terms of a given type

(Asked by: username_0 on 2016-08-22)

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?

**Tags:** ds.algorithms, co.combinatorics, lambda-calculus, combinatorics, typed-lambda-calculus

> **Comments:**
> **username_1**: 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?  
> **username_0**: @NoamZeilberger I am trying to find the smallest simply typed function that returns a natural number or a sequence of natural numbers.  
> **username_1**: 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.  

---

## 1 answers

### Answer by username_2 on 2016-08-22. Score: 6 | Accepted answer

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

Yakushev & Jeuring, [*Enumerating Well-Typed Terms Generically*](http://www.cogsys.wiai.uni-bamberg.de/aaip09/aaip09_submissions/enumerating.pdf)

Fetsher & *al*, [*Making Random Judgments: Automatically Generating
Well-Typed Terms from the Definition of a Type-System*](http://users.eecs.northwestern.edu/~baf111/random-judgments/random-judgments-esop15.pdf)

to the more theoretical

Grygiel & Lescanne, [*Counting and generating lambda terms*](https://hal.inria.fr/ensl-00740034v1/document)

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.

> **Comments:**
> **username_3**: Is the Fetsher et al algorithm complete? It's a random generator.  
> **username_1**: there was another recent paper on this from Paul Tarau: http://arxiv.org/abs/1608.03912  
> **username_2**: 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.  

---

