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.

Let’s start with *untyped* lambda calculus terms.

```
> 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!

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.

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

[1] http://arxiv.org/abs/0903.5505

[2] http://www.siam.org/proceedings/analco/2011/anl11_03_bodinio.pdf

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

http://scholar.google.com/scholar?hl=en&q=Enumerating%20Well-Typed%20Terms%20Generically

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.