1
$\begingroup$

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

$\endgroup$
0
3
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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