Overview
In the previous post, “Intro to Design of Computational Calculi 3,” we covered program equivalence and operational semantics. In this first part of two, we will discuss the injection of names into ρ-calculus.
Pure ρ-calculus is an elegant, abstract, minimal model for asynchronous, concurrent computation. It was designed to be useful, powerful, and efficient, but not necessarily “user-friendly.” As is, it does not provide a robust programming language. This can be easily remedied by injecting names. This is how Rholang was born.
Injecting names into rho-calculus
Syntax
In building ρ-calculus, we have extensively discussed the role of processes and names and the rules under which they operate. However, in this abstract treatment, we did not connect these constructs to anything more concrete than “programs” and “code.” To make ρ-calculus more practical, we can inject names that are not just quoted processes. We can give semantic meaning (in terms of the pure ρ-calculus) to an auxiliary supply of names by mapping the names to a specified namespace. This is the process of constructing Rholang from ρ-calculus (in the end, we get more ground terms besides 0).
Let M be a set of names (i.e. URIs, email addresses, characters, numbers, etc.). We define the collection of ρ-calculus processes, P[M], under the injection of the names M by
P[M] ::= 0 | for(m ← n)P | n!(Q) | P|Q | *x
x ::= @P
m,n ::= x | M
Let’s investigate each line here. We make a distinction between the names native to ρ-calculus (i.e. quoted processes) and the injected names (i.e those from the set M).
- P[M] ::= 0 | for(m ← n)P | n!(Q) | P|Q | *x
As in pure ρ-calculus, we still have the stopped process 0, parallel composition, and dereference of a quoted process. The two differences here are that we may now also send and receive messages on injected name channels. This means that it is now possible to send/receive messages on channels corresponding to the names from the set M.
- x ::= @P
This is the usual identification of native names (i.e. quoted processes) with a hint of subtlety due to the fact that processes may now mention injected names as well.
- m,n ::= x | M
This is what tells us that in addition to the native names, the injected names may be used for sending and receiving. Piecing all these declarations together, we see that native names still play the same role here as in pure ρ-calculus, but the injected names may not be dereferenced. This makes sense considering that they do not directly correspond to any process.
Using injection, we can provide a step-by-step mapping from user-friendly programming languages down to ρ-calculus. As an example of this principle, we can encode the ‘select’ construct into ρ-calculus, even though ρ-calculus doesn’t have the syntactic construct ‘select’.
Semantics
The idea for ρ-calculus is to be a minimal framework that can be understood well and have the ability to inject useful things into it. Injected items do not have an immediate semantic interpretation in ρ-calculus. Once we have demonstrated a compilation, the semantics move over to the tuplespace, by becoming data that can be added or queried, because this is more efficient. This step-by-step encoding of features into ρ-calculus is how Rholang was born.
In the context of blockchains
In the expression:
for(y ← x)P | x!(Q1) |…| x!(Qn)
we think of y as an address that does not yet have a value. A comm event will occur, reducing the expression. Once the comm event occurs, y will be replaced by another name, giving the address a value. We know that this has happened once we see the unguarded process P; this is when the transaction is committed. Here, there are multiple clients submitting values to the given address so this represents a race condition. Since this expression reduces, we refer to it as a redex.
Every validator that is validating in the namespace that includes x, runs a copy of this redex. Since there are several valid reductions of this redex, the validators in this namespace must run consensus (Casper) to determine the winner of the race condition. Once consensus is reached, all validators record the winning value as showing up at the address y.
For the validators not validating in this namespace, they simply don’t care about this redex. This feature paralellizes computations happening in different namespaces.
For the full details on how the operational semantics of process calculi and tuplespaces come into play in the context of blockchains, Greg refers us to the paper “Mobile Processes for Programming the New Blockchain.”
Summary
In this first of two parts, we discussed the methodology of injecting names into ρ-calculus for the purpose of creating a user-friendly programming language, Rholang. We briefly described how we exploit the intrinsic semantics of the tuplespace and use independent namespaces to make computations more efficient in the context of a blockchain.
In part two of this lecture, we explore two variants of the operational semantics for ρ-calculus: process annihilation and contextualized communication.
References
- Currin, Denman, Eykholt, Meredith. Mobile Process Calculi for Programming the Blockchain: Release 1.0
- Denman, Eykholt, Meredith. RChain Platform Architecture