Overview

 

 
In the first part, we discussed “Injecting Names into ρ-calculus,” which is what allows us to create the programming language, Rholang, from the computational calculus, ρ-calculus.
In this second and final part, we will explore two variants of the operational semantics for ρ-calculus. These variants turn out to be more suitable for modeling biological and physical phenomena than the π-calculus or ambient calculus. The first variant deals with process annihilation, which is a relationship between processes reminiscent of matter/antimatter annihilation. The second variant deals with contextualized communication and allows for ease of communicating between different protocol layers.
 

Process annihilation

 
In the first variant, we modify the operational semantics by adding a precondition to the comm rule. Let’s start by defining what it means for two processes to annihilate each other. Two processes P, Q annihilate, denoted P ⊥ Q, means:
∀R. (P|Q →* R)  ⇒ R →* 0
which is to say that if P running in parallel with Q reaches some state R, then that state R eventually reaches 0. The implication then is that all reduction paths lead to 0 (why?). Even if there is recursion occurring within the processes, this relationship ensures termination. Just to be exceedingly clear, the expression A →∗ B means the process A eventually reduces to the process B, or in other words, A reduces to B in finitely many steps (including zero steps).
Comm rule for annihilating processes:
xt = @T, xs = @S, S ⊥ T  ⇒  for(y ← xt)P | xs!(Q)  → P{@Q/y}
On the surface, this definition is self-referential (we define process annihilation in terms of reductions and then annihilation implies something about reductions, how can it be?), and one may rightfully wonder if it ever gets off the ground. To get off the ground, we show that the stopped process annihilates itself:
0|0 ≡ 0  ⇒ 0|0 →* 0  ⇒ 0 ⊥ 0
for(@0 ← @0)0 | @0!(0)  → 0
Therefore, 0 ⊥ 0, or in other words, @0 is its own co-channel. In general, we say that xs and xt are in a channel/co-channel relationship. And we are officially off the ground! Now that we know 0 ⊥ 0, we then get:
for(@0 ← @0)0|@0!(0) → 0
which implies:
for(@0 ← @0)0 ⊥ @0!(0)
In fact, we have also shown the existence of an infinite family of names which can serve as either end (source or target) of a channel.
The ground serves as the base case of this well-founded condition, which means we can implement this code in Scala.
In the case of physical phenomena, there is an explicit reductionist viewpoint. The dynamics of higher level phenomena are supposed to be accounted for by the dynamics of lower level phenomena. The hierarchy goes something like this:
Biological dynamics ← chemical dynamics ← physical dynamics ← quark dynamics ← field/string dynamics ← maybe something more fundamental…?
In this computational model, operations at one scale depend on operations at another scale. This is analogous to the compositionality we observe in nature. This compositionality is fundamentally different from what we have in the λ-calculus and π-calculus.
 

Contextualized communication

 
In the second variant, we modify the operational semantics by contextualizing the comm rule. This variant has the advantage of addressing issues of interoperability of different protocol layers. Contexts are of the form:
K ::= [ ] | for(y ← x)K | x!(K) | K|Q
and we use the convention:
K[P] := K{P/[ ]}
Contexts basically give us a way to knock “holes” in processes so that we may insert other processes.
Communication in the context K is the comm rule
CommK : for(y ← x)P | x!(Q) → P{@K[Q]/y}
It turns out that knocking holes in types, like the type for processes, is related to the notion of a derivative from ordinary calculus [1]. We will discuss this concept further in later posts.
The motivation for thinking about things in this way: HTTP is typically written over top of TCP. In many cases, you may have applications which are used to talking to other applications at the TCP level (or HTTP level). You may want to connect them so that the TCP applications can talk to the HTTP applications. An adapter is needed to unpack HTTP requests and turn them into TCP requests (or package TCP requests and turn them into HTTP requests). This adapter code can be modeled with a context K which is providing the adapter, packaging and unpackaging requests at different protocol levels.
Adapting between different protocol levels, represented by different contexts, is given by composition of the contexts:
CommK :  for(y ← x)P | x!(Q) → P{@K[Q]/y}
CommK’ :  for(y ← x)P | x!(Q) → P{@K’[Q]/y}
CommK◦K’:  for(y ← x)P | x!(Q) → P{@K[K’[Q]]/y}
Mathematicians like to understand the operational semantics for process calculi in terms of category theory by creating categorical models. In the categorical models of process calculi, a way to preserve behavioral structure has been missing. The CommK rule gives the first ever way to compose operational semantics while preserving behavioral structure. We will explore category theory and categorical models in more depth in future posts.
 

Summary

 
In this second and final part of the fourth DoCC lecture, we discussed two variants of the operational semantics for ρ-calculus: process annihilation and contextualized communication. Both variations offer a notion of compositionality which resembles the way complex, natural processes are built from more elementary one. This compositionality contributes one of the many ways that RChain plans to achieve massive scalability.
 

Reference

 

1. McBride, Connor. Derivative of a Regular Type is its Type of One-Hole Context