Combinators as addresses

Posted in Programming by Mike Stay on 2008 January 30

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, $(xy)$ means “ $x$ applied to $y.$ ” Note the position of the term $c$ in each case:

identity
$I:X \to X$
$(Ic) = c$
cut
$B:(Y\to Z) \to (X \to Y) \to (X \to Z)$
$(((Ba)b)c) = (a(bc))$
braid
$C:(X\to Y\to Z) \to (Y \to X \to Z)$
$(((Ca)b)c) = ((ac)b)$

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

$x \mapsto ((r(xs))t),$

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

$((C[x\mapsto (r(xs))])t).$

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

$((C((Br)[x \mapsto (xs)]))t).$

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

$((C((Br)((C[x \mapsto x])s)))t).$

And finally, we replace $\,[x\mapsto x]$ with $I:$

$((C((Br)((CI)s)))t)$

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

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

$S:$ the variable may appear in either subtree, since $(((Sa)b)c) = ((ac)(bc)).$
$K:$ the variable does not appear in this subtree, since $((Ka)c) = a.$
$I:$ this leaf is a copy of the variable, since $(Ic) = c.$

About these ads

4 comments

4 Responses

Subscribe to comments with RSS.

sigfpe said, on 2008 February 1 at 4:11 pm

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

Reply
reperiendi said, on 2008 February 1 at 6:17 pm

OK, 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”)?

Reply
reperiendi said, on 2008 February 3 at 10:14 pm

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

Reply
reperiendi said, on 2008 February 4 at 12:32 pm

Another 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

Reply

reperiendi