Abstraction elimination

$\lambda$-calculus is named for the binder in that language. The language itself is very simple. We start with an infinite set of variables $x, y, z, \ldots$ and then define the terms to be

$$t, t' ::= \left\{ \begin{array}{lr}x & variable \\ \lambda x.t & abstraction \\ (t\; t') & application\end{array}\right.$$

Schönfinkel’s idea was roughly to “sweep the binders under the rug”. We’ll allow binders, but only in the definition of a “combinator”, one of a finite set of predefined terms. We don’t allow binders in any expression using the combinators themselves; the binders will all be hidden “underneath” the name of the combinator.

To eliminate all the binders in a term, we start at the “lowest level”, a term of the form $t = \lambda x.u,$ where $u$ only has variables, combinators, and applications; no abstractions! Then we’ll try to find a way of rewriting $t$ using combinators instead. Since the lambda term $\lambda x.(v\; x)$ behaves the same as $v$ itself, if we can find some $v$ such that $v x = u$, then the job’s done.

Suppose $u=x$. What term can we apply to $x$ and get $x$ itself back? The identity function, obviously, so our first combinator is

$$I = \lambda x.x.$$

What if $u$ doesn’t contain $x$ at all? We need a “konstant” term $K_u$ such that $(K_u\; x)$ just discards $x$ and returns $u.$ At the same time, we don’t want to have to specify a different combinator for each $u$ that doesn’t contain $x$, so we define our second combinator $K$ to first read in which $u$ to return, then read in $x$, throw it away, and return $u:$

$$K = \lambda u x.u.$$

Finally, suppose $u$ is an application $u = (w\; w').$ The variable $x$ might occur in $w$ or in $w'$ or both. Note that if we recurse on each of the terms in the application, we’ll have terms $r, r'$ such that $(r\; x) = w$ and $(r'\; x) = w'$, so we can write $u = ((r\; x)\; (r'\; x)).$ This suggests our final combinator should read in $r, r'$, and $x$ and “share” $x$ with them:

$$S = \lambda r r'x.((r\; x)\; (r'\; x)).$$

If we look at the types of the terms $S, K,$ and $I$, we find something interesting:

$$\begin{array}{rl}I:&Z \to Z\\K:&Z \to Y \to Z\\S:&(Z \to Y\to X)\to (Z\to Y) \to Z \to X\end{array}$$

The types correspond exactly to the axiom schemata for positive implicational logic!

The $S K I$-calculus is a lot easier to model formally than the $\lambda$-calculus; we can use a tiny Gph-enriched Lawvere theory (see the appendix) to capture the operational semantics and then derive the denotational semantics from it.

$\pi$-Calculus

As computers got smaller and telephony became cheaper, people started to connect them to each other. ARPANET went live in 1969, grew dramatically over the next twenty years, and eventually gave rise to the internet. ARPANET was decommissioned in 1990; that same year, Robin Milner published a paper introducing the $\pi$-calculus. He designed it to model the new way computation was occurring in practice: instead of serially on a single computer, concurrently on many machines via the exchange of messages. Instead of applying one term to another, as in the lambda and SK calculi, terms (now called “processes”) get juxtaposed and then exchange messages. Also, whereas in $\lambda$-calculus a variable can be replaced by an entire term, in the $\pi$-calculus names can only be replaced by other names.

Here’s a “good parts version” of the asynchronous $\pi$-calculus; see the appendix for a full description.

$$\begin{array}{rll}P, Q ::= \quad& 0 & do\; nothing \\ \;|\; & P|Q & concurrency \\ \;|\; &for (x \leftarrow y) P & input \\ \;|\; & x!y & output \\ \;|\; & \nu x.P & new\; name \\ \;|\; & !P& replication \end{array}$$

$$x!z \;|\; for(y \leftarrow x).P \Rightarrow P\{z/y\}\quad communication\; rule$$

There are six term constructors for $\pi$-calculus instead of the three in $\lambda$-calculus. Concurrency is represented with a vertical bar |, which forms a commutative monoid with 0 as the monoidal unit. There are two binders, one for input and one for introducing a new name into scope. The rewrite rule is reminiscent of a trace in a compact closed category: $x$ appears in an input term and an output term on the left-hand side, while on the right-hand side $x$ doesn’t appear at all. I’ll explore that relationship in another post.

The syntax we use for the input prefix is not Milner’s original syntax. Instead, we borrowed from Scala, where the same syntax is syntactic sugar for $M(\lambda x.P)(y)$ for some monad $M$ that describes a collection. We read it as “for a message $x$ drawn from the set of messages sent on $y$, do $P$ with it”.

For many years after Milner proposed the $\pi$-calculus, researchers tried to come up with a way to eliminate the bound names from a $\pi$-calculus term. Yoshida was able to give an algorithm for eliminating the bound names that come from input prefixes, but not those from new names. Like the abstraction elimination algorithm above, Yoshida’s algorithm produced a set of concurrent combinators. There’s one combinator $m(a, x)$ for sending a message $a$ on the name $x$, and several others that interact with $m$’s to move the computation forward (see the appendix for details):

$$\begin{array}{rlr} d(a,b,c) | m(a,x) & \Rightarrow m(b,x) | m(c,x) & (fanout)\\ k(a) | m(a,x) & \Rightarrow 0 & (drop) \\ fw(a,b) | m(a,x) & \Rightarrow m(b,x) & (forward) \\ br(a,b) | m(a,x) & \Rightarrow fw(b,x) & (branch\; right)\\ bl(a,b) | m(a,x) & \Rightarrow fw(x,b) & (branch\; left) \\ s(a,b,c) | m(a,x) & \Rightarrow fw(b,c) & (synchronize)\end{array}$$

Unlike the $S K I$ combinators, no one has shown a clear connection between some notion of type for these combinators and a system of logic.

Reflection

Several years ago, Greg Meredith had the idea to combine the set of $\pi$-calculus names and the set of $\pi$-calculus terms recursively. In a paper with Radestock he introduced a “quoting” operator I’ll write & that turns processes into names and a “dereference” operator I’ll write * that turns names into processes. They also made the calculus higher-order: they send processes on a name and receive the quoted process on the other side.

$$x!\langle Q\rangle \;|\; for(y \leftarrow x).P \Rightarrow P\{\&Q/y\}\quad communication\; rule$$

The smallest process is 0, so the smallest name is &0. The next smallest processes are

$$\&0\langle 0 \rangle \quad and \quad for(\&0 \leftarrow \&0) \; 0,$$

which in turn can be quoted to produce more names, and so on.

Together, these two changes let them demonstrate a $\nu$-elimination transformation from $\pi$ calculus to their reflective higher-order (RHO) calculus: since a process never contains its own name ($\&P$ cannot occur in $P$), one can use that fact to generate names that are fresh with respect to a process.

Another benefit of reflection is the concept of “namespaces”: since the names have internal structure, we can ask whether they satisfy propositions. This lets Meredith and Radestock define a spatial-behavioral type system like that of Caires, but more powerful. Greg demonstrated that the type system is strong enough to prevent attacks on smart contracts like the $50M one last year that caused the fork in Ethereum.

In our most recent pair of papers, Greg and I consider two different reflective higher-order concurrent combinator calculi where we eliminate all the bound variables. In the first paper, we present a reflective higher-order version of Yoshida’s combinators. In the second, we note that we can think of each of the term constructors as combinators and apply them to each other. Then we can use $S K I$ combinators to eliminate binders from input prefixes and Greg’s reflection idea to eliminate those from $\nu.$ Both calculi can be expressed concisely using Gph-enriched Lawvere theories.

In future work, we intend to present a type system for the resulting combinators and show how the types give axiom schemata.

Appendix

Gph-theory of $S K I$-calculus

• objects
  • $T$
• morphisms
  • $S, K, I\colon 1 \to T$
  • $(-\; -)\colon T \times T \to T$
• equations
  • none
• edges
  • $\sigma\colon (((S\; x)\; y)\; z) \Rightarrow ((x\; z)\; (y\; z))$
  • $\kappa\colon ((K\; x)\; z) \Rightarrow x$
  • $\iota\colon (I\; z) \Rightarrow z$

$\pi$-calculus

• grammar
  • $\begin{array}{rll}P, Q ::= \quad & 0 & do\; nothing \\ \;|\; & P|Q & concurrency \\ \;|\; &for (x \leftarrow y).P & input \\ \;|\; & x!y & output \\ \;|\; & \nu x.P & new\; name \\ \;|\; & !P& replication \end{array}$
• structural equivalence
  • free names
    • $FN(0) = \{\}$
    • $FN(P|Q) = FN(P) \cup FN(Q)$
    • $FN(for (x \leftarrow y).P) = \{y\} \cup FN(P) - \{x\}$
    • $FN(x!y) = \{x,y\}$
    • $FN(\nu x.P) = FN(P) - \{x\}$
    • $FN(!P) = FN(P)$
  • 0 and | form a commutative monoid
    • $P|0 \equiv P$
    • $P|Q \equiv Q|P$
    • $(P|Q)|R \equiv P|(Q|R)$
  • replication
    • $!P \equiv P\;|\;!P$
  • $\alpha$-equivalence
    • $for (x \leftarrow y).P\equiv for (z \leftarrow y).P\{z/x\}$ where $z$ is not free in $P$
  • new names
    • $\nu x.\nu x.P \equiv \nu x.P$
    • $\nu x.\nu y.P \equiv \nu y.\nu x.P$
    • $\nu x.(P|Q) \equiv (\nu x.P)|Q$ when $x$ is not free in $Q$
• rewrite rules
  • $x!z \;|\; for(y \leftarrow x).P \Rightarrow P\{z/y\}$
  • if $P \Rightarrow P'$, then $P\;|\; Q \Rightarrow P'\;|\; Q$
  • if $P \Rightarrow P'$, then $\nu x.P \Rightarrow \nu x.P'$

To be clear, the following is not an allowed reduction, because it occurs under an input prefix:

$$for(v \leftarrow u).(x!z \;|\; for(y \leftarrow x).P) \nRightarrow for(v \leftarrow u).P\{z/y\}$$

Yoshida’s combinators

• grammar
  • atom: $Q ::= 0 \;|\; m(a,b) \;|\; d(a,b,c) \;|\; k(a) \;|\; fw(a,b) \;|\; br(a,b) \;|\; bl(a,b) \;|\; s(a,b,c)$
  • process: $P ::= Q \;|\; \nu a.P \;|\; P|P \;|\; !P$
• structural congruence
  • free names
    • $FN(0) = \{\}$
    • $FN(k(a)) = \{a\}$
    • $FN(m(a,b)) = FN(fw(a,b)) = FN(br(a,b)) = FN(bl(a,b)) = \{a, b\}$
    • $FN(d(a,b,c)) = FN(s(a,b,c)) = \{a,b,c\}$
    • $FN(\nu a.P) = FN(P) - \{x\}$
    • $FN(P|Q) = FN(P)\cup FN(Q)$
    • $FN(!P) = FN(P)$
  • 0 and | form a commutative monoid
    • $P|0 \equiv P$
    • $P|Q \equiv Q|P$
    • $(P|Q)|R \equiv P|(Q|R)$
  • replication
    • $!P \equiv P\;|\;!P$
  • new names
    • $\nu x.\nu x.P \equiv \nu x.P$
    • $\nu x.\nu y.P \equiv \nu y.\nu x.P$
    • $\nu x.(P|Q) \equiv (\nu x.P)|Q$ when $x$ is not free in $Q$
• rewrite rules
  • $d(a,b,c) | m(a,x) \Rightarrow m(b,x) | m(c,x)$ (fanout)
  • $k(a) | m(a,x) \Rightarrow 0$ (drop)
  • $fw(a,b) | m(a,x) \Rightarrow m(b,x)$ (forward)
  • $br(a,b) | m(a,x) \Rightarrow fw(b,x)$ (branch right)
  • $bl(a,b) | m(a,x) \Rightarrow fw(x,b)$ (branch left)
  • $s(a,b,c) | m(a,x) \Rightarrow fw(b,c)$ (synchronize)
  • $!P \Rightarrow P|!P$
  • if $P \Rightarrow P'$ then for any term context $C$, $C[P] \Rightarrow C[P']$.

Gph-theory of RHO Yoshida combinators

• objects
  • $N, T$
• morphisms
  • $0\colon 1 \to T$
  • $k\colon T \to T$
  • $m\colon N \times T \to T$
  • $fw,br,bl\colon N^2 \to T$
  • $d,s\colon N^3 \to T$
  • $|\colon T^2 \to T$
  • $*\colon N \to T$
  • $\&\colon T \to N$
• equations
  • 0 and | form a commutative monoid
    • $P|0 = P$
    • $P|Q = Q|P$
    • $(P|Q)|R = P|(Q|R)$
  • $*\&P = P$
• edges
  • $\delta\colon d(a,b,c) | m(a,P) \Rightarrow m(b,P) | m(c,P)$
  • $\kappa\colon k(a) | m(a,P) \Rightarrow 0$
  • $\phi\colon fw(a,b) | m(a,P) \Rightarrow m(b,P)$
  • $\rho\colon br(a,b) | m(a,P) \Rightarrow fw(b,\&P)$
  • $\lambda\colon bl(a,b) | m(a,P) \Rightarrow fw(\&P,b)$
  • $\sigma\colon s(a,b,c) | m(a,P) \Rightarrow fw(b,c)$

Gph-theory of RHO $\pi$-like combinators

• objects
  • $T$
• morphisms
  • $C, 0, |, for, !, \&, *, S, K, I\colon 1 \to T$
  • $(-\; -)\colon T\times T \to T$
• equations
  • 0 and | form a commutative monoid
    • $((|\; 0)\; P) = P$
    • $((|\; ((|\; P)\; Q))\; R)=((|\; P)\; ((|\; Q)\; R)$
    • $((|\; P)\; Q) = ((|\; Q)\; P)$
• edges
  • $\sigma\colon(((S\; P)\; Q)\; R) \Rightarrow ((P\; R)\; (Q\; R))$
  • $\kappa\colon((K\; P)\; Q) \Rightarrow P$
  • $\iota\colon(I\; P) \Rightarrow P$
  • $\xi\colon((|\; C)\; ((|\; ((for\; (\&\; P))\; Q))\; ((!\; (\&\; P))\; R))) \Rightarrow ((|\; C)\; (Q\; (\&\; R)))$
  • $\epsilon\colon((|\; C)\;(*\; (\&\; P))) \Rightarrow ((|\; C)\; P)$