Back

UpAn Equational Relation for

External Choice

There is no primitives for external choice for ambient calculus because it is simulated by using parallel composition and restriction primitives.

As an example of the simulation, we define an external choice which we can use for both deterministic and non-deterministic purpose as follows:

Definition 1 (External Choice Operation ``+'')

$\mbox{Let }B\mbox{ and }C$ be any processes of ambient calculus. Then, we define$b[B]+c[C]$ as follows:

$$\hspace{-1em}\begin{array}[b]{ll}b[B]+c[C]\\\stackrel{\m......}[\mbox{\it out $c$}] \vert C)]).\\\end{array} \end{array}$$

$\Box$Example 1   We explain the behavior of the choice operation ``+'' by the following transitions: when the ambient $n[\mbox{\it in $a$}.$$\mbox{\it in $b$}]$ (we call it a traveling ambient) is running parallel to $a[b[]]+a[c[]]$, that is,  the traveling ambient can enter into either the ambient $a[\cdots]$ of $a[b[]]$ or $a[\cdots]$ of $a[c[]]$. Suppose it happened to choose the former:
 
 

$$\begin{array}[t]{ll}\begin{array}[t]{ll}\mbox{$\Yields^{\m......ace{12.3em} \vert c[])]),\end{array} \end{array} \end{array}$$

then, the capability $\mbox{{\it go}\rm ($\mbox{\it in $n$}.\mbox{\it out $n$}$)}$ in $a[\cdots b[]]$ is activated and consumed:
 
 

$$\begin{array}[t]{ll}\begin{array}[t]{ll}\mbox{$\Yields^{\m......ce{12.3em} \vert c[])]),\end{array} \end{array} \end{array}$$

then, the ambients $\mbox{\it trash}[]$ go out of the ambient $a[\cdots b[]]$:
 
 

$$\begin{array}[t]{ll}\begin{array}[t]{ll}\mbox{$\Yields^{\m......2.3em} \vert c[])]),\end{array} \end{array}\\\end{array}$$

since the ambient $\mbox{\it trash}[]$ appeared as a sibling of the ambient $a[\cdots b[]]$ and $a[\cdots c[]]$, they can move into the ambient $\mbox{\it trash}[]$:

$$\begin{array}[t]{ll}\begin{array}[t]{ll}\mbox{$\Yields^{\m......a$}] \vert c[])]]),\end{array} \end{array}\\\end{array}$$

then, the only ambient which have been chosen by traveling ambient (that is, $a[\cdots b[]]$ in this case) can escape from the ambient $\mbox{\it trash}[]$:
 
 

$$\begin{array}{ll}\begin{array}[t]{ll}\mbox{$\Yields^{\mbox......e{9.65em} \vert c[])]]),\end{array} \end{array} \end{array}$$

finally, the traveling ambient can reach the destination:

$$\begin{array}[t]{ll}\begin{array}[t]{ll}\mbox{$\Yields^{\m......e{9.65em} \vert c[])]] ).\end{array} \end{array} \end{array}$$ The contents of the ambient $\mbox{\it trash}[\cdots]$ are invisible from the environment, we find that our ``+'' can behave as an ideal choice operator. $\Box$

 Back