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.

About these ads
This entry was posted in combinatorics and tagged , , , , , . Bookmark the permalink.

10 Responses to Counting linear lambda terms

  1. Sjoerd Visscher says:

    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.

  2. roy_hu says:

    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.

    • Brent says:

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

  3. gasche says:

    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.

    • Brent says:

      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 \lambda f g x y. (1 2, 3 4), 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.

    • roy_hu says:

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

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

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

  6. Bruno says:

    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…

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

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