We work in interaction calculus. However, we will need a special non-deterministic agent Amb. To represent this agent, we also extend interaction calculus, but in a more conservative fashion than it was previously suggested in the original paper.
Instead, we prepend the list of its auxiliary ports with its extra principal port and introduce conversion for configurations to represent non-deterministic behavior of Amb:
<t1,..., tn | t = Amb(u, v, w), Δ> = <t1,..., tn | u = Amb(t, v, w), ∆>.
We assume that any interaction system’s signature Σ is implicitly extended by Amb with Ar(Amb) = 3, while its set of rules is implicitly extended with
α[x1,..., xn] >< Amb[y, α(x1,..., xn), y].
Instead, we prepend the list of its auxiliary ports with its extra principal port and introduce conversion for configurations to represent non-deterministic behavior of Amb:
<t1,..., tn | t = Amb(u, v, w), Δ> = <t1,..., tn | u = Amb(t, v, w), ∆>.
We assume that any interaction system’s signature Σ is implicitly extended by Amb with Ar(Amb) = 3, while its set of rules is implicitly extended with
α[x1,..., xn] >< Amb[y, α(x1,..., xn), y].
