%%% 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 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 the use of \Lc\ 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.

Where I say conjecture it is something that I would like you to try to verify or refute!

\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}.

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.

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.

\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}

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.

\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.

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.

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). 

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

Conjecture: If term $\App{t}{e''}$, where $t = \App{e}{e'}$, contains a needed redex, then t contains a needed redex.

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.

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.

\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 not containing $@_E$ give a system isomorphic with Lazy--\Lc\ while terms  not containing $@_L$ 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.

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.

The big conjecture is that {\em if} the marking preserves the property that, for every subterm $\AppE{e}{e'}$ 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.

$@_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.

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.

Please review those proofs. I conjecture that the form of equivalence suggested is using an approach to simulation which cannot be placed in the same form as the simulations we have been considering. 

I have produced a translation with combines use of $@_L$ and $@_E$ within a single framework. This appears in the Term Graph Rewriting book. I conjecture that 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.

I conjecture that 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.

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.

Under the assumption that $@_E$ only marks needed terms or redexes, I conjecture that the translation for the enhanced calculus is correct.

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.

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