Encoding an infinitely looping process with state in the pi-calculus

Question

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

Answer 1

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.

2. J. Aranda, C. Di Giusto, C. Palamidessi, F. D. Valencia, On Recursion, Replication and Scope Mechanisms in Process Calculi.