%% Start LaTeX Document
\documentstyle{llncs}
%\documentstyle[11pt]{article}
%\documentstyle[fullpage,11pt,amssymbols]{article}
%\input{BoxedEPS}
%\HideDisplacementBoxes
%\SetOzTeXEPSFSpecial
\marginparwidth 0pt
\oddsidemargin  0pt
\evensidemargin  0pt
\marginparsep 0pt

\topmargin   0pt

%\textwidth   6.5in
%\textheight  8.5 in

\input{diagrams} % Paul Taylor's Macro Package
\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.
\newtheorem{thm}{Theorem}[section]
\newtheorem{lem}{Lemma}[section]
\newtheorem{cor}{Corollary}[section]
\newtheorem{ex}{Example}[section]
\newtheorem{rem}{Remark}[section]
\newtheorem{prop}{Proposition}[section]
%%%%\newtheorem{proof}{Proof}
%\newenvironment{proof}{{\it Proof:}}{{\it Q.e.d.}}
\newenvironment{akn}{\noindent{\bf Acknowledgments }}{}
\newenvironment{pruuf}{\noindent{\bf Proof }}{}
\newtheorem{deff}{Definition}[section]
\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}$}}
\newenvironment{prsk}{\noindent{\bf Proof sketch }}{}
\newenvironment{altpr}{\noindent{\bf Alternative proof }}{}
\newcommand{\inputpic}[1] {\begin{center} \input{#1} \end{center}}
\newcommand{\ssq}{\subseteq}
\newcommand{\sset}{\subset}
\hyphenation{meta-var-ia-ble}
\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{\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{\fin}{\in}
%\newcommand{\lleq}{\triangleleft}
%\newcommand{\lles}{\triangleleft}
\newcommand{\lleq}{\unlhd}
\newcommand{\lles}{\lhd}
\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{\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{\setm}{\setminus}
\newcommand{\crea}{\vdash}
\newcommand{\emp}{\emptyset}
\newcommand{\cfr}{complete family-reduction}
\newcommand{\cfrs}{complete 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}}

 
\title{Relative Normalization in Deterministic Residual Structures}
\author{John Glauert and Zurab Khasidashvili}
\institute{School of Information Systems, UEA \\
Norwich NR4 7TJ England \\
jrwg@sys.uea.ac.uk, zurab@sys.uea.ac.uk
\thanks{This work was supported by the Engineering and Physical Sciences
Research Council of Great Britain under grant GR/H 41300}}

 
\maketitle

 

\begin{abstract}
This paper generalizes the Huet\&L\'evy theory of normalization by
neededness to an abstract setting. We define \emph{Stable Deterministic
Residual Structures} (SDRS) and {\em Deterministic Family Structures} 
(DFS) by axiomatizing
some properties of the residual relation and the family relation on redexes
in an {\em Abstract Rewriting System}. We present two proofs of the {\em
Relative Normalization Theorem}, one for SDRSs for {\em regular stable}
sets, and another for DFSs for all stable sets of
desirable `normal forms'. We further prove the {\em Relative Optimality
Theorem} for DFSs. We extend this result
to deterministic {\em Computation Structures\/} which are deterministic
{\em Event
Structures\/} with an extra relation expressing {\em self-essentiality}.
\end{abstract}

 

\section{Introduction}

A normalizable term, in a rewriting system, may have an
infinite reduction, so it is important to have a {\em normalizing}
strategy which enables one to construct reductions to normal
form. It is well known that the leftmost-outermost strategy is
normalizing in the $\lambda$-calculus~\cite{[C.F.]}.

For Orthogonal Term
Rewriting Systems (OTRSs), a general normalizing strategy, called
the {\em needed} strategy, was found by Huet and L\'evy
in~\cite{[H.L.]}. The needed strategy always contracts a {\em
needed} redex -- a redex whose residual is to be contracted in
any reduction to normal form. Huet and L\'evy showed that any
term $t$ not in normal form has a needed redex, and that repeated
contraction of needed redexes in $t$ leads to its normal form
whenever there is one.


\delete{
Barendregt et al.~\cite{[B.K.K.S.]} generalized the concept of
neededness to the $\lambda$-calculus, and studied neededness also w.r.t.
head-normal forms, proving
correctness of the two needed strategies for computing normal
forms and head-normal forms, respectively. In~\cite{[Mar]}, Maranget
studied a strategy that computes a weak head-normal form of a term in an
OTRS. Normalization w.r.t. another interesting set of `normal forms', that
of constructor head-normal forms in constructor OTRSs, is
studied by N\"ocker~\cite{[Nok.thi.]}. Antoy et al.~\cite{[Ant]}
designed a needed {\em narrowing\/} strategy.  A
different approach to normalization in orthogonal rewrite systems was
developed in Kennaway~\cite{[Kenn]}.
}


Barendregt et al.~\cite{[B.K.K.S.]}, Maranget~\cite{[Mar]}, and
N\"ocker~\cite{[Nok.thi.]} studied neededness w.r.t. head-normal forms, weak
head-normal forms, and constructor head-normal forms, respectively. Sekar and
Ramakrishnan~\cite{[SeRa]} study normalization via {\em necessary\/} set of
redexes.  Kennaway et al.~\cite{[K-tra]} studied needed strategy for infinitary
OTRSs. A different approach to normalization is developed in
Kennaway~\cite{[Kenn]} and
Antoy\&Middeldorp~\cite{[AnMi]}. Antoy et al.~\cite{[Ant]} designed a needed
narrowing strategy.
 Gardner~\cite{[Gar]} described a {\em complete\/} way of encoding
neededness information using a type assignment system.



In~\cite{[ctrs]}, the present authors address the question of
normalization relative to a desired set of final terms,
considering the properties that a set of terms must
possess in order for the neededness theory of Huet and L\'evy
still to make sense. This work is done in the context of orthogonal {\em
Expression Reduction Systems\/} (OERS)~\cite{[OCRS]}, a form of
higher-order rewriting which subsumes Term Rewriting and the
$\lambda$-calculus.
Natural conditions are imposed on $\stab$, called {\em stability}, that are
necessary and sufficient for the following {\em Relative Normalization\/}
(RN for short) theorem to hold:  each $\stab$-normalizable term not in
$\stab$ (not in {\em $\stab$-normal form\/}) has at least one
$\stab$-needed redex, and repeated contraction of $\stab$-needed redexes in
a term $t$ will lead to an $\stab$-normal form of $t$ whenever there is
one. It is shown also that if a stable $\stab$ is {\em regular},
i.e., if $\stab$-unneeded redexes cannot duplicate $\stab$-needed ones,
then the $\stab$-needed strategy is hypernormalizing as well.

In this paper, we further generalize the Huet\&L\'evy theory, by
abstracting from the structure of terms. We study relative normalization in
{\em Deterministic Residual Structures} (DRSs).   A DRS is an {\em Abstract
Reduction Systems} (ARSs) which has a {\em residual relation\/} 
between redexes in
the source and target terms of each transition.
Redexes of $t$ may be erased by reduction of $u$, new redexes may be
introduced in $s$, while other redexes of $s$ are considered {\em
residuals} of redexes in $t$, as specified by the residual relation.
Further, the residual relation is generalized to all reductions, and {\em
permutation-equivalence} on reductions, referred to below as {\em
L\'evy-equivalence}, and the {\em embedding relation}, which induces a
partial ordering on the reduction space, is introduced, as is done for the
\lc\  in~\cite{[levy],[le80]}. Sufficient conditions needed to define the
above concepts in an abstract setting were stated in Stark~\cite{[Sta]} and
Gonthier et al.~\cite{[GLM]}.


\delete{
Our paper is very close in spirit to \cite{[GLM]}, where several axioms are
imposed on the residual relation making it possible to define an abstract
notion of standard reduction and prove an {\em Abstract Standardization
Theorem} of which the Standardization Theorems in the \lc, orthogonal
TRSs~\cite{[H.L.]} and left-normal CRSs~\cite{[Kl.CRS]} are special cases.
The way standardization is understood in that paper requires a {\em
nesting} relation on redexes in a term, and some axioms giving its
important properties. Standard reductions then become some kind of
outside-in reductions.
}


In~\cite{[Sta]}, Stark defines {\em Concurrent Transition Systems} (CTSs)
and uses them to develop a model of concurrent computation,
studying ways of building machine networks with concurrent machines as
basic objects. On the other hand, Gonthier et al.~\cite{[GLM]} were
interested in studying more syntactic properties, such as standardization,
of orthogonal rewrite systems in an abstract setting. The way
standardization is understood in that paper requires a {\em nesting}
relation on redexes in a term, and some axioms giving its important
properties. Standard reductions then become some kind of outside-in
reductions. However, the \cite{[GLM]} axioms are rather restrictive, since
say orthogonal DAGs~\cite{[Mar91],[Mar],[KKSdV]} do not satisfy
them.\footnote{Counterexamples to axioms 2 and 3 of~\cite{[GLM]} were
pointed out by R.~Kennaway.}

Our DRSs are more refined than CTSs, since in the latter the residual
relation is non-duplicating. We do not impose a nesting relation on
redexes, but are still able to prove the \rn\ theorem for all {\em regular}
stable sets $\stab$. (We actually prove  the Relative Hypernormalization
theorem.)  We only use a form of Berry's {\em stability\/}
axiom~\cite{[berry]}.
We show that without the latter axiom the \rn\
theorem fails. The method employed to prove the \rn\ theorem is similar to
that in~\cite{[colog]}, and is based on the fact that $\stab$-needed steps
can be pushed before $\stab$-unneeded steps, in any reduction, without
affecting the number of $\stab$-needed steps.
The important
difference is that in~\cite{[colog]} we made heavy use of the notion of
{\em descendant of subterms} -- a refinement of the residual notion for
redexes -- which is a very syntactic notion, and therefore much
more difficult to axiomatize.

Since for {\em irregular} stable $\stab$, $\stab$-unneeded redexes can
duplicate $\stab$-needed ones, the above proof method does not work; for
the same reason, the $\stab$-needed strategy is not hypernormalizing any
more. Therefore, to prove \rn\ for irregular stable $\stab$, we define the
{\em Deterministic Family Structure\/} (DFS) as a DRS with a very liberal 
notion of {\em
family} relation \cite{[levy],[le80]} and a {\em contribution} relation on
families, expressing the notion of (at least one member of) a family to be
needed to create another family. For DFSs, the proof of the \rn\ theorem for
all stable $\stab$ from \cite{[ctrs]} works perfectly.


\delete{
We show that DFSs are stable DRSs, so the previous \rn\
theorem (for stable DRSs w.r.t. regular stable sets) is subsumed by this
one; however the previous \rn\ theorem is also useful since checking for
Berry's stability is much simpler than  constructing a sound family
relation.
}



An advantage of the first RN theorem is that checking for Berry's stability
is much simpler than  constructing a sound family relation.
For example, the \lc~\cite{[levy],[le80]}, orthogonal TRSs~\cite{[Mar]},
Interaction Systems~\cite{[AL]}, and orthogonal CRSs (and
ERSs)~\cite{[Kl.CRS],[K.S.]} form DFSs, hence stable DRSs. For other
higher-order rewriting systems, such as HRSs~\cite{[Nip.b]} and
HORSs~\cite{[Oos.th],[OR94]}, which do form stable DRSs, to our knowledge,
it is not yet known if they form DFSs too (though it is very likely that the
latter is the case).

For DFSs we show that a strategy that only contracts, in an arbitrary order,
redexes that belong to $\stab$-needed families but which need not be
$\stab$-needed themselves, is still $\stab$-normalizing. As a corollary,
any {\em $\stab$-needed complete family-reduction}, which contracts all
members of a family containing an $\stab$-needed redex in a multi-step, is
$\stab$-normalizing. Similarly to \cite{[le80]}, we show that the latter
reductions are optimal in the sense that they reach $\stab$ in the least
number of family-reduction steps.

Using the family axioms, we give an Event Structure
(ES)~\cite{[Win]} semantics to DRSs, by considering redex-families as
events. We define {\em Deterministic Computation Structures} (DCS) as
Deterministic {\em Prime ESs\/} with an extra relation $\alpha \rhd e$
 to express
the fact that an event $e$ is {\em inessential} for a set of events
$\alpha$, a {\em configuration}. This enables us to define
L\'evy-equivalence on prime deterministic ESs. For DCSs, the theory of
relative normalization can be applied.


The paper is organized as follows. In the next section, we introduce stable
DRSs and give some examples. In Section~\ref{S.rn.sdrs.}, we prove the \rn\
theorem for regular stable sets $\stab$ in an SDRS $R$, and demonstrate
that if $R$ is not stable, then the theorem fails. In
Section~\ref{S.rn.fs.}, we introduce DFSs, compare them
with stable DRSs, and prove the RN theorem for all stable $\stab$. In
Section~\ref{S.opt.fs.}, we strengthen the latter result, and prove the
{\em Relative Optimality} theorem for any DFS. Finally, in
Section~\ref{S.norm.es.}, we extend the obtained results to Event
Structures. Conclusions appear in Section~\ref{S.concl.}.

\end{document}

\section{Deterministic Residual Structures}


In this section we define {\em Deterministic Residual Structures} (DRSs)
which are {\em Abstract Reduction Systems\/} (ARSs) satisfying certain
properties concerning residuals.
The definition and some results about ARSs can be found e.g.,
in~\cite{[Kl.TRS]}. Our definition is slightly different. 
An ARS is a
triple $A$ = ({\em Ter},{\em Red},$\ar$)
where {\em Ter} is a set of {\em terms}, ranged over by
$t,s,o,e$; {\em Red} is a set of {\em redexes} (or {\em redex occurrences}),
ranged over by $u,v,w$; and
$\ar:Red\ar (Ter\times Ter)$ is a function such that for any $t\in Ter$
there is only a finite set of $u\in Red$ such that $\ar(u)=(t,s)$,
written $t\red{u}s$. This set will be known as the redexes of term $t$, where
$u\subt t$ denotes that
$s$ is a member of the redexes of $t$ and $U\subts
t$ denotes that $U$ is a subset of the redexes.
Note
that $\ar$ is a {\em total\/} function, so one can identify $u$ with the
triple $t\red{u}s$.
A {\em 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\leq Q$ denotes
that $P$ is an initial part of $Q$. $\,\,\,\emptyset_t$ denotes the empty
reduction starting from $t$.
\delete{$Pu$ denotes a redex $u$ in the final term $ft(P)$ of $P$.
 $u$ also denotes the reduction that contracts $u$.} We use $U,V,W$ to
denote sets of redexes of a term.

DRSs are similar to Stark's {\em Determinate Concurrent Transition
Systems} (DTCS) \cite{[Sta]}, to {\em Abstract Reduction Systems} of Gonthier et
al.~\cite{[GLM]},
and to van Oostrom's {\em Descendant Rewriting Systems}~\cite{[Oos.th]}.
The main difference from DCTSs is that Stark considers  a non-duplicating
residual relation (and we do not distinguish a {\em start state}). The
difference from ARSs of~\cite{[GLM]} is that we do
not have a nesting relation on redexes and the corresponding axioms, and
the stability axiom is modified accordingly. The
difference from van Oostrom's DRSs is that in the latter the notion of {\em
descendant} of any subterm/position of a term is formalized, not only the
notion of residual of redexes.


\begin{deff}\em
\label{D.levy.str.}
{\bf (Deterministic Residual Structure)}  A {\em Deterministic Residual
Structure\/} (DRS) is a pair $R=(A, /)$, where $A$ is an ARS
and
$/$ is a {\em 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 {\em 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$ {\em duplicates\/} $v$.
If $v/u=\emptyset$, then $u$ {\em erases\/} $v$.
A redex of $s$
which is not a residual of any $v\subt t$ under $u$ is said to be
\delete{
{\em $u$-new\/} or
}
{\em created\/} by $u$.
The set of residuals of a
redex under any reduction is defined by transitivity.

A {\em development} of a set $U$ of redexes in a term $t$ is a reduction
$P:t\doar $ that only contracts residuals of redexes from $U$; the
development $P$ is {\em complete} if $U/P$, the set of residuals under $P$
of redexes from $U$, is empty $\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, called {\em Finite Developments (FD)}~\cite{[GLM]} and {\em
acyclicity\/}~(which appears as axiom $(4)$ in~\cite{[Sta]}):

$\bullet$ [FD]  All developments are terminating; all co-initial complete
developments of the same set of redexes end at the same term; and residuals
of a redex under all complete co-initial developments of a set of redexes
are the same.

$\bullet$  [acyclicity] Let $u,v\subt t$, let $u\not= v$, and let
$u/v=\emp$. Then $v/u\not=\emp$.
\ed


The properties of the residual relation are all standard, and we refer
to~\cite{[H.L.],[levy],[le80],[Sta]} for details. Hence,
we assume that, in a DRS $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 that {\em L\'evy-equivalence} or {\em
permutation-equivalence} is defined as the smallest relation on co-initial
reductions satisfying: $U+ V/U\leeqv V+U/V$ and $Q\leeqv Q'\,
\Rightarrow \, 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$.
The above relations can
equivalently be defined also using Klop's method of commutative diagrams.
We will often use Klop's diagrams in definitions and proofs. The method  is
well described in~\cite{[Kl.CRS],[Bar]}.


\bd
We call a DRS $R$ {\em stable} (SDRS) if the following axiom is satisfied
\suppress{(see Figure~\ref{berry-stab})}:

$\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 by $u/v$.


\begin{figure}
\begin{diagram}[height=2em,width=2em]
 t      & \rTo^u       & e             & \rTo^w           & {}  \\
 \dTo^v &              &  \dOnto_{v/u}  &                 &      \\
s       & \rOnto_{u/v} & o              & \rOnto_{w/(v/u)}   & {}  \\
\end{diagram}
%\caption{Berry's Stability}\label{berry-stab}
\end{figure}

\ed


\zurab{Intuitively, stability means that a 
redex cannot arise from two unrelated sources.}


It is easy to verify that the $\lambda$-calculus~\cite{[levy]}, orthogonal
TRSs~\cite{[H.L.]}, orthogonal Higher-Order Rewriting Systems
(HORSs)~\cite{[OR94],[Oos.th]},  and hence other orthogonal higher-order
rewrite systems as well (such as CRSs~\cite{[Kl.CRS]}, ERSs~\cite{[OCRS]},
and HRSs~\cite{[Nip.b]}), and Orthogonal Term Graph Rewriting Systems
\cite{[KKSdV]} form DRSs; the latter are equivalent to Maranget's
orthogonal DAG (Directed Acyclic Graphs) rewriting systems, defined via
labelled orthogonal TRSs. All these are stable, and can be shown so
without using any notion of labelling.

\delete{as can be checked just using an appropriate notion of descendant
which assigns the contractum to the contracted redex, as defined
in~\cite{[OCRS]} for ERSs -- labelling is not necessary. (The descendant
notion defined e.g., in~\cite{[B.K.K.S.]} is essentially the residual
notion, and is not useful for this purpose.)
}



\section{The Relative Normalization Theorem for regular stable sets}
\label{S.rn.sdrs.}


In this section, we prove that, for any {\em
regular} stable $\stab$ in a stable DRS $R$, an $\stab$-normal form of an
$\stab$-normalizable term can be found by contracting $\stab$-needed
redexes in it, even if every $\stab$-needed step is preceded by a finite
number of $\stab$-unneeded steps. We show that without the assumption of
stability for $R$, this result breaks down. Further, examples from
\cite{[ctrs]} show that the stability of $\stab$ is necessary for the
Relative (Hyper)normalization theorem to hold. This shows that the
stability of $\stab$ for a Berry--stable $R$ provides a unique notion of
stability for the computation system $(R,\stab)$.  


\begin{deff}\em
\label{D.rel.need.}
(\cite{[ctrs]}) \delete{Let $\Pi$ be a set of reductions and $\stab$ be a
set of terms in a DRS $R$. We call a redex  $u$ in $t$ {\em $\Pi$-needed}
if at least one residual of it is contracted in every reduction of $\Pi$,
and call it {\em $\Pi$-unneeded} otherwise.} We call a redex $u\subt t$
{\em $\stab$-needed}, written $NE_\stab (u,t)$, 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}, written $UN_\stab (u,t)$, otherwise.
\delete{(Thus $\stab$-neededness coincides with neededness w.r.t. the set
of all $\stab$-normalizing reductions.)}
\end{deff}




\begin{deff}\em
(\cite{[ctrs]}) (1) We call a set $\stab$ of terms {\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 doesn't contain redexes
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.

(2) We call a stable set $\stab$ {\em regular\/} if $\stab$-unneeded
redexes cannot duplicate $\stab$-needed ones.
\end{deff}

Obviously, stability and regularity coincide in non-duplicating systems.
Below $\stab$ (resp. $\reg$) will usually denote a (resp. regular) stable
set of terms in some DRS. For simplicity, we only consider stable sets
$\stab$ that are closed under reduction; obviously, closure of $\stab$
under reduction implies its closer under parallel moves.

The most appealing examples of stable sets are the
set of normal forms~\cite{[H.L.]}, the set of head-normal
forms~\cite{[B.K.K.S.]}, the set of weak-head-normal forms in OTRSs (a
partial result is in~\cite{[Mar]}), and the set of
constructor-head-normal forms for constructor
TRSs~\cite{[Nok.thi.]}. All the above sets are closed under reduction, and
are regular. Other examples include weak-head-normal forms (up to
garbage-collection, modulo a congruence) in Yoshida's $\lambda f$-calculus
(an environment calculus)~\cite{[Yos]} and the set of {\em answers\/} in
{\em call-by-need} $\lambda$-calculus of Ariola et al.~\cite{[A.F.]}; both
are conditional rewrite systems. An example of an OTRS with an irregular
stable $\stab$ is given in Remark~\ref{R.irreg.no.hyper.}.


\delete{
\bdl{D.ext.reductions.}
We call $P:t\doar s$ {\em external} to $Q:t\doar e$ if for every elementary
diagram $D(u,v)$ in a diagram $D(P,Q)$ of $P$ and
$Q$~\cite{[Kl.CRS],[Bar]}, whatever order of construction of developments
in the elementary diagrams is used, one has $u\not= v$. We call $P$
external to a set of redexes $U\subts t$ if $P$ doesn't contract residuals
of redexes in $U$ (i.e., iff $P$ is external to the development $U$). We
will say that $P$ is external to $u\subt t$ if it is external to $\{u\}$.
\ed
}


\zurab{
The following definition introduce the notion of a reduction being {\em
external\/} to another, co-initial one. For
syntactic systems externality is a natural concept relating to overlap between
components of terms involved in reduction steps. In an abstract setting it
expresses the absence of shared (residuals of) redexes. 
}

\bdl{D.ext.reductions.}
$\bullet$ Let $u\in U\subts t$ and $P:t\doar$. We call $P$ {\em external\/}
to $U$ (resp. $u$) if $P$ does not contract residuals of redexes in $U$
(resp. residuals of $u$).

$\bullet$ Let $P:t_0\dored{P_i}t_i\red{u_i}t_{i+1}\doar$ and
$Q:t_0=s_0\dored{Q_j}s_j\red{v_j}s_{j+1}\doar$. We call $P$ {\em
external\/} to $Q$ if for any $i,j$,  $U_{i,j}\cap
V_{i,j}=\emp$, where $U_{i,j}=u_i/(Q_j/P_i)$ and
$V_{i,j}=v_j/(P_i/Q_j)$).

\begin{diagram}[height=1.8em,width=1.8em]
t_0          &\rOnto^{P_i}& & t_i       &\rTo^{u_i}   & t_{i+1} & &\rOnto &{}\\
\dOnto<{Q'_j}&            & &\dTo<{Q_j/P_i}&         & \dOnto & & &     \\
{}       &\rOnto^{P_i/Q_j}& & {}    & \rOnto^{U_{i,j}} & {}     &  &   &{}\\
\dTo<{v_j}   &         & &\dOnto^{V_{i,j}} &             & \dOnto &  & &   \\
{}           &\rOnto      & &  {}       & \rOnto      & {}   & &   &{}\\
\dOnto       &            & &          &             &       & &  &   \\
{}           &        & & {}        &          &  {}   & &   &{}\\
\end{diagram}
\ed

Obviously, $P$ is external to the set $U$ iff it is external to any
development of $U$, and is external to a redex $u$ iff it is external to
the reduction contracting $u$.



\bll{L.external.rem.ext.}
Let $P:t_0\red{v_0}t_1\red{v_1}\ldots\ar t_n$ be external to
$U=\{u_1,\ldots,u_n\}\subts t_0$, and let $Q_0:t_0\doar o_0$. Then
$P'=P/Q_0$ is external to $U'=U/Q_0$. If $P$ is $\stab$-normalizing, then
so is $P'$.

\begin{pruuf}
Let $P_i:t_0\red{v_0}t_1\red{v_1}\ldots\ar t_i$, $Q_i=Q_0/P_i$, and
$P'_{i+1}=v_i/Q_i$, $(0\leq i<n)$ \suppress{(See Figure~\ref{extern-red})}.
Since $P$
is external to $U$, we have
for each $i$ that $v_i\not\in U/P_i$. Therefore, $v_i/Q_i\cap
U/(P_i+Q_i)=\emptyset$ (since the residuals of different redexes are
different). Thus \delete{by \Pr{L.perm.equiv.}.(3),} $v_i/Q_i\cap
U/(Q_0+P'_1+\ldots+P'_{i})=\emptyset$. Hence, $P'_{i+1}$ is external to
$U'/(P'_1+\ldots+P'_{i})$. This means that $P'$ is external to $U'$. If $P$
is $\stab$-normalizing, then so is $P'$ by stability of $\stab$.


\begin{figure}
\begin{diagram}[height=2em,width=2em]
 t_0  & \rTo^{v_0=P_1} & t_1  & \rOnto   & t_{n-1} &  \rTo^{v_{n-1}} & t_n   \\
 \dOnto^{Q_0}&     &  \dOnto^{Q_1} &   &     \dOnto^{Q_{n-1}}   &   &
\dOnto_{Q_n}\\
o_0  & \rOnto_{P'_1} & o_1  & \rOnto  & o_{n-1} &  \rOnto_{P'_{n}} &   o_n   \\
\end{diagram}
\suppress{\caption{Preservation of External Reductions}\label{extern-red}}
\end{figure}
\end{pruuf}
\el


\begin{cor}\em
\label{T.3.1.c.}
 For any stable $\stab$, residuals of $\stab$-unneeded redexes under any
reduction remain $\stab$-unneeded.
\end{cor}





\bll{L.disj.red.creat.}
Let $P:t\doar s$ be external to $Q:t\doar e$, in an SDRS, and let $P$
create redexes $W\subts s$. Then the residuals $W/(Q/P)$ of redexes in $W$
are created by $P/Q$, and $Q/P$ is external to~$W$.


\bproof
By induction on the number $n$ of elementary diagrams in $D(P,Q)$. The case
$n=1$ is the axiom [stability]. So let say $\vert P\vert>1$, i.e., $P=u+N$
with $\vert N\vert>0$ \suppress{(see Figure~\ref{disj-redex})}. Then
$W=W_u/N\cup
W_N$, where $W_u$ is the set of
redexes created by $u$, and $W_N$ is the set of redexes created by (i.e.,
along) $N$. By the induction assumption, $Q/u$ is external to $W_u$, and
the redexes in $W_u/(Q/u)$ are created by $u/Q$. By
\Lr{L.external.rem.ext.}, $Q/P=(Q/u)/N$ is external to $W_u/N$. By the
induction assumption, $Q/P=(Q/u)/N$ is external to $W_N$ and redexes in
$W_N/(Q/P)$ are created by $N/(Q/u)$. Hence $Q/P$ is external to $W$, and
since $W/(Q/P)=W_N/(Q/P)\cup W_u/((Q/u)\sqcup N)$, redexes in $W/(Q/P)$ are
created by $P/Q$.

\begin{figure}
\begin{diagram}[height=1.5em,width=4em]
  t            & \rOnto^{Q}   &   e     \\
 \dTo^{u}   &              &     \dOnto \\
 {}           & \rOnto^{Q/u}&  {}          \\
\dOnto^{N}     &              &     \dOnto \\
  s        & \rOnto_{Q/P=(Q/u)/N}&  {}    \\
\end{diagram}
\suppress{\caption{External Redex Creation}\label{disj-redex}}
\end{figure}
\eproof
\el


\begin{lem}\em
\label{L.4.1.c.stab.}
Let $\stab$ be stable, let $t\not\in \stab$, $t\red{u}e$, $UN_\stab (u,t)$,
and let $w\subt e$ be a $u$-new redex, in a stable DRS. Then $UN_\stab
(w,e)$.

\begin{pruuf}
If $e\in \stab$, then every redex in $e$ is $\stab$-unneeded; so suppose
$e\not\in \stab$. $UN_\stab (u,t)$ implies existence of an
$\stab$-normalizing $P:t\doar s$ that does not contract residuals of $u$.
By \Lr{L.disj.red.creat.}, $P/u$ does not contract residuals of $w$. Also,
$P/u$ is $\stab$-normalizing since $\stab$ is closed under parallel moves.
Hence $w$ is $\stab$-unneeded.
\end{pruuf}
\end{lem}



The following example shows that, in the above lemma, stability of the DRS
is necessary.


\bel{E.nec.of.stab.for.norm.the.}
Let terms in the DRS $R$ be $t=I(I(x))$, $s=I(x)$, and $e=x$; redexes in
$t$ be $u=t$ and $v=I(x)$, $s$ contain the only redex $w=s$, and $x$
doesn't contain a redex; let the reduction relation be given by
$Red=\{t\red{u}s, \,t\red{v}s, \,s\red{w}x\}$, let the residual relation be
empty except for empty reductions, for which the residual relation is
identity, and let $\stab=\{x\}$. (Obviously, this is not, and cannot be,
the usual residual relation for orthogonal TRSs.) Then $\stab$ is stable
and regular, both $u$ and $v$ are $\stab$-unneeded, and both create the
redex $w\subt s$ that is $\stab$-needed. Note also that the Relative
Hypernormalization theorem (proved below) is not valid for $(R,\stab)$
since $t\not\in \stab$ is $\stab$-normalizable but doesn't contain an
$\stab$-needed redex.
\ee


\delete{
\begin{deff}\em
\label{D.4.1.}
We call  $P:t_0\ar t_1\ar\ldots$  {\em $\stab$-(un)needed}, written
$NE_\stab (P)$, (resp. $UN_\stab (P)$) if it contracts only
$\stab$-(un)needed redexes. $NE_\stab \vert P\vert$ denotes the number of
$\stab$-needed steps in $P$. We call $P$ {\em $\stab$-quasi-needed} if
$NE_\stab \vert P\vert=\infty$ and  call it {\em $\stab$-semi-needed} if it
can be expressed as $P=P_{1}+P_{2}$  with $NE_\stab (P_{1})$  and $UN_\stab
(P_{2})$. In the latter case, we call $P_1$ the {\em $\stab$-needed part}
of $P$ and denote by  $NE_\stab [P]$ ($P_1$ can be infinite, in which case
$P_2=\emptyset$).
\end{deff}
}


\begin{deff}\em
\label{D.4.1.}
We call  $P:t_0\ar t_1\ar\ldots$  {\em $\stab$-(un)needed}, written
$NE_\stab (P)$, (resp. $UN_\stab (P)$) if it contracts only
$\stab$-(un)needed redexes. We call $P$ {\em $\stab$-quasi-needed\/} if it
contracts infinitely many $\stab$-needed redexes, and  call it {\em
$\stab$-semi-needed} if it can be expressed as $P=P_{1}+P_{2}$  with
$NE_\stab(P_{1})$  and $UN_\stab (P_{2})$. In the latter case, we call
$P_1$ the {\em $\stab$-needed part} of $P$ ($P_1$ can be infinite, in which
case $P_2=\emptyset$).
\end{deff}


We now describe an algorithm that, for a {\em regular\/} stable
$\reg $ in a DRS $R$, transforms any finite or infinite reduction $P$ into
an $\reg $-semi-needed reduction $K(P)$. The algorithm is as follows: find
in $P$ the leftmost subreduction $P_0:t\red{u}s\red{v}o$ such
that $UN_\reg (u,t)$ and $NE_\reg (v,s)$. Let $P=P_1+P_0+P_2$. By
Lemma~\ref{L.4.1.c.stab.}, $v$ is a residual of a redex $v'\subt t$, which
is $\reg$-needed by Corollary~\ref{T.3.1.c.}. Since $\reg$ is regular, $v$
is the only residual of $v'$, hence $P_0$ and $P'_0=v'+u/v'$ are both
complete developments of the set $u,v'\subt t$, thus $P_0\leeqv P'_0$. Now
replace $P_0$ by $P'_0$ in $P$. Transform the obtained reduction $P'$ in
the same way, and so on, as long as possible. Obviously, by regularity of
$\reg$, the number of $\reg$-unneeded steps in $P'$ preceding $v'$ is less
than the number preceding $v$ in $P$, and the number of $\reg$-needed steps
in $P$ and $P'$ coincide.


\delete{
The regularity of $\reg $ is essential for termination of the
transformation process, and for preservation of $\reg $-quasi-neededness of
the reduction under transformation. The latter property is crucial for our
method for proving termination of an $\reg$-needed reduction starting from
an $\reg $-normalizable term.
}



\begin{lem}\em
\label{L.4.4.}
Let $P$ be a finite or infinite reduction in an SDRS, and let $\reg$ be regular.

(1) If $P$ ends at a term in $\reg$, then $K(P)$ is a finite
$\stab$-semi-needed reduction whose $\stab$-needed part ends at a term in
$\reg$ as well.

(2) If $P$ is $\stab$-quasi-needed, then $K(P)$ is an infinite
$\stab$-needed reduction.

\begin{pruuf}
(1) Since the transformation doesn't change the number of  $\reg$-needed
steps in $P$, it follows that $K(P)$ is $\reg$-semi-needed, and it ends at
$\reg$ since $K(P)\leeqv P$. The step of $K(P)$ entering $\reg$ is the last
$\reg$-needed step of $K(P)$ by stability of $\reg$. (2) Immediate from the
construction of $K(P)$.
\end{pruuf}
\end{lem}



\delete{
\begin{cor}\em
\label{T.4.1.}
If a term  $t\not\in \reg$ in an  SDRS has an $\reg$-normal form, then $t$
has an $\reg$-needed $\reg$-normalizing reduction, and any
$\reg$-normalizing reduction starting from $t$, with a minimal length, is
$\reg$-needed.
\end{cor}
}




\begin{lem}\em
\label{L.pers.need.}
Let $\reg$ be a regular stable set of terms in a DRS $R$, and let
$t\red{u}s$. Then any $\reg$-needed redex $v\subt t$ different from $u$ has
an $\reg$-needed residual.

\begin{pruuf}
If $t$ is not $\reg$-normalizable, then neither is $s$, and all redexes in
$t$ and $s$ are $\reg$-needed. So suppose $t$ is $\reg$-normalizable
($t\not\in \reg$ since $t$ contains an $\reg$-needed redex), and suppose on
the contrary that each residual $v_i$ of $v$ in $s$ is $\reg$-unneeded. By
closure of $\reg$ under parallel moves, $s$ is $\reg$-normalizing too. By
\delete{\Cr{T.4.1.}} \Lr{L.4.4.}.(1), there is an $\reg$-needed
$\reg$-normalizing reduction $P:s\doar o$. Since by \Cr{T.3.1.c.} all
residuals of each $v_i$ along $P$ are $\reg$-unneeded, $P$ is external to
all $v_i$. Therefore, $u+P$ is external to $v$ and is $\reg$-normalizing --
a contradiction, since $NE_\reg (v,t)$.
\end{pruuf}
\end{lem}








\begin{lem}\em
\label{L.4.5.}
Let  $t_{0}$  have  an $\reg$-quasi-needed  reduction and $t_0\red{u}s_0$.
Then $s_0$ also has an $\reg$-quasi-needed reduction.

\begin{pruuf}
By Lemma~\ref{L.4.4.}, $t_{0}$ has an infinite $\reg$-needed reduction
$P:t_0 \red{u_{0}}t_{1}\red{u_{1}}\ldots$.  Let $U_{i}=u/(u_{0}+ \ldots
+u_{i-1})$,  $i=0,1, \ldots $. \suppress{(see the diagram in
Figure~\ref{Di.ess.}.} It follows from finiteness of developments that
there  are infinitely  many numbers $k$ such that $u_{k}\not\in U_{k}$
(otherwise there should be a number $m$ such that
$t_m\red{u_m}t_{m+1}\red{u_{m+1}}\ldots$ is an infinite
$U_{m}$-development). By Lemma~\ref{L.pers.need.}, $u_{k} \not\in U_{k}$
and $NE_\reg (u_{k},t_{k})$ imply that $u_{k}$ has at least one
$\reg$-needed $U_{k}$-residual  in  $s_{k}$,  i.e. $u_k/U_k$ contains  at
least  one  $\reg$-needed  step. Hence  $P/u$ is $\reg$-quasi-needed.
\end{pruuf}


\begin{figure}
\begin{diagram}[height=2em,width=2em]
t_0    &   \rTo^{u_0}  &   t_1   &   \rTo^{u_1}  &   t_2    &  \rOnto  &   {} \\
 \dTo^{u=U_0}  &     & \dOnto^{U_1} &          & \dOnto^{U_2}&         &      \\
s_0    &   \rOnto_{u_0/U_0}  &   s_1   &   \rOnto_{u_1/U_1}  &   s_2    &
\rOnto  &   {} \\
\end{diagram}
\suppress{\caption{Preservation of Quasi-needed Reductions}\label{Di.ess.}}
\end{figure}

\delete{
\begin{altpr}
Let $P:t_{0}\red{u_{0}}t_{1}\red{u_{1}}\ldots $ contain infinitely many
$\reg$-needed steps. It is easy to see that, in Figure~\ref{Di.ess.}, there
are infinitely many numbers $k$ such that   $NE_\reg (u_{k},t_{k})$ and
$u_k\not\in U_k$. Indeed, otherwise there  would be  a number $m$ such that
in $P_m:t_m\red{u_{m}}t_{m+1}\red{u_{m+1}}\ldots$ all contracted
$\reg$-needed redexes are residuals of $u$. But this is impossible, since,
by Lemma~\ref{L.4.4.}, $K(P_{m})$ would be an infinite development. By
Lemma~\ref{L.pers.need.},  $u_k\not\in U_k$ and $NE_\reg (u_{k},t_{k})$
imply that $u_{k}$ has  at  least  one  $\reg$-needed $U_{k}$-residual in
$s_{k}$,  i.e., $u_k/U_k$ contains  at least  one  $\reg$-needed  step.
Hence  $P/u$ is $\reg$-quasi-needed.
%By \Lr{L.4.4.}, $NE_\reg [K(P/u)]$ is an infinite $\reg$-needed reduction.
\end{altpr}
}
\end{lem}



\begin{thm}\em
\label{T.4.2.}
{\bf (Relative Hypernormalization)} Let $\reg$ be a regular stable set of
terms in a stable DRS $R$, and let $t\not\in \reg$ be a term in $R$. Then

(1) $t$ contains at least one $\reg$-needed redex.

(2) $t$ has an $\reg$-normal form  iff it does not possess a reduction in
which infinitely many times $\reg$-needed redexes are contracted.

\begin{pruuf}
(1) By \Dr{D.rel.need.} if $t$ is not $\reg$-normalizing, and by
\delete{\Cr{T.4.1.}} \Lr{L.4.4.} otherwise. (2) ($\Rightarrow$) Let
$t\dored{P}s\in \reg$. Suppose on the contrary that there is an
$\reg$-quasi-needed $Q$ starting from $t$. Then by \Lr{L.4.5.} $Q/P$ is
$\reg$-quasi-needed as well -- a contradiction, since all terms of $Q/P$
are in $\reg$, by the closure of $\reg$ under reduction, and therefore
$Q/P$ must be $\reg$-unneeded. ($\Leftarrow$) By (1), one can repeatedly
contract $\reg$-needed redexes in $t$, unless a term in $\reg$ is reached;
the latter is inevitable since $t$ doesn't have an infinite $\reg$-needed
reduction.
\end{pruuf}
\end{thm}

%


 
\begin{rem}\em
\label{R.irreg.no.hyper.}
If $\stab$ is not regular, then \Lr{L.4.4.} doesn't  hold. Indeed, consider
the example from~\cite{[ctrs]}: take OTRS $R=\{f(x)\ar h(f(x),f(x)),\,a\ar
b\}$ and take for $\stab$ the set of terms not containing occurrences of
$a$. It is easy to check that $\stab$ is stable, but is not regular, since
the outermost redex in $t=f(a)$ is $\stab$-unneeded, while the innermost
one is $\stab$-needed. Then $P:f(a)\ar h(f(a),f(a))\ar  h(f(b),f(a))\ar
h(f(b),h(f(a),f(a)))\ar  h(f(b),h(f(b),f(a)))\ar\ldots$ is
$\stab$-quasi-needed, while the $\stab$-needed part $Q:f(a)\ar f(b)$ of
$K(P)$ is $\stab$-normalizing, and $P/Q=f(b)\ar h(f(b),f(b))\ar
h(f(b),h(f(b),f(b)))\ar\ldots$ is $\stab$-unneeded, thus not
$\stab$-quasi-needed any more. Because of that, the proof of \Lr{L.4.5.}
fails, and the $\stab$-needed strategy need not be hypernormalizing.
\end{rem}







\section{Relative Normalization in Deterministic Family Structures}
\label{S.rn.fs.}


In order to generalize the \rn\ theorem to all stable sets in DRSs, we
introduce {\em Family structures\/} (FSs) by defining a notion of {\em
family\/} in a DRS, and by imposing some axioms on the {\em contribution\/}
relation on families. This enables us to repeat the proof of the \rn\
theorem in~\cite{[ctrs]} for all DFSs, and makes explicit the properties of
family relation needed to develop an abstract theory of optimal
normalization.



\bdl{D.DRS.}
{\bf (Deterministic Family Structure)}  A {\em Deterministic Family Structure}
(DFS for short) is a
triple ${\cal F} =(R,\fami,\contr)$, where $R$ is a DRS;  $\fami$ is an
equivalence  relation on redexes with {\em histories}; and $\contr$ is the
{\em 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$ {\em with history} $Q$) is called a {\em copy} of
a redex $Pu$ if $P\lleq Q$, i.e.,  $P+Q/P\leeqv Q$, and $v$ is a
$Q/P$-residual of $u$; the {\em zig-zag} relation $\zfami$ is the symmetric
and transitive closure of the copy relation~\cite{[le80]}. The {\em family}
relation $\fami$ is an equivalence relation among redexes with histories
containing $\zfami$. A {\em 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:

$\bullet$ [initial] Let $u,v\subt t$ and $u\not= v$, in $R$.
Then $Fam(\emptyset_t u) \not=Fam(\emptyset_t v)$.

$\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$ [termination] Any reduction that contracts redexes of a finite
number of families is terminating.

\suppress{\noindent (One might prefer to consider [contribution] as the
definition of
$\contr$ rather than as axiom.)}
\ed


 One can check that all the existing definitions of family relation in the
literature~\cite{[levy],[K.S.],[Mar],[AL]} satisfy the above axioms. Hence
our definition is consistent. The reason for considering more notions of
family than just the zig-zag is that we want to be more flexible and able
to consider a large class of sharing mechanisms as legal; there are sharing
mechanisms that are strictly larger than zig-zag, e.g., the one
in~\cite{[AL]}.  


Let us call $Cone(\phi)=\{\phi_i\,\,\vert\,\,\phi_i\contr \phi\}$ the  {\em
cone} of $\phi$.


\bpl{P.fam.prop.}
In any DFS ${\cal F}$:

$\bullet$ [irreflexivity] $\phi\not\contr \phi$.

$\bullet$ [transitivity] If $\phi\contr \phi'$ and $\phi'\contr \phi''$,
then $\phi\contr \phi''$.

$\bullet$ [cone] $\phi\contr\psi\Rightarrow Cone(\phi)\subset Cone(\psi)$
(i.e.,  $Cone(\phi)\subseteq Cone(\psi)$ and $Cone(\phi)\not= Cone(\psi)$).

$\bullet$ [finiteness] For any $\phi$, $Cone(\phi)$ is finite, and
$Cone(\emptyset_t u)=\emptyset$ for any $u\subt t$.

$\bullet$ [antisymmetry] If $Cone(\phi)= Cone(\psi)$ and $\phi\not=\psi$,
then $\phi\not\contr \psi$ (and $\psi\not\contr \phi$).

\bproof
[irreflexivity], [transitivity], and [finiteness] follow immediately from
[contribution].  [cone] follows from [irreflexivity] and [transitivity].
[antisymmetry] follows from [cone].
\eproof
\ep


The following example shows that, in a DRS with $\fami$ and
$\contr$, [initial], [creation] and [contribution] do not imply  [termination].


\begin{ex}\em
\label{E.sta.no.fa.st.}
 Consider the ARS $R$ given by the Figure~\ref{non-hyper},
where the redex $x$ creates $u$ and $v$; $u_1$ and $u'_{2a}$ create $w$;
$v/u=v'$; $u/v=\{u_1,u_2\}$; $u_1/u_2=u'_1$, $u_2/u_1=u'_2$;
$u'_2/w=\{u'_{2a},u'_{2b}\}$; $w/u'_2=\emptyset$,
$u'_{2a}/u'_{2b}=\emptyset$, $u'_{2b}/u'_{2a}=u'_2$. All the $u$s are
residuals of $u$, hence belong to the same family $U$. Similarly, $v$ and
$v'$ must be in the same family too, say $V$. Further, take $X=\{x\}$, take for
$W$ the set of all contracted $w$s (with histories), and define the contribution
relation on $X,U, V,W$ by $X\contr V,U$ and $U\contr W$. Since the only
infinite reduction goes through the cycle infinitely many times, and each
time the contracted $w$ is {\em created\/} by $u'_{2a}$, all developments
in the figure are terminating.
It remains to note that [FD] and the other family axioms but [termination]
 are satisfied too. Note that the DRS $R$ is stable.
\delete{
Further, the only other possible family relation on $R$ is the one that
merges the families $U$ and $V$ into one family, but [termination] is still
not valid. Thus $R$ cannot be turned into a DFS.
}
\begin{figure}
\begin{diagram}[height=1.6em,width=1.6em]
& \rTo^x & \cdot  & & \rTo^v     &              & \cdot &              & \\
&        &        & &            & \ldTo_{u_2}  &       & \rdTo_{u_1}  & \\
&        & \dTo^u & & \cdot      &              &       &              &
\cdot & \pile{\rTo^w \\ \lTo_{u_{2a}'}} &             & \cdot \\
&        &        & &            & \rdTo^{u_1'} &       & \ldTo^{u_2'} &
&         & \ldTo_{u_{2b}'} \\
&        & \cdot  & & \rTo_{v'} &              & \cdot &              &
\pile{\rTo^{\emptyset} \\ \lTo_{\emptyset}}  & \cdot \\
\end{diagram}
\caption{Independence of the axiom [termination]}\label{non-hyper}
\end{figure}
\end{ex}


\bll{L.drs.stab.pdrs.}
Any DFS ${\cal F}$ is a stable DRS.

\bproof
We want to show that if $u,v\subt t$ are different redexes, $t\red{u}e$,
$t\red{v}s$, $e\dored{v/u}o$, and $u$ creates a redex $w\subt e$, then the
redexes in $w/(v/u)\subt o$ are not $u/v$-residuals of redexes of $s$.
\delete{(see Figure~\ref{elem-diag})} By axioms [creation] and
[contribution], for any redex $w'\subt s$, $Cone(Fam(w'))=\emptyset$ if
$w'$ is not a new redex, and $Cone(Fam(w'))=\{Fam(v)\}$ otherwise; and
$Cone(Fam(w))=\{Fam(u)\}$. Hence the redexes in $w/(v/u)$ and $s$ are in
different families by [initial], and the lemma follows (since
$\zfami\ssq\fami$).
\eproof
\el

\delete{
The following example shows that a DFS not satisfying [initial] need
not be stable.
}

The following example shows that a DRS with $\fami$ and $\contr$ relations
satisfying all DFS axioms but [initial]  need
not be stable.

\begin{ex}\em
\label{E.fs.no.sta.}
Consider the DRS $R$ given by the Figure~\ref{F.stab.init.}, where $w$ and $w'$
are created by $u$ and $v$, respectively, $u/v=u'$, $v/u=v'$,
$w/v'=w'/u'=w^*$. Then the sets $U=\{u,u',v,v'\}$ and $W=\{w,w',w^*\}$ with
the contribution relation $U\contr W$ do satisfy the DFS axioms except for
[initial], but the underlying
DRS $R$ is not stable.

\begin{figure}
\begin{diagram}[height=1.6em,width=1.6em]
 t      & \rTo^u       & e             & \rTo^w           & o^*  \\
 \dTo^v &              &  \dTo_{v'}  &                 & \dOnto^{\emptyset}\\
s       & \rTo_{u'} & o              &                  &    \\
\dTo^{w'}  &            &                &  \rdOnto_{w^*}  &   \\
o^*     & \rOnto^{\emptyset} &            &                   &  o^*  \\
\end{diagram}
\caption{Berry-stability and the Property [initial]}\label{F.stab.init.}
\end{figure}
\end{ex}





\begin{lem}\em
\label{L.4.1.c.}
Let $\stab$ be stable, $t\not\in \stab$, $t\red{u}t'$, $UN_\stab (u,t)$,
and let $u'\subt t'$ be a $u$-new redex, in a DFS ${\cal F}$. Then
$UN_\stab (u',t')$.

\begin{pruuf}
By \Lr{L.4.1.c.stab.}  and \Lr{L.drs.stab.pdrs.}.
\end{pruuf}
\end{lem}



Now we can generalize the RN theorem, proved in~\cite{[ctrs]} for
orthogonal ERSs \cite{[OCRS]}, to all DFSs. We now allow for arbitrary
stable sets $\stab$.

Below $FAM(P)$ denotes the set of families (whose member redexes are)
contracted in $P$.

\begin{thm}\em
\label{T.ex.M-need.}
{\bf (Relative Normalization)} Let $\stab$ be a stable set of terms in
a Deterministic Family Structure~$\cal F$.

(1) Any $\stab$-normalizable term $t$ in $\cal F$ not in $\stab$-normal form
contains an $\stab$-needed redex.

(2) If $t$ is $\stab$-normalizable, then any $\stab$-needed reduction
starting from $t$ eventually terminates at a term in $\stab$.

\begin{pruuf}
(1) Let $P:t\doar s'\ar s\red{u}e$ be an $\stab$-normalizing reduction with
$s\not\in \stab$. By the stability of $\stab$, $u$ is $\stab$-needed. By
Corollary~\ref{T.3.1.c.} and Lemma~\ref{L.4.1.c.}, it is either created by
or is a residual of an $\stab$-needed redex of $s'$, and (1) follows by
repeating the argument.

(2) Let $P:t\doar s$ be an $\stab$-normalizing reduction and
$Q:t\red{u_0}t_1\red{u_1}\ldots$ be an $\stab$-needed reduction. Further,
let $Q_i:t\red{u_0}t_1\red{u_1}\ldots\red{u_{i-1}}t_i$ and $P_i=P/Q_i$
$(i\geq 1)$ \suppress{(see Figure~\ref{term-need})}. By $\zfami\ssq\fami$,
$FAM(P_i)\ssq FAM(P)$. Since $Q$ is $\stab$-needed and $P_i$ is
$\stab$-normalizing (by the closure of $\stab$ under parallel moves), at
least one residual of $u_i$ is contracted in $P_i$. Therefore, again by
$\zfami\ssq\fami$, $Fam(u_i)\in FAM(P_i)$. Hence $FAM(Q)\ssq FAM(P)$ and
$Q$ is terminating by \delete{\Pr{P.BCT.}.(1).} [termination].

\begin{figure}
\begin{diagram}[height=1.5em,width=4em]
  t            & \rOnto^{P}   &   s     \\
 \dOnto^{Q_i}   &              &     \dOnto \\
 t_i           & \rOnto_{P_i}&  {}          \\
\dTo^{u_i}     &              &     \dOnto \\
t_{i+1}        & \rOnto_{P_{i+1}}&  {}    \\
\dOnto          &              &     \dOnto \\
 {}          & \rOnto       &  {}         \\
\end{diagram}
\suppress{\caption{Termination of Needed Reduction}\label{term-need}}
\end{figure}
\end{pruuf}
\end{thm}


\zurab{
Note that we haven't used the acyclicity axiom in the proofs. However, it is
necessary and sufficient to insure that the set of normal forms is stable. Note
also that only by using \Tr{T.ex.M-need.} can we prove the analogue of
\Lr{L.pers.need.} for all stable~$\stab$.
}


\delete{
\begin{rem}\em
Note that only by using \Tr{T.ex.M-need.} can we prove the analogue of
\Lr{L.pers.need.} for all stable~$\stab$.
\end{rem}

\begin{lem}\em
\label{L.3.3.c.}
 Let $\stab$ be a stable set of terms in a DFS ${\cal F}$, and let
$t\red{u}s$. Then any $\stab$-needed redex $v\subt t$ different from $u$
has an $\stab$-needed residual in~$s$.

\begin{pruuf}
Same as the proof of \Lr{L.pers.need.}, but using \Tr{T.ex.M-need.} instead
of \delete{\Cr{T.4.1.}} \Lr{L.4.4.}.
\end{pruuf}
\end{lem}
}



\section{The Relative Optimality Theorem}
\label{S.opt.fs.}


In this section, we define {\em weakly $\stab$-needed\/} redexes, and show
that their contraction in an $\stab$-normalizable term $t$ leads to an
$\stab$-normal form of $t$. \delete{This generalizes the result of
L\'evy~\cite{[le80]} stating that needed family-reduction is normalizing,
and is useful for strictness analysis.} We also generalize L\'evy's
Optimality theorem~\cite{[le80]} to all stable sets $\stab$ in any DFS.


\bd
We call a family $\phi$ relative to $t$ {\em $\stab$-needed\/} if any
reduction from $t$ to a term in $\stab$ contracts at least one member of
$\phi$. We call redexes in $\stab$-needed families {\em weakly
$\stab$-needed}.

\ed


\delete{
\begin{deff}\em
\label{D.weak.need.}
Let $P:t\red{u_0}t_1\red{u_1}t_1\ldots\red{u_{n-1}}t_n$ in an
FS ${\cal F}$, and let $\stab$ be a set of terms of $R$. We call $u\in
t_i$ {\em weakly $\stab$-needed w.r.t. $t\red{u_0}t_1\red{u_1}t_1\ldots\ar
t_i$} if $u$ is in the family of an $\stab$-needed redex occurring in some
$t_j$. A reduction is {\em weakly $\stab$-needed} if each redex
contracted in it is (w.r.t. the initial reduction).
\end{deff}
}


\begin{thm}\em
\label{T.cor.weak.need.}
Let $\stab$ be a stable set of terms in a Deterministic Family 
Structure ${\cal F}$, and $t$ be an
$\stab$-normalizable term in $\cal F$. Then any weakly $\stab$-needed
reduction starting from $t$ is terminating.

\begin{pruuf}
By [termination], since there is only a finite number of $\stab$-needed
families relative to $t$ (the number doesn't exceed the length of any
$\stab$-normalizing reduction starting from $t$).
\end{pruuf}
\end{thm}

The above theorem allows one to propagate
$\stab$-neededness information, obtained from earlier terms, along the
reduction, and to contract safely (without a danger of missing an
$\stab$-normal form whenever it exists) any residual of an $\stab$-needed
redex, even if it is no longer $\stab$-needed.



\begin{deff}\em
A multistep reduction $P:t_0\doar t_1\doar\ldots\doar t_n$ is
called a {\em family-reduction} if each $P_i:t_i\doar t_{i+1}$ is
a development of a set $U_i$ of redexes belonging to the same
family. $\Vert P\Vert$ will denote the number of multisteps in
$P$. The family-reduction $P$ is {\em complete} if each $P_i$ is
the complete development of a maximal set of redexes of $t_i$
belonging to the same family. A family-reduction $P$ is called
{\em $\stab$-needed\/} if each $U_i$ contains at least one $\stab$-needed
redex (i.e., if the (single-step) reduction corresponding to  $P$
is weakly $\stab$-needed).

\end{deff}


\begin{cor}\em
Let $\stab$ be a stable set of terms in a DFS ${\cal F}$, and
$t$ be an
$\stab$-normalizable term in $\cal F$. Then any  $\stab$-needed
family-reduction staring from $t$ is eventually $\stab$-normalizing.
\end{cor}



\begin{lem}\em
\label{L.fam.compl.}
Every family is contracted at most once in any complete
family-reduction.

\begin{pruuf}
Let $P_n:t_0\dored{U_0}t_1\dored{U_1}\ldots \dored{U_{n-1}}t_n$
be a complete family-reduction. We show by induction on $n=\Vert
P\Vert$ that $(a)_n$: all families contracted in $P_n$ are
different; and $(b)_n$: there is no redex in $t_n$ whose family
has been contracted in $P_n$.  The
case $n=0$ is clear. Further, $(a)_n$ follows immediately from
$(a)_{n-1}$ and $(b)_{n-1}$. Again by $(a)_{n-1}$ and
$(b)_{n-1}$, and by the completeness of $P_n$, all redexes in $t_n$ that
are residuals of redexes of $t_{n-1}$ are in families that have not been
contracted
before. By [creation], for the family $\phi$ of a new redex in $t_n$, we
have $Fam(U_{n-1})\contr \phi$; by $(a)_{n-1}$, $(b)_{n-1}$, and
[contribution], $Fam(U_{n-1})\not\contr Fam(U_i)$, for any $i\leq n-1$.
Hence $Cone(Fam(U_i))\not=Cone(\phi)$, and $(b)_n$ follows.
\end{pruuf}
\end{lem}




\begin{thm}\em
\label{T.unif.opt.}
{\bf (Relative Optimality)}
Let $\stab$ be a stable set of terms in a Deterministic Family Structure ${\cal
F}$,
and $t$ be an
$\stab$-normalizable term in $\cal F$. Then any  $\stab$-needed
$\stab$-normalizing complete family-reduction $Q:t\doar e\in\stab$ is
$\stab$-optimal in the sense that it has a minimal number of
family-reduction steps.

\begin{pruuf}
Similar to the case of the
$\lambda$-calculus~\cite{[le80]}. Let $P:t\doar s$ be an
$\stab$-normalizing family-reduction. It follows from the proof
of Theorem~\ref{T.ex.M-need.} that $FAM(Q)\subseteq FAM(P)$ \suppress{(see
Figure~\ref{term-need})}.
Hence, by Lemma~\ref{L.fam.compl.}, $\Vert
Q\Vert=Card(FAM(Q))\leq Card(FAM(P))\leq\Vert P\Vert$, where
$Card(FAM(Q))$ denotes the number of families in $FAM(Q)$.
\end{pruuf}
\end{thm}



\section{Relative Normalization in Event Structures}
\label{S.norm.es.}



In this section, we give an {\em Event Structure\/} semantics to DFSs.
Smoothness of the interpretation justifies our choice of family axioms. We
also generalize the RN theorems to ESs by giving the reverse translation.
To this end, we equip ESs with an extra operation $\rhd$ expressing {\em
redundancy} of events, thereby enhancing the match between DFSs and
corresponding ESs.

Recall that an {\em Event Structure} (ES)~\cite{[Win]} is a triple ${\cal
E}=(E, Con, \vdash)$, where $E$ is a set of {\em events}, ranged over by
$e, e_1,\ldots$; the {\em consistency predicate} $Con$ is a non-empty set
of subsets of $E$, denoted by $X, Y, \ldots$; and $\vdash\,\,\ssq Con\times E$
is the {\em enabling} relation, such that $Y\ssq X\in Con \Rightarrow Y\in
Con$ and $X\vdash e \wedge X\ssq Y\in Con\Rightarrow Y\vdash e$.  We call
an ES {\em deterministic\/} (DES) if its consistency predicate is the
powerset of $E$. Below we only consider deterministic ESs, therefore will
omit reference to the consistency predicate $Con$. In a DES, a {\em
configuration} $\alpha$ is a subset of $E$ such that, for any
$e\in \alpha$, there are $e_1,\ldots,e_n=e$ such that
$\{e_0,\ldots,e_{i-1}\}  \vdash e_i$, for all $i\leq n$~\cite{[Win]}.
A DES is {\em
stable\/} if $X\vdash e\,\,\wedge\,\, Y\vdash e\Rightarrow X\cap Y \vdash
e$~\cite{[Win]}.

\bd
To a DFS ${\cal F}_t=(R_t,\fami,\contr)$, where $R_t$ is a (sub)DRS whose
term domain is the graph of a term $t$ (i.e., the set of terms to which $t$
is reducible), we associate the DES ${\cal E}_{{\cal F}_t}=(E_{{\cal F}_t},
\vdash_t)$,  where

$\bullet$ $E_{{\cal F}_t}=FAM(t)$, the set of all families $\phi$ of ${\cal
F}_t$ relative to $t$; and

$\bullet$ $X\vdash_t \phi$ iff $X\ssq FAM(t)$ and there is a complete
family-reduction $P:t\doar s$ with $FAM(P)\ssq X$ such that $s$ contains a
member of $\phi$.
\ed



\bl
 For any complete family-reduction $P:t\doar s$ with $FAM(P)=Cone(\phi)$,
in the DFS ${\cal F}_t$ defined above, $s$ contains a member of
$\phi$. Thus $Cone(\phi)$ is the smallest set enabling $\phi$.

\bproof
Let $Qu\in\phi$, $Q$ a complete family-reduction. By [contribution],
$FAM(P)\ssq FAM(Q)$, hence $P\lleq Q$. Thus $Q\leeqv P+V_1+\ldots+V_m$.
\zurab{If $P$ doesn't contain members of $\phi$, then there is  $i$ such that
$V_i$ creates a member of $\phi$.} Thus, by
[creation], $FAM(V_i)\in Cone(\phi)=FAM(P)$ -- a contradiction, since
$P+V_1+\ldots+V_m$ cannot contract members of $\phi$ more than once, by
\Lr{L.fam.compl.}.
\eproof
\el


\bc
For any DFS ${\cal F}_t$, the DES ${\cal E}_{{\cal F}_t}=(FAM(t), \vdash_t)$
is stable.
\ec




A {\em prime\/} DES~\cite{[Win]} is a couple ${\cal E}^{\leq}=(E, \leq)$, where
the {\em causal dependency relation} $\leq$ is a partial order on $E$, such
that  $\{e'\,\vert\, e'\leq e\}$ is finite for any $e\in E$. {\em
Configurations\/} of ${\cal E}^{\leq}$ are {\em left-closed subsets\/}
$\alpha,\beta,\ldots$ of $E$, i.e., subsets $\{\alpha\ssq E\,\vert\, e\in E
\,\wedge\, e'< e\Rightarrow e'\in\alpha\}$. As pointed out
in~\cite{[Win]}, every stable DES $\cal E$ can be turned into
a prime DES ${\cal E}^{\ssq}$ by taking configurations of $\cal E$ as
events of ${\cal E}^{\ssq}$ and by taking $\ssq$ as the causal dependency
relation. It follows from \Pr{P.fam.prop.} that ${\cal E}^{\leq}_{{\cal
F}_t}=(FAM(t),\contr^=)$ is a prime DRS with an isomorphic domain of
configurations:

\delete{a
standard procedure, application of which to ${\cal E}_{{\cal F}_t}$
produces the prime DES ${\cal E}^{\ssq}_{{\cal F}_t}=(Cone(FAM(t)), \ssq)$,
where $Cone(FAM(t))$ is the set of cones of families in $FAM(t)$.}


\bt
For any DFS ${\cal F}_t$, ${\cal E}^{\leq}_{{\cal F}_t}=(FAM(t),\contr^=)$
is a prime DES.
\et



\bd
Let ${\cal E}=(E,\leq)$ be a prime DES with an extra relation $\rhd\ssq
FConf(\cal E) \times E$, where $FConf(\cal E)$ is the set of finite
configurations of $\cal E$, satisfying the following axiom:

\delete{
$\bullet$ $\alpha\rhd e\Rightarrow \alpha\cup\{e\}\in FConf(\cal E)$;
}

$\bullet$   $\alpha\rhd e\,\wedge\,\alpha\ssq \beta\, \in FConf({\cal E})
\,\Rightarrow \beta\rhd e$;


\delete{
$\bullet$  $\alpha\rhd e\,\wedge\,e'< e\,\Rightarrow\, \alpha\,\rhd\, e'$;

$\bullet$  $\alpha\rhd e\,\wedge\,\beta\rhd e \Rightarrow\alpha\cap\beta\rhd e$.


$\bullet$  $\alpha\rhd e \Rightarrow \exists \alpha_e\in FConf({\cal
E}).\,\, \alpha_e \rhd e\,\wedge\,(\beta\rhd e \Rightarrow \alpha_e \ssq
\beta)$
}

\noindent Then we call ${\cal C}=({\cal E}, \rhd)$ a {\em Deterministic
Computation Structure\/} (DCS). We read $\alpha\,\rhd\, e$ as: `$e$ is {\em
$\alpha$-inessential}'. On $FConf({\cal C})=FConf({\cal E})$, we define
L\'evy-equivalence as follows:

\delete{
$\bullet$ $\alpha\leeqv \beta$ iff $\forall e\in \alpha\backslash \beta
\cup \beta\backslash \alpha.\,\,\,\, \alpha\cap \beta\rhd e$.
}

$\bullet$ $\alpha\leeqv \beta$ iff $SE(\alpha)=SE(\beta)$, where
$SE(\alpha)=\{e\in\alpha\,\,\vert\,\,\alpha\not\rhd e\}$ is the set of {\em
self-essential\/} events of $\alpha$.

\ed



\delete{The $\rhd$-axioms imply that $\leeqv$ is indeed an equivalence
relation.}
In ${\cal E}_{{\cal F}_t}$, let the configurations be sets
$FAM(Q)$ of
complete family-reductions $Q$;
and define $FAM(Q)\rhd_t\phi$ iff there is a (finite) complete family-reduction
$P\leeqv Q$  with $\phi\not\in FAM(P)$. Then $\rhd_t$ satisfies the above
$\rhd$-axiom. So we can actually speak
of translation of  ${\cal F}_t$ into a DCS ${\cal C}_{{\cal F}_t}=({\cal
E}_{{\cal F}_t}, \rhd_t)$.



\begin{rem}\em
One can show \zurab{using acyclicity} further that for finite complete-family
reductions $P$ and $Q$, $P\leeqv Q$ iff $SE(FAM(P))=SE(FAM(Q))$.
\end{rem}


\bd
To a DCS ${\cal C}=({\cal E}, \rhd)$, we associate a DRS $R_{\cal
C}$ as follows:


$\bullet$ The terms of $R_{\cal C}$ are
L\'evy-equivalence classes $\lclas{\alpha},\lclas{\beta},\ldots$ of finite
configurations of ${\cal C}$;

$\bullet$ The reduction relation of $R_{\cal C}$ consists of sets of pairs of
terms
$u=(\lclas{\alpha},\lclas{\beta})$,
where $\beta=\alpha\cup\{e\}$;  (Note that $\lclas{\alpha}=\lclas{\beta}$
iff $\beta\rhd e$.)

$\bullet$ The residual relation is defined as follows: if
$u=(\lclas{\alpha},\lclas{\alpha\cup\{e\}})$ and
$v=(\lclas{\alpha},\lclas{\alpha\cup\{e'\}})$, then
$u/v=(\lclas{\alpha\cup\{e'\}},\lclas{\alpha\cup\{e',e\}})$. (Thus
$u/v=\emptyset$ iff
$\lclas{\alpha\cup\{e'\}}\leeqv\lclas{\alpha\cup\{e',e\}}$.)
\ed


Note that Stark's encoding of ESs into CTSs~\cite{[Sta]} (which are DRSs as
well) would (or at least
may) interpret configurations that are different as sets (but may be the
same semantically) as different states. For example, consider the ES,
corresponding to the rewrite system $\{f(x)\ar c,\, a\ar b\}$ with the
graph of $t=f(a)$ as the set of terms, whose events are $t\red{a}f(b)$ and
$t\red{f(a)} c$ (the steps $f(b)\red{f(b)}c$ and $t\red{f(a)} c$ represent
the same event); and whose configurations are $\alpha=\{f(a)\}$,
$\beta=\{a\}$, and $\gamma=\{a, f(a)\}$. Then Stark's encoding would
consider $\alpha$, $\beta$ and $\gamma$ as different configurations, while
we can identify $\alpha$ with $\gamma$, which is more natural if the
information that $\alpha\rhd a$ is provided.

\delete{Using the $\rhd$-axioms,} One can easily verify that $R_{{\cal C}}$ is
indeed a DRS.  The translation of DCSs into DRSs enables us to extend
the theory of relative normalization from DRSs to DCSs, and  in particular,
to DESs (since DESs are DCSs with the empty $\rhd$ relation).

\bt
Let $\stab$ be a stable set of configurations in a Deterministic
Computation Structure.
Then execution of $\stab$-needed events leads to configurations in
$\stab$, even if a finite number of $\stab$-unneeded events are executed as
well.
\et


\section{Conclusions and future work}
\label{S.concl.}



We have proven two abstract versions of the \rn\ theorem: one in DRSs for
regular stable sets $\reg$, and another in DFSs for all stable $\stab$, and
extended it to deterministic Event Structures. We believe that our
first proof is the simplest existing proof among those that use the notion
of residual, though it covers all the existing normalization results,
except for the one in~\cite{[ctrs]}, which is covered by our second RN
theorem. It is remarkable that, unlike the proofs in
~\cite{[C.F.],[H.L.],[B.K.K.S.]}, our proof doesn't use the notion of standard
reduction. Similar proofs for
orthogonal CRSs in~\cite{[K.S.]} and for orthogonal DAGs
in~\cite{[Mar91],[Mar]} use an even stronger termination argument, expressed by
[termination] axiom; they
used suitable labelling systems to define notions of family.
Our second proof can be seen as a generalization of that proof method,
which was used already by L\'evy in~\cite{[levy],[le80]}. It would be
interesting to investigate whether it is possible to prove our second theorem
already for stable DRSs, i.e., without family axioms, but possibly some much
weaker axioms.

 
\delete{
The proofs of the normalization of the needed (essential) strategy
in~\cite{[colog],[rta]} do not use the Standardization theorem either, but
they are based on the notion of {\em descendant of subterms} rather than
that of residual of redexes, which is a very syntactic notion, therefore
much more difficult to axiomatize. The proofs of the normalization of
needed strategy for orthogonal CRSs by Kennaway and Sleep~\cite{[K.S.]} and
for orthogonal DAG rewriting by Maranget~\cite{[Mar91],[Mar]} use an even
stronger termination argument -- termination of developments of any finite
set of co-initial families. They both used suitable labelling systems to
define notions of family. Our second proof can be seen as a generalization
of that proof method, which was used already by L\'evy
in~\cite{[levy],[le80]}. Our first theorem covers both above results and
our proof is much simpler because it doesn't use any notion of family.
}

Obviously, our family axioms are too weak to prove certain properties of
families
which arise from using labelling notions, and studying its
refinements certainly seems useful. Nevertheless, our axioms are powerful enough
to build the normalization and optimality theory, and to bridge DRSs with
Event Structures (thereby defining a denotational semantics for DRSs). Indeed,
in DFSs it is possible to do much more --
e.g., study {\em infinitary} normalization, define the notion of {\em
independence\/} of computations, and turn L\'evy's reduction space into a
{\em Vector Space}, etc. This is the subject of forthcoming papers. Some
extra axioms on duplication behaviour are needed, but no nesting relation
is necessary, so many machine models are still covered.

\delete{
An interesting question is whether our second theorem can also be proved
for stable DRSs, i.e., without family axioms, but some much weaker axioms.
One way to do this is to guarantee the axiom [termination], and to show
that, if in an SDRS one defines the contribution relation according to
[contribution], then [creation] is satisfied if the zig-zag is taken for
the family relation. However, this is non-trivial, and is left for a future
research.
}

\vspace{0.20cm}

%\section*{Acknowledgements}

\begin{akn}
We thank  J.~R.~Kennaway, J.-J.~L\'evy, L.~Maranget, V.~van Oostrom, and
M.~R.~Sleep for useful comments.
\end{akn}



\begin{thebibliography}{AFMOW94}

\delete{
\bibitem{[Acz]}
 Aczel P. A general Church-Rosser theorem. Preprint, University of
Manchester, 1978.
}


\bibitem[{AEH94}]{[Ant]} Antoy S., Echahed R., Hanus M. A needed narrowing
strategy. In: Proc. of the $21^{st}$ ACM Symposium on Principles of
Programming Languages, POPL'94, Portland, Oregon, 1994.


\bibitem[{AnMi94}]{[AnMi]} Antoy S. and Middeldorp A.
A Sequential Reduction Strategy. In  Proc.
of the $4^{th}$ International Conference on Algebraic and Logic
Programming, ALP'94, Madrid, Springer LNCS. vol. 850, p.~168-185, 1994.


\bibitem[{AFMOW94}]{[A.F.]}
 Ariola Z.M., Felleisen M., Maraist J., Odersky M., Wadler P.
 A Call-By-Need Lambda Calculus.
 In: Proc.\ ACM Conference on Principles of Programming Languages, 1995.

\bibitem[{AsLa93}]{[AL]} Asperti A., Laneve C. Interaction Systems I: The
theory of optimal reductions.  Mathematical Structures in Computer Science,
vol.~11, Cambridge University Press, 1993, p.~1-48.


\bibitem[{Bar84}]{[Bar]}
Barendregt H. P. The Lambda Calculus, its Syntax and Semantics.
North-Holland, 1984.


\bibitem[{BKKS87}]{[B.K.K.S.]}
Barendregt H. P., Kennaway J. R., Klop J. W., Sleep M. R. Needed
Reduction and spine strategies for the lambda calculus.
Information  and Computation, v.~75, no.~3, 1987, p.~191-231.


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


\bibitem[{CuFe58}]{[C.F.]}
Curry H.~B., Feys R. Combinatory Logic. vol.~1, North-Holland, 1958.

\delete{
\bibitem[{DeJo90}]{[D.J.]}
Dershowitz  N.,  Jouannaud  J.-P.  Rewrite Systems. In: J. van
Leeuwen  ed. Handbook of  Theoretical Computer Science, Chapter~6, vol.~B,
1990, p.~243-320.
}

\bibitem[{Gar94}]{[Gar]} 
Gardner P. Discovering needed reductions using
type theory.  In: Proc. of the $2^{nd}$ International Symposium on
Theoretical Aspects of Computer Software, TACS'94,  Springer LNCS, v.~789,
M.~Hagiya, J.~C.~Mitchell, eds. Sendai, 1994, p.~555-574.

\bibitem[{GlKh94}]{[ctrs]}
Glauert J.R.W., Khasidashvili Z.  Relative Normalization in
Orthogonal Expression Reduction Systems. In: Proc. of the
$4^{th}$ International workshop on Conditional (and Typed) Term
Rewriting Systems, CTRS'94, Springer LNCS, vol.~968, N.~Dershowitz, ed.
Jerusalem, 1994, p.~144-165.  


\bibitem[{GLM92}]{[GLM]}
Gonthier G., L\'evy J.-J., Melli\`es P.-A. An abstract Standardisation
theorem. In: Proc. of the $7^{th}$ Annual IEEE Symposium on Logic in
Computer Science, LICS'92, Santa Cruz, California, IEEE Computer Society
Press, 1992, p.~72-81.


\bibitem[{HuL\'e91}]{[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. MIT Press, 1991.


\bibitem[{Ken89}]{[Kenn]}
Kennaway  J.R.  Sequential   evaluation  strategy  for
parallel-or and related reduction systems. Annals of Pure and
Applied Logic 43, 1989, p.31-56.


\bibitem[{KeSl89}]{[K.S.]}
Kennaway J. R., Sleep M. R. Neededness is hypernormalizing in  regular
combinatory reduction systems. Preprint, School of Information Systems,
University of East Anglia, 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: M.~R. Sleep, M.~J. Plasmeijer, and
M.~C.~J. D., eds. Term Graph Rewriting: Theory and Practice. John Wiley,
1993.

\bibitem[{KKSV96}]{[K-tra]} 
Kennaway J. R., Klop J. W., Sleep M. R, de Vries F.-J. Transfinite
reductions in orthogonal term graph rewriting. Information and Computation,
To appear.


\bibitem[{Kha88}]{[colog]}
Khasidashvili Z. $\beta$-reductions and $\beta$-developments of
$\lambda$-terms with the least number of steps. In: Proc. of the
International Conference on Computer Logic COLOG'88, Tallinn
1988, Springer LNCS, v.~417, P.~Martin-L\"of and G.~Mints, eds.
1990, p.~105--111.


\bibitem[{Kha92}]{[OCRS]}
Khasidashvili Z. The Church-Rosser theorem in Orthogonal Combinatory
Reduction Systems. Report 1825, INRIA Rocquencourt, 1992.



\bibitem[{Kha93}]{[rta]}
Khasidashvili Z. Optimal normalization in orthogonal term rewriting
systems. In: Proc. of the $5^{th}$ International Conference on Rewriting
Techniques and Applications, RTA'93, Springer LNCS, vol.~690, C. Kirchner,
ed. Montreal, 1993, p.~243-258.

\delete{
\bibitem[{Kha94}]{[caap]}
Khasidashvili Z.  On higher order recursive program schemes.  In:
Proc. of the $19^{th}$ International Colloquium on Trees in
Algebra and Programming, CAAP'94, Springer LNCS, vol.~787, S.
Tison, ed. Edinburgh, 1994, p.~172-186.
}

\bibitem[{Klo80}]{[Kl.CRS]}
Klop J. W.  Combinatory Reduction Systems. Mathematical Centre
Tracts  n. 127,  CWI, Amsterdam, 1980.


\bibitem[{Klo92}]{[Kl.TRS]}
Klop J. W. Term  Rewriting Systems.  In:  S. Abramsky, D. Gabbay,
and T. Maibaum eds.  Handbook  of Logic in Computer Science, vol.
II, Oxford University Press, 1992, p.~1-116.

\delete{
\bibitem[{KOR93}]{[kor]}
 Klop J. W., van Oostrom V., van Raamsdonk F. Combinatory reduction
systems: introduction and survey. In: To Corrado B\"ohm, J. of Theoretical
Computer Science 121, 1993, p.~279-308.
}

\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, Academic Press, 1980,
p.~159-192.


\bibitem[{Mar91}]{[Mar91]}
Maranget L. Optimal derivations in weak $\lambda$-calculi and in orthogonal
Term Rewriting Systems. In: Proc. of the $17^{th}$ ACM Symposium on
Principles of Programming Languages, POPL'91, p.~255-269.


\bibitem[{Mar92}]{[Mar]}
Maranget L.  La strat\'egie paresseuse. Th\`ese de l'Universit\'e
de Paris VII, 1992.

\bibitem[{Nip93}]{[Nip.b]}
 Nipkow T. Orthogonal higher-order rewrite systems are confluent. In: Proc.
of the $1^{st}$ International Conference on Typed Lambda Calculus and
Applications, TLCA'93, Springer LNCS, vol.~664, Bazem M., Groote J.F., eds.
Utrecht, 1993, p.~306-317.



\bibitem[{N\"ok94}]{[Nok.thi.]}
N\"ocker E. Efficient Functional Programming. Compilation and
Programming Techniques. Ph.D. Thesis, Catholic University of
Nijmegen, 1994.


\bibitem[{Oos94}]{[Oos.th]}
 Van Oostrom V. Confluence for Abstract and Higher-Order Rewriting. Ph.D.
Thesis, Free University of Amsterdam,~1994.

\delete{
\bibitem[{OR93}]{[OR93]}
Van Oostrom V., van Raamsdonk F. Comparing Combinatory Reduction Systems
and Higher-Order Rewrite Systems. In: Proc. of the $1^{st}$ International
workshop on Higher-Order Algebra, Logic, and Term Rewriting, HOA'93,
Springer LNCS, vol.~816, Heering J., Meinke K., M\"oller B., Nipkow T.,
eds. Amsterdam, 1993, p.~276-304.
}

\bibitem[{OR94}]{[OR94]}
Van Oostrom V., van Raamsdonk F. Weak orthogonality implies confluence: the
higher-order case. In: Proc. of the $3^{rd}$ International Conference on
Logical Foundations of Computer Science, 
LFCS'94, Springer LNCS, vol.~813, Narode A., Matiyasevich Yu.~V. eds.
St.~Petersburg, 1994. p.~379-392.

\bibitem[{SeRa90}]{[SeRa]} 
Sekar R.C., Ramakrishnan I.V. Programming in Equational Logic: Beyond
Strong Sequentiality. Proc. of the $5^{th}$ IEEE Symposium on Logic in
Computer Science, LICS'95, Philadelphia, 1990. p.~230-242.


\bibitem[{Sta89}]{[Sta]}
Stark E.~W. Concurrent transition systems. Theoretical Computer Science,
vol.~64, 1989, p.~221-270.


\bibitem[{Win80}]{[Win]}
Winskel G. Events in Computation. Ph.D. Thesis, University of Edinburgh, 1980.


\bibitem[{Yos93}]{[Yos]}
Yoshida N. Optimal reduction in weak \lc\ with shared environments. In
Proc. of ACM Conference on Functional Programming Languages and Computer
Architecture, FPCA'93, Copenhagen, 1993, p. 243-252.
\end{thebibliography}
\end{document}
%% End LaTeX Document






