reperiendi

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.

4 comments

Yoneda embedding as contrapositive and call-cc as double negation

Posted in Category theory, Math, Programming by Mike Stay on 2008 January 26

Consider the problem of how to represent negation of a proposition P when we only have implication and falsehood:

P \to {\rm F}.

Since {\rm F} \to {\rm F} is true and {\rm T} \to {\rm F} is false, this does what we want.

The contrapositive says \neg Q \to \neg P has the same truth value as P \to Q. Using only implication, the contrapositive of P \to Q is

(Q \to {\rm F}) \to (P \to {\rm F}).

What if we don’t even have falsehood? Well, we can pick any proposition X to represent falsehood and form

(Q \to X) \to (P \to X).

The Yoneda embedding takes a category C^{\rm op} and produces a category \mbox{HOM}(C, \mbox{Set}):

\begin{array}{ccccccc}\mbox{Yoneda}_X: & C^{\rm op} & \to & \mbox{HOM}(C, \mbox{Set}) \\ & P & \mapsto & \mbox{hom}(P, X) \\ & f:P \to Q & \mapsto & \mbox{Yoneda}_X(f): & \mbox{hom}(Q, X) & \to & \mbox{hom}(P, X) \\ & & & & k & \mapsto & k \circ f \end{array}

This embedding is better known among computer scientists as the continuation passing style transformation.

In a symmetric monoidal closed category, like lambda calculus, we can move everything “inside:” every morphism f:P \to Q has an internal version f:I\to P \multimap Q. The internal Yoneda embedding of f is

\mbox{Yoneda}_X(f):I \to (Q \multimap X) \multimap (P \multimap X).

Here I is the “unit” type; notice how the target type is isomorphic under the Curry-Howard isomorphism to the contrapositive. This is a term that maps a continuation k:Q\multimap X and a value p:P to k(f(p)).

To get double negation, first do the Yoneda embedding on the identity to get

\mbox{Yoneda}_X(1_P):hom(P,X) \to hom(P,X),

then uncurry, braid, and recurry to get

\mbox{Yoneda}_X(1_P):P \to hom(hom(P,X),X),

or, internally,

\mbox{Yoneda}_X(1_P):I\to P \multimap ((P\multimap X)\multimap X).

This takes a value p to a function value k\mapsto k(p).

Call-with-current-continuation expects a term that has been converted to CPS style as above, and then hands it the remainder of the computation in k.

2 comments

The category GraphUp

Posted in Category theory, Programming by Mike Stay on 2008 January 17

The category GraphUp of graphs and Granovetter update rules has

  • directed finite graphs as objects
  • morphisms generated by Granovetter rules, i.e. the following five operations:
    • add a new node. (creation, refcount=0)
    • given a node x, add a new node y and an edge x\to y. (creation, refcount=1)
    • given edges x\to y and x \to z, add an edge y\to z. (introduction, ++refcount)
    • remove an edge. (deletion, --refcount)
    • remove a node and all its outgoing edges if it has no incoming edges. (garbage collection)

It’s a monoidal category where the tensor product is disjoint union. Also, since two disjoint graphs can never become connected, they remain disjoint.

Programs in a capability-secure language get interpreted in GraphUp. A program’s state graph consists of nodes, representing the states of the system, and directed edges, representing the system’s transitions between states upon receiving input. A functor from a program state graph to GraphUp assigns an object reference graph as state to each node and an update generated by Granovetter rules to each edge.

leave a comment

Polyadic asynchronous asymmetric pi calculus

Posted in Programming by Mike Stay on 2008 January 2

\begin{array}{rll} P :=\\& \mbox{send } \langle y_1, \ldots, y_n\rangle \mbox{ on } \bar{x}. & |\\& \mbox{receive } \langle y_1, \ldots, y_n\rangle \mbox{ on } x; P &|\\& (P|P) &|\\& \mbox{new }y; P & |\\& !P\end{array}

where y is either an input channel x or an output channel \bar{x}, and x is taken from a countably infinite set.

Structural congruence:

  • \mbox{new } y; P \equiv \mbox{new } y'; P' [with y' replacing y] if y' does not appear in P. (alpha conversion)
  • (P|P') \equiv (P'|P) (parallel processes)
  • ((P|P')|P'') \equiv (P|(P'|P'')) (association)
  • \mbox{new } y; \mbox{new } y'; P \equiv \mbox{new } y'; \mbox{new } y; P (restriction)
  • !P \equiv (P|!P) (replication)
  • \mbox{new } y; (P|P') \equiv \mbox{new } y; P|P' if y is not free in P'.

Reduction rules:

  • (\mbox{send } \langle y_1, \ldots, y_n \rangle \mbox{ on } \bar{x}. | \mbox{ receive } \langle y'_1, \ldots, y'_n \rangle\mbox{ on } x; P) \to P [with y_i replacing y'_i]
  • If P_1 \to P_2 then (P_1|P_3) \to (P_2|P_3)
  • If P_1 \to P_2 then \mbox{new } y; P_1 \to \mbox{new } y; P_2
  • If P_1 \equiv P_2, \; P_2 \to P_3, and P_3 \equiv P_4, then P_1 \to P_4

leave a comment

Haskell monads for the category theorist

Posted in Category theory, Math, Programming by Mike Stay on 2008 January 1

A monad in Haskell is about composing almost-compatible morphisms. Typically you’ve got some morphism f:A\to B and then you think of a reason that you’d rather have f':A \to TB, where T:{\rm Data} \to {\rm Data} is a functor. In Haskell, though, you don’t define functors right out: you define type constructors, which are like the map of objects in a functor. You have to define the map of morphisms separately.

To define the map of morphisms, we have to define unit (aka return) and bind. We define {\rm unit}:(A \multimap B) \to (A \multimap TB) to be the category-theorist’s unit \eta composed with the input. Applying {\rm unit} to f gives

A\xrightarrow{f} B \xrightarrow{\eta} TB.

To compose “half-functored” morphisms like f', we define {\rm bind}:TA \times (A\multimap TB)\to TB like this: given an input a:TA and a morphism like f', bind produces

TA \xrightarrow{Tf'} TTB \xrightarrow{\mu_B} TB.

So a “monad” in Haskell is always the monad for categories, except the lists are of bindable half-functored morphisms like f' rather than lists of composable morphisms.

A side-effect monad has T(A) = A\times E, where E is the data type for the environment on which the morphism is to act. The IO monad is a specific instance of a side-effect monad with the environment being the keyboard queue, disk drive, network, etc.

6 comments