# reperiendi

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

### 4 Responses

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

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

OK, that’s a good idea–I’ll have a look.