This is the first time I ask a question on cstheory, so I am very sorry for my english. I have a (maybe very trivial) problem when trying to find a well-form representation for a root of a recursive equation in pi-calculus.

buffer(x) = out!<x>.buffer<x> + in?(y).buffer<y>

The equation above represents behaviors of a "mutable" single data buffer, it is very simple: the buffer's states are parameterized by x, that means its data cell's value is x. So the buffer can be read by the channel out! and updated by the channel in?. The buffer is somehow a fixpoint of the equation.

Firstly, it seems to me that it is easy to find out a well-formed representation for buffer (using the basic syntax of pi-calculus). The persistent output can be represented by replicating like !out. But latter, for the input, it is not easy as it seems.

Can anybody give me some suggestions ?

(I try to express some reactions from suggestions of @Martin Berger)

If we take an input with $\overline{in}\langle z \rangle$:

$\overline{in}\langle z \rangle \vert buffer(x) \rightarrow buffer(z)$ (recursive definition)

$\overline{in}\langle z \rangle \vert (\nu a)\big(\overline{a}\langle x\rangle | !a(x).( in(y).\overline{a}\langle y \rangle + \overline{out}\langle x \rangle.\overline{a}\langle x \rangle\big) \Rightarrow$ $(\nu a)\big(\overline{a}\langle z\rangle | !a(x).( in(y).\overline{a}\langle y \rangle + \overline{out}\langle x \rangle.\overline{a}\langle x \rangle\big) $ (encoding version)

And now we get an output with $out(t).P$:

$out(t) . P \vert buffer(z) \rightarrow P\lbrace z/t\rbrace \vert buffer(z)$ (recursive definition)

$out(t) . P \vert (\nu a)\big(\overline{a}\langle z\rangle | !a(x).( in(y).\overline{a}\langle y \rangle + \overline{out}\langle x \rangle.\overline{a}\langle x \rangle\big) \Rightarrow$ $P\lbrace z/t \rbrace \vert (\nu a)\big(\overline{a}\langle z \rangle | !a(x).( in(y).\overline{a}\langle y \rangle + \overline{out}\langle x \rangle.\overline{a}\langle x \rangle\big)$ (encoding version)

  • 2
    $\begingroup$ What is "the basic syntax of pi-calculus"? The original presentation uses parametric equations. Replication was introduced later. $\endgroup$ Dec 14, 2011 at 14:48
  • 1
    $\begingroup$ The simple encoding proposed below has a strict alternation between using $in$/$out$ and triggering new instances of the replication, so the situation you sketch in your amendment cannot occur. $\endgroup$ Dec 15, 2011 at 0:29
  • $\begingroup$ Ahh!!I have misunderstood your idea. Now it works. Thank you. $\endgroup$ Dec 15, 2011 at 15:47

2 Answers 2


The paper “On Recursion, Replication and Scope Mechanisms in Process Calculi” by Jesús Aranda, Cinzia Di Giusto, Catuscia Palamidessi, and Frank D. Valencia gives an encoding of the polyadic pi-calculus with recursive definitions in terms of the polyadic pi-calculus with replication and vice versa. The essence of the encoding (in the first direction) is to replace the recursive definition by the replication of a process, so that each invocation of the recursive definition results in a new process.

  • $\begingroup$ Thank you very much. I understand now the rule of encoding. It works. $\endgroup$ Dec 15, 2011 at 15:44

Here is a simple encoding: $ (\nu a)(\overline{a}\langle x\rangle | !a(x).\big( in(y).\overline{a}\langle y \rangle\ +\ \overline{out}\langle x \rangle.\overline{a}\langle x \rangle\big) $.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.