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.

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

About these ads
This entry was posted in haskell. Bookmark the permalink.

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 [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

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

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s