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.


5 Answers 5


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.

  • $\begingroup$ Wow, thanks, is it possible you could represent this is pseudo code? I'd definitely understand that better as I don't have a cs degree. $\endgroup$
    – MetaStack
    Commented Sep 20, 2018 at 10:36
  • 3
    $\begingroup$ @LegitStack Well, the above is pseudo-code :) You can define a recursive function $lambda(n)$ and then use if n%2==0 .... The only nontrivial step is finding $n,m$ such that $p(n,m)=k$: this can be done by trying all pairs $n,m$ with $n,m\leq k$ (faster algorithms also exist) $\endgroup$
    – chi
    Commented Sep 20, 2018 at 12:19
  • 1
    $\begingroup$ Indeed, per Wikipedia, the inverse of this particular pairing function can be found via $a=\left\lfloor\frac12(\sqrt{8k+1}-1)\right\rfloor,b=\frac12a(a+1),n=b-k,m=a-n$. $\endgroup$ Commented Sep 20, 2018 at 23:12

As has been mentioned, this is just enumerating terms from a context free language, so definitely doable. But there's more interesting math behind it, going into the field of analytical combinatorics.

The paper Counting and generating terms in the binary lambda calculus contains a treatment of the enumeration problem, and a lot more. To make things simpler, they use something called the binary lambda calulus, which is just an encoding of lambda terms using De Bruijn indices, so you don't have to name variables.

That paper also contains concrete Haskell code implementing their generation algorithm. It's definitely effectively possible.

I happen to have written an implementation of their approach in Julia.


Yes. Take something that enumerates all possible ASCII strings. For each output, check if it is a valid lambda calculus syntax that defines a function; if not, skip it. (That check can be done.) That enumerates all lambda calculus functions.

  • 5
    $\begingroup$ Essentially, all problems like this are solved by invoking the typing monkey... $\endgroup$
    – xuq01
    Commented Sep 20, 2018 at 6:08
  • 5
    $\begingroup$ Or you could directly enumerate lambda calculus terms. A lot faster than random strings as every output is a properly formatted term. That would be like replacing the typing monkeys with a Shakespeare play generator. $\endgroup$
    – Dan D.
    Commented Sep 20, 2018 at 9:37
  • $\begingroup$ It wouldn't be a like "Shakespeare play generator", because interesting lambda terms are very very rare: okmij.org/ftp/Haskell/AlgorithmsH1.html#random-term $\endgroup$
    – Theo H
    Commented Dec 9, 2023 at 22:29

Sure. We can directly generate them according to the definition of lambda terms.

In Haskell, we define the data type first,

data LC a  =  Var  a                -- Constructor <type> <type> ...
           |  App (LC a) (LC a)     --
           |  Lam  a     (LC a)     --  ... alternatives ...

instance Show a => Show (LC a)      -- `LC a` is in Show if `a` is in Show, and
    show (Var i)    =  [c | c <- show i, c /= '\'']
    show (App m n)  =  "("  ++ show m       ++ " " ++ show n ++ ")"
    show (Lam v b)  =  "(^" ++ show (Var v) ++ "." ++ show b ++ ")"

and then with the use of a fair(er) join,

lambda :: [a] -> [LC a]
lambda vars  =  terms 
  terms  =  fjoin [ map Var vars ,
                    fjoin [ [App t s | t <- terms] | s <- terms ] ,
                    fjoin [ [Lam v s | v <- vars ] | s <- terms ] ]

  fjoin :: [[a]] -> [a]
  fjoin xs  =  go [] xs             -- fairer join
      go [] []  =  []
      go a  b   =  reverse (concatMap (take 1) a) ++ go 
                       (take 1 b ++ [t | (_:t) <- a]) (drop 1 b)

we just enumerate them, as e.g.

> take 20 $ lambda "xyz"
[x,y,(x x),z,(y x),(^x.x),(x y),(^y.x),((x x) x),(^x.y),(y y),(^z.x),(x (x x)),
 (^y.y),(z x),(^x.(x x)),((x x) y),(^z.y),(y (x x)),(^y.(x x))]

> take 5 $ drop 960 $ lambda "xyz"
[(((x x) y) (z x)),(^y.(^x.((x x) (x x)))),((^x.(x x)) (^x.(x x))),(^x.((^z.x) 
 y)),((z x) ((x x) y))]

Look, the famous $\Omega = (\lambda x . xx)( \lambda x . xx )$ term is in there not that far down from the top!

fjoin is equivalent to Omega monad's diagonal.


I've come across one tool online that can generate sample strings from a regular expression: https://www.browserling.com/tools/text-from-regex. You can generate a lot of sample lambda terms by inputting something like this:

(\( (lambda \w\. )* \w+ \))* 

Of course to get terms with arbitrary levels of nesting, you are going to need to use a context-free grammar, which is a more descriptive tool for defining a language than a regular expression. I haven't come across an existing tool for generating sample language sentences based on a context-free grammar definition, but there's no reason one couldn't be built.

  • 3
    $\begingroup$ The $\lambda$-terms are not regular expressions (as you note). It is harmful to answer a beginner's question this way because it obscures an important distinction (namely between context-free grammars and regular expressions). $\endgroup$ Commented Sep 20, 2018 at 13:42

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.