Counting linear lambda terms

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, \(\lambda f. \lambda x. f x\) and \(\lambda f. \lambda x. f (f x)\) are different, since they can be distinguished by passing them the arguments (say) \(\lambda y. y + 1\) and \(0\). However, \(\lambda a. a\) and \(\lambda b. (\lambda c. c) b\) are indistinguishable.

Remember, you can only use lambda, function application, and tupling. Using undefined in particular does not count.

1. \(\forall a. a \to a\)
2. \(\forall a. a \to a \to a\)
3. \(\forall a. (a,a) \to (a,a)\)
4. \(\forall a b. (a \to b) \to (a \to b) \to a \to a \to (b,b)\)
5. \(\forall a. (a \to a) \to a \to a\)

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

1. One (the identity function).
2. Two: we can return either the first or the second argument. (This is the type of Church-encoded booleans.)
3. Four: return the first value twice, or the second value twice, or both in either order.
4. Eight: there are four ways to apply the two functions to the two values of type \(a\) (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.
5. 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):

1. Can you write down a type with exactly three different inhabitants?
2. 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 \(\lambda x.t\), \(x\) must occur free in \(t\) exactly once. (Note, however, that type arguments may be used multiple times.) For example, \(\lambda x. \lambda f. f x\) is linear, but \(\lambda x. \lambda f. f (f x)\) is not (since \(f\) is used twice), nor is \(\lambda x. \lambda f. x\) (since \(f\) is ignored). For dealing with tuples, assume there are no projection functions like fst or snd, only pattern-matching like \(\lambda (x,y). (y,x)\); 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:

1. Can you write down a type with exactly three different linear inhabitants?
2. 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.