## Combinators as addresses

In linear lambda calculus, you must use each bound variable exactly once in a term. A term with a single bound variable is a full binary tree of applications in which one of the leaves is the bound variable, so it makes sense to ask, “which leaf?”

Three combinators are universal for the free linear lambda calculus on a countable set of types. In the description below, means “ applied to ” Note the position of the term in each case:

- identity

- cut

- braid

A full binary tree of applications is either a leaf or an application of a left subtree to a right subtree. says that this leaf is the variable in question; says that the variable is in the right subtree; and says it’s in the left subtree. So, for example, in the linear lambda term

appears in the left subtree, so applying abstraction elimination once gives

Now is on the right; eliminating again in the bracketed term gives

Now is on the left; eliminating again in the bracketed term gives

And finally, we replace with

to get a term with no bound occurrences of The “I-terminated” list of combinators we added, in this case tells us exactly where in the tree the variable appeared.

In the (nonlinear) lambda calculus, the variable may appear in either branch or not at all. The and combinators are a universal basis for this calculus, and can be interpreted as

- the variable may appear in either subtree, since
- the variable does not appear in this subtree, since
- this leaf is a copy of the variable, since

sigfpesaid, on 2008 February 1 at 4:11 pmYou should compare this with Huet’s zipper and Conor McBride’s notion of differentiating types.

Given a tree, a zipper for the tree is a type that corresponds to a tree along with the address of a slot in the tree from which an element has been excised. McBride generalised this to any (regular) type, not just trees. The cool thing is that the type of a structure along with the address of an excised element is given by a type of derivative.

reperiendisaid, on 2008 February 1 at 6:17 pmOK, that’s a good idea–I’ll have a look.

I’ve read your post about infinitesimal types; have you seen Joyal’s species (aka “structure types”)?

reperiendisaid, on 2008 February 3 at 10:14 pmOK, Huet’s zipper is exactly Joyal’s species (invented in 1981), what Baez & Dolan translate as “structure types.” (See week202 of This Week’s Finds or the Fall ’03 QG notes here: http://math.ucr.edu/home/baez/qg-fall2003/ )

The relation you noticed with B and C is real. In Haskell, you can have parameterized types, called “type constructors,” rather like functions whose inputs are types instead of values. The “context” type constructor is just type-lifted linear logic.

reperiendisaid, on 2008 February 4 at 12:32 pmAnother thing to notice is that S and K are linear up to their last argument; S doubles it last input, while K deletes it.

(((S I) I) x) = (x x)

((K I) x) = I