\documentstyle[twocolumn]{article}

\input{diagrams} % Paul Taylor's Macro Package

\setlength{\textheight}{8.75in}
\setlength{\columnsep}{2.0pc}
\setlength{\textwidth}{6.8in}
\setlength{\topmargin}{0.25in}
\setlength{\headheight}{0.0in}
\setlength{\headsep}{0.0in}
\setlength{\oddsidemargin}{-.19in}
\setlength{\parindent}{1pc}


\title{An Abstract Concept of Optimal Implementation \\
\small {\bf (Extended Abstract)} }


\author{Zurab Khasidashvili   \\
NTT Basic Research Laboratories\\
Atsugi, Kanagawa 243-01 Japan \\
{\tt zurab@theory.brl.ntt.co.jp}
\and
John Glauert \\
School of Information Systems, UEA \\
Norwich NR4 7TJ England \\
{\tt jrwg@sys.uea.ac.uk}
}

\date{}
\begin{document}
\newcommand{\doar}{\mbox {$\,\ \rightarrow\kern-0.7em\rightarrow\ $}}


%\newcommand{\john}[1]{} % Comment out text.
%\newcommand{\zurab}[1]{} % Comment out text.
\newcommand{\john}[1]{\{{\bf John: \sf #1}\}} % Highlight text.
\newcommand{\zurab}[1]{\{{\bf Zurab: \sf #1}\}} % Highlight text.
\newcommand{\delete}[1]{} % Comment out text.
\newcommand{\suppress}[1]{} % Comment out text.
%\newcommand{\suppress}[1]{\{\{{\sf #1}\}\}} % Highlight text.
\newcommand{\incl}[1]{#1} % include text.
%\newcommand{\incl}[1]{} % exclude text.
\newcommand{\excl}[1]{} % exclude text.
%\newcommand{\excl}[1]{\{#1\}} % include text.


\newtheorem{thm}{Theorem}[section]
\newtheorem{lem}[thm]{Lemma}% [section]
\newtheorem{cor}[thm]{Corollary}% [section]
\newtheorem{ex}[thm]{Example}% [section]
\newtheorem{rem}[thm]{Remark}% [section]
\newtheorem{nota}[thm]{Notation}% [section]
\newtheorem{prop}[thm]{Proposition}% [section]
\newtheorem{deff}[thm]{Definition}% [section]
\newtheorem{conv}[thm]{Convention}% [section]

\newenvironment{akn}{\noindent{\bf Acknowledgments }}{}
\newenvironment{pruuf}{\noindent{\bf Proof }}{}
\newenvironment{prsk}{\noindent{\bf Proof sketch }}{}
\newenvironment{altpr}{\noindent{\bf Alternative proof }}{}

\newcommand{\notation}{{\bf Notation }}
%\newcommand{\note}{{\bf Note }}
\newcommand{\newl}{\mbox{ }\\}


\newcommand{\ar}{\rightarrow}
\newcommand{\undl}{\underline}
\newcommand{\impl}{\Rightarrow}
%\newcommand{\doar}{\twoheadrightarrow}
\newcommand{\trar}{\Rightarrow}
\newcommand{\red}[1]{\mbox{$\stackrel{#1}{\ar}$}}
\newcommand{\dored}[1]{\mbox{$\stackrel{#1}{\doar}$}}
\newcommand{\inputpic}[1] {\begin{center} \input{#1} \end{center}}
\newcommand{\ssq}{\subseteq}
\newcommand{\sset}{\subset}
\hyphenation{meta-var-ia-ble}
\newcommand{\imply}{\,\Rightarrow\,}

\newcommand{\vect}[1]{\mbox{$\overline{#1}$}}
\newcommand{\rpsim}{\mbox{$\stackrel{r}{\psim}$}}
\newcommand{\rpessim}{\mbox{$\stackrel{r}{\pessim}$}}
\newcommand{\ressim}{\mbox{$\stackrel{r}{\essim}$}}
\newcommand{\rsim}{\mbox{$\stackrel{r}{\sim}$}}
\newcommand{\muer}[1]{\mbox{$[{#1}]_{\mu}$}}
\newcommand{\lclas}[1]{\mbox{$\langle{#1}\rangle_L$}}
\newcommand{\sclas}[1]{\mbox{$\langle{#1}\rangle_S$}}
\newcommand{\ines}[2]{\mbox{$\overbrace{#1}^{#2}$}}
\newcommand{\unin}[2]{\mbox{$\undl{#1}_{#2}$}}
\newcommand{\dist}[2]{\mbox{$\vert{#1},{#2}\vert$}}
\newarrow{Co}<--->
\newcommand{\pessim}{\prec\!\!\prec}
\newcommand{\steq}{\approx_{st}}
\newcommand{\essim}{\approx}
\newcommand{\psim}{\prec}
\newcommand{\orth}{\perp}
\newcommand{\esorth}{\perp_{es}}
%\newcommand{\subt}{\subseteq}
\newcommand{\subt}[0]{\in}
\newcommand{\subts}[0]{\subseteq}


\newcommand{\contr}{\hookrightarrow}
\newcommand{\zcontr}{\hookrightarrow_z}
\newcommand{\scontr}{\hookrightarrow_s}
\newcommand{\contre}{\underline{\hookrightarrow}}
\newcommand{\zcontre}{\underline{\hookrightarrow}_z}
\newcommand{\fin}{\in}
\newcommand{\lleq}{\unlhd_L}
\newcommand{\lles}{\lhd_L}
\newcommand{\zleq}{\unlhd_z}
\newcommand{\zles}{\lhd_z}
\newcommand{\zgeq}{\unrhd_z}
\newcommand{\zgre}{\rhd_z}
\newcommand{\leeqv}{\approx_L}
\newcommand{\snpp}{\approx_{sn}}
\newcommand{\inter}{\ddagger}
\newcommand{\ind}{\perp}
\newcommand{\hole}{\circ}
\newcommand{\restr}{\vert}
\newcommand{\exten}{\updownarrow}


\newcommand{\fami}{\simeq}
\newcommand{\zfami}{\simeq_z}
\newcommand{\sfami}{\simeq_s}

\newcommand{\stan}{STA}
\newcommand{\stav}[1]{STV(#1)}

\newcommand{\Tr}[1]{Theorem~\ref{#1}}
\renewcommand{\Pr}[1]{Proposition~\ref{#1}}
\newcommand{\Cr}[1]{Corollary~\ref{#1}}
\newcommand{\Lr}[1]{Lemma~\ref{#1}}
\newcommand{\Dr}[1]{Definition~\ref{#1}}
\newcommand{\lc}{$\lambda$-calculus}
\newcommand{\ovl}{\overline}
\newcommand{\unl}{\underline}
\newcommand{\bd}{\begin{deff}\em}
\newcommand{\bdl}[1]{\begin{deff}\em\label{#1}}
\newcommand{\bl}{\begin{lem}\em}
\newcommand{\bll}[1]{\begin{lem}\em\label{#1}}
\newcommand{\bp}{\begin{prop}\em}
\newcommand{\bpl}[1]{\begin{prop}\em\label{#1}}
\newcommand{\bt}{\begin{thm}\em}
\newcommand{\btl}[1]{\begin{thm}\em\label{#1}}
\newcommand{\bel}[1]{\begin{ex}\em\label{#1}}
\newcommand{\bc}{\begin{cor}\em}
\newcommand{\bcl}[1]{\begin{cor}\em\label{#1}}
\newcommand{\bproof}{\begin{pruuf}}
\newcommand{\eproof}{\end{pruuf}}
\newcommand{\ed}{\end{deff}}
\newcommand{\el}{\end{lem}}
\newcommand{\ep}{\end{prop}}
\newcommand{\et}{\end{thm}}
\newcommand{\ee}{\end{ex}}
\newcommand{\ec}{\end{cor}}
\newcommand{\suf}{($\Rightarrow$)}
\newcommand{\nec}{($\Leftarrow$)}
\newcommand{\setm}{\setminus}
\newcommand{\crea}{\vdash}
\newcommand{\emp}{\emptyset}
\newcommand{\cfr}{family-reduction}
\newcommand{\cfrs}{family-reductions}
\newcommand{\qp}{quasi-persistently}
\newcommand{\stc}{strongly cofinal}
\newcommand{\rn}{RN}
\newcommand{\trnt}{the Relative Normalization theorem}
%\newcommand{\qp}{quasi-persistently}
%\newcommand{\stc}{strongly cofinal}
\newcommand{\pmn}{persistently $\stab$-needed}
\newcommand{\qprn}{quasi-persistently $\reg$-needed}
\newcommand{\qpmn}{quasi-persistently $\stab$-needed}
\newcommand{\das}{\downarrow_{\stab}}
\newcommand{\dar}{\downarrow_{\reg}}
\newcommand{\stab}{{\cal S}}
\newcommand{\reg}{{\cal R}}

\newcommand{\extrr}[1]{\mbox{$\stackrel{#1}{\rightharpoonup}$}}
\newcommand{\lextrr}[1]{\mbox{$\stackrel{#1}{\leftharpoonup}$}}
\newcommand{\extr}{\mbox{$\rightharpoonup$}}
\newcommand{\lextr}{\mbox{$\rightharpoonup$}}
\newcommand{\staeq}{\approx_S}
\newcommand{\leng}[1]{\mbox{$\vert{#1}\vert$}}
%\newcommand{\doextr}{\mbox{$\rightharpoonup^*$}}
\newcommand{\doextr}{\mbox{$\,\ \rightharpoonup\kern-0.7em\rightharpoonup\ $}}
\newcommand{\err}[2]{\mbox{$ST_{{#1}}({#2})$}}
\newcommand{\Le}{L\'evy}


\newcommand{\pc}{permutation-equivalence}
\newcommand{\pt}{permutation-equivalent}
\newcommand{\Lc}{\Le-equivalence}
\newcommand{\Lt}{\Le-equivalent}

\newcommand{\lin}[1]{\mbox{${#1}_I $}}
\newcommand{\calF}{{\cal F}}
\newcommand{\calR}{{\cal R}}


\maketitle



\section{Introduction}


In order to achieve optimal evaluation of $\lambda$-terms, L\'evy
introduced a notion of \emph{redex-family} to capture the concept of
redexes of the `same origin'. The hope was that it would be possible to mimic
multi-step reductions which contract whole families in a term by reduction
of some graph representation, in which every multi-step would be
represented by contraction of a single graph redex~\cite{[levy],[le80]}.
Such an implementation has indeed been achieved by Lamping~\cite{[Lam]} and
Kathail~\cite{[Kath]}, reviving interest in optimal graph reduction.
Maranget~\cite{[Mar91]} generalized \Le's optimality theory to Orthogonal
Term Rewriting Systems (OTRSs), Gonthier et al~\cite{[GAL]} simplified
Lamping's technique, and Asperti and Laneve generalized both L\'evy's
optimality theory and Gonthier's implementation to Interaction
Systems, which cover most of the languages  with a constructor-destructor
discipline~\cite{[AL],[AL2]}. More recently, van Oostrom generalized the
optimality theory to the whole class of orthogonal Higher-Order Rewriting
Systems (HORSs)~\cite{[Oos]}, and Guerrini developed a general theory of
sharing-graph rewriting~\cite{[Gue.th]}.

\Le\ introduced the family concept in three different ways: via an
appropriate
notion of \emph{labelling}, via \emph{extraction}, and by \emph{zig-zag}.
He showed that they all yield the same
concept, in the \lc. The same holds for all orthogonal HORSs $R$ if all
three family concepts are defined in the refinement of $R$ which decomposes
every original $R$-step into first-order or TRS-step and a number of
substitution
steps~\cite{[Oos]}. However, the zig-zag family can be defined directly in
$R$, and this yields a different, weaker, family concept~\cite{[AL]}.
Independently and much earlier, Kennaway and Sleep~\cite{[K.S.]} defined
a concept of labelling for orthogonal Combinatory Reduction Systems (CRSs),
improving Klop's original labelling system for CRSs~\cite{[Kl.CRS]},
which covers orthogonal TRSs and Interaction Systems. Their labelling is
different from both Maranget's labelling for OTRSs~\cite{[Mar91]} and
Asperti-Laneve's labelling for Interaction Systems~\cite{[AL]}.


This variety of family concepts, and development of alternative graph
rewriting algorithms for optimal implementation of orthogonal rewriting
systems (e.g.,~\cite{[SPE],[Mar91]}) created the need to
develop an abstract notion of family general enough to cover all the
existing notions, and refined enough to enable proof of normalization and
optimality results. Such structures were introduced by the
authors in~\cite{[rndrs]} as \emph{Deterministic Family
Structures} (DFSs) building on recent developments of
abstract reduction systems with an axiomatized residual relation,
such as the \emph{Concurrent Transition Systems} (CTSs) of
Stark~\cite{[Sta]} and the \emph{Abstract Reduction Systems} (ARSs) of
Melli\`es et al~\cite{[GLM],[Mel]}.


Our DFSs are defined as \emph{Deterministic Residual Structures} (DRSs)
with an axiomatized family relation. DRSs, in turn, are Abstract Reduction
Systems with an axiomatized residual relation, similar to CTSs
and ARSs, but with the difference that, unlike CTSs, the
residual relation can be duplicating in DRSs and, unlike ARSs, there is no
nesting relation on redexes defined or axiomatized in DRSs. Despite its highly
abstract nature, a counterpart of the \emph{stability}
property of Berry~\cite{[berry]} enabled us to prove the normalization
theorem for all DRSs, and  not only w.r.t. normal forms, but in general for
\emph{regular stable sets} of `results'; all interesting sets
of final terms, such as head-normal forms, weak head normal forms, etc,
fall in the category of regular stable term-sets~\cite{[ctrs],[rndrs]}.
Further,  in DFSs one can prove the optimality theorem~\cite{[rndrs]}.


In this paper, we continue the abstract study of optimality
theory started in~\cite{[rndrs]}. We introduce an abstract
concept of
\emph{L\'evy-implementation}: With a DFS $\cal F$ we associate a
\emph{non-duplicating} DRS $\calR_I$, called the implementation of $\cal
F$, whose steps exactly correspond to complete family-reduction steps in
$\cal F$. It is not difficult to show that needed reductions in
$\calR_I$ (w.r.t. any stable set of results) correspond exactly to needed
complete family-reductions in $\calF$, implying that the former indeed
`implement' optimal computations in $\calF$ in the sense of
L\'evy~\cite{[levy],[le80]}.




Further, we show that the family relation on $\calR_I$ induced by that of
$\calF$ coincides with zig-zag, which is the weakest family sharing. At
first sight, one might think that there is no need or possibility of
a stronger sharing in non-duplicating SDRSs. However, this is not the case
as the example of Asperti and Laneve~\cite{[AL]} demonstrating `inadequacy'
of
L\'evy's extraction algorithm for Interaction Systems is, when considered
as an Abstract Reduction System, a non-duplicating SDRS.  This example
shows that zig-zag does not coincide with the labelling and
their extraction families based on the \emph{shift} operation.
These effects are caused by the fact that more than one members of a family
can be created by a single
step -- the reduction step $t=\mu(\lambda x.(xx))\ar (\mu(\lambda x.(xx))
\,\mu(\lambda x.(xx)))=s$, according to the $\mu$-rule $\mu(\lambda x.
X)\ar [\mu(\lambda x. X)/x]X$, simultaneously creates the two $\mu$-redexes
in $s$; these redexes are
intuitively in the same family, but cannot be related by zig-zag, nor
by an extraction procedure similar to L\'evy's. We call such families
\emph{non-separable.}


Actually, we show that the sharing concept formalized in DFSs is
\emph{compositional}: any sharing can be decomposed into a weaker sharing
(such as zig-zag, when the latter forms a family-relation) and a
non-separable sharing in the non-duplicating DRS implementing that weaker
sharing. To this end, we investigate the family relation in non-duplicating
DFSs. We show that zig-zag forms a family-relation in every non-duplicating
SDRS, and that it is the only separable family relation in such SDRSs.
These results are obtained by defining an abstract extraction procedure and
showing that zig-zag coincides with our extraction-family relation.

Because of space limitation, all proofs are omitted; they can be found
in~\cite{[acoi-rep],[atoe-tcs]}.


\section{Deterministic Residual and Family Structures}
\label{S.drfs.}


In this section we recall very briefly DRSs and DFSs. We refer
to~\cite{[atoe-tcs]} for a detailed exposition and many examples. Here we
can only give formal definitions.



A DRS is an \emph{Abstract reduction System} (ARS) with an axiomatized
residual relation. An ARS~\cite{[Hin]} is a triple $A$ =
(\emph{Ter},\emph{Red},$\ar$)
where \emph{Ter} is a set of \emph{terms}, ranged over by
$t,s,o,e$; \emph{Red} is a set of \emph{redexes} (or \emph{redex occurrences}),
ranged over by $u,v,w$; and $\ar:Red\mapsto (Ter\times Ter)$ is a (total)
function such that for any $t\in Ter$
there is only a finite set of \emph{redexes} $u\in Red$ such that
$\ar(u)=(t,s)$, written $t\red{u}s$. Below, $u\subt t$ denotes that
$u$ is a member of the redexes of $t$ and $U\subts
t$ denotes that $U$ is a subset of the redexes. A \emph{reduction} is a sequence
$t\red{u_1}t_2\red{u_2}\ldots$. Reductions are denoted by $P,Q,N$. We write
$P:t\doar s$ or $t\dored{P}s$ if $P$ denotes a reduction (sequence) from
$t$ to $s$. $\,\,\vert P\vert$ denotes the length of $P$.
$P+Q$ denotes the concatenation of $P$ and $Q$.
We use $U,V,W$ to denote sets of redexes of a term.



The DRS concept is based on~\cite{[le80],[H.L.]}. DRSs model orthogonal
term as well as graph rewrite systems, both first and
higher order, and including the \lc\ and its sharing evaluation models,
with the standard Church notion of residual.


\bdl{D.levy.str.}
A DRS is a pair ${\cal R}=(A, /)$, where $A$ is an ARS and
$/$ is a \emph{residual} relation on redexes relating redexes in the source
and target term of every reduction $t\red{u}s\in A$, such that
for $v\subt t$, the set $v/u$ of \emph{residuals of $v$ under $u$} is a
set of redexes of $s$; a redex in $s$ may be a residual of only one redex
in $t$ under $u$, and $u/u=\emptyset$. If $v$ has more than one
$u$-residual, then $u$ \emph{duplicates} $v$.
If $v/u=\emptyset$, then $u$ \emph{erases} $v$.
A redex of $s$
which is not a residual of any $v\subt t$ under $u$ is said to be
\emph{$u$-new} or \emph{created} by $u$.
The set $u/P$ of residuals of $u$ under any reduction $P$ is defined by
transitivity.

A \emph{development} of $U\subts t$ is a reduction $P:t\doar $ that only
contracts residuals of redexes from $U$; it is \emph{complete} if
$U/P=\cup_{u\in U}\,u/P=\emptyset$. Development of $\emptyset$ is
identified with the empty reduction. $U$ will also denote a complete
development of $U\subts t$. The residual relation satisfies the following
two axioms:

$\bullet$ [FD] (\cite{[GLM]}) All developments are terminating; all complete
developments of $U\subts t$ end at the same term; and residuals
of a redex $v\subt t$ under all complete developments of $U$ are the same.

$\bullet$  [weak acyclicity] (\cite{[Sta]}) Let $u,v\subt t$, let $u\not=
v$, and let $u/v=\emp$. Then $v/u\not=\emp$.

We call a DRS $\cal R$ \emph{stable} (SDRS) if:

$\bullet$ [stability] If $u,v\subt t$ are different redexes, $t\red{u}e$,
$t\red{v}s$, and $u$ creates a redex $w\subt e$, then the redexes in
$w/(v/u)$ are not $u/v$-residuals of redexes of $s$, i.e.,  they are
created along $u/v$ .
\ed


Similarly to~\cite{[H.L.],[levy],[le80],[Sta]}, in a DRS $\cal R$
the residual relation on redexes is extended
to all co-initial reductions as follows: $(P_1+P_2)/Q=P_1/Q+P_2/(Q/P_1)$
and $P/(Q_1+Q_2)=(P/Q_1)/Q_2$, and \emph{L\'evy-equivalence} or
\emph{permutation-equivalence} is defined as the smallest relation on co-initial
reductions satisfying: $U+ V/U\leeqv V+U/V$ and $Q\leeqv Q'\,
\Longrightarrow \, P+Q+N\leeqv P+Q'+N$, where $U$ and $V$ are complete
developments of redex sets in the same term. Further,
one defines $P\lleq Q$ iff $P/Q=\emptyset$, and
can show that $P\leeqv Q$ iff
$P\lleq Q$ and $Q\lleq P$; and $P\lleq Q$ iff $Q\leeqv P+N$ for some $N$.
Intuitively, $P\leeqv Q$ means that $P$ can be obtained from $Q$ by
a number of permutations of adjacent steps.



DFSs are DRSs where in addition a notion of \emph{redex-family} is
axiomatized so that the essence of sharing in the sense of
L\'evy~\cite{[levy],[le80]} is
captured, and all the known family notions satisfy these axioms.



\bdl{D.DRS.}
A DFS is a triple ${\cal F} =({\cal
R},\fami,\contr)$, where
$\cal R$ is a DRS;  $\fami$ is an equivalence  relation on redexes with
\emph{histories}; and $\contr$ is the \emph{contribution} relation on
co-initial families, defined as follows:

(1)  For any co-initial reductions $P$ and $Q$, a redex $Qv$ in the final
term of $Q$ (read as $v$ \emph{with history} $Q$) is called a \emph{copy} of
a redex $Pu$, written $Pu\zleq Qv$, if  $P+Q/P\leeqv Q$ and $v$ is a
$Q/P$-residual of $u$; the \emph{zig-zag} relation $\zfami$ is the symmetric
and transitive closure of the copy relation~\cite{[le80]}. The \emph{family}
relation $\fami$ is an equivalence relation among redexes with histories
containing $\zfami$. A \emph{family} is an equivalence class of the family
relation; families are ranged over by $\phi,\psi,\ldots$. $Fam(\,\,)$
denotes the family of its argument.


(2) The relations $\fami$ and $\contr$ satisfy the following axioms:

$\bullet$ [initial] Let $u,v\subt t$ and $u\not= v$, in $\cal R$.
Then $Fam(\emptyset_t u) \not=Fam(\emptyset_t v)$, where $\emp_t$ is the
empty reduction starting from $t$.

$\bullet$ [contribution] $\phi\contr \phi'$ iff for any $Pu\fin \phi'$, $P$
contracts at least one redex in $\phi$.

$\bullet$ [creation] If $e\dored{P}t\red{u}s$ and $u$ creates
$v\subt s$, then  $Fam(Pu)\contr Fam((P+u)v)$.

$\bullet$ [FFD] (\emph{Finite Family Developments}) Any reduction that
contracts redexes of a finite number of families is terminating.
\ed

Note that the [contribution] can be viewed as a definition of $\contr$
rather than as an axiom. Hence sometimes we will consider a DFS as a pair
${\cal F} =({\cal R},\fami)$.


We call an SDRS with a non-duplicating, resp. non-duplicating and
non-erasing, residual relation \emph{affine} (ASDRS), resp. \emph{linear}.



\bdl{D.sep.fam.}
(1) We call an affine DFS a \emph{zig-zag} DFS, AZDFS, if its family
relation is the zig-zag~$\zfami$.

(2) We call an affine DFS \emph{separable}, if, for any redex $Pv$, $v$
cannot create two different redexes in the same family, that is, if $v$
creates $w',w''$ and $w'\not= w''$, then $Fam((P+v)w')\not= Fam((P+v)w'')$.
\ed


Even linear DFSs need not be zig-zag or separable DFSs: in the
linear SDRS given by the reduction graph
\begin{diagram}[height=1.5em,width=1.5em]
\label{D.perm.cl.}
       &        &       &             &\bullet &               &        \\
       &        &       & \ruTo^{v_1} &    &  \rdTo^{v'_2} &         \\
\bullet & \rTo^u &\bullet &             &    &               &\bullet \\
       &        &       & \rdTo_{v_2} &    & \ruTo_{v'_1}  &         \\
       &        &       &             &\bullet &               &        \\
\end{diagram}
where $u$ creates $v_1$ and $v_2$, $v'_1=v_1/v_2$ and $v'_2=v_2/v_1$, we
can set all $v$s to belong to the same family $\phi$, and $u$ to form its
own family $\psi$, and define $\psi\contr\phi$. Then we get a DFS which is
not an AZDFS as for example $uv_1\not\zfami uv_2$. That DFS is not separable
either, as $u$ creates two different members of the family $\phi$. We could
also define
$\{v_1,v'_1\}$ and $\{v_2,v'_2\}$ to form separate families $\phi_1$ and
$\phi_2$, and define $\psi\contr \phi_1,\phi_2$, and this would yield
an AZDFS.






\section{Zig-zag vs Extraction}
\label{S.zi.ext.}


In this section, we introduce an abstract \emph{extraction} algorithm for ASDRSs
and show that zig-zag related redexes (with histories) have the same
canonical representatives w.r.t. extraction, up to an equivalence on
histories. L\'evy introduced an extraction procedure for the \lc\
in~\cite{[levy],[le80]} in order to prove decidability of the family
relation. His extraction procedure is effective, and gives canonical
representations of families, which are unique, thus implying the
decidability of the family relation. For higher order rewrite systems whose
reduction steps are more complicated, there are two conceptually different
extensions of L\'evy's extraction algorithm. The first is due to
Asperti and Laneve~\cite{[AL]}, and the second to van
Oostrom~\cite{[Oos]}.

The `problem' arises because a redex can create a number of
redexes `intuitively' in the same family without the help of
previous steps, something which cannot happen in the \lc\
or term rewriting.  That these redexes are intuitively in the same
family, can be seen after decomposing the rewrite step into two parts --
the \emph{TRS part} that only creates new symbols, and the
\emph{substitution part}, that performs all (often nested) substitutions.
The substitution part can duplicate or erase the redexes created during the
TRS part, and all substitution copies of a redex created by the TRS-part
are viewed to belong
to the same family, as labels of such redexes are the same. Such redexes
cannot be related by the zig-zag if one works with the original
system~\cite{[AL]}, but can be related if one works in the refinement of
the original system~\cite{[Oos]}. Now, the difference between the two
approaches is that Asperti and Laneve decided to accept the inadequacy
of the zig-zag, but extended L\'evy's extraction algorithm by the
\emph{shift} operation which relates all copies of the simultaneously
created redexes of the same family to a canonical representative, thus
making extraction match the labelling; the resulting family-relation is
non-separable. On the contrary, van Oostrom
works with the refined rewrite systems and no operation like shift is necessary
to ensure coincidence of labelling, extraction and zig-zag families.
Since we want to define an extraction procedure adequate for zig-zag,
we do not need an operation modelling \emph{shift}.


Another relevant extraction procedure is studied by Kennaway et
al.~\cite{[KKSdV]} for orthogonal Term Graph Rewriting Systems (TGRSs).
That paper is concerned with Event Structure~\cite{[Win89]} semantics for
orthogonal TGRSs and does not mention families explicitly: pre-events there
correspond to redexes with histories and events correspond to zig-zag
families.  The extraction algorithm in~\cite{[KKSdV]}, called there the
\emph{minimization} algorithm, is based on a syntactic concept of the
contribution relation on redexes and is technically different from our
extraction algorithm. Note that TGRSs are non-duplicating rewrite systems,
hence our extraction algorithm, as well as other results in this paper
concerning ASDRSs, apply to orthogonal TGRSs.


\bdl{D.can.re.his.}
(1) We call $P:t_0\red{u_0}t_1\red{u_1}\ldots$ \emph{standard} if every
$u_i$ is \emph{$P$-needed}, i.e., any $Q:t_i\doar$ permutation-equivalent
to the tail $P_i:t_i\doar$ of $P$ contracts at least one residual of $u_i$.
We write $P\staeq Q$ if $P\leeqv Q$ and both $P$ and $Q$ are standard.
For any standard $P$, we define $\sclas{P}=\{Q\,\vert\,Q\staeq P\}$.

(2) Let $P:t\doar s$ and $v\subt s$. We call $Pv$ \emph{canonical} if $P$
is standard and, for any $Q\leeqv P$, the last step in $Q$ creates $v$.
\ed


Note that if $P\staeq P'$, then $Pv$ is canonical iff so is $P'v$. So
canonical forms we speak of are actually objects $\sclas{P}v$, for standard
finite reductions $P$. Our extraction algorithm transforms any redex with
history into a canonical one, and the main result of this section is that
redexes are zig-zag related iff they have the same canonical form.


The `syntactic' extraction procedures in~\cite{[le80],[AL],[Oos]} (without
the \emph{shift} operation) can quickly be summarized as follows: First,
given a $Pu$, one must standardize $P+u$ according to a left-to-right
outside-in standardization procedure, and if $P'+u'+P''$ is the standard
variant of $P+u$, where $u$ is a $P''$-residual of $u'$, one starts the
extraction procedure from $P'u'$. Now, if the last step, say $w$, of
$P'$ does not create $u'$, then the contraction of $w$ can be `omitted' in
$P'$. Otherwise there is a non-empty
tail $P'_2$ of $P'$, say $P'=P'_1+v+P'_2$, that takes place either in a
part disjoint from $v$ or inside an argument of $v$, and in
both cases $v$ does not contribute to the creation of $u'$, therefore is
`omitted' by the extraction step. Since redexes in DRSs do not have any
structure, these `syntactic' extraction algorithms cannot be applied to
ASDRSs. The same is true for the extraction algorithm in~\cite{[KKSdV]}.
Instead, our extraction algorithm (when applied to $Pu$) checks every
standard variant of $P$ in order to find
one whose last step does not create $u$ and therefore can be omitted. The
following lemma says that we can indeed restrict our search to standard
reductions only:



\bll{L.sta.ex.dec.}
Let $Q:t\dored{P}s\red{u}e$, where $u$ does not create $v\subt e$. Then
there is a standard $Q'\leeqv Q$ such that $Q':t\dored{P'}s'\red{u'}e$,
where $P'u'\zleq Pu$ and $u'$ does not create $v$. Furthermore, any
standard variant of $Q$, and in particular $Q'$ above, can be constructed
effectively.
\el



Let $\sclas{P}v$ not be canonical. By \Dr{D.can.re.his.}, there is
$Q:t\dored{P'}e\red{u}s$ such that $Q\leeqv P$ and $v$ is a $u$-residual of
some $v'\subt e$. By \Lr{L.sta.ex.dec.}, $Q$ can be chosen standard. In
$Q$, $u$ does not `contribute' to $v$, and in the search for a shortest
reduction that creates a redex in the zig-zag class of $Qv$, contraction of
$u$ can be omitted -- $P'v'\zfami Pv$ and $\leng{P'}<\leng{P}$ since all
standard L\'evy-equivalent reductions have the same (minimal)
length~\cite{[dndrs]}.  The transformation of $Pv$ into $P'v$ is
denoted by $Pv\extr P'v'$, and is called an \emph{extraction} step.

For example, consider the ASDRS corresponding to the TRS $R=\{f(x)\ar
g(x),\, a\ar b,\,b\ar c\}$, let $P:f(a)\ar g(a)\ar g(b)$, and let $v=b$ in
$g(b)$. Then $Pv$ is not canonical, as $P\staeq Q:f(a)\ar f(b)\ar g(b)$ and
the last step of $Q$ does not create $v$ -- the latter is the residual of
$v'=b$ in the final term of $P': f(a)\ar f(b)$. Hence we can perform an
extraction step $Pv\extr P'v'$. The latter redex is in extraction normal
form.

\btl{P.on.ca.for.}
{\bf (Extraction vs Zig-zag)}
Every redex $Pv$ in an ASDRS has exactly one extraction normal form
$\sclas{P^*}v^*$ which is canonical. Furthermore, $Pv\zfami Qw$ iff their
canonical forms coincide.
\et


This theorem, together with computability of extraction
normal forms, implies decidability of the zig-zag relation in ASDRSs.




\section{Affine Families}
\label{S.li.zi.fa.}




Using \Tr{P.on.ca.for.}, it is possible to show that zig-zag satisfies all
family axioms. That is:


\btl{T.lin.dr.sta.df.}
Let $\cal R$ be an ASDRS. Then ${\cal
F_R}=(R,\zfami)$ is an affine zig-zag DFS.
\et



In order to relate zig-zag with separability, we first study affine
separable families. In particular, we show that in separable DFSs, and only
in such DFSs, there is no real sharing (in the affine case) -- all
reductions are in fact \emph{complete family-reductions}. Recall that a
complete family-reduction is a multi-step reduction contracting, in each
multi-step, all members of a single family in parallel. This enables to us
to show the equivalence of zig-zag and separability in ASDRSs:


\btl{T.sep.eq.ig.}
An affine DFS $\cal F$ is separable iff it is a zig-zag DFS.
\et

An important example where a non-separable sharing is
reasonable is the \emph{lazy call-by-value} \lc,
$\lambda_{LV}$~\cite{[Plo75]}. It is obtained from the \lc\ by allowing
only $\beta$-redexes whose arguments are \emph{values} (i.e, variables or
abstractions $\lambda x.t$), and that are not in the scope of
$\lambda$-occurrences (we assume that there are no $\delta$-rules in the
calculus). it is easy to see that $\lambda_{LV}$ forms a linear SDRS. Now
consider the reduction
$$t\red{w} o=\overbrace{((\lambda
x.u)y)}^{v_1} \overbrace{((\lambda x.u)y)}^{v_2}\doar uu=s,$$ where
$t=w=(\lambda x.(xy)(xy))\lambda x. u$ and $u$ is
a $\lambda_{LV}$-redex such that $x$ does not occur free in it. It is reasonable
to share the two occurrences of $u$ in $s$, but in order to make the
reduction graph of $t$ a DFS (in particular, for the [contribution] axiom
to be satisfied), we need to share $v_1$ and $v_2$ as well, although the
two are not related.  This goes beyond L\'evy's concept of sharing, and the
resulting DFS is not separable as the contraction of $w$ creates two
different redexes, $v_1$ and $v_2$, of the same family. Note that the
occurrences of $u$ in $s$ are \emph{created} by $v_1$ and $v_2$, as the
occurrences of $u$ in $t$ and $o$ are not $\lambda_{LV}$-redexes (they are
not admissible).





\section{Implementation DFSs}
\label{S.impl.drs.}


We now define the \emph{implementation} $\lin{\cal F}$ of a DFS $\cal F$,
whose reductions correspond to complete family-reductions in $\cal F$,
hence the name.  We will assume that the
reduction graph of $\calF$ is the reduction graph of an \emph{initial}
term, denoted by $t_\emp$, and that families are considered relative to
$t_\emp$, i.e, all histories start with $t_\emp$.



\bdl{D.lin.dfs.drs.}
Let ${\cal F}=({\cal R},\fami,\contr)$ be a DFS, where $\calR=(A,/)$ and
$A=(Ter,Red,\ar)$. The \emph{implementation}
or \emph{L\'evy-implementation} of ${\cal F}$ is the AZDFS $\lin{{\cal
F}}=({\cal R}_I,\fami_I,\contr_I)$, where

$\bullet$ the branches of the reduction graph of the underlying ARS $A_I$ of
${\cal R}_I=(A_I,/_I)$ are complete family-reductions starting from
$t_\emp$, each edge (i.e., a reduction step) being a multi-step contracting
a family of redexes.

$\bullet$ the residual relation $/_I$ is defined as follows: let $U$ and $V$
be complete sets of redexes in two $\fami$-families, in a term $s$, and let
$U:s\ar_I o$ be the multi-step contracting $U$. Then $V/_I U$ is the
multi-step $o\ar_I  e$ contracting all members of the set $V/U$.

$\bullet$ the family and contribution relations $\fami_I,\contr_I$ in
$\lin{{\cal F}}$ are those induced by $\fami$ and $\contr:$ let $P_I$ and
$Q_I$ be reductions in $\calR_I$ corresponding to complete
family-reductions $P$ and $Q$ in $\calF$; then $P_IU\fami_I Q_IV$ iff for
any $u\in U, v\in V$,
$Pu\fami Qv$; and $Fam(P_IU)\contr_I Fam(Q_IV)$ iff $Fam(Pu)\contr
Fam(Qv)$.
\ed


We first  verify that $\lin{{\cal F}}$ in the above definition is indeed
an affine DFS. Note that $\lin{{\cal F}}$ is separable as
its steps contract entire $\fami$-families, hence it is an AZDFS by
\Tr{T.sep.eq.ig.}:



\btl{T.line.zig.}
For any DFS ${\cal F}$, $\lin{{\cal F}}$ is an AZDFS.
\et

Next we show that any sharing $\fami$ in an SDRS stronger than zig-zag can
be decomposed into any weaker sharing $\fami'$ and a \emph{non-separable}
sharing $\fami^*$ in the implementation of $\fami'$.



\bdl{D.str.sh.}
Let $\calF=(\calR,\fami)$ and $\calF'=(\calR,\fami')$ be DFSs. We say that
$\calF$ has a \emph{stronger} sharing than $\calF'$, written
$\calF\geq\calF'$,  if $\fami'\ssq\fami$.
\ed


\btl{T.dec.sh.}
Let $\calF=(\calR,\fami)$ and $\calF'=(\calR,\fami')$ be DFSs. Then $\calF
>\calF'$ iff there is a non-separable family relation $\fami^*$ on the
implementation DRS $\calR'_I$ of $\calF'$ such that $\calF^*_I=\calF_I$,
where $\calF^*=(\calR'_I,\fami^*)$.
\et


Thus, in particular, the study of a sharing in an SDRS strictly larger than
the zig-zag can be reduced to studying zig-zag (when it is a
family-relation) and studying non-separable affine families.



In order to prove that implementation DRSs can simulate optimal
family-reductions in DFSs, let us recall the relative optimality theorem
from~\cite{[rndrs]}:


\begin{deff}\em
\label{D.rel.need.}
 Let $\stab$ be a set of terms in a DRS:

(1)  We call a
redex $u\subt t$ {\em $\stab$-needed} if
at least one residual of it is contracted in any reduction from $t$ to a
term in $\stab$, and call it {\em $\stab$-unneeded} otherwise. We call a
multi-step $U\subts t$ $\stab$-needed if it
contracts at least one $\stab$-needed redex.

(2) We call $\stab$ {\em stable\/} if: (a)
$\stab$ is {\em closed under parallel moves}: for any $t\not\in \stab$, any
$P:t\doar o\in \stab$, and any $Q:t\doar e$ which does not contain terms
in $\stab$, the final term of $P/Q$ is in $\stab$; and  (b) $\stab$ is {\em
closed under unneeded expansion}: for any $e\red{u}o$ such that $e\not\in
\stab$ and $o\in \stab$, $u$ is $\stab$-needed.
\end{deff}



\bt
\label{T.unif.opt.}
{\bf (Relative Optimality~\cite{[rndrs]})}
Let $\stab$ be a stable set of terms in a DFS $\calF$, and let $t$ be an
$\stab$-normalizable term in $\cal F$. Then any  $\stab$-needed complete
family-reduction $Q$ starting from $t$ is eventually $\stab$-normalizing
and is $\stab$-optimal in the sense that it has a minimal number of
family-reduction steps.
\et


We show that the implementation DRSs $\lin\calF$ do indeed correctly
`implement' complete family-reductions in DFSs $\calF$:


\btl{T.impl.theo.}
{\bf (Optimal Implementation)}
Let $\stab$ be a stable set of terms in a DFS $\calF$ and let $\lin\stab$ be
its corresponding stable set of terms in $\lin\calF$. Then $\lin\stab$ is
stable and $\lin\stab$-needed
$\lin\stab$-normalizing reductions in $\lin\calF$ are $\lin\stab$-optimal in
$\lin\calF$, and they correspond to $\stab$-optimal complete family-reductions
in~$\calF$.
\et



\section{Conclusions}
\label{S.con.}



We have studied a way to \emph{simulate} or \emph{interpret} duplicating
(conflict-free) reductions with non-duplicating ones, and have investigated
construction of DFSs from non-duplicating SDRSs. DFSs are the unique
abstract framework (among many operational/transition models) enabling such
an interpretation, which makes them a basic framework to model duplicating
computation, and the results presented in this paper demonstrate that the
axiomatization of sharing offered by DFSs is a correct one.


Although in the introduction we have motivated our abstract study of shared
evaluation from an operational point of view, our results (although so far
limited to the conflict-free case) are fundamental in the study of both
sequential and concurrent semantics of languages related to the \lc. For
example, although the seminal work by Kahn and Plotkin~\cite{[K.P.]} does
not mention residuals or families explicitly, an analog of
\Tr{P.on.ca.for.} is established there for the linear (but not
conflict-free) case. And the (implicit) construction of zig-zag DFSs from a
linear residual relation is the key idea behind the so called
\emph{representation theorems} relating computational structures (such as
Concrete Data Structures, [Stable or Prime] Event Structures, or [Prime]
Information Systems) with the corresponding domains of
computation~\cite{[K.P.],[Win89],[Sco],[L.W.],[Zha91]}.


The results presented in this abstract have been used essentially in
constructing a fully adequate Event Structure style semantics for all
orthogonal reduction systems~\cite{[dpes]}. The latter construction covers
for example the construction of Event Semantics for orthogonal graph
rewriting systems in~\cite{[KKSdV],[Sch]}. These results have also been
used in the
definition of \emph{independence} of computations, and construction of
Euclidian Geometry from the reduction spaces in orthogonal rewrite
systems~\cite{[icalp]}. Finally, the results have recently been used in the
study of \emph{stable computational semantics} unifying
Boudol's~\cite{[Bou]} computational semantics with Winskel's~\cite{[Win89]}
Stable Event Structure semantics (in the conflict-free
case)~\cite{[stable]}. In particular, we prove a representation theorem for
domains generated by pairs $(\calR,\stab)$ and $(\calF,\stab)$ which refine
Berry's~\cite{[berry]} $dI$-domains, and in the special case when $\calR$
and $\calF$ are linear these domains coincide with $dI$-domains.




\begin{thebibliography}{99}

\bibitem[{AL93}]{[AL]}
Asperti A., Laneve C. Interaction systems~I: the
theory of optimal reductions.  MSCS 11:1-48, 1993.

\bibitem[{AL96}]{[AL2]}
Asperti A., Laneve C. Interaction systems~II: the practice of optimal
reductions.  TCS 159(2):191-244, 1996.


\bibitem[{Ber79}]{[berry]}
Berry G. Mod\'eles compl\'etement ad\'equats et stables des
$\lambda$-calculs typ\'es. Th\`ese de l'Uni\-ver\-sit\'e
de Paris VII, 1979.

\bibitem[{Bou85}]{[Bou]}
Boudol G. Computational semantics of term rewriting systems. In: Algebraic
methods in semantics. Nivat M., Reynolds J.C., eds.
Cambridge Univ. Press, 169-236, 1985.

\bibitem[{GK94}]{[ctrs]}
Glauert J. R. W., Khasidashvili Z. Relative normalization in orthogonal
expression reduction systems.  CTRS'94, LNCS 968:144-165, 1994.

\bibitem[{GK96}]{[rndrs]}
Glauert J. R. W., Khasidashvili Z. Relative normalization in deterministic
residual structures.   CAAP'96, LNCS 1059:180-195, 1996.

\bibitem[{GAL92}]{[GAL]}
Gonthier G., Abadi M., L\'evy J.-J. The geometry of optimal lambda
reduction.  POPL'92, 15-26, 1992.

\bibitem[{GLM92}]{[GLM]}
Gonthier G., L\'evy J.-J., Melli\`es P.-A. An abstract standardisation
theorem.  LICS'92, 72-81, 1992.

\bibitem[{Gue96}]{[Gue.th]}
Guerrini S. Theoretical and practical issues of optimal implementations of
functional languages. Ph.D. Thesis, University of Pisa,~1996.

\bibitem[{Hin69}]{[Hin]}
Hindley R.J. An abstract form of the Church-Rosser theorem I. JSL
34(4):545-560, 1969.

\bibitem[{HL91}]{[H.L.]}
Huet G., L\'evy J.-J. Computations in orthogonal rewriting
systems. In: Computational Logic, Essays in Honor of Alan
Robinson, J.-L.~Lassez and G.~Plotkin, eds., p.~394-443, MIT Press, 1991.

\bibitem[{KP93}]{[K.P.]}
Kahn G., Plotkin G.D. Concrete domains. In: To Corrado B\"ohm, TCS
121:186-277, 1993.

\bibitem[{Kat90}]{[Kath]}
Kathail V. Optimal Interpreters for lambda-calculus based functional
languages, Ph.D. thesis, MIT, 1990.


\bibitem[{KS89}]{[K.S.]}
Kennaway J. R., Sleep M. R. Neededness is hypernormalizing in  regular
combinatory reduction systems. Technical Report, UEA Norwich, 1989.


\bibitem[{KKSV93}]{[KKSdV]}
Kennaway J.R., Klop J W., Sleep M.R, de Vries F.-J. Event structures and
orthogonal term graph rewriting. In:~\cite{[SPE]}, 141-156, 1993.


\bibitem[{Kha98}]{[stable]}
Z. Khasidashvili, Stable computational semantics of conflict-free rewrite
systems. Draft. Available at http://www.sys.uea.ac.uk/\~{}zurab.

\bibitem[{KG96}]{[dndrs]}
Khasidashvili Z.,  Glauert J. R. W. Discrete normalization in deterministic
residual structures.   ALP'96, LNCS 1139:135-149, 1996.


\bibitem[{KG97}]{[acoi-rep]}
Khasidashvili Z.,  Glauert J. R. W.  An abstract concept of optimal
imple\-men\-ta\-tion, Technical Report SYS-C97-01, UEA Norwich,~1997.


\bibitem[{KG97a}]{[icalp]}
Khasidashvili Z., Glauert J. R. W. The geometry of orthogonal reduction
spaces.  ICALP'97, LNCS~1256:649-659, 1997. Full version:  Technical Report
SYS-C98-04, UEA Norwich, 1998.


\bibitem[{KG97b}]{[dpes]}
Khasidashvili Z., Glauert J. R. W.  Relating conflict-free stable transition and
event models. MFCS'97, LNCS 1295:269-278, 1997.


\bibitem[{KG98}]{[atoe-tcs]}
Khasidashvili Z., Glauert J. R. W. An abstract theory of optimal
evaluation. Draft. Available at http://www.sys.uea.ac.uk/\~{}zurab.



\bibitem[{Klo80}]{[Kl.CRS]}
Klop J. W.  Combinatory reduction systems. Mathematical Centre
Tracts  no.~127,  CWI, Amsterdam, 1980.


\bibitem[{Lam90}]{[Lam]}
Lamping J. An algorithm for optimal lambda calculus reduction.
 POPL'90,  16-30, 1990.

\bibitem[{LW84}]{[L.W.]}
Larsen K., Winskel G. Using information systems to solve recursive domain
equations effectively.  LNCS 173, 1984.


\bibitem[{L\'ev78}]{[levy]}
L\'evy J.-J. R\'eductions correctes et optimales dans le
lambda-calcul. Th\`ese de l'Universit\'e de Paris VII, 1978.


\bibitem[{L\'ev80}]{[le80]}
L\'evy J.-J. Optimal reductions in the lambda-calculus. In: To
H. B. Curry: Essays on Combinatory Logic, Lambda-calculus and
Formalism, Hindley J. R., Seldin J. P. eds.,
pp.~159-192, Academic Press, 1980.


\bibitem[{Mar91}]{[Mar91]}
Maranget L. Optimal derivations in weak $\lambda$-calculi and in orthogonal
term rewriting systems.  POPL'91,255-269, 1991.


\bibitem[{Mel96}]{[Mel]}
Melli\`es P.-A. Description abstraite des syst\`emes de r\'e\'ecriture.
Th\`ese de l'Universit\'e Paris 7, 1996.


\bibitem[{Oos96}]{[Oos]}
van Oostrom V. Higher order families. RTA'96,
 LNCS 1103:392-407, 1996.


\bibitem[{Plo75}]{[Plo75]}
Plotkin G.  Call-by-name, call-by-value and the $\lambda$-calculus.
TCS 1:125-159, 1975.


\bibitem[{Sch94}]{[Sch]}
Schied G. On relating rewrite systems and graph grammars to event
structures. GTCS'94, LNCS, 776:326-340, 1994.

\bibitem[{SPE93}]{[SPE]}
Sleep M.R., Plasmeijer M.J., van Eekelen M.C.J.D. , eds.
Term Graph Rewriting: Theory and Practice,  John Wiley, 1993.

\bibitem[{Sco82}]{[Sco]}
Scott D. Domains for denotational semantics. ICALP'82, LNCS 140:577-613, 1982.


\bibitem[{Sta89}]{[Sta]}
Stark E.~W. Concurrent transition systems.
TCS 64(3):221-269, 1989.

\bibitem[{Win89}]{[Win89]}
Winskel G. An introduction to event structures.
 LNCS 354:364-397, 1989.

\bibitem[{Zha91}]{[Zha91]}
Zhang G.-Q. Logic of Domains. Birkh\"auser, 1991.

\end{thebibliography}

\end{document}



