9

Scope extrusion is the key advance of $\pi$-calculus over earlier calculi such as CCS. Scope extrusion is the source of $\pi$-calculus' power of expressing (in a succint and compositional way) other forms of computation. You are correct that there are two forms of binders, one for variable to be substituted for, and one for names whose scope can be extruded....


9

If we separate the notion of channel names from variables, we can make the ν-binder a true binder where the variable following ν is a normal bound variable and we only need to add a reduction rule for it, which is just like the reference cell allocation in ML: (νx)P ⟶ P[c/x] where c is a globally fresh channel name. Then, everything made sense to me. ...


8

This is a really interesting question and only partially understood. The $ \newcommand{\OUT}[2]{\overline{#1} #2 } $ precise answer to such questions depends in subtle ways on exactly what the ambient $\pi$-calculus is and exactly what feature you are encoding. For sums you need to realise that there are different kinds of sums for example input ...


7

There are plenty such typing systems. Most work is based on the linear/affine typing system introduced in (1) and generalised in (2). Here are the main works on this subject. In (3) the typing system ensures a precise match with PCF (int its call-by-name variant -- changing to call-by-value is easy). In (4) the typing system gives a precise interpretation ...


3

The process $P{\langle 0, c, d\rangle}$ in the context of a recursively defined process like $$ P{\langle count, c, d\rangle} \quad\stackrel{\text{def}}{=}\quad c(v).(\overline{d}\langle count+v \rangle\ |\ P{\langle count+v, c, d\rangle}) $$ does the job, although we might quibble about how exact it models the original program. However, there is no ...


3

The key to understanding scope management in $\pi$-calculi is to look at the structural congruence $P \equiv Q$ and at the notions of free name $\newcommand{\FN}[1]{\text{fn}(#1)}\FN{P}$ and free variable $\newcommand{\FV}[1]{\text{fv}(#1)}\FV{P}$. The great novelty that distinguishes $\pi$-calculi from its predecessors is the ability to extrude scope. It is ...


2

Sequential execution is an edge case of concurrent computation. Robin Milner said this clearly in his Turing award lecture "Elements of interaction" (CACM, 36(1), 1993): I reject the idea that there can be a unique conceptual model, or one preferred formalism, for all aspects of something as large as concurrent computation, which is in a sense the whole of ...


2

Let me clarify the setting, which has nothing to do with $\pi$-calculus or bisimulation. The first thing you have to realise that it does not make much sense to talk about a programming language without reference to the notion of program equivalence you intend to impose on the language. That's because We usually identify certain programs (e.g. f(x:int) = {...


1

You should $\alpha$-rename to avoid conflict with the variable names. That is, you should prove weakening of the form: $\Gamma \vdash (\upsilon y) P$ implies $\Gamma, x : T \vdash (\upsilon y) P$. $\alpha$-equivalence and capture-avoiding substitution is an important concept to understand in type theory: I would recommend studying this concept for the ...


1

Milner defines the SCCS calculus in [1]. This is a generalization of CCS where the actions form an abelian group, and where the communication rule is defined as in my question. [1] Milner, R. Calculi for synchrony and asynchrony. 1983. https://www.sciencedirect.com/science/article/pii/0304397583901147


Only top voted, non community-wiki answers of a minimum length are eligible