<p>The process $P{\langle 0, c, d\rangle}$ in the context of a recursively defined process like </p>

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

<p>does the job, although we might quibble about how exact it models the original program. However, there is no problem with a more explicit modelling of state.</p>

<p>Translation from recursion to replication is folklore, easy and already discussed in (1): let's assume you have a process $P$ and it uses recursive definitions $X_1\langle \vec{a}_1\rangle = Q_1$, ..., $X_n\langle \vec{a}_n\rangle = Q_n$, where for simplicity we assume that no $Q_i$ uses recursively defined processes. (This restriction is easy to lift.) Then any use of $X_i\langle \vec{a}\rangle$ in $P$ is replaced by an output $\overline{x_i}\langle \vec{a}\rangle$. Let's call the resulting process $P_{new}$. Now the process</p>

<p>$$
   (\nu x_1 ... x_n) ( P_{new} \ |\ !x_1(\vec{a}_1).Q_1 \ |\ ... \ |\ !x_n(\vec{a}_n).Q_n )
$$</p>

<p>does without recursion what $P$ does with recursion. We might say that each recursive equation is replaced by a 'recursion server'.
I'm glossing over a few details here. For more, see e.g. (2).</p>

<p><hr>
<sup></p>

<ol>
<li><p>R. Milner, <a href="http://www.lfcs.inf.ed.ac.uk/reports/91/ECS-LFCS-91-180/" rel="nofollow noreferrer">The Polyadic pi-Calculus: A Tutorial</a>.</p></li>
<li><p>J. Aranda, C. Di Giusto, C. Palamidessi, F. D. Valencia, <a href="http://www.lix.polytechnique.fr/~fvalenci/papers/fmco07.pdf" rel="nofollow noreferrer">On
Recursion, Replication and Scope Mechanisms in Process Calculi.</a>
</sup></p></li>
</ol>

CC BY-SA 3.0
2017-01-28T08:31:37.443Z
2017-02-04T12:53:28.700Z
2017-02-04T12:53:28.700Z
Martin Berger
<p>Suppose I have a process that informally does this</p>

<pre><code>int count = 0
forever do
    receive x on some channel c;
    count += x;
    output count on some channel d;
</code></pre>

<p>(here ";" means sequential composition -- so P ; Q means do P, and then do Q)</p>

<p>I know how to implement the sequential composition in the pi-calculus -- that was answered in another question here. I also think I know how to model a state variable like count in the pi-calculus.</p>

<p>But what I can't seem to encode in the pi-calculus is the infinite loop. To do that I would either need recursive process definitions, or use replication somehow. But I can't work out the correct way to use replication here -- because I can't work out what process I am replicating (since the use of state means the process being replicated is different every time).</p>

<p>Any help would be great.</p>

<p>thanks
graham</p>

<pi-calculus>
Encoding an infinitely looping process with state in the pi-calculus
gym
# Encoding an infinitely looping process with state in the pi-calculus

(Asked by: username_0 on 2017-01-28)

Suppose I have a process that informally does this
int count = 0
forever do
    receive x on some channel c;
    count += x;
    output count on some channel d;

(here ";" means sequential composition -- so P ; Q means do P, and then do Q)
I know how to implement the sequential composition in the pi-calculus -- that was answered in another question here. I also think I know how to model a state variable like count in the pi-calculus.
But what I can't seem to encode in the pi-calculus is the infinite loop. To do that I would either need recursive process definitions, or use replication somehow. But I can't work out the correct way to use replication here -- because I can't work out what process I am replicating (since the use of state means the process being replicated is different every time).
Any help would be great.
thanks
graham

**Tags:** pi-calculus

---

## 1 answers

### Answer by username_1 on 2017-01-28. Score: 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 problem with a more explicit modelling of state.

Translation from recursion to replication is folklore, easy and already discussed in (1): let's assume you have a process $P$ and it uses recursive definitions $X\_1\langle \vec{a}\_1\rangle = Q\_1$, ..., $X\_n\langle \vec{a}\_n\rangle = Q\_n$, where for simplicity we assume that no $Q\_i$ uses recursively defined processes. (This restriction is easy to lift.) Then any use of $X\_i\langle \vec{a}\rangle$ in $P$ is replaced by an output $\overline{x\_i}\langle \vec{a}\rangle$. Let's call the resulting process $P\_{new}$. Now the process

$$
(\nu x\_1 ... x\_n) ( P\_{new} \ |\ !x\_1(\vec{a}\_1).Q\_1 \ |\ ... \ |\ !x\_n(\vec{a}\_n).Q\_n )
$$

does without recursion what $P$ does with recursion. We might say that each recursive equation is replaced by a 'recursion server'.
I'm glossing over a few details here. For more, see e.g. (2).

---

1. R. Milner, [The Polyadic pi-Calculus: A Tutorial](http://www.lfcs.inf.ed.ac.uk/reports/91/ECS-LFCS-91-180/).
2. J. Aranda, C. Di Giusto, C. Palamidessi, F. D. Valencia, [On
   Recursion, Replication and Scope Mechanisms in Process Calculi.](http://www.lix.polytechnique.fr/~fvalenci/papers/fmco07.pdf)


---

