# Parametric equation in pi-calculus

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)

• What is "the basic syntax of pi-calculus"? The original presentation uses parametric equations. Replication was introduced later. – Martin Berger Dec 14 '11 at 14:48
• The simple encoding proposed below has a strict alternation between using $in$/$out$ and triggering new instances of the replication, so the situation you sketch in your amendment cannot occur. – Martin Berger Dec 15 '11 at 0:29
• Ahh!!I have misunderstood your idea. Now it works. Thank you. – Ta Thanh Dinh Dec 15 '11 at 15:47

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