doc/pseudoambients.lyx
author Tony Garnock-Jones <tonygarnockjones@gmail.com>
Wed, 16 Jan 2019 17:15:58 +0000
changeset 438 1fe179d53161
parent 0 ea4e1a00864c
permissions -rw-r--r--
Add missing primitive implementation for the plain interpreter.

#LyX 1.3 created this file. For more info see http://www.lyx.org/
\lyxformat 221
\textclass article
\language english
\inputencoding auto
\fontscheme palatino
\graphics default
\paperfontsize default
\spacing single 
\papersize a4paper
\paperpackage widemarginsa4
\use_geometry 0
\use_amsmath 0
\use_natbib 0
\use_numerical_citations 0
\paperorientation portrait
\secnumdepth 3
\tocdepth 3
\paragraph_separation indent
\defskip medskip
\quotes_language english
\quotes_times 2
\papercolumns 2
\papersides 1
\paperpagestyle default

\layout Title

Pseudo-ambients
\layout Author

Tony Garnock-Jones <tonyg@kcbbs.gen.nz>
\layout Date

1 November 2004
\layout Standard

The idea is to take a calculus much like Cardelli's Mobile Ambients, and
 short-circuit the routing so that paths are one element long and always
 take you directly to the given port.
 
\begin_inset Formula $\nu$
\end_inset 

 is interpreted as allocation; the store holds allocated ports.
 Ports/locations have exactly one parent, except for the top location, 
\begin_inset Formula $\top$
\end_inset 

, which has no parent.
 The parent of a location is the location at which the 
\begin_inset Formula $\nu$
\end_inset 

 was executed.
 This gives rise to a tree of locations.
 Ports do not move once they are defined, and are garbage collected when
 no longer referenced, in the usual manner.
\layout Standard


\begin_inset Formula \begin{eqnarray*}
\nu x.P &  & \textrm{allocation}\\
P\vert Q &  & \textrm{par}\\
\left\langle \tilde{x}\right\rangle  &  & \textrm{output message}\\
(\widetilde{x}).P &  & \textrm{input message}\\
!(\widetilde{x}).P &  & \textrm{replicated input}\\
x[P] &  & \textrm{relocation}\\
\mathbf{lift}\, x(y).P &  & \textrm{reflection}\\
\mathbf{eval}\, x &  & \textrm{evaluation}\end{eqnarray*}

\end_inset 


\layout Standard

Processes are written with an environment 
\begin_inset Formula \[
\mathcal{E}\subset\{ x\mapsto a\,\vert\, x,a\in\mathcal{L}\}\]

\end_inset 

with ports/locations 
\begin_inset Formula $a,b,c,\top\in\mathcal{L}$
\end_inset 

, and processes 
\begin_inset Formula $P$
\end_inset 

, 
\begin_inset Formula $Q$
\end_inset 

, 
\begin_inset Formula $R$
\end_inset 

:
\layout Standard


\begin_inset Formula \[
\mathcal{E}\vdash a[P]\,\Vert\, b[Q]\,\Vert\, c[R]\]

\end_inset 


\layout Standard

so reduction proceeds as in figure 
\begin_inset LatexCommand \ref{cap:Reduction-rules}

\end_inset 

, where 
\begin_inset Formula $\sigma$
\end_inset 

 are appropriate substitutions.
 Note that the rule for lift is currently not very well defined.
\layout Standard


\begin_inset Float figure
wide true
collapsed false

\layout Standard


\begin_inset Formula \begin{align*}
\mathcal{E}\vdash a[\nu x.P] & \rightarrow\mathcal{E}\cup\{ x\mapsto a\}\vdash a[P] & \textrm{R-alloc}\\
\mathcal{E}\vdash a[P\vert Q] & \rightarrow\mathcal{E}\vdash a[P]\Vert a[Q] & \textrm{R-par}\\
\mathcal{E}\vdash a[\langle\tilde{x}\rangle]\,\Vert\, a[(\tilde{y}).P] & \rightarrow\mathcal{E}\vdash a[P\sigma] & \textrm{R-comm}\\
\mathcal{E}\vdash a[\langle\tilde{x}\rangle]\,\Vert\, a[!(\tilde{y}).P] & \rightarrow\mathcal{E}\vdash a[P\sigma]\,\Vert\, a[!(\tilde{y}).P] & \textrm{R-repcomm}\\
\mathcal{E}\vdash a[x[P]] & \rightarrow\mathcal{E}\vdash x[P] & \textrm{R-reloc}\\
\frac{\alpha=\{ a\vert a\mapsto x\in\mathcal{E}\},\,\mathbf{P}=x[P_{0}]\,\Vert\,{\displaystyle \prod_{a\in\alpha}}a[P_{a}]}{\mathcal{E}\lyxlock\vdash a[\mathbf{lift\,}x(y).P]\,\Vert\,\mathbf{P}} & \rightarrow\mathcal{E}\cup\{ y\mapsto a\}\vdash a[P\sigma]\,\Vert\,\left\lceil \mathbf{P}\right\rceil ^{y} & \textrm{R-reflect}\end{align*}

\end_inset 


\layout Caption


\begin_inset LatexCommand \label{cap:Reduction-rules}

\end_inset 

Reduction rules
\end_inset 


\the_end