Tag Info

10

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....

10

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

Membrane Computing is a model that is based on the possibility or not of movement of molecules through membranes; also on possible reactions of these molecules inside a membrane compartment. While this is not specifically talking about proteins, in reality some of these molecules and the channels through which they pass would be proteins. Here is an ...

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 ...

4

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 ...

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


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) = {...

2

There are models of how to compute with arbitrary chemical reactions using molecules that drift around and randomly collide. They crop up in parallel computing models sometimes. It's probably not what you're looking for, but it might be interesting to learn about. For an example, the ambient calculus. The process calculus wikipedia page includes some others.

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