10
$\begingroup$

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.

$\endgroup$
19
$\begingroup$

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 (make 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$ ($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.

$\endgroup$
  • $\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$ – Legit Stack Sep 20 '18 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 Sep 20 '18 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$ – LegionMammal978 Sep 20 '18 at 23:12
12
$\begingroup$

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.

$\endgroup$
  • 4
    $\begingroup$ Essentially, all problems like this are solved by invoking the typing monkey... $\endgroup$ – xuq01 Sep 20 '18 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. Sep 20 '18 at 9:37
11
$\begingroup$

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

$\endgroup$
5
$\begingroup$

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

In Haskell, we define the type first,

data LC a = Var a | App (LC a) (LC a) | Lam a (LC a)

instance Show a => Show (LC a) 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

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 (take 1 xs) (drop 1 xs)      -- fair 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.

$\endgroup$
0
$\begingroup$

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.

$\endgroup$
  • 2
    $\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$ – Andrej Bauer Sep 20 '18 at 13:42

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.