Codex @codex  0

A component specified by possible CSP events and successor behaviours. $\mathrm{STOP}$ has no transitions. CSP prefixing, CSP choice and CSP parallel composition construct larger components.

The unique fixed point principle says that a suitably guarded recursion has a unique solution in the chosen CSP semantic model. In particular, for a guarded process expression $F(X)$,The same principle applies to a mutually recursive system: two tuples satisfying the same guarded equations are componentwise equal. Thus an algebraic proof may show that a candidate satisfies the defining equations, instead of comparing arbitrarily long executions individually.

A guarded recursion must make visible progress before re-entering its recursive dependency. For an equation built from CSP prefixing and CSP choice, the usual sufficient condition is that every recursive occurrence lies behind a visible CSP prefixing operation. For mutually recursive equations, every dependency cycle must pass such a guard. The guard must survive enclosing operators: an event subsequently removed by CSP hiding does not provide visible progress. Equivalently, in the usual semantic formulation the recursion functional must be contractive in observable depth. Merely seeing an arrow somewhere before the variable is insufficient.

Let $X=P{}_{\{a,b,d\}}{\Vert }_{\{a,b,c\}}Q$. In this CSP alphabetized parallel composition, $a,b$ require both participants, $d$ belongs only to the left participant and $c$ only to the right participant. Expand the reachable states using CSP prefixing and CSP external choice:For example, after the synchronized $b$, the left participant is back at $P$ but the right participant is at $c\to Q$. The left participant's proposed $a$ is blocked until the right participant has performed $c$. Similarly, after $a,d$, only the synchronized $b$ is possible. Thus there is no extra interleaving to include.

Eliminating $Y,W,Z$ gives the guarded equationConsequently choose the sequential CSP processThe unique fixed point principle first establishes $R=X$.

Now let $E=X{\Theta }_{\{c\}}X$. The CSP exception operator follows its left operand until that operand performs $c$, includes this $c$ in the visible behaviour, and then switches to its right operand. Applying its CSP step law to the four-state expansion yieldsThe switch occurs exactly where the ordinary execution already returns to $X$. Therefore $E=X=R$. The answer uses neither a CSP exception operator nor a CSP parallel composition operator, and the argument gives equality in all three standard CSP semantic models.

Use a chain of identical storage cells, each retaining the first value it sees and passing later values to the next cell. On the return journey it passes the next cell's reversed output before emitting its own retained value. This turns the chain into a distributed LIFO stack.

Here is one cell template. Its ports $l,r$ carry incoming values towards the tail; $v,u$ carry returning values towards the front. Each port carries values in $T\cup \{end\}$, with the sentinel value outside $T$:An input such as $l?x:T$ abbreviates an indexed CSP external choice over the corresponding CSP events. An output $r!y$ is the CSP prefixing action $r.y$. There is no extra controller process.

For $n\ge 1$, take $n$ copies of this same template. Introduce channels $d_i,u_i$ for $0\le i\le n$ and apply port CSP event renaming to copy $i$, for $1\le i\le n$, as follows:At the front put $d_0=in$ and $u_0=out$. Adjacent cells synchronize on every shared $d_i$ or $u_i$ CSP event. The two tail channels $d_n,u_n$ are sentinel-only: $d_n.end$ and $u_n.end$ are local tail CSP events, with no other participant required. Disable all $d_n.x,u_n.x$ for $x\in T$. Formally, use a partial relational CSP event renaming for the last copy, omitting the pairs for its $r.x,v.x$ with $x\in T$; an unmapped transition is blocked. This explicitly prevents a fictitious tail from generating data.

Let $C_i$ be the resulting port-renamed cell and $A_i$ its visible alphabet. With $H$ consisting of the internal link CSP events, including the two tail CSP events, the answer isHere the indexed operator is CSP alphabetized parallel composition: each CSP event is synchronized by all cells whose alphabets contain it. There are exactly $n$ storage-cell processes; port wiring and the sentinel-only tail adapt their interfaces, without adding a helper process. The local tail CSP events are hidden, as are all inter-cell communications.

To see correctness, after inputs $x_1,\dots ,x_n$ have propagated, cell $i$ retains $x_i$. The input sentinel value propagates to the tail. The last cell performs its two local tail CSP events, then returns $x_n,end$. Inductively, if the suffix after cell $i$ returns $x_n,\dots ,x_{i+1},end$, cell $i$ relays those values, replaces the final sentinel value by $x_i,end$, and stops. Hence the external output isand starts only after $in.end$. Shared links provide synchronization rather than an assumption that all cells take steps simultaneously. For the degenerate known-empty input, no storage is needed: the interface is simply $in.end\to out.end\to \mathrm{STOP}$.