Enzymatic interaction

It is traditional for me, around this time of year, to provide holiday (brain) candy for folks in my technical community. This year's offering comes from a conversation with Marius Buliga about chemlambda in which he referred to β-reduction in the λ-calculus as an enzyme. This got me to thinking about explicitly modeling the COMM rule in the π-calculus as an enzyme. It turns out you can do this quite easily and it has a lot of applications!

For simplicity, i'll use the reflective, higher-order π-calculus, but extend the basic calculus with a primitive process, COMM:

P, Q ::= 0 | COMM | x?( y )P | x!( P ) | *x | P|Q
x, y ::= @P

(Note that i've adopted a slightly friendlier syntax since i first developed the reflective π-calculus. Instead of writing « P » and » x «, i now write @P and *x. This echoes the C and C++ programming language notation for acquiring a reference and dereferencing a pointer, respectively -- which is the key insight of the reflective calculus. We can get a kind of pointer arithmetic for channel names if we treat them as quoted process terms.)

Structural equivalence includes alpha-equivalence and makes ( P, | , 0 ) a commutative monoid. Of interest to us is

COMM | P = P | COMM

So, COMM mixes into a parallel composition.

Notice that COMM cannot penetrate an abstraction barrier, i.e. 

x?( y )P | COMM != x?( y )( P | COMM )

Enzymatic reduction in reflective π-calculus

There is an interesting design choice as to whether

x!( Q ) | COMM = x!( Q | COMM ) 

Treating COMM as enzymatic, the COMM-rule

x?( y )P | COMM | x!( Q ) → P{ @Q/y } | COMM 

results in the standard dynamics, if there is just one COMM process in the expression. If there are more COMM processes, then we get a spectrum of so-called true concurrency semantics, with the usual true concurrency semantics identified with the limiting equation

COMM = COMM | COMM

which allows to saturate a parallel composition with COMM in every place where an interaction could take place.

Writing COMMⁱ  for COMM | ... | COMM ( i times ), another set of dynamics arise from rules of the form

x?( y )P | COMMⁿ | x!( Q ) → P{ @Q/y } | COMM^m

with m < n

This bears resemblance to the Ethereum platform's idea of "gas" for a smart contract's calculation. Mike Stay points out that associating a cost with communication makes it look like an action in physics. Notice that you can get some very interesting dynamics with COMM-consuming interaction rules in the presence of COMM-releasing abstractions.

One example interpretation that i think works well and provides significant motivation is to treat COMM as a compute node. A finite number of COMMs represent a finite number of nodes on which processes can run. Likewise, it is possible to model acquisition and release of nodes with cost-based COMM-rules and certain code factorings. For example, call a process inert if P | COMM cannot reduce and purely inert if P inert and P != Q | COMM for any Q. Now, suppose

COMM: x?( y )P | COMMⁿ | x!( Q ) → P{ @( Q | COMM )/y } | COMM^n-1

and only allow purely inert processes in output position, i.e. x!( Q ), with Q inert. Then interaction acquires a node and dereference, *x releases one. For example,

x?( y )( *y ) | COMM | x!( Q ) 

→ 

*@( COMM | Q ) 

≡ 

COMM | Q

In terms of possible higher category theory models, the reification of the 2-cell-like COMM-rule as a 1-cell-like COMM process ought to provide a fairly simple way to make one of Mike Stay's recent higher category models work without suffering too many reductions, which has been the principal stumbling block of late. Notice that in this setting we can treat x?( y )( COMM | P ) as an explicit annotation by the programmer that interaction under an abstraction is admitted. If they want to freeze abstraction contexts, they just don't put COMM under an abstraction where an interaction could take place. In more detail

x?( y )( u?( v )P | COMM | u!( Q ) )

constitutes a programmer-supplied annotation, it's okay to reduce under the ( y )-abstraction, while

x?( y )( u?( v )P | u!( Q ) )

is an indication that the term under this abstraction is frozen, until it is released by communication on x.

Compositional interpretations of physical processes

This very simple insight of Marius' that interaction is enzymatically enabled creates a wide variety of dynamics that have broad range of applications! Merry Christmas to all and a Happy New Year!