Just a little something with which I’ve been idly occupying spare brain cycles lately… read on for an interesting puzzle.

### Warm up: counting lambda terms

Consider a stripped-down version of Haskell’s type system with only natural numbers, polymorphism, functions, and tuples: no type classes, no algebraic data types, no base types other than Nat, and no bottom/undefined. (For those versed in the PL lingo, I mean System F extended with pairs — or we could even Church-encode the pairs, it doesn’t matter.)

Now for an easy warm-up exercise: for each of the following types, how *many different* terms are there with the given type? By *different* I mean *observably different*; two terms are different if and only if there exist inputs for which they produce different outputs. For example, and are different, since they can be distinguished by passing them the arguments (say) and . However, and are indistinguishable.

Remember, you can only use lambda, function application, and tupling. Using `undefined`

in particular does not count.

The answers (stop reading if you want to work out the answers for yourself):

- One (the identity function).
- Two: we can return either the first or the second argument. (This is the type of Church-encoded booleans.)
- Four: return the first value twice, or the second value twice, or both in either order.
~~Eight: there are four ways to apply the two functions to the two values of type (apply one of them to both, or match them up one-to-one), and then two ways to order the results.~~Whoops, even I found this one tricky. Thanks to gasche for the correct answer (sixteen); see the comments.- Omega: we can apply the function to the second argument any natural number of times.

Hopefully you didn’t find that too hard (although perhaps you found the fourth one a bit tricky). Now for a few more (easy) warm-up questions (I won’t bother giving the answers):

- Can you write down a type with exactly
*three*different inhabitants? - Can you come up with a scheme for constructing types inhabited by
*any given natural number*of different terms?

### Counting linear lambda terms

And now for the interesting twist. We will now restrict ourselves to only *linear* lambda terms. By a “linear” term I mean, intuitively, one in which every input is used exactly once: inputs may be neither ignored nor duplicated. Put another way, every time we see , must occur free in exactly once. (Note, however, that *type* arguments may be used multiple times.) For example, is linear, but is not (since is used twice), nor is (since is ignored). For dealing with tuples, assume there are no projection functions like `fst`

or `snd`

, only pattern-matching like ; hence, using a tuple linearly simply means using each of its components exactly once. We could make all of this fully precise with a suitable type system, of course, but I hope this intuitive explanation will suffice.

Now go back and look at the four types listed above. How many *linear* inhabitants does each type have?

OK, that’s slightly more interesting but still not that hard; hopefully you came up with one, zero, two, four, and one. But now for the fun:

- Can you write down a type with exactly
*three*different linear inhabitants? - Can you come up with a scheme for constructing types inhabited by
*any given natural number*of different linear terms? If not, can you characterize the natural numbers for which such types do exist?

I’ll write more in a future post. For now, have fun, and feel free to post discussions, questions, solutions, etc. in the comments.

I was thinking: when a type occurs n times in a positive position it also has to occur n times in a negative position. And then you can permute the mappings from negative to positive positions. So that would mean that types exist for natural numbers in the form of products of factorial numbers.

But that doesn’t account for the fact that the output of a function cannot be routed to the input of itself. (Otherwise type 5 would have had 2 inhabitants.)

A type like

`a -> a -> a -> (a -> a) -> (a, (a, a))`

has 3 * 3! inhabitants.Back to the drawing board.

Ignoring the linear requirement, to construct types inhabited by any given natural number of different terms, couldn’t the type simply be (a, a, …, a) -> a? Or its curried form.

Yes, indeed. (But this obviously won’t work with the linear requirement in place, since most of the inputs will be ignored.)

I count 16 different elements in your fourth type: as you said, there are four ways to choose which function to apply, but there are also four ways to choose which parameters to pass.

Whoops, you’re right, thanks! Here’s a perhaps simpler way to think about it: any term of this type will be of the form , and we have an independent binary choice for what to put in the place of each number: f or g in place of 1 and 3, and x or y in place of 2 and 4). And it’s not hard to see that each choice results in an observationally different function.

I noticed the same thing but couldn’t post a comment. Weird.

Pingback: Counting linear lambda terms: Mersenne numbers « blog :: Brent -> [String]

Pingback: Enumerating linear inhabitants « blog :: Brent -> [String]

Hi!

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…

Pingback: More counting lambda terms « blog :: Brent -> [String]