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)