## More counting lambda terms

Yesterday someone submitted a comment to an old post of mine about counting linear lambda terms, asking the following question:

I am interested in a similar problem: given a natural number N, what is the number of different symply-typed closed lambda terms with size smaller than N?

They don’t need to be observationally different. They should be different modulo renaming of variables and types, though. So:

lambda x^A.x and lambda y^B.y

should be considered the same…

Do you know where I can find the answer? Answers using any kind of size measurement would be fine for me…

It’s an interesting question, and I thought it would make for a good way to illustrate one of my favorite techniques when trying to research a combinatorial question like this. Namely, write a program to compute the first few values by brute force, then look it up in the Online Encyclopedia of Integer Sequences and follow the references.

``````> module CountSTLC where
>
> type Nat = Int  -- just pretend
``````

A type for deBruijn-indexed lambda terms.

``````> data Tm = Var Nat
>         | App Tm Tm
>         | Lam Tm
>   deriving (Eq, Ord, Show)
``````

We’ll define the size of a term as the number of constructors used by its representation in the above data type.

``````> size :: Tm -> Nat
> size (Var _)     = 1
> size (App t1 t2) = 1 + size t1 + size t2
> size (Lam t)     = 1 + size t
``````

Here’s a function to generate all the closed `Tm`s of a given size. We pass along an index giving the current level of nesting (so we know what variables are available).

``````> genAll :: Nat -> [Tm]
> genAll = genAll' 0
>   where
``````

There are no terms of size zero (or smaller).

``````>     genAll' _   n | n <= 0 = []
``````

The only terms of size 1 are variables. We can choose to refer to any of the currently enclosing lambdas.

``````>     genAll' ctx 1 = map Var [0 .. ctx-1]
``````

Otherwise, we could have an application (splitting the available size between the two sides in all possible ways) or a lambda (remembering to increment the nesting level).

``````>     genAll' ctx n = [ App t1 t2
>                     | n1 <- [1 .. n-2]
>                     , t1 <- genAll' ctx n1
>                     , t2 <- genAll' ctx (n - n1 - 1)
>                     ]
>                  ++ (map Lam (genAll' (succ ctx) (n-1)))
``````

Let’s see what we get:

``````*CountSTLC> genAll 4
[ Lam (App (Var 0) (Var 0))
, Lam (Lam (Lam (Var 0)))
, Lam (Lam (Lam (Var 1)))
, Lam (Lam (Lam (Var 2)))
]``````

Looks reasonable: there are four closed lambda terms of size 4. Now let’s count:

``````*CountSTLC> map (length . genAll) [1..10]
[0,1,2,4,13,42,139,506,1915,7558]``````

Searching for this sequence on OEIS turns up something promising, with a bit of information including a formula for computing the counts directly. It also has a link to someone’s research but unfortunately it seems dead. But it does have the email address of the person who submitted this sequence, and emailing him might be a good start!

This is all well and good, but the commenter actually asked for simply typed lambda calculus terms. The first size-4 lambda term above is not well-typed, since it involves a self-application. Can we modify our program to only generate well-typed lambda terms? This seems much more difficult. I may write about it in a future post. For now I’ll leave it as an exercise for the interested and motivated reader! Assistant Professor of Computer Science at Hendrix College. Functional programmer, mathematician, teacher, pianist, follower of Jesus.

### 5 Responses to More counting lambda terms

1. Luke says:

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.95.2624

I suspect this is the paper the broken link was referring to. It was on a server under the user id juewang, which is the author of this paper. The results seem relevant.

2. Alexis D says:

There is a paper  from the author of the OEIS note and another one  doing asymptotic enumeration.

3. John Tromp says:

http://en.wikipedia.org/wiki/Binary_lambda_calculus#Lambda_encoding
counts the number of closed lambda terms where size is measured in bits (for a straightforward binary encoding).
OEIS entries A195691, A114851, and A114852
list both simple and efficient Haskell programs for computing
open, closed, and normal form terms respectively.

regards,
-John

4. Sean Leather says:
5. Pierre Lescanne says:

I published with Katarzyna Grygiel a paper entitled “Counting and generating lambda terms” http://arxiv.org/abs/1210.2610 which addresses in particular the problem of counting simply typeable terms. In particular, notice the sequence https://oeis.org/A220471 on the Online Encyclopedia of Integer Sequences.

This site uses Akismet to reduce spam. Learn how your comment data is processed.