Lambda Calculus Generator

Question

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.

Answer 1

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.

Answer 2

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.

Answer 3

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.

Answer 4

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
  where
    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 
  where
  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
      where 
      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.

Answer 5

The following lambda term written in de-Bruijn notation

T = (λ 1 1) (λ (λ λ λ 1 (2 (λ λ λ 3 1 (2 (λ 2)))) (3 (λ 4 (λ 4 (2 1))))) (1 1)) (λ 1)

is a binary tree containing all closed lambda terms. That is, for every closed lambda term t, there exists a sequence of booleans b1,b2..bt such that t = T b1 b2 ... bt. For example, you may check that

I = T 1 1 0 1 0 1 1 0 1 0 0 0 1 1 0 1 0 0 0

K = T 1 1 0 1 0 0 1 1 1 1 1 1 0 1 0 0 0 0 0 0 0

S = T 1 1 1 0 1 0 1 1 1 0 0 1 1 0 0 1 0 0 1 0 1 0 1 1 0 0 1 0 0 0 0

with booleans 0 = \x\y.x and 1 = \x\y.y Even T itself appears infinitely many times within T.

The way this works is that the sequence of booleans is effectively decoded with 1 denoting prefix application, and 0 denoting the term λxλyλz.x z(y(λ_.z)) which forms a one point basis.

Answer 6

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.