<p>The paper <a href="http://www.lix.polytechnique.fr/Labo/Jesus.Aranda/publications/Fmco07.pdf" rel="nofollow">“On Recursion, Replication and Scope Mechanisms in Process Calculi”</a> 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. </p>

CC BY-SA 3.0
2011-12-15T15:44:02.407Z
Thank you very much. I understand now the rule of encoding. It works.
Ta Thanh Dinh
CC BY-SA 3.0
2011-12-14T12:35:56.763Z
2011-12-17T21:32:56.423Z
2011-12-17T21:32:56.423Z
Dave Clarke
<p>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)
$.</p>

CC BY-SA 3.0
2011-12-14T17:10:22.647Z
2011-12-14T17:10:22.647Z
Martin Berger
<p>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.</p>

<pre><code>buffer(x) = out!&lt;x&gt;.buffer&lt;x&gt; + in?(y).buffer&lt;y&gt;
</code></pre>

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

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

<p>Can anybody give me some suggestions ?</p>

<p>(I try to express some reactions from suggestions of @Martin Berger)</p>

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

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

<p>$\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)</p>

<p>And now we get an output with $out(t).P$:</p>

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

<p>$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)</p>

CC BY-SA 3.0
2011-12-14T14:48:09.250Z
What is "the basic syntax of pi-calculus"? The [original presentation](http://www.lfcs.inf.ed.ac.uk/reports/89/ECS-LFCS-89-85/) uses parametric equations. Replication was introduced later.
Martin Berger
CC BY-SA 3.0
2011-12-15T00:29:11.657Z
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.
Martin Berger
CC BY-SA 3.0
2011-12-15T15:47:20.543Z
Ahh!!I have misunderstood your idea. Now it works. Thank you.
Ta Thanh Dinh
<lo.logic><pl.programming-languages><process-algebra><pi-calculus>
Parametric equation in pi-calculus
Ta Thanh Dinh
# Parametric equation in pi-calculus

(Asked by: username_0 on 2011-12-14)

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!.buffer + in?(y).buffer

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 @username_1)
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)

**Tags:** lo.logic, pl.programming-languages, process-algebra, pi-calculus

> **Comments:**
> **username_1**: What is "the basic syntax of pi-calculus"? The [original presentation](http://www.lfcs.inf.ed.ac.uk/reports/89/ECS-LFCS-89-85/) uses parametric equations. Replication was introduced later.  
> **username_1**: 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.  
> **username_0**: Ahh!!I have misunderstood your idea. Now it works. Thank you.  

---

## 2 answers

### Answer by username_2 on 2011-12-14. Score: 5 | Accepted answer

The paper [“On Recursion, Replication and Scope Mechanisms in Process Calculi”](http://www.lix.polytechnique.fr/Labo/Jesus.Aranda/publications/Fmco07.pdf) 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.

> **Comments:**
> **username_0**: Thank you very much. I understand now the rule of encoding. It works.  

---

### Answer by username_1 on 2011-12-14. Score: 2

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


---

