Parametric equation in pi-calculus

Question

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)

Answer 1

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.

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