Lambda Calculus Generator

I don't know where else to ask this question, I hope this is a good place.

I'm just curious to know if its possible to make a lambda calculus generator; essentially, a loop that will, given infinite time, produce every possible lambda calculus function. (like in the form of a string).

Since lambda calculus is so simple, having only a few elements to its notation I thought it might be possible (though, not very useful) to produce all possible combinations of that notation elements, starting with the simplest combinations, and thereby produce every possible lambda calculus function.

Of course, I know almost nothing about lambda calculus so I have no idea if this is really possible.

Is it? If so, is it pretty straightforward like I've envisioned it, or is it technically possible, but so difficult that it is effectively impossible?

PS. I'm not talking about beta-reduced functions, I'm just talking about every valid notation of every lambda calculus function.

Sure, this is a standard encoding exercise.

First of all, let $p : \mathbb N^2 \to \mathbb N$ any bijective computable function, called a pairing function. A standard choice is

$$
p(n,m) = \dfrac{(n+m)(n+m+1)}{2}+n
$$

One can prove that this is a bijection, so given any natural $k$, we can compute $n,m$ such that $p(n,m)=k$.

To enumerate lambda terms, fix any enumeration for variables names: $x_0,x_1,x_2,\ldots$.

Then, for each natural number $i$, print $lambda(i)$, defined recursively as follows:

• if $i$ is even, let $j=i/2$ and return variable $x_j$

• if $i$ is odd, let $j=(i-1)/2$

• if $j$ is even, let $k=j/2$ and find $n,m$ such that $p(n,m)=k$; compute $N=lambda(n), M=lambda(m)$; return application $(NM)$

• if $j$ is odd, let $k=(j-1)/2$ and find $n,m$ such that $p(n,m)=k$; compute $M=lambda(m)$; return abstraction $(\lambda x_n.\ M)$

This program is justified by the following "algebraic" bijection involving the set of all lambda terms $\Lambda$:

$$
\Lambda \simeq \mathbb N + (\Lambda^2 + \mathbb N \times \Lambda)
$$

which is read as "the lambda terms, syntactically, are the disjoint union of 1) variables (represented as a natural), 2) applications (made by two lambda terms), and 3) abstraction (a pair variable/natural + lambda term)".

Given that, we recursively apply computable bijections $\mathbb N^2 \simeq \mathbb N$ (i.e. the function $p$) and $\mathbb N + \mathbb N \simeq \mathbb N$ (the standard even/odd one) to obtain the algorithm above.

This procedure is general, and will work on almost any language generated through a context-free grammar, which will provide a similar isomorphism to the one above.

StackExchange Computer Science Q#97539, answer score: 24