%%% Start of LaTeX Document %%%
\documentstyle[11pt]{article}
%\documentstyle[a4,11pt]{article}
%\documentstyle[11pt]{mnotes}    

% 1in margins at left and right
\oddsidemargin=0in
\evensidemargin=0in
\textwidth=6.25in              % A4 paper is 8.25in wide

% 1in margins at top and bottom
\headheight=0pt
\headsep=0pt
\topmargin=0in
\textheight=9.7in              % A4 paper is 11.7in high

\pagestyle{plain}
\setlength{\parindent}{0cm}
\setlength{\parskip}{\medskipamount}
\setlength{\itemsep}{\smallskipamount}

\title{Notes on Using Small Processes to Implement Functional Languages}
\author{
        {\it John Glauert} \\
	{\em jrwg@sys.uea.ac.uk}}
%\reportref{Draft}
\date{Version 3}

\newenvironment{conjecture}{\noindent{\bf Conjecture: }}{}
\newenvironment{conclusion}{\noindent{\bf Conclusion: }}{}
\newenvironment{assignment}[1]{\noindent{\bf Assignment for {#1}: }}{}

\newcommand{\sembrac}[1]{[\![ #1 ]\!]}
\newcommand{\infer}[3]
           {\vspace{.2cm}
            \hbox{${\displaystyle {\frac {#1}{#2}}\hspace{.5cm}{#3}}$}
            \vspace{.2cm}}
% New macros
%\input{john-pi-macros}
% Process notation
\newcommand{\parprocs}[2]{{#1}\,|\,{#2}}
\newcommand{\restrict}[2]{({\nu}\,{#1})\,(\,{#2}\,)}
\newcommand{\replicate}[2]{!\,{#2}}
\newcommand{\guardedrep}[3]{!\,({#2} \cdot {#3})}
\newcommand{\recdef}[2]{{\bf rec} {\recvar {#1}} \cdot {#2}}
\newcommand{\guardedrec}[3]{{\bf rec} {\recvar {#1}} \cdot {#2} \cdot
(\,\parprocs {#3} {\recvar {#1}}\,)}
\newcommand{\recvar}[1]{{#1}}
\newcommand{\agtuse}[2]{\recvar {#1} ({#2})}
\newcommand{\agtdef}[3]{\agtuse {#1} {#2} = {#3}}
\newcommand{\inpact}[3]{{#1}({#2}) \cdot {#3}}
\newcommand{\inpacta}[2]{{#1}({#2})}
\newcommand{\outact}[3]{\overline{#1}\,{#2} \cdot {#3}}
\newcommand{\outacta}[2]{\overline{#1}\,{#2}}
\newcommand{\match}[3]{{#1}={#2} \cdot {#3}}
\newcommand{\inaction}{0}
\newcommand{\pair}[2]{{#1}\,{#2}}
\newcommand{\triv}{}
%\input{john-proc-macros}
% New Process notation
\newcommand{\PruleChange}[3]{{#1}\;?\;{#2} & := & {#3}}
\newcommand{\PruleSpawn}[3]{{#1}\;?\;{#2} & \rightarrow & (\,{#3}\,)}
\newcommand{\Prule}[4]{{#1}\;?\;{#2} & \rightarrow & (\,{#3}\,)\;:=\;{#4}}
\newcommand{\Ppar}[2]{{#1}\,|\,{#2}}
\newcommand{\Pcall}[2]{{#1}\,!\,{#2}}
\newcommand{\Pdef}[2]{{#1}:\,{#2}}
% Translation representation
\newcommand{\transwhere}[3]{& & {\makebox[1.5cm][l]{where}}
{#1}\;?\;{#2}\;\cdot\;(\,{#3}\,)}
\newcommand{\transand}[3]{& & {\makebox[1.5cm][l]{and}}
{#1}\;?\;{#2}\;\cdot\;(\,{#3}\,)}
\newcommand{\F}{Facile}
\newcommand{\Cham}{Chemical Abstract Machine}
\newcommand{\Lc}{$\lambda$--calculus}
\newcommand{\LC}{$\lambda$--Calculus}
\newcommand{\Lx}{$\lambda$--expression}
\newcommand{\Pc}{$\pi$--calculus}
\newcommand{\PC}{$\pi$--Calculus}
\newcommand{\PPC}{Polyadic $\pi$--Calculus}
\newcommand{\PPc}{polyadic $\pi$--calculus}
\newcommand{\RA}{{\em return-address\/} channel}
\newcommand{\Whnf}{weak head--normal form}
% Source representation
\newcommand{\Labs}[2]{\lambda{#1}.\,{#2}}
\newcommand{\Lapp}[2]{{#1}\,{#2}}
\newcommand{\App}[2]{{#1}\,@\,{#2}}
\newcommand{\AppL}[2]{{#1}\,@_L\,{#2}}
\newcommand{\AppE}[2]{{#1}\,@_E\,{#2}}
\newcommand{\Ltriv}{()}
\newcommand{\Lpair}[2]{({#1},{#2})}
% Translation representation
\newcommand{\transexp}[2]{\sembrac{#1}_{#2}}
\newcommand{\transdef}[3]{\transexp{#1}{#2} & = & {#3}}
% End of macros
\begin{document}
\maketitle

\section{Introduction}

This document is an attempt to formalise some of the questions about using process networks to model, or implement, functional languages.

Since the \Lc\ is used in a possibly non--standard way, I try to formalise its use in this context. I will go on to relate this work to Milner's original work on Functions as Processes and to other more recent work.

\begin{conjecture}
Where I say conjecture it is something that I would like you to try to verify or refute! This is similar to an assignment, but is hopefully a properly stated conjecture.
\end{conjecture}

\begin{conclusion}
Once one of us has come back with a proof or refutation, or a reference to the same elsewhere, I will add a note to that effect.
\end{conclusion}

\subsubsection*{Version 3}

This revises the document in the light of discussions, posing some more fundamental questions about marked rewriting schemes.

\subsubsection*{Version 2}

This contains more discussion about the process translations, giving the translation scheme and examples of its use.

\subsubsection*{Version 1}

This is the initial release containing many errors no doubt.

\section{\LC\ Questions}

\subsection{\LC\ Syntax}

The language is given by:
\begin{eqnarray*}
e & ::= &  x \mid \Labs{x}{e} \mid \Lapp{e}{e} \\
v & ::= &  \Labs{x}{e}  
\end{eqnarray*}
$v$ is the class of {\Whnf}s for closed terms.

We will begin by being interested just in rewriting closed terms to \Whnf.
The assumption will be that this is the world we are considering. It will be made clear where statements or claims are being made about more general reduction.

\subsection{\LC\ Semantics}
We will define the reduction relation for \Lc\ terms using a set of inference rules.

\subsubsection{Full \LC}
The following rules would apply to full \Lc. We have the $BETA$ rule and a set of rules which allow reduction of a redex in any context:

\begin{center}
\begin{tabular}{lcl}
$BETA: \:\: (\lambda x.e)\;e' \:{\rightarrow}\: e\,[e'/x]$
\end{tabular}

\begin{tabular}{lcccl}
$APPL: \:\: {\infer{e \:{\rightarrow}\: e''}
       {e\;e' \:{\rightarrow}\: e''\;e'}
       { }}$
& &
$APPR: \:\: {\infer{e' \:{\rightarrow}\: e''}
       {e\;e' \:{\rightarrow}\: e\;e''}
       { }}$
& &
$LAMB: \:\: {\infer{e \:{\rightarrow}\: e'}
       {\lambda x.e \:{\rightarrow}\: \lambda x.e'}
       { }}$
\end{tabular}
\end{center}

This reduction relation defines a one--step strategy which allows reduction of any redex. Of course this allows us to choose non--standardizing sequences.

By imposing conditions on the sequences we can get sensible strategies and this can be done in some cases by using different inference rules for identifying redexes. We are rarely going to consider reduction under a $\lambda$ so the $LAMB$ rule will not appear.

\subsubsection{Lazy--\LC}
The following specifies reduction to \Whnf\ using the {\em normal--order} strategy of the lazy--\LC. This has just $APPL$ and the $BETA$
rule:
\begin{center}
\begin{tabular}{lccl}
$BETA: \:\: (\lambda x.e)\;e' \:{\rightarrow}\: e\,[e'/x]$
& &
$APPL: \:\: {\infer{e \:{\rightarrow}\: e''}
       {\Lapp{e}{e'} \:{\rightarrow}\: \Lapp{e''}{e'}}
       { }}$
\end{tabular}
\end{center}

In closed terms there is a tree of application or $@$ nodes with abstractions $\Labs{x}{e}$ at the leaves. Unless the term is an abstraction, in which case it is in \Whnf, there will be a single redex identified by the relation above.

\subsubsection{Candidate Redexes}
It is hard to avoid using the term {\em redex} for instances of the $BETA$ rule, even though the reduction relation may not choose them. We will call the chosen redexes {\em candidate redexes} or just {\em candidates}.

\begin{conjecture}
There is an accepted term for candidate redexes. Was it {\em admissable} redexes?
\end{conjecture}

A property we might be interested in is whether candidates remain candidates even if another candidate is chosen at a given step. Clearly under the full \Lc\ relation every redex is a candidate so it is only possible to get rid of candidates by reducing them or erasing them. I seem to remember that these were called {\em persistently needed} redexes

\begin{conjecture}
In the lazy--\Lc\ there is never more than one candidate, which is always reduced. If we are interested in reduction to \Whnf\ then I conjecture that the normal--order strategy, as defined above, leads to minimal {\Whnf}s.
\end{conjecture}

\subsubsection{Eager--\LC}
Taking full \Lc\ but omitting the $LAMB$ rule gives:

\begin{center}
\begin{tabular}{lcl}
$BETA: \:\: (\lambda x.e)\;e' \:{\rightarrow}\: e\,[e'/x]$
\end{tabular}

\begin{tabular}{lccl}
$APPL: \:\: {\infer{e \:{\rightarrow}\: e''}
       {e\;e' \:{\rightarrow}\: e''\;e'}
       { }}$
& &
$APPR: \:\: {\infer{e' \:{\rightarrow}\: e''}
       {e\;e' \:{\rightarrow}\: e\;e''}
       { }}$
\end{tabular}
\end{center}

\begin{conjecture}
This does not identify candidates under $\lambda$, but after reduction, residuals or descendents of some candidates might be under $\lambda$. Hence I conjecture that fair reduction under this scheme will lead to {\Whnf}s, but not necessarily minimal {\Whnf}s.
\end{conjecture}

\subsubsection{Properties of Candidates}
I am interested in schemes where candidates, once identified, are always reduced eventually. That is to say that all their residuals are reduced. In other words we have complete development of all candidates and generated candidates.

This corresponds to using the relation to identify redexes which are then reduced in parallel and in any order. An even stronger condition seems necessary where we require that every candidate heads a strongly normalising term since the choice of reduction sequence might concentrate on that redex and candidates it creates before considering other candidates. In a parallel implementation there may be no way to communicate immediately that a candidate has been erased by a reduction on a remote machine, it must be permitted for erasing of terms to be delayed indefinitely.

Under this sort of arrangement it would be important to choose candidates carefully. There are two approaches:

Firstly, one could say that the semantics of the system require such complete developments, so the programmer must choose programs for which it is acceptable.

Secondly, one could use schemes for chosing candidates which never permit infinite reductions where finite reductions exist.

\subsubsection{Needed Redexes}
I take the definition that a candidate is {\Whnf}--needed if the redex or some descendent is reduced in every reduction to \Whnf. Clearly a \Whnf\ contains no {\Whnf}--needed redexes.

\begin{conjecture}
I conjecture that if a term has a \Whnf\ and a {\Whnf}--needed redex then by reducing that redex first we reach a \Whnf, though not necessarily the minimal one. Similarly we could reduce an arbitrary residual of the redex at any point without creating infinite reductions.
\end{conjecture}

Here are some conjectures about {\Whnf}--neededess and transitivity of needed indexes. This is mainly in the context of the Eager--\Lc. I will generally use needed to mean {\Whnf}--needed.

Firstly, $\lambda$ is a constructor and $@$ the only function symbol in the \Lc. Rewriting replaces $@$ symbols and the only ways for a non--redex $@$ outside a $\lambda$ to become a redex is for its rator to be rewritten to a $\lambda$ (an abstraction). 

\begin{conjecture}
If term $t = \App{(\Labs{x}{e})}{e''}$ contains a needed redex, then t itself is needed.
\end{conjecture}

\begin{conjecture}
If term $\App{t}{e''}$, where $t = \App{e}{e'}$, contains a needed redex, then t contains a needed redex.
\end{conjecture}

\begin{conjecture}
If these are true, then if $e''$ in the above contains a needed redex, then we can keep on reducing on the left spine while it is in the second form and then reduce according to the first form and I conjecture that the needed redex will up on the left spine at some point.
\end{conjecture}

\begin{conjecture}
The system is not confluent since different paths can reach different {\Whnf}s. {\em But} if all residuals of {\Whnf}--needed redexes are contracted, then we do have confluence.
\end{conjecture}

\section{Markings and Conditional Rewriting}
The various reduction relations defined above specify conditional rewriting systems. We take an underlying system, the full \Lc, but constrain it so that only certain redexes are candidates.

Since the reduction relation defined above is contained in the relation for the full \Lc, it is clear that reduction is preserved, but normal forms may not be preserved and normalising strategies might be excluded. This is the case for a call--by--value system, for example.

\begin{conjecture}
I conjecture that by adding marked application operators and perhaps lambda operators it is possible to produce a rewriting system from these inference rules so that arbitrary rewriting simulates the relation defined. A simple process of discarding markings would recover the {\Lx}s.
\end{conjecture}

In the above, I assume that the initial term will be marked according to some algorithm, reduced, and the resulting term unmarked.
In the scheme to come, we use multiple markings with the idea that an initial term could be marked in more than one way.

In such an environment we need to establish a suitable concept of correctness for such markings.

\begin{assignment}{John}
What does it mean for a marking to be correct? It will obviously depend on a number of factors:
\begin{itemize}
\item The algorithm for marking or transforming an initial term
\item The rewriting relation for marked terms
\item The property of the underlying system which is of interest
\end{itemize}
\end{assignment}

My expectation is that rewriting marked terms should be strongly normalising and for correctly marked initial terms, the resulting normal form will satisfy the property of interest.

For the present application it is generally the case that we want the system to reach \Whnf\ correctly for those terms with a \Whnf.

The relations above define one--step reductions. Even though there may be several candidates, it is assumed that just one is chosen. This may erase other candidates, or place them in contexts where they are no longer candidates.

When studying parallel implementation, I am interested in reductions where any redex which has been a candidate is secured (hope I am using the term correctly). This might involve Gross--Knuth steps where every step reduces every candidate.

\begin{assignment}{John}
The concept of correctness above is probably defined for one--step reduction. What conditions must be satisfied by a system if some sort of parallel reduction is to be correct? This requires a definition of the concept of correctness for parallel reduction. There is also a need for a definition of fair reduction where the one--step strategy is non--deterministic.
\end{assignment}

\section{Enhanced \LC}
Here we consider working with a \Lc\ with two sorts of application:

\subsection{Enhanced \LC\ Syntax}

The language is given by:
\begin{eqnarray*}
e & ::= &  x \mid \Labs{x}{e} \mid \AppL{e}{e} \mid \AppE{e}{e} \\
v & ::= &  \Labs{x}{e}  
\end{eqnarray*}
$v$ is the class of {\Whnf}s for closed terms.

There is a simple mapping to the \Lc\ by mapping both application operators to one.

\subsection{Enhanced \LC\ Semantics}
We will define the reduction relation for enhanced \Lc\ terms using a set of inference rules.

\begin{center}
\begin{tabular}{lccl}
$BETA_L: \:\: \AppL{(\Labs{x}{e})}{e'} \:{\rightarrow}\: e\,[e'/x]$
& &
$BETA_E: \:\: \AppE{(\Labs{x}{e})}{e'} \:{\rightarrow}\: e\,[e'/x]$
\end{tabular}

\begin{tabular}{lccl}
$APPL_L: \:\: {\infer{e \:{\rightarrow}\: e''}
       {\AppL{e}{e'} \:{\rightarrow}\: \AppL{e''}{e'}}
       { }}$
& &
$APPL_E: \:\: {\infer{e \:{\rightarrow}\: e''}
       {\AppE{e}{e'} \:{\rightarrow}\: \AppE{e''}{e'}}
       { }}$
\end{tabular}

\begin{tabular}{lcl}
$APPR_E: \:\: {\infer{e' \:{\rightarrow}\: e''}
       {\AppE{e}{e'} \:{\rightarrow}\: \AppE{e}{e''}}
       { }}$
\end{tabular}
\end{center}

A first observation is that terms only containing $@_L$ give a system isomorphic with lazy--\Lc\ while terms only containing $@_E$ give a system isomporphic with eager \Lc.

Clearly we can reduce arbitrary terms in this language and the semantics says what forms can be generated. However, we are interested in ways that this system simulates forms of the \Lc.

\begin{conjecture}
Any sensible definition of correctness should show that this system is correct for reaching \Whnf\ by marking initial terms with only $@_L$.
\end{conjecture}

Also, reduction of the \Lc\ is possible by mapping applications to $@_L$ or $@_E$, reducing to \Whnf\, if possible, then mapping back. Every step in the simulation is equivalent to a full \Lc\ step, though the reduction may not be normalising if $@_E$ is used. Hence it may not be correct for \Whnf any more than full \Lc\ is.

\begin{assignment}{John}
It is not clear that there {\em is} any sensible way to use $@_E$ markings in such a way that correctness for \Whnf\ is preserved. We have observed elsewhere that we cannot compose subterm markings in general.
\end{assignment}

\begin{conjecture}
The big conjecture is that {\em if} the marking preserves the property that, for every subterm  $\AppE{e}{e'}$ which is reachable from the root by a path through the first argument of $@_L$ nodes or either argument of $@_E$ nodes, there is a redex in $e'$ which is needed in the whole term, {\em then} the system is correct for reaching {\Whnf}s, though not necessarily minimal ones. Since we are not clear about our definition of correctness at this stage, it is not possible to make progress on this conjecture.
\end{conjecture}

\begin{conjecture}
$@_E$ reductions (non--spine reductions) seem to offer the source of perpetual reductions for terms {\em with} a \Whnf. I conjecture that doing all these reductions first will lead to a maximal \Whnf\ in some way.
\end{conjecture}

It is not clear how often an analysis could identify these needed arguments. It may be more realistic to identify needed variables: given $\Labs{x}{e}$ we know that whenever the result of applying this function is needed, so is its argument.

Concerning parallel implementation, my later translations {\em may} continue to compute under $\lambda$s but an equivalent sequence could have been chosen which completes reduction before substitution of the resulting term under a $\lambda$.


\section{Translation to Process Networks}
Milner has described translations of the Lazy--\Lc\ into the \Pc\ and has gone on to prove the correctness of the translation.

I have produced a translation with combines use of $@_L$ and $@_E$ within a single framework. This appears in the Term Graph Rewriting book and is repeated below. However, I see from the actual {\em implementation} which I have produced, that the complete translation adds a process which sends a value in the form of a reply channel to the translated expression. Although I do not discuss it here, there is also a process which receives a value on the reply channel and prints it.
\begin{eqnarray*}
\sembrac{ {M} } & = & \restrict{u}{\parprocs{\sembrac{M}_{u}}{\restrict{c}{\outacta{u}{c}}}} \\
\\
\sembrac{ x }_{u} & = & \guardedrep{X}{\inpacta{u}{v}}{\outacta{x}{v}} \\
\sembrac{ k }_{u} & = & \guardedrep{X}{\inpacta{u}{v}}{\outacta{v}{k}} \\
\sembrac{ \Labs{x}{M} }_{u} & =
 & \guardedrep{X}{\inpacta{u}{\pair{x}{q}}}{\sembrac{M}_{q}} \\
\sembrac{ \AppL{M}{N} }_{u} & =
 & \restrict{t}{\restrict{f}{\parprocs
 {\parprocs{\sembrac{M}_{f}}{\outacta{f}{\pair{t}{u}}}}
 {\guardedrep{X}{\inpacta{t}{v}}{\restrict{a}{\parprocs{\outacta{a}{v}}{\sembrac{N}_{a}}}}}}} \\
\sembrac{ \AppE{M}{N} }_{u} & =
 & \restrict{a}{\restrict{f}{\parprocs
 {\parprocs{\sembrac{M}_{f}}{\outacta{f}{\pair{a}{u}}}}
 {\sembrac{N}_{a}}}}
\end{eqnarray*}

Or in original style:
\newcommand{\rec}{{\bf rec}}
\newcommand{\res}[1]{\backslash #1}
\begin{eqnarray*}
\sembrac{ {M} } & = & (\,\sembrac{M}_{u}\,|\,u!c.()\,)\,\res{c}\,\res{u} \\
\\
\sembrac{ x }_{u} & = & \rec\,X.\,u?v\,.\,(\,x!v.()\,|\,X\,) \\
\sembrac{ k }_{u} & = & \rec\,X.\,u?v\,.\,(\,v!k.()\,|\,X\,) \\
\sembrac{ \Labs{x}{M} }_{u} & = &
\rec\,X.\,u?(x,q)\,.\,(\,\sembrac{M}_{q}\,|\,X\,) \\
\sembrac{ \AppL{M}{N} }_{u} & = &
(\,\sembrac{M}_{f}\,\,|\,f!(t,u).()\,|\,{\bf
rec}\,X\,.\,t?v.(\,a!v.()\,|\,
\sembrac{N}_{a}\,|\,X\,)\,\res{a}\,)\,\res{f}\,\res{t} \\
\sembrac{ \AppE{M}{N} }_{u} & = &
(\,\sembrac{M}_{f}\,|\,f!(a,u).()\,|\,
\sembrac{N}_{a}\,)\,\res{f}\,\res{a}
\end{eqnarray*}

\begin{assignment}{Zurab}
The paper by Milner proves the correctness of various translations of the \Lc\ to \Pc. We need to understand what he means by correctness in this context. We need to apply the concept to the marked systems we are investigating.
\end{assignment}

\begin{assignment}{John}
I believe that the correctness concept is related back to one--step strategies, in the sense that Milner is dealing with deterministic systems and shows that the results are consistent with a series of single steps. How can the concept be extended to parallel systems which are not necessarily deterministic? In our case, we want to reach some \Whnf\ but do not insist that the result is minimal.
\end{assignment}

\begin{conjecture}
If attention is restricted to the system where only $@_L$ is used, then the same proof techniques as those used by Milner can be applied, showing that the Lazy--\Lc\ is correctly implemented. This might be done from scratch, {\em or} by demonstrating that the two translations are related in some simple structural fashion.
\end{conjecture}

\begin{conjecture}
There is some useful concept of deterministic evaluation obeyed by the translations of Milner and by my own. This will enable communativity laws to demonstrate that interleaved evaluation corresponds to sequences of steps which each correspond to a single $BETA$ reduction.
\end{conjecture}

\begin{conjecture}
By adding in the $@_E$ translation, I believe that some sort of determinism is retained, though I conjecture that some networks can be generated which can continue to compute even though they correspond to erased terms. I am not sure how a set of residuals is represented. It may be that the neededness condition expresses itself in the fact that at least one potential communication always exists between networks for such terms and the rest of the process network.
\end{conjecture}

\begin{conjecture}
Under the assumption that the marking of the initial term is correct (roughly that $@_E$ only marks needed terms or redexes), I conjecture that the translation for the enhanced calculus is correct. This may well need the definition of correctness in a parallel context, so cannot be considered yet.
\end{conjecture}

I believe this will require proof that it is safe to always compute $@_E$ redexes first, since if reduction of those redexes is delayed, one or more residual could be erased {\em or} placed under a $\lambda$, when it would cease to be a candidate.

The problem is because the translation sets up parallel networks to evaluate function and argument of each $@_E$ redex. The argument continues to be evaluated even if it is erased in the \Lc\ world.

\subsection{Analysis of $\AppL{(\Labs{x}{x})}{N}$}
If we expand $\sembrac{\AppL{(\Labs{x}{x})}{N}}_{u}$ we end up with:
\begin{eqnarray*}
\restrict{t}{\restrict{f}{\parprocs
 {\parprocs
  {\guardedrep{X}{\inpacta{f}{\pair{x}{q}}}
  {\guardedrep{X}{\inpacta{q}{v}}{\outacta{x}{v}}}}
 {\outacta{f}{\pair{t}{u}}}}
 {\guardedrep{X}{\inpacta{t}{v}}{\restrict{a}{\parprocs{\outacta{a}{v}}{\sembrac{N}_{a}}}}}}}
\end{eqnarray*}
Unravelling the leftmost replication and communicating on channel $f$ gives:
\begin{eqnarray*}
\restrict{t}{\restrict{f}{\parprocs
 {\parprocs{\guardedrep{X}{\inpacta{f}{\pair{x}{q}}}{\guardedrep{X}{\inpacta{q}{v}}{\outacta{x}{v}}}}
 {\guardedrep{X}{\inpacta{u}{v}}{\outacta{t}{v}}}}
 {\guardedrep{X}{\inpacta{t}{v}}{\restrict{a}{\parprocs{\outacta{a}{v}}{\sembrac{N}_{a}}}}}}}
\end{eqnarray*}
It may not be a structural rule, but it must be a theorem that $\restrict{f}{\inpact{f}{v}{P}}$ is behaviourally equivalent to the empty process. Similarly,
$\restrict{f}{\guardedrep{X}{\inpacta{f}{v}}{P}}$. Hence the above is equivalent to:
\begin{eqnarray*}
\restrict{t}{\parprocs
 {\guardedrep{X}{\inpacta{u}{v}}{\outacta{t}{v}}}
 {\guardedrep{X}{\inpacta{t}{v}}{\restrict{a}{\parprocs{\outacta{a}{v}}{\sembrac{N}_{a}}}}}}
\end{eqnarray*}
This has ignored the additional context in which translations are placed. We see that the expression has {\em not} reduced to the translation $\sembrac{N}_{u}$ as might be hoped. However, when we do introduce the context, all comes right:

The only interaction betwen this and some other system must be to take input on channel $u$ so we will consider the full system $\sembrac{\AppL{(\Labs{x}{x})}{N}}$ or $\restrict{u}{\parprocs{\restrict{c}{\outacta{u}{c}}}{\sembrac{\AppL{(\Labs{x}{x})}{N}}_{u}}}$ or:
\begin{eqnarray*}
\restrict{u}{\parprocs{\restrict{c}{\outacta{u}{c}}}{\restrict{t}{\parprocs
 {\guardedrep{X}{\inpacta{u}{v}}{\outacta{t}{v}}}
 {\guardedrep{X}{\inpacta{t}{v}}{\restrict{a}{\parprocs{\outacta{a}{v}}{\sembrac{N}_{a}}}}}}}}
\end{eqnarray*}
Unravelling the first replication, communicating on $u$ and observing that $u$ will not occur free in $\sembrac{N}_{a}$:
\begin{eqnarray*}
\restrict{t}{\parprocs
 {\restrict{c}{\outacta{t}{c}}}
 {\guardedrep{X}{\inpacta{t}{v}}{\restrict{a}{\parprocs {\outacta{a}{v}}{\sembrac{N}_{a}}}}}}
\end{eqnarray*}
Unravelling the remaining replication, and communicating on $t$, which is then restricted to the replication:
\begin{eqnarray*}
\restrict{a}{\parprocs{\restrict{c}{\outacta{a}{c}}}{\sembrac{N}_{a}}}
\end{eqnarray*}
We compare this with the original:
\begin{eqnarray*}
\restrict{u}{\parprocs{\restrict{c}{\outacta{u}{c}}}{\sembrac{\AppL{(\Labs{x}{x})}{N}}_{u}}}
\end{eqnarray*}
and see that the effect of the application has been simulated in this simple context.

\end{document}
%%% End of LaTeX Document %%%
