\documentclass{llncs}
\pagestyle{plain}
\usepackage{latexsym}
\usepackage{graphicx}

%\documentclass{article}
%\usepackage{graphicx}

%\input{amssym.def}
%\input{amssym}
%\pagestyle{empty}
%\setlength{\textheight}{8.75in}
%\setlength{\columnsep}{2.0pc}
%\setlength{\textwidth}{6.8in}
%\setlength{\footheight}{0.0in}
%\setlength{\topmargin}{0.25in}
%\setlength{\headheight}{0.0in}
%\setlength{\headsep}{0.0in}
%\setlength{\oddsidemargin}{-.19in}
%\setlength{\parindent}{1pc}
%\makeatletter

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

\begin{document}
%\date{}

%%%%%%%%%%%%%% general macros %%%%%%%%%%%%%


\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{\PTr}[1]{{\bf of Theorem~\ref{#1}:}}
\newcommand{\PPr}[1]{{\bf of Proposition~\ref{#1}:}}
\newcommand{\PCr}[1]{{\bf of Corollary~\ref{#1}:}}
\newcommand{\PLr}[1]{{\bf of Lemma~\ref{#1}:}}



\newcommand{\ben}{\begin{enumerate}}
\newcommand{\een}{\end{enumerate}}
\newcommand{\bit}{\begin{itemize}}
\newcommand{\eit}{\end{itemize}}
\newcommand{\bds}{\begin{description}}
\newcommand{\eds}{\end{description}}


\newcommand{\crl}{\mbox {$\,\ -\kern-0.5em <\ $}}
\newcommand{\ccrl}{\mbox{$\stackrel{c}{\crl}$}}



\newcommand{\zurab}[1]{\{{\bf Zurab: \sf #1}\}} % Highlight text.
\newcommand{\john}[1]{\{{\bf John: \sf #1}\}} % Highlight text.
\newcommand{\delete}[1]{} % Comment out text.
\newcommand{\suppress}[1]{} % Comment out text.
%\newcommand{\suppress}[1]{\{\{{\sf #1}\}\}} % Highlight 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{proof}{{\it Proof:}}{{\it Q.e.d.}}
\newenvironment{akn}{\noindent{\bf Acknowledgments }}{}
\newenvironment{pruuf}{\noindent{\bf Proof }}{}
\newenvironment{poll}[1]{\noindent{\bf Proof of Lemma~\ref{#1}}}{}
\newenvironment{potl}[1]{\noindent{\bf Proof of Theorem~\ref{#1}}}{}
\newenvironment{popl}[1]{\noindent{\bf Proof of Proposition~\ref{#1}}}{}
\newenvironment{pocl}[1]{\noindent{\bf Proof of Corollary~\ref{#1}}}{}

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

%%%%%%%  end of general macros %%%%%%%%%%%%%




\newcommand{\newl}{\mbox{ }\\}
\newcommand{\ar}{\rightarrow}
\newcommand{\undl}{\underline}
\newcommand{\impl}{\Rightarrow}
%\newcommand{\doar}{\twoheadrightarrow}
\newcommand{\doar}{\mbox {$\,\ \rightarrow\kern-0.7em\rightarrow\ $}}
\newcommand{\doarp}{\mbox{$\stackrel{+}{\doar}$}}
\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{\con}[1]{\mbox{$\lceil{#1}^{\leq}\rceil$}}
\newcommand{\coni}[1]{\mbox{$\lceil{#1}^{\geq}\rceil$}}
\newcommand{\ocon}[1]{\mbox{$\lceil{#1}^{<}\rceil$}}
\newcommand{\oconi}[1]{\mbox{$\lceil{#1}^{>}\rceil$}}


\newcommand{\ssq}{\subseteq}
\newcommand{\sset}{\subset}
\newcommand{\sssq}{\subseteq_{\stab}}
\newcommand{\ssset}{\subset_{\stab}}


\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{\ines}[2]{\mbox{$\overbrace{#1}^{#2}$}}
\newcommand{\unin}[2]{\mbox{$\undl{#1}_{#2}$}}
\newcommand{\dist}[2]{\mbox{$\vert{#1},{#2}\vert$}}



%%%%%    new arrows   %%%%%%%%%
%\newarrow{Co}<--->
%\newarrow{Implies}  ===={>>}
%\newarrow{Dashto}   {}{dash}{}{dash}{>>}
%\newarrow{Dotsto}  ....{>>}


\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{\contre}{\underline{\hookrightarrow}}
\newcommand{\zcontr}{\hookrightarrow_z}
\newcommand{\pcontr}{\hookrightarrow_{\cal P}}
\newcommand{\leng}[1]{\mbox{$\vert{#1}\vert$}}

\newcommand{\emb}{\preceq}
\newcommand{\stemb}{\prec}

\newcommand{\calR}{{\cal R}}
\newcommand{\calF}{{\cal F}}


\newcommand{\fcE}{{\cal L}(E)}
\newcommand{\fcC}{{\cal L}({\cal C})}
\newcommand{\fcP}{{\cal L}({\cal P})}
\newcommand{\fcR}{{\cal L}_{fin}({\cal R})}
\newcommand{\cR}{{\cal L}({\cal R})}

\newcommand{\fin}{\in}
%\newcommand{\lleq}{\triangleleft}
%\newcommand{\lles}{\triangleleft}

\newcommand{\leeqv}{\approx_L}
\newcommand{\seqv}{\approx_{\stab}}
\newcommand{\speqv}{\approx_{\stab'}}
\newcommand{\lleq}{\unlhd_L}
\newcommand{\lles}{\lhd_L}
\newcommand{\sleq}{\unlhd_{\stab}}
\newcommand{\sles}{\lhd_{\stab}}
\newcommand{\spleq}{\unlhd_{\stab'}}
\newcommand{\sples}{\lhd_{\stab'}}
\newcommand{\sqleq}{\sqsubseteq}
\newcommand{\sqles}{\sqsubset}

\newcommand{\bleq}{\unlhd_{\stab_{\cal B}}}
\newcommand{\bles}{\lhd_{\stab_{\cal B}}}
\newcommand{\beqv}{\approx_{\stab_{\cal B}}}

\newcommand{\fleq}{\unlhd_{fair}}
\newcommand{\fles}{\lhd_{fair}}
\newcommand{\feqv}{\approx_{fair}}

\newcommand{\oleq}{\unlhd_{\Omega}}
\newcommand{\oles}{\lhd_{\Omega}}
\newcommand{\ileq}{\unlhd_{\stab_{\cal I}}}
\newcommand{\iles}{\lhd_{\stab_{\cal I}}}


\newcommand{\lclas}[1]{\mbox{$\langle{#1}\rangle_L$}}
\newcommand{\sclas}[1]{\mbox{$\langle{#1}\rangle_{\stab}$}}
\newcommand{\spclas}[1]{\mbox{$\langle{#1}\rangle_{\stab'}$}}
\newcommand{\snp}[1]{\mbox{$[{#1}]_{\stab}$}}
\newcommand{\sunp}[1]{\mbox{$[{#1}]_{\stab}^-$}}

\newcommand{\sjoin}{\sqcup_{\stab}}
\newcommand{\smeet}{\sqcap_{\stab}}
\newcommand{\pcap}{\cap}
\newcommand{\ljoin}{\sqcup_L}
\newcommand{\lmeet}{\sqcap_L}



\newcommand{\pfcP}{{\cal L}^{\leeqv}({\cal P})}
\newcommand{\efcP}{{\cal L}^{\lleq}({\cal P})}
\newcommand{\pfcC}{{\cal L}^{\leeqv}({\cal C})}
\newcommand{\efcC}{{\cal L}^{\lleq}({\cal C})}

\newcommand{\pfcR}{{\cal L}_{fin}^{\leeqv}({\cal R})}
\newcommand{\efcR}{{\cal L}_{fin}^{\lleq}({\cal R})}
\newcommand{\ecR}{{\cal L}^{\lleq}({\cal R})}
\newcommand{\pcR}{{\cal L}^{\leeqv}({\cal R})}


\newcommand{\spfcP}{{\cal L}^{\speqv}({\cal P})}
\newcommand{\sefcP}{{\cal L}^{\spleq}({\cal P})}
\newcommand{\spfcR}{{\cal L}^{\seqv}({\cal R})}
\newcommand{\sefcR}{{\cal L}^{\sleq}({\cal R})}

\newcommand{\spfcC}{{\cal L}^{\speqv}({\cal C})}
\newcommand{\sefcC}{{\cal L}^{\spleq}({\cal C})}
\newcommand{\spfcF}{{\cal L}^{\seqv}({\cal F})}
\newcommand{\sefcF}{{\cal L}^{\sleq}({\cal F})}

\newcommand{\era}{\rhd}
\newcommand{\sea}{ST(\alpha)}
\newcommand{\seb}{ST(\beta)}
\newcommand{\seg}{ST(\gamma)}
\newcommand{\lsea}{ST_{\lera}(\alpha)}
\newcommand{\lseb}{ST_{\lera}(\beta)}
\newcommand{\lseg}{ST_{\lera}(\gamma)}

\newcommand{\lclasa}{\lclas{\alpha}}
\newcommand{\lclasb}{\lclas{\beta}}
\newcommand{\lclasg}{\lclas{\gamma}}


\newcommand{\spclasa}{\spclas{\alpha}}
\newcommand{\spclasb}{\spclas{\beta}}
\newcommand{\spclasg}{\spclas{\gamma}}


\newcommand{\isom}{\rightleftharpoons}


\newcommand{\lce}[1]{\mbox{$\overline{{#1}} $}}
\newcommand{\rs}[1]{\mbox{$[{#1}] $}}
\newcommand{\stan}{STA}
\newcommand{\stav}[1]{STV(#1)}
\newcommand{\lin}[1]{\mbox{${#1}_I $}}


\newcommand{\snf}[1]{FAM_{\stab}(#1)}
\newcommand{\spne}[1]{[(#1)]_{\stab'}}




\newcommand{\eleeqv}{\approx_\rhd}
\newcommand{\lrhd}{\rhd_\approx}
\newcommand{\lera}{\rhd_\approx}
\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{\pfami}{\simeq_{\cal P}}
\newcommand{\redc}[1]{\mbox{$[{#1}]$}}
\newcommand{\err}[2]{\mbox{$ST_{{#1}}({#2})$}}
\newcommand{\staeq}{\approx_S}
\newcommand{\Le}{L\'evy}

\newcommand{\ip}[2]{\mbox{$\lceil{#1}\rceil^{{#2}}$}}
%\newcommand{\ms}[2]{\mbox{$\lceil{#1}\rceil^{({#2})}$}}
\newcommand{\fp}[2]{\mbox{$\lceil{#1}\rceil_{{#2}}$}}

%\newcommand{\con}[1]{\mbox{$\lceil{#1}^{\leq}\rceil$}}


\newcommand{\suf}{($\Rightarrow$)}
\newcommand{\nec}{($\Leftarrow$)}
\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{\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{\imply}{\,\Rightarrow\,}


\newcommand{\pc}{permutation-equivalence}
\newcommand{\pt}{permutation-equivalent}



\title{Stable Computational Semantics \\ of Conflict-free Rewrite Systems}


\author{Zurab Khasidashvili\inst{1} \and John Glauert\inst{2}}

\institute {Logic and Validation Technology \\ 
Design Technology Division \\ 
Intel, IDC, Haifa, Israel \\ 
\email{Zurab.Khasidashvili@intel.com}  \\ 
\and
School of Computing Sciences, UEA \\
Norwich NR4 7TJ, UK \\
\email{\john{J.Glauert@uea.ac.uk}}
}

\maketitle
%\thispagestyle{empty}



\begin{abstract}
 We study  orderings $\sleq$ on reductions \john{in the style of L\'evy} reflecting the growth of 
information w.r.t. \emph{(super)stable} sets $\stab$ of `values' (such as 
head-normal forms or B\"ohm-trees). 
We show that sets of co-initial reductions ordered by
 $\sleq$ form finitary $\omega$-algebraic complete lattices, \john{and hence} form
 computation and Scott domains.  As a consequence, we obtain a relativized
 version of \john{the} \emph{computational semantics} proposed by Boudol for term
 rewriting systems.  Furthermore, we give a pure domain-theoretic
 characterization of the orderings $\sleq$ in the spirit of Kahn and
 Plotkin's \emph{concrete domains}.  These constructions are carried out 
in the framework of  \emph{Stable Deterministic Residual Structures},
 which are abstract reduction systems with an axiomatized residual
 relations on redexes, \john{that} model all orthogonal (or conflict-free)
 reduction systems as well as many other interesting computation structures.
\end{abstract}



\section{Introduction}



The idea of representing or identifying a process (or a program, or a term) with the domain of all its computations is not new in semantics: for example, this idea is central in the study of event structure semantics of programming languages extensively developed by Winskel, Nielsen and Plotkin~\cite{[Win],[NPW],[Win89]}. Berry and L\'evy~\cite{[B.L.]} were the first who tried to base algebraic semantics~\cite{[N.R.]} of recursive programs on an ordering on the set of \emph{computations} rather than on the set of \emph{terms}; they used L\'evy's~\cite{[levy],[le80]} \emph{embedding} relation $\lleq$ on reductions for that purpose, which we will explain shortly; the transitive and reflexive closure of $\lleq$ yields \emph{L\'evy}- or \emph{permutation-equivalence} $\leeqv$ on reductions. \john{Permutation-equivalent reductions result \john{from one} another by permuting concurrent consecutive steps, hence the name.} Developing this ideas further,  Boudol~\cite{[Bou]} proposed a \emph{computational} approach to semantics of term rewriting systems~\cite{[D.J.],[Klo92]} in general.  Boudol's idea was to define the semantics of a term $t$ in a term rewriting system $(\Sigma, R)$ (where $\Sigma$ is an alphabet and $R$ is a set of rewrite rules) via the set of $\leeqv$-classes of all $\lleq$-maximal computations starting from $t$. \delete{Therefore he extended $\lleq$ to non-deterministic (i.e., not necessarily orthogonal) rewrite systems and proved that $\lleq$ is a complete partial order (cpo), which implies that $\lleq$-maximal elements are well defined.} In the case of deterministic (or conflict-free or orthogonal) TRSs, a term has exactly one (up to $\leeqv$) $\lleq$-maximal computation, which corresponds to a \emph{fair} computation~\cite{[Klo92]}. To support his computational approach to semantics, Boudol defined \emph{interpretations} of TRSs in the usual algebraic style (i.e., the class of interpretations coincides with the class of $\Sigma$-algebras) and showed that the computational semantics coincides with the algebraic one.


 However, \john{\delete{already}} Boudol~\cite{[Bou]} \john{remarked} that, besides being a cpo,
 ``\emph{$\lleq$ seems to have generally no `good' properties (even for
 deterministic TRSs)}''. To clarify the problem, \john{we observe} that,
 according to  Kahn and Plotkin~\cite{[K.P.]}, a `good' domain into which
 to interpret programs must be at least \emph{coherent} and
 \emph{$\omega$-algebraic}; they call such domains \emph{computation
 domains}.\footnote{Definitions of all order-theoretic concepts used in
 this paper can be found in the appendix~A.} And according to
 Scott~\cite{[Sco]}, `good' domains are \emph{consistently complete}
 $\omega$-algebraic cpos; such domains are called \emph{Scott domains}.
 To quote Plotkin, `Algebraicity is \john{an} important idea which formalizes
 some intuitive ideas of \emph{finiteness} and objects as \emph{limits}
 of their finite approximations. Algebraicity allows definitions of
 \emph{computability} to provide links with recursion function theory
 and allow results on \emph{definability}. \john{Is the next sentence right? construction of constructions?} It allows easy construction
 of constructions as \emph{powerdomains} and enables us to visualise
 domains as \emph{completions} of structures of finite
 information'~\cite{[Plo83]}. Further, Kahn and Plotkin~\cite{[K.P.]},
 Girard~\cite{[Gir87]}, Winskel~\cite{[Win89]}, and many others argue
 that it is reasonable to require `good' domains to be \emph{finitary},
 because in this way finite elements are `really' finite, i.e., represent
 only a finite amount of information (built up from a finite number of
 components), \john{and} thus cannot be decomposed infinitely.  But $\lleq$ is not
 finitary, and the $\lleq$-glb of two finite elements needs not be finite.
 To recover `good' properties of the reduction space, Boudol~\cite{[Bou]}
 \john{studied} the sub-space of all \emph{strongly needed}
 reductions~\cite{[H.L.]} and proved that \john{a reduction space thus restricted}
 is finitary and $\omega$-algebraic, and conjectured that it corresponds
 to the domain of configurations of an event structure and moreover forms
 a \emph{concrete domain}~\cite{[K.P.]}.
\delete{Boudol then proved that strongly needed reductions are sufficient to
compute the value of a term in \emph{sequential} deterministic TRSs (which
are a variant of \emph{strongly sequential} systems of Huet and
L\'evy~\cite{[H.L.]} where needed redexes can be found affectively).
}

There had been other similar proposals to construct domains with rich algebraic properties out of the reduction space \john{of} a reduction system.  For example, in order to construct an event structure semantics for orthogonal (term graph) rewriting systems with non-duplicating residual relation, Kennaway et al.~\cite{[KKSdV]} restrict themselves to needed reductions of normalizable terms; the resulting domain is finitary and \emph{distributive} (or equivalently, \emph{prime algebraic}). Finitary distributive domains (also called \emph{$dI$-domains} or \emph{stable domains}) are exactly domains of configurations/states (ordered by the subset relation) generated by \emph{stable} event structures~\cite{[Win],[NPW],[Win89]}, and are commonly accepted domains to model concurrency. Melli\`es~\cite{[Mel97]} restricts himself to \emph{external}~\cite{[H.L.]} reductions, after having factorised any reduction into an external part followed by an internal reduction, similar to often used factorization of reductions into needed and unneeded parts. In the case of deterministic systems, \john{all} external redexes are needed, and strongly needed redexes are \john{all} external.

Thus in all these cases, a \emph{linear} subspace of reductions is identified on which $\lleq$ forms $dI$-domains. This works because event structures are equivalent to linear reduction systems (where there is no erasure or duplication of redexes): in linear systems, $\lleq$ corresponds to the subset ordering on states of an event structure, all \pt\ reductions correspond to the same state, \emph{prime intervals} of \john{the} event structure represent reduction steps~\cite{[Win89]}, and events can be seen as \john{\delete{as}} equivalence-classes of prime-intervals~\cite{[Win89]}, which are nothing but \emph{zig-zag}-classes~\cite{[levy],[le80]} of the corresponding reduction steps~\cite{[Cur]}. This correspondence is further extended in~\cite{[mfcs-tcs]} (for the case of stable conflict-free systems), where  prime event structures (which are equivalent to stable ones~\cite{[Win89]})\john{, with an axiomatized \emph{erasure} relation, are defined. These} are to non-duplicating reduction systems what event structures are to linear ones.


In order to achieve a stable event structure semantics, or equivalently, to construct a $dI$-domain out of a reduction space, \john{rather than restricting the reduction space,} one could weaken \pc\ into an equivalence relation whose equivalence classes would correspond to the same state of a stable event structure. This observation led Laneve~\cite{[Lan94]} to introduce \emph{distributive permutation equivalence} in the \lc\ which only equates reductions resulting one from another by permutation of steps that cannot erase or duplicate one another. The distributive equivalence coincides with \pc\ on needed reductions in non-duplicating orthogonal rewriting systems, but is strictly weaker in the case of even $\lambda_I$-calculus, where there is no erasure of redexes. Similarly, Corradini et al~\cite{[CGM]} based their construction on an equivalence relation generated by permutations of
disjoint redexes only, in a general categorical model of rewriting.



In this paper we propose a general method to construct finitary computation domains from computation spaces based on new orderings which, \john{unlike} L\'evy's permutation embedding and Laneve's distributive embedding, we believe \emph{truly} express the growth of information along computations, in the spirit of Scott's idea of Information Systems~\cite{[Sco]} which underlies the whole theory of semantics of programming languages. We thereby further extend Boudol's computational approach to semantics, and develop a `relativized' version of it for calculi where redexes can be duplicated and/or erased. We restrict ourselves to the conflict-free case. Based on~\cite{[Bou],[Mel]}, we hope that our constructions can be generalized to the general case.



To fully understand the problem, let us examine once again L\'evy's hugely successful idea of `\emph{less work $\lleq$}' and of `\emph{the same work $\leeqv$}'. For co-initial finite reductions $P,Q$ in an orthogonal rewrite system (e.g. the \lc), $P$ is less than $Q$, written $P\lleq Q$, if what remains of $P$ after $Q$, the \emph{residual} $P/Q$ of $P$ after $Q$, is empty. And $P$ and $Q$ do the same work, $P\leeqv Q$, if $P\lleq Q$ and $Q\lleq P$. The `real life' counterparts of an ordering relation, such as `greater', `older', `stronger', refers to, or is \emph{relative} with respect to, a \emph{particular}  aspects of the object/subject one is interested in. But L\'evy's ordering lacks that relativity property: Suppose we are interested in computing the normal forms of a $\lambda$-term $t=Kx(IIx)$, where $K=\lambda x.\lambda y.x$ and $I=\lambda x.x$. Let $P:t\red{I}Kx(Ix)$ and $Q:t\red{I}Kx(Ix)\red{I}Kxx$. Clearly $P\lles Q$. But both $P$ and $Q$ are unneeded, and neither makes progress towards computation of the normal form obtainable from $t$ in one $K$-step $t\red{K}x$. In this circumstances, does it really make sense to say that `$Q$ is \emph{greater} (i.e., does \emph{more} work) than $P$'?

To correct this situation, we introduced in~\cite{[GK02]} orderings 
$\sleq$ on reductions relative to particular sets $\stab$ of finite or 
infinite \emph{values} one may be interested in, such as normal forms, 
head-normal forms, weak head-normal forms, \emph{B\"ohm-trees}~\cite{[Bar]},
\emph{L\'evy-Longo-trees}~\cite{[le76],[Lon]}, or
\emph{Berarducci-trees}~\cite{[Ber96]}, 
in the \lc, or root-stable forms in orthogonal \john{TRSs.} 
Such values are expressed via \emph{super(stable)} sets of reductions
in  \emph{Stable Deterministic Residual Structures} (SDRSs)~\cite{[rndrs]}.
SDRSs are Abstract Reduction
Systems~\cite{[Hin],[Klo92]} with \john{an} axiomatized \emph{residual} relations on 
redexes, enabling one to define permutation equivalence on reductions.  
SDRSs cover
all conflict-free term and (sharing-) graph/net rewrite systems, and many
other interesting computational structures, and we abstract from \john{inessential}
syntactic structure of the objects. 
In SDRSs one can give abstract proofs of the normalization and 
minimality theorems~\cite{[rndrs],[GK02]}, relative to \john{(super)stable} 
sets of reductions. Recall from~\cite{[Win89]}
that families of configurations in stable event structures whose enabling
relation have a similar `minimality' property generate $dI$-domains. 
The concept of \emph{stability} of an
event structure can be expressed in terms of our concept of stable
reduction (configuration) sets:  it is trivial to check that an event
structure is stable~\cite{[Win89]} iff for any event $e$, the set of all
configurations containing $e$ is stable (according to our definition of
stability).


Here we show that the orderings $\sleq$, which we call (temporarily)
\emph{reduction orderings}, form finitary $\omega$-algebraic complete
lattices on $\seqv$-equivalence classes of co-initial reductions (where
$\seqv=\sleq\cap\unrhd_\stab$). An ordering $\sleq$ need not be distributive
in general, since for example if we take for $\stab$ the set of all
normalizing reductions in the $\lambda_I$-calculus, then $\sleq$ coincides
with $\lleq$, and Laneve~\cite{[Lan94]} has demonstrated that $\lleq$ is
not distributive (even) for the case of $\lambda_I$-calculus. However,
any $\sleq$ contains a substructure which is a $dI$-domain. This
substructure corresponds to $\stab$-needed complete-family
reductions~\cite{[levy],[le80]}. (The sub-space of complete-family
reductions generates a non-duplicating computation space as families do not
duplicate one another; as we have already mentioned,  non-duplicating
reduction systems are equivalent to event structures with erasure, and the
glb operation can simply be expressed via ordinary set-theoretic
intersection on $\stab$-needed events/families~\cite{[mfcs-tcs]}.) Thus the
reduction orderings can be seen as a \emph{refinement} of $dI$-domains which
reflect computations more closely: they \emph{directly} reflect duplication
of redexes which $dI$-domains cannot, and this is the reason for the loss of
the distributivity property.


Furthermore, we show that reduction orderings can be generated by the
permutation ordering $\lleq$ on \emph{non-erasing} conflict-free reduction
systems that are free from \emph{(syntactic) accidents} (i.e., co-initial
reductions that end at the same term are permutation-equivalent). Actually,
in such systems, $\lleq$ coincides with the reduction relation $\doar$ (hence
the name -- reduction ordering), which enables us to give an equivalent
domain-theoretic definition of reduction orderings. This result is an analog
of the well known \emph{representation theorems} for concrete
domains~\cite{[K.P.]}, \john{$dI$-domains}~\cite{[Win89]} and
Scott-domains~\cite{[Sco],[LW93]}, and the key idea is to equip partial
orders with a well-behaved \emph{residual information}.


The following example demonstrates the differences between the domain
constructions for duplicating systems discussed above.


\bel{E.lan.}
Consider the $\lambda_I$-term $t=(\lambda x.xx)(Iz)$, where
$I=\lambda x.x$,  used by Laneve~\cite{[Lan94]}
to demonstrate that L\'evy-equivalence need not generate a $dI$-domain from
the reduction space of a $\lambda$-term.
\footnote{Or else take $t=2\times (0\times 1)$ and consider the rewrite
system with rules $2\times x \ar x+x$ and $x\times 1\ar x$ (so for example
we don't have $0+0\ar 0$ and $0+0$ is a normal form (=result).}
Figures~\ref{fig:reg_order}.(1)-(4) display the reduction space of
$t$, and the Hasse diagrams corresponding to the reduction
ordering (w.r.t. normal forms), to Laneve's\john{\delete{~\cite{[Lan94]}}} \emph{distributive
permutation ordering}, to Khasidashvili and Glauert's~\cite{[mfcs-tcs]}
\emph{event ordering}, and Boudol and Melli\`es'~\cite{[Bou],[Mel97]}
\emph{external ordering}. Clearly,
the reduction ordering describes the computation space of $t$ most closely
(the corresponding Hasse diagram coincides with the reduction graph of $t$).
The distributive permutation ordering is not even a lattice (despite the fact
\john{that} the \lc\ is conflict-free), but the downward
closure of any element is a distributive lattice.
The external ordering (roughly) corresponds to call-by-name computation
and cannot adequately account for either call-by-value computation from $t$
or for all needed ones (note that call-by-value computation from $t$ to normal
form is shorter than the two external computations to normal form, hence is
computationally interesting). The event ordering cannot
adequately account for call-by-need computation; it
accounts well for call-by-value and needed complete family computaions
from $t$, but this
need not be true for all terms since complete family-reductions fail in
general to compute minimal normal forms (see~\cite{[fsttcs],[GK02]} for a
\john{counter}-example, as well as for a characterization of
reductions computing minimal normal forms).
None of these orderings can account for unneeded steps, but such steps do
not make any progress towards the normal form.

\begin{figure}
\begin{center}
\includegraphics[width=4.8in]{reg_order.eps}
%\includegraphics[height=2.0in]{reg_order.eps}
%\include{reg_order.eps}
\caption{A circuit (the boxes represent latches; controls are 
not shown)}
\label{fig:reg_order}
\end{center}
\end{figure}
\end{ex}
\john{(figure does not work for me)}

The paper is organized as follows. In the next section, we recall SDRSs 
and the reduction orderings. 
Section~\ref{S.stab.red.dom.} contains the construction of finitary
$\omega$-algebraic complete lattices based on reduction orderings. In
Section~\ref{S.rep.th.} we give a domain-theoretic definition of reduction
orderings. In Section~\ref{S.DFS-order} we breifly \john{discuss} reduction
ordering in SDRSs with \john{an} axiomatized family relation~\cite{[levy],[le80]}. 
Conclusions appear in Section~\ref{S.concl.}.



\section{Preliminaries: Residuals, stability, and normalization}



Since SDRSs~\cite{[rndrs]} have been used in a number of papers, we do not 
discuss syntactic structures covered by SDRSs and do not give illustrating
examples of introduced concepts.\footnote{For convenience, we include formal
definition in an appendix.} These structures are based on \john{\delete{already}}
classical work of L\'evy~\cite{[levy],[le80],[B.L.],[H.L.]}, and in recent
years there have been many interesting discoveries around the subject of
optimality, both of syntactic and semantic nature. \john{\delete{The reader not interested
in detailed proofs and not willing to enter these axiomatic frameworks
could as well}The reader unfamiliar with these axiomatic frameworks might} think of an SDRS as his or her favorite conflict-free
reduction system, such as Combinatory Logic, \lc, Interaction Nets,
Interaction Systems, orthogonal Term-Graph (or DAG) Rewrite Systems, etc.


We recall that an \emph{Abstract Reduction Systems}
is a triple $A = (Ter,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\mapsto (Ter\times Ter)$
is a function such that for any $t\in Ter$ there is only a finite set of
redexes $u\in Red$ such that $\ar(u)=(t,s)$, written $t\red{u}s$. One can
identify $u$ with the triple $t\red{u}s$. \suppress{\footnote{Klop's
ARSs~\cite{[Kl.TRS]} are pairs $(Ter,\ar)$, and do not allow one to
distinguish transitions with the same source and target terms.}} A {\em
reduction} is a sequence $t\red{u_1}t_2\red{u_2}\ldots$.


\begin{nota}
We write $u\subt t$ if $u$ is a member of the redexes of $t$,  and write $U\subts t$ if $U$ is a subset of the redexes. Reductions are denoted by $P,Q,N$. We write $P:t\doar s$ or $t\dored{P}s$ if $P$ denotes a reduction \john{\delete{(sequence)}} from $t$ to $s$. $Q:t\doar$ may be finite as well as infinite. $P+Q$ denotes the concatenation of $P$ and $Q$.  $u$ also denotes the reduction that contracts $u$.  Further, for any reduction $Q$, $\ip{Q}{k}$ will denote the initial part of $Q$ of length $k$, provided $k\leq \leng{Q}$ (the length of $Q$), and $\fp{Q}{k}$ will denote the tail of $Q$ starting from the $(k+1)$th step; thus $Q=\ip{Q}{k}+\fp{Q}{k}$. Finally, we write $P\leq Q$ if $P$ is an initial part of $Q$.
\end{nota}

\excl{
DRSs axiomatize the properties of residuals which are used
in~\cite{[le80],[H.L.]} to define L\'evy-embedding and permutation equivalence on reductions. DRSs are similar to Stark's {\em Determinate Concurrent Transition Systems}~\cite{[Sta]} and {\em Abstract Reduction Systems} of Gonthier et al.~\cite{[GLM]}. Unlike DCTSs, the residual relation in DRSs may be  duplicating, and unlike ARSs of~\cite{[GLM]},  we do not have a nesting relation on redexes (and as a consequence, DRSs cover many computation structures, e.g., term graph rewriting systems~\cite{[KKSdV]}, not covered by ARS of~\cite{[GLM]}).
}



In a DRS $\cal R$, the residual relation on redexes is extended
to all co-initial finite reductions exactly as in syntactic orthogonal rewrite systems~\cite{[H.L.],[levy],[le80],[Sta]}: $(P_1+P_2)/Q=P_1/Q+P_2/(Q/P_1)$
and $P/(Q_1+Q_2)=(P/Q_1)/Q_2$.\footnote{Note that $P/Q$ is defined uniquely only if it is viewed as a \emph{multi-step} reduction, each multi-step being a complete development of a set of redexes. It is sound however to consider $P/Q$ as a reduction obtained by sequentializations of the corresponding multi-step reduction, and we will freely switch between the two interpretations\john{\delete{? a multi-step in general}}.}  \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'\,
\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 \emph{strong Church-Rosser property} states that, for any co-initial finite reductions $P,Q$, $P\sqcup Q\leeqv Q\sqcup P$, where $P\sqcup Q=P+Q/P$, and is $\lleq$-lub of $P$ and $Q$. Finally, we will need the following \emph{Cube Lemma}: for any finite co-initial reductions $P,Q$ and $N$, \john{= or $\leeqv$?} $N/(P\sqcup Q)= N/(Q\sqcup P)$.


Given a set $\stab$ of reductions in a DRS $\calR$ and a term $t$ in $\calR$, we call $t$ \emph{$\stab$-normalizable} if $\stab$ contains a reduction $P$ starting from $t$; $P$ is then called $\stab$-normalizing. \suppress{Further, $\stab_t$ will denote the set of all reductions in $\stab$ that start from $t$. Thus $t$ is $\stab$-normalizable iff $\stab_t\not=\emp$, and $\stab$ consists of all $\stab$-normalizing reductions.}




\bdl{D.rel.ord.}
Let $\stab$ be a set of reductions in a DRS.

(1)  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$).

(2) We call $u\subt t$ \emph{$\stab$-unneeded} if there is a reduction $Q\in\stab$ staring from $t$ that is external to $u$, and call it \emph{$\stab$-needed} otherwise.

(3) Let $P,Q$ be co-initial reductions. If $P$ and $Q$ are both finite, then we define $P\sleq Q$ if $P/Q$ is $\stab$-unneeded. Otherwise,  $P\sleq Q$ if for any finite $P'\leq P$ there is a finite $Q'\leq Q$ such that $P'\sleq Q'$. Further, $P\seqv Q$ iff $P\sleq Q$ and $Q\sleq P$. We call $\sleq$ and $\seqv$ respectively $\stab$-\emph{embedding} and $\stab$-\emph{equivalence}. $\sclas{P}$ denotes the $\seqv$-equivalence class of $P$ (we will show below that $\seqv$ is an equivalence relation). We write $\sclas{P}\sleq\sclas{Q}$ if $P\sleq Q$.
\ed


It is immediate from the definition that $\lleq \ssq \sleq$.


\bdl{D.clo.reduc.sets.}
Let $\stab$ be a set of reductions in a DRS.

(1)  We call $\stab$ \emph{stable} iff:

[CS] \emph{$\stab$ is suffix-closed}: if $P'\not\in\stab$, then
$P'+P''\in\stab$ implies $P''\in\stab$.

[CE] \emph{$\stab$ is closed under $\stab$-embedding}: $P\in\stab$
and $P\sleq Q$ implies $Q\in\stab$.

[CN] \emph{$\stab$ is closed under neededness}: every non-empty
$P\in\stab$ contracts at least one $\stab$-needed redex.

Furthermore, we call $\stab$ \emph{regular} iff:

[Reg]  In no term can an $\stab$-unneeded redex duplicate an 
$\stab$-needed one.

(3) Finally, we call $\stab$ \emph{superstable} iff:

[Min] For any $\stab$-normalizable term $t$, $\stab$ contains 
a unique, up to $\leeqv$, $\lleq$-minimal element starting from $t$.  
Such reductions will be called $\stab$-minimal.
\ed


We call a (regular, super) stable set of reductions in a DRS $\calR$ a
\emph{(regular, super) stable semantics} of $\calR$. Below $\stab$ will 
denote a stable (regular or superstable) semantics of a DRS. \\


\bdl{D.can.sn.}
(1) Let $\stab$ be a stable semantics of an SDRS $\calR$ and let $P:t\doar$. The \emph{$\stab$-needed part of $P$}, $\snp{P}$, is a finite or infinite reduction defined by: $\snp{P}=u+\snp{P/u}$, where $u\subt t$ is the redex whose residual along $P$ is contracted first among $\stab$-needed steps in $P$, if any.

(2) We call a reduction $P:t_0\ar t_1\ar\ldots$ \emph{$\stab$-needed fair} if
for any $\stab$-needed redex $v\in t_i$, $v_i\sleq \fp{P}{i}$.
\ed


\btl{ne.fa.norm.reg.}
(\cite{[GK02]}) Let $\stab$ be a regular stable semantics of an SDRS $\calR$, 
and let $t$ be $\stab$-normalizable. Then any $\stab$-needed fair reduction is
$\stab$-normalizing.
\et




\excl{
\begin{rem}\em
\label{R.depth.}
Let $\stab$ is a regular stable semantics for an SDRS with an additional
property that every non-empty subset of redexes $U\subts t$  contains a
\emph{non-duplicable element}, i.e., a redex $u\in U$ such that $u$ has
at most one residual along any reduction contracting redexes in $U$ and
created redexes. All interesting examples of SDRS have that latter property.
For example, external redexes are non-duplicable~\cite{[H.L.]}, and the
leftmost-outermost redex in any CL or $\lambda$-term is external. Then
similarly to the case of regular stable sets of
results~\cite{[fsttcs],[Mel98]}, for any finite $P$, $\sclas{P}$ contains
a $\lleq$-minimal element.\footnote{The minimality result
in~\cite{[fsttcs]}, mentioned already in the introduction, is obtained
for concrete systems, orthogonal Expression Reduction Systems, but it
immediately generalizes to SDRSs in which every subset of redexes in a
term has a non-duplicable element; the result fails for irregular stable
sets~\cite{[fsttcs]}.}  This result is a counterpart of Berry's stability
theorem and the stability property in event structures, but somewhat
strengthened, since as we have already discussed, $\bleq$ is a refinement
of the classical B\"ohm topology.  However, to extend this result to
infinite $P$ as well, one will need SDRSs equipped with a metric associating
a \emph{depth} to every redex, and to restrict the reduction space to
\emph{strongly convergent} reductions only~\cite{[Ken96]}. This goes beyond
the scope of this paper. Restriction to strongly convergent reductions seems
also necessary to insure stability of  sets of co-initial fair reductions
(cf.~\cite{[mfcs-tcs]}).
\end{rem}
}


\section{Properties of reduction domains}
\label{S.stab.red.dom.}


This section contains the construction of $\omega$-algebraic finitary
complete lattices from the reduction spaces of SDRSs.

First of all, we show that $\sleq$ is a partial order, which requires the
following simple characterization of $\sleq$ via $\lleq$.

\bll{sleq.via.leq.}
Let $P$ and $Q$ be finite co-initial reductions in an SDRS $\calR$ with
regular stable semantics $\stab$. Then $P\sleq Q$ iff $P\lleq Q+Q'$ for
some $\stab$-unneeded~$Q'$.
\el


\bll{L.tra.fin.}
Let $P,Q$ and $N$ be co-initial reductions in an SDRS $\calR$ with regular
stable semantics $\stab$, and let $P\sleq Q\sleq N$. Then $P\sleq N$.

\excl{
\bproof
First assume that $P,Q$ and $N$ are finite. By \Lr{sleq.via.leq.},
$P\sleq Q\sleq N$ implies $P\lleq Q+Q'$ and $Q\lleq N+N'$ for some
$\stab$-unneeded $Q'$ and $N'$. But $Q\lleq N+N'$ implies $Q+Q'\lleq
N+N'+Q^*$ (see the figure), where $Q^*=Q'/((N+N')/Q)$ is $\stab$-unneeded.
Thus $P\lleq N+N'+Q^*$ where $N'+Q^*$ is $\stab$-unneeded, and $P\sleq N$
by \Lr{sleq.via.leq.}. Thus the lemma is proved when $P,Q$ and $N$ are
finite. Now let us consider the general case.  By \Dr{D.rel.ord.} and
$P\sleq Q$, for any finite $P'\leq P$ there is a finite $Q'\leq Q$ such
that $P'\sleq Q'$. Similarly, there is a finite $N'\leq N$ such that
$Q'\sleq N'$, thus $P'\sleq N'$, implying again by \Dr{D.rel.ord.} that
$P\sleq N$.
\begin{diagram}[height=1.6em,width=1.6em]
{}         & \rOnto^{N}    &  {}      &\rOnto^{N'}   &  {}  \\
\dOnto<{Q}   &          &\dOnto   &         & \dOnto_\emp     \\
{}     &\rOnto   & {}    & \rOnto  & {}   \\
\dOnto<{Q'}   &          &\dOnto  &             &  \dOnto_{Q^*}   \\
{}      &\rOnto       &  {}       & \rOnto      & {}   \\
\end{diagram}
\eproof
}
\el


\bcl{P.sleq.po.}
Let $\stab$ be a regular stable semantics of an SDRS $\calR$. Then $\seqv$
is an equivalence relation, and consequently $\sefcR=(\spfcR,\sleq)$ is a
partial order, where $\spfcR=\cR/_{\seqv}$ and $\cR$ is a set of 
 co-initial reductions in $\calR$.
\ec



Recall the definition of \john{the} $\lleq$-meet operation from~\cite{[GK02]}. 
Let $\Phi$ be a set of reductions starting from $t$,
in a DRS. Then the \emph{$\lleq$-meet} of reductions in $\Phi$, written
$\lmeet \Phi$, is defined as follows: Let $U\ssq t$ be the maximal subset
such that $U\lleq \Phi$, and let $t\dored{U}s$ be a 
complete development of $U$
(or the multi-step contracting $U$). Then $\lmeet \Phi=U+\lmeet (\Phi/U)$.

\zurab{This example must be corrected.} Note that $P \lmeet Q$ need not be a $\sleq$-glb of $P$ and $Q$ even in a DRS corresponding to a Recursive Program Scheme: Let $R=\{g(x)\ar h(x,E(x)),\,E(x)\ar a\}$, let $t=g(g(g(x)))$, let $P:t\ar h(g(g(x)),E(g(g(x))))\ar h(g(h(x,E(x))),E(g(g(x))))$, and let $Q:t\ar g(h(g(x),E(g(x))))\ar g(h(h(x,E(x)),E(g(x)))).$ Then $t$ contains three redexes: $u,v$ and $w$, listed in the top-down order, and none of them are erased in both $P$ and $Q$, thus $P\lmeet Q=\emp$, while $w\sleq P,Q$ for the set $\stab$ of all normalizing reductions. This suggests the following definition:


\bdl{D.mj.rel}
Let $\stab$ be a stable semantics of an SDRS $\calR$, and let $\Phi$ be a set of reductions in $\calR$ starting from $t$. Then:

(1) {\bf ($\stab$-meet)}  \emph{$\stab$-meet} of $\Phi$, written $\smeet \Phi$, is defined as follows: Let $U\ssq t$ be the maximal subset such that $U\sleq\Phi$, and let $t\dored{U}s$. Then $\smeet \Phi=U+\smeet (\Phi/U)$.

(2) {\bf ($\stab$-join)} \emph{$\stab$-join} of reductions in $\Phi$, written $\sjoin \Phi$, is defined as follows: Let $V\ssq t$ be the set of all
redexes that are contracted in the first step of one of the reductions in
$\Phi$, and let $t\dored{V}e$. Then $\sjoin \Phi=V+\sjoin (\Phi/V)$. 

(3)  {\bf ($L$-join)} We define $\ljoin \Phi = \sjoin \Phi$.
\ed
\delete{Delete this paragraph: 
\emph{$L$-join} of reductions in $\Phi$, written
$\ljoin \Phi$, is defined as follows: Let $V\ssq t$ be the set of all
redexes that are contracted in the first step of one of the reductions in
$\Phi$, and let $t\dored{V}e$. Then $\ljoin \Phi=V+\ljoin (\Phi/V)$.
}

We need the following two simple lemmas to prove that $\smeet$ and $\sjoin$
are indeed meet and join operations for $\sleq$.

\bll{l.eq.sun.sun.}
Let $P,Q$ be finite reductions in an SDRS with regular stable semantics
$\stab$, let $P\lleq Q$, and let $Q$ be $\stab$-unneeded. Then so is $P$.

\excl{
\bproof
Suppose on the contrary $P=P'+v+P''$, where $v$ is $\stab$-needed. Then By
\Lr{P.cre.res.need.}.(1) and \Lr{P.cre.res.need.}.(3), $Q/P'$ is
$\stab$-unneeded and $v/(Q/P')$ contains at least one ($\stab$-needed)
redex, contradicting $P\lleq Q$.
\eproof
}
\el



\bll{L.sle.pr.res.}
Let $P\sleq Q$ in an SDRS with a regular stable semantics $\stab$, and let
$N$ be finite and co-initial with $P$. Then $P/N\sleq Q/N$.

\excl{
\bproof
It is enough to prove the lemma for finite $P,Q$. By \Lr{sleq.via.leq.}, $P\lleq Q+Q'$ for some $\stab$-unneeded $Q'$, implying that $P/N\lleq Q/N+Q^*$, where $Q^*=Q'/(N/Q)$ is  $\stab$-unneeded by \Lr{P.cre.res.need.}.(1). Hence $P/N\sleq Q/N$ again by \Lr{sleq.via.leq.}.
\eproof
}
\el

\john{I think some of the following needs some motivation. Where is this lemma taking us?} Below we use $\Phi$ to denote sets of co-initial reductions. Further, for
example we write $P\lleq\Phi$ iff $\forall Q\in\Phi . \,Q\lleq P$;
$\ip{\Phi}{k}$ will denote the set of initial parts, of the length $k$, of
reductions in $\Phi$; etc.

First note that if $\Phi$ consists of two finite reductions $P$ and $Q$,
then $P\sqcup Q\leeqv P\ljoin Q$, although $P\sqcup Q$ and $P\ljoin Q$ are
different as multi-step reductions.\delete{Delete: Secondly, note that some of the
multi-steps in $\ljoin \Phi$ may be empty. This is simply for convenience
in proofs.}
 Further, since every term contains a finite number of redexes,
a finite subset of $\Phi$ is enough to generate any particular step in
$\ljoin \Phi$ (even if $\Phi$ contains an infinite number of reductions).
More precisely:



\bll{L.jo.fin.joi.}
Let $\Phi$ be a set of reductions in a DRS. Then for any
$k\leq \leng{\ljoin\Phi}$, there is a finite subset $\Phi[k]\ssq\Phi$ such
that $\ip{\ljoin\Phi}{k} = \ljoin\ip{\Phi[k]}{k}\leeqv
\sqcup\ip{\Phi[k]}{k}$.
\el



\bll{L.int.glb.}
Let $\Phi$ be a set of co-initial reductions in a DRS. Then
$\ljoin\Phi$ is a (unique up to $\leeqv$) $\lleq$-lub of~$\Phi$.

\bproof
It is immediate from the definition of $\ljoin$ that $\Phi\lleq \ljoin\Phi$. Now let $\Phi\lleq P$ and let us show $\ljoin\Phi\lleq P$, i.e., that $\ip{\ljoin\Phi}{k}\lleq \ip{P}{l_k}$ for any $k$ and some $l_k$. 
By \Lr{L.jo.fin.joi.}, 
$\ip{\ljoin\Phi}{k}=\ljoin \ip{\Phi[k]}{k}\leeqv \sqcup \ip{\Phi[k]}{k}$.
 Let $l_k$ be such that $\ip{\Phi[k]}{k}\lleq \ip{P}{l_k}$. Then  $(\ljoin \ip{\Phi[k]}{k})/\ip{P}{l_k}\leeqv (\sqcup \ip{\Phi[k]}{k})/\ip{P}{l_k}\leeqv \sqcup (\ip{\Phi[k]}{k}/\ip{P}{l_k})=\emp$, and we are done.
\eproof
\el

\btl{T.int.glb.rel}
Let  $\stab$ be a regular stable semantics of an SDRS $\calR$, and let
$\Phi$ be a set of co-initial reductions in $\calR$. Then:

(1) $\smeet\Phi$ is a (unique up to $\seqv$) $\sleq$-glb of~$\Phi$.

(2) $\sjoin\Phi$ is a (unique up to $\seqv$) $\sleq$-lub of~$\Phi$.

\bproof
(1) Let $\smeet\Phi=Q:t_0\dored{U_0}t_1\dored{U_1}t_2\doar\ldots$. It is
immediate from \Dr{D.mj.rel} that $Q\sleq\Phi$. Thus we need to show that
for any $P$, $P\sleq\Phi\imply P\sleq Q$, that is, for any $n\leq \leng{P}$,
$\ip{P}{n}\sleq Q$. We show this by induction on $n$. The case $n=0$ (i.e.,
$P=\emp$) is clear. So let $n=k+1$, and let $\ip{P}{k}\sleq Q$. Then
$\ip{P}{k}\sleq \ip{Q}{l_k}$ for some $l_k$. We can assume that
$\ip{Q}{l_k}$ ends at $t_m$ for some $m$. Now assume that the $(k+1)th$
step $v$ of $P$ has an $\stab$-needed residual $v'$ under
$\ip{Q}{l_k}/\ip{P}{k}$ (otherwise, there is nothing to prove). Since
$\ip{P}{k}/ \ip{Q}{l_k}$ is $\stab$-unneeded, 
by \Lr{P.cre.res.need.}.(2) there 
must be an $\stab$-needed redex $v''$ in the final term $t_m$ of
$\ip{Q}{l_k}$ such that $v'$ is its $(\ip{P}{k}/ \ip{Q}{l_k})$-residual.
Furthermore, $v'$ is the only $(\ip{P}{k}/ \ip{Q}{l_k})$-residual of $v''$
by regularity of $\stab$, thus $v''\sleq P/\ip{Q}{l_k}$. But $P\sleq \Phi$,
hence $P/\ip{Q}{l_k}\sleq \Phi/\ip{Q}{l_k}$ by \Lr{L.sle.pr.res.}. Thus,
$v''\sleq \Phi/\ip{Q}{l_k}$, and $v''$ must be contracted in $U_m$ (by
\Dr{D.mj.rel}). Hence $v'/(U_m/(\ip{P}{k}/ \ip{Q}{l_k}))=\emp$, and we
are done.
\begin{diagram}[height=1.5em,width=1.5em]
t_0          &\rOnto^{\ip{P}{k}}& &  \cdot       &\rTo^{v}   & {} {} \\
\dOnto<{\ip{Q}{l_k}}&            & &\dOnto   &         &      \\
t_{m}     &\rOnto^{\ip{P}{k}/\ip{Q}{l_k}}& & \cdot    & \rTo^{v'} & {}  \\
\dOnto{v''\in U_{m}}   &         & &\dOnto  &             &     \\
{}      &      & & {}      &       &  {}  \\
\end{diagram}

(2) By \Lr{L.int.glb.}.(2), $\Phi\lleq\sjoin\Phi$, implying
$\Phi\sleq\sjoin\Phi$.  Now let $\Phi\sleq P$
and let us show $\sjoin\Phi\sleq P$, i.e., that
$\ip{\sjoin\Phi}{k}\sleq \ip{P}{l_k}$ for any $k$ and some $l_k$.
By \Lr{L.jo.fin.joi.}, $\ip{\sjoin\Phi}{k}=\sjoin \ip{\Phi[k]}{k}\leeqv
\sqcup \ip{\Phi[k]}{k}$,  and $\Phi\sleq P$ implies $\ip{\Phi[k]}{k}\sleq P$.
Let $l_k$ be such that $\ip{\Phi[k]}{k}\sleq \ip{P}{l_k}$. Then
$(\sjoin \ip{\Phi[k]}{k})/\ip{P}{l_k}\leeqv (\sqcup
\ip{\Phi[k]}{k})/\ip{P}{l_k}\leeqv \sqcup (\ip{\Phi[k]}{k}/\ip{P}{l_k})$,
and $\sqcup (\ip{\Phi[k]}{k}/\ip{P}{l_k})$ is $\stab$-unneeded by
\Lr{P.cre.res.need.}.(1). Thus $(\sjoin \ip{\Phi[k]}{k})/\ip{P}{l_k}$ is
$\stab$-unneeded by \Lr{l.eq.sun.sun.}, i.e., $\sjoin \ip{\Phi}{k}\sleq
\ip{P}{l_k}$, implying $\sjoin\Phi\sleq P$.
\eproof
\et


\bcl{C.stab.lat.}
Let $\stab$ be a regular stable semantics of an SDRS $\calR$. Then $\sefcR$
is a complete lattice with meet and join operations $\sjoin$ and $\smeet$
defined by: $\sjoin\sclas{\Phi}=\sclas{\sjoin\Phi}$ and
$\smeet\sclas{\Phi}=\sclas{\smeet\Phi}$.
\ec



Now we can soundly define the relativized computational semantics for an
SDRS $\calR$ as follows: Let $\stab$ be a regular stable semantics of
$\calR$, and let $t$ be an $\stab$-normalizable term in $\calR$. Then
the \emph{value} of $t$ in $\calR$ w.r.t. $\stab$ is the $\sleq$-maximal
$\seqv$-equivalence class of reductions starting from $t$, in $\sefcR$.
Thus for example in the case of B\"ohm-semantics, the B\"ohm-tree $BT(t)$
of $t$ is represented by the set of all reductions computing $BT(t)$, which
form the $\bleq$-maximal $\beqv$-class of reductions starting from $t$
(where $\stab_B$ is the set of all reductions computing 
B\"ohm-trees, see \cite{[GK02]} for details).



\bll{L.dev.dom.fin.}
Let $\stab$ be a regular stable semantics of an SDRS $\calR$, let $U\subt t$
be a set of $\stab$-needed redexes in $t$, let $N:t\doar$ be $\stab$-needed,
and let $N\sleq U$. Then $N$ is a development of $U$, thus is finite.
\el


This lemma is used in the proof of the following crucial lemma for
establishing finiteness of~$\sefcR$.


\bll{L.finfin.}
Let $\stab$ be a regular stable semantics of an SDRS $\calR$, let $P\sleq Q$,
and let $\snp{Q}$ be finite. Then so is $\snp{P}$.
\el



Hence, by \Lr{P.cre.res.need.}.(4), we can soundly define $\sclas{P}$ to be \emph{finite}
iff $P$ contracts only a finite number of $\stab$-needed redexes, or
equivalently if $\snp{P}$ is finite. The following lemma justifies our
definition:


\bll{fin.el.}
Let $\stab$ be regular stable semantics for an SDRS $\calR$. Then $\sclas{P}$
is  finite iff it is a finite element of $\sefcR$.

\excl{
\bproof
\suf\ Let $\sclas{P}$ be finite. We can assume by \Lr{L.finfin.} that $P$ is
$\stab$-needed and finite. Now let $\sclas{\Phi}$ be directed and
$\sclas{P}\sleq \sclas{\sjoin\Phi}$. Then $P\sleq \sjoin\Phi$, and by
\Lr{L.jo.fin.joi.}, $P\sleq \sjoin\Phi[k]$ for some $k$, where
$\Phi[k]\ssq\Phi$ is finite. Since $\sclas{\Phi}$ is directed, $\exists
N\in\Phi.\sjoin\Phi[k]\sleq N$. Thus $\sclas{P}\sleq \sclas{N}\in
\sclas{\Phi}$, which means that $\sclas{P}$ is finite in $\sefcR$.
\nec\ Let $\sclas{P}$ be finite in $\sefcR$, and let $P$ be infinite
(otherwise $\sclas{P}$ is trivially finite). It is immediate from
\Dr{D.mj.rel} that  $P= \sjoin \{\ip{P}{k}\vert k\in {\cal N}\}$,
thus $P\sleq \sjoin \{\ip{P}{k}\vert k\in {\cal N}\}$, and clearly
$\{\ip{P}{k}\vert k\in {\cal N}\}$ is directed. Hence by finiteness of
$\sclas{P}$ in $\sefcR$, $P\sleq \ip{P}{n}$ for some $n$, which by
definition of $\sleq$ means that $\fp{P}{n}$ is $\stab$-unneeded. Hence
$\sclas{P}$ is finite.
\eproof
}
\el


Now, using Lemmas~\ref{fin.el.} and \ref{P.cre.res.need.}.(4) and \Tr{T.int.glb.rel}, we
can prove finiteness and algebraicness of~$\sefcR$:

\btl{P.stab.lat.fin.}
Let $\stab$ be a regular stable semantics for an \john{SDRS} $\calR$. Then
$\sefcR$ is a finitary $\omega$-algebraic complete lattice.

\bproof
(Algebraicness)  Let $Q$ be a reduction in $\calR$ and let $\Phi=\{N\vert
\sclas{N}\, finite,\, N\sleq Q\}$. Then $\sclas{\Phi}$ consists of all
finite elements of $\sefcR$ dominated by $\sclas{Q}$. It follows from
\Lr{sleq.via.leq.} and \Lr{P.cre.res.need.}.(1) that 
for any finite subset $\Phi' \subseteq \Phi$, $\sjoin\Phi' \in \Phi$
(since we can assume that all reductions in $\Phi$ are finite), thus
$\sclas{\Phi}$ is
directed. Thus we want to prove that $\sclas{\sjoin\Phi}=\sclas{Q}$.
It is immediate from \Dr{D.mj.rel} that $Q=\sjoin \{\ip{Q}{n}\vert n
\leq\leng{Q}\}$. But $\{\ip{Q}{n}\vert n\leq\leng{Q}\}\ssq\Phi$, thus
$Q=\sjoin \ip{Q}{n}\sleq \sjoin\Phi$. On the other hand, $\sjoin\Phi$ is
the $\sleq$-lub of $\Phi$ by \Tr{T.int.glb.rel}, thus $\sjoin\Phi\sleq Q$.
Hence $\sclas{\sjoin\Phi}=\sclas{Q}$.

(Finiteness) Let $\sclas{P}$ be finite in $\sefcR$. By Lemmas~\ref{fin.el.}
and \ref{P.cre.res.need.}.(4), we can assume $P$ to be $\stab$-needed and finite. Suppose
on the contrary that $\sclas{P}$ dominates an infinite number of elements of
$\sefcR$. Then by \Lr{P.cre.res.need.}.(4) there is an infinite set $\Phi$ of
$\stab$-needed reductions such that $\Phi\sleq P$. Since the reduction tree
corresponding to $\Phi$ is finitely-branching (because a term may contain
only a finite number of redexes), $\Phi$ must contain an infinite
$\stab$-needed reduction $Q\sleq P$ (by K\"{o}nig's Lemma), contradicting \Lr{L.finfin.}.


\eproof
\et


The above theorem fails for (irregular) stable semantics $\stab$ in general:
Consider the DRS $\calR$ generated by $R=\{f(x)\ar h(f(x),f(x)),\,a\ar b\}$,
restricted to the reduction graph ${\cal G}(t)$ of $t=f(a)$, and take
for $\stab_{ter}$ the set of terms not containing occurrences of $a$. Then
the corresponding set $\stab$ of $\stab_{ter}$-normalizing reductions is
stable but not regular, and the set of $\seqv$-classes of reductions in
${\cal G}(t)$ does not contain a finite element except the bottom element,
implying that $\calR$ is not algebraic. (Indeed, if a reduction $P$
contracts infinitely many $\stab$-needed redexes, then, for any finite $m$,
$\sqcup_{k \leq m}\ip{P}{k}\sles \sqcup_{k<\infty}\ip{P}{k}\seqv P$, thus
$\sclas{P}$ is not finite; And if $P$ contracts a finite 
number of $\stab$-needed redexes, we can assume that the last step of
$P$ is $\stab$-needed, thus has the form $C[f(a)]\red{u} C[f(b)]$.
But the step $u$
is the $\sleq$-lub of the set of (strictly $\sles$-smaller) finite
initial parts of the reduction $C[f(a)]\ar C[h(f(a),f(a))]\ar
C[h(f(b),f(a))]\ar C[h(f(b),h(f(a),f(a)))]\ar C[h(f(b),h(f(b),f(a))]\ar\ldots$.
Hence $u$, and thus $P$ itself, are not finite.)
\footnote{The same DRS was used in~\cite{[jlc2]} to demonstrate failure of
the \emph{hypernormalization theorem} w.r.t. irregular stable sets of results
in general.}
\excl{Recall also that irregular stable sets $\stab$ may behave badly
w.r.t. the minimality property mentioned in Remark~\ref{R.depth.}.}


\section{A representation theorem for the reduction orderings}
\label{S.rep.th.}


In previous sections, we defined reduction orderings $\sleq$ as orderings
generated by pairs $(\calR,\stab)$, where $\stab$ is a regular stable
semantics for an SDRS $\calR$. Now we wish to give an equivalent definition
in domain-theoretic terms. Such results in the literature are called
\emph{representation theorems}: for example, concrete domains (defined by
restricting partial orders with a number of axioms) are exactly the domains
generated by \emph{Information Matrices}~\cite{[K.P.]} (often called
\emph{Concrete Data Structures}~\cite{[Cur]}), $dI$-domains are domains
generated by \emph{Prime} (or equivalently, \emph{Stable}) \emph{Event
Structures}~\cite{[Win89]}, and Scott domains are domains generated by
\emph{Information Systems}~\cite{[Sco],[LW93]}.


To define (i.e., to fully characterize) orderings $\sleq$ domain-theoretically,
we note that $\sleq$ is built from a pair $(\calR,\stab)$, and in the
transition from $(\calR,\stab)$ to $\sleq$ some information, namely the
\emph{residual information}, gets ignored. This suggests that, up to some
isomorphism, $(\calR,\stab)$ is nothing but $\sleq$ equipped with an
appropriate residual information. The idea of partial orders with residuals
is not precisely new: all the above mentioned representation results
implicitly use a \emph{linear} residual concept. In the case of reduction
orderings, the crucial step enabling \john{us} to define the correct residual relation
is the observation that all reduction orderings can actually be generated as
permutation orderings $\lleq$ on some \emph{non-erasing} SDRSs $\calR_\stab$
that are \emph{(syntactic) accident-free} (to be defined shortly).


The next definition shows how to define such `projections' of $\sleq$ onto
$\lleq$. There, it is enough (and convenient) to consider only
\emph{comma-SDRSs} $\calR$, whose underlying ARSs are reduction graphs of a
fixed \emph{initial term}.  The $\stab$-projection of any SDRS
consists of (isomorphic copies) of projections of its comma-(sub)SDRSs.



\bdl{D.stab.proj.}
{\bf ($\stab$-projection)}
Let $\calR$ be a comma-SDRS with a regular stable semantics $\stab$. Then
the \emph{$\stab$-projection} of $\calR$ is an SDRS $\calR_\stab$ defined as
follows:

$\bullet$ Terms in $\calR_\stab$ are $\seqv$-classes $\sclas{P}$ of finite
\emph{initial} reductions $P$ in~$\calR$ (that is, $P$ startes with the 
initial term);

$\bullet$  Arrows in $\calR_\stab$ are pairs $\sclas{P}\ar_\stab \sclas{P+u}$,
where $u$ is an $\stab$-needed redex in the final term of $P$. (The empty
redex in $\sclas{P}$ can be defined as the pair $\sclas{P}\red{\emp}_\stab
\sclas{P}$.)

$\bullet$  The residual relation $/_\stab$ in $\calR_\stab$ is defined as
follows: Let $\sclas{P}\red{u^*}_\stab \sclas{P+u}$ and
$\sclas{P}\red{v^*}_\stab \sclas{P+v}$ in $\calR_\stab$. Then for any
$\stab$-needed $v'\in v/u$, $\sclas{P+u}\red{v'^*}_\stab\sclas{P+u+v'}$
is a $u^*$-residual of $v$, written  $v'^*\in v^*/_\stab u^*$.
\ed


Thus any redex $Pu$ in $\calR$ (whose \emph{history} $P$ is an initial 
reduction) is assigned a unique redex
$\sclas{P}\ar_\stab \sclas{P+u}$ in $\calR_\stab$, although different
redexes (with histories) in $\calR$ may have the same corresponding redex
in $\calR_\stab$. This assignment induces a function $h$ from (parts of)
initial reductions in $\calR$ to initial reductions in $\calR_\stab$ with
the following properties:

$\bullet$ If $P=P_1 +P_2$ is an initial reduction in $\calR$, then
$h(P_1+P_2)=h(P_1)+h(P_2)$;

$\bullet$ If $N$ is an initial reduction in $\calR$, then $h(N)=\emp$ iff
$N$ is $\stab$-unneeded.


Although the converse of $h$ is not a function, for any initial reduction
$P'$ in $\calR_\stab$ there is a unique $\stab$-needed initial reduction
in $\calR$, noted $h'(P')$, that contracts the `same' redexes as $P'$,
i.e., $h(h'(P'))=P'$, and therefore $h'(h(P))=P$ for any $\stab$-needed
initial reduction $P$ in $\calR$. Thus $(h,h')$ gives an isomorphism
between $\stab$-needed initial reductions in $\calR$ and initial reductions
in $\calR_\stab$. Using these properties of $h$, we can quite easily prove
the correctness of \Dr{D.stab.proj.}. First a definition:


\bdl{D.acc.free.}
Let $\calR$ be a comma-SDRS. We call $\calR$ \emph{good} if it is
\emph{non-erasing} and \emph{accident-free}:

$\bullet$ [NE]: for any co-initial distinct redexes $t\red{u}s$ and
$t\red{v}e$ in $\calR$, $v/u\not= \emp$.

$\bullet$ [AF]: for any initial reductions $P$ and $Q$ in $\calR$ that end
at the same term, $P\leeqv Q$.\footnote{A simple pair of co-initial
reductions, namely $P:IIx\red{Ix}Ix$ and $Q:IIx\red{IIx} Ix$, that end at
the same term but are not L\'evy-equivalent was given by
L\'evy~\cite{[levy]}, where this phenomenon is called a \emph{syntactic
accident}.}
\ed




\bll{L.proj.lem.}
Let $\calR$ be a comma-SDRS with a regular stable semantics $\stab$.
Then $\calR_\stab$ is a good SDRS. (Hence in particular \Dr{D.stab.proj.}
is sound.)
\el


For a comma-SDRS $\calR$, assume that ${\cal L}^{\lleq}(\calR)$ and
${\cal L}^{\sleq}(\calR)$ denote the corresponding orderings w.r.t.
the initial term. Now we can easily prove the desired result:


\btl{T.isom.proj.}
Let $\stab$ be a regular stable semantics of a comma-SDRS $\calR$. Then
${\cal L}^{\lleq}(\calR_\stab)$ and ${\cal L}^{\sleq}(\calR)$ are isomorphic.

\bproof
Since initial reductions in $\calR_\stab$ are exactly reductions $h(P)$ for
initial ($\stab$-needed) reductions $P$ in $\calR$, the lemma follows immediately from the
fact that $P\sleq Q$ in $\calR$ iff $h(P)\lleq h(Q)$ in $\calR_\stab$
(for the latter, see the proof of \Lr{L.proj.lem.}).
\delete{
Define $f:{\cal L}^{\sleq}(\calR)\mapsto {\cal L}^{\lleq}(\calR_\stab)$ and
$g:{\cal L}^{\lleq}(\calR_\stab)\mapsto {\cal L}^{\sleq}(\calR)$ by:
$f(\sclas{P})=\lclas{\snp{P}}$ and $g:(\lclas{P'})=\sclas{P'}$, where
$P$ and $P'$ are any finite initial reductions in $\calR$ and $\calR_\stab$,
 respectively. Now since $P\seqv \snp{P}$ in $\calR$ and $\snp{P'}=P'$ in
 $\calR$ (remember that $P'$ is also an $\stab$-needed initial reduction
 in $\calR$), we have immediately from the definitions of $f$ and $g$ that
 $$g(f(\sclas{P}))=g(\lclas{\snp{P}})=\sclas{\snp{P}}=\sclas{P}$$ and
 $$f(g(\lclas{P'}))=f(\sclas{P'})=\lclas{\snp{P'}}=\lclas{P'}.$$ Thus the
 pair $f,g$ gives the required isomorphism.
}
\eproof
\et


In fact, in non-erasing SDRSs, $\lleq$ coincides with the \emph{fair} ordering $\fleq$, i.e., the ordering $\fleq$  where $\stab_{fair}$ is the set of all fair (\cite{[Klo92]}) reductions; this follows immediately from the fact that at least one residual of any redex $u\in t$ in a non-erasing SDRS must be contracted in every fair reduction starting from $t$ (and from the fact that a reduction is fair iff so is any of its tails).



Furthermore, because of accident-freeness, in good SDRSs (differently from SDRSs in general) there is at most one step between any pair of terms $(t,s)$, thus the reduction relation can be given as sets of pairs. That is, a good SDRS is a triple $\calR=(Ter,\ar, /)$, where $Ter$ is a set of objects (called terms) containing an initial term $t_\emp$, $\ar$ is a set of pairs, and $/$ is a residual relation (satisfying SDRS-axioms). Furthermore, in good SDRSs $\calR$, $\lleq$ on finite elements is isomorphic to $\doar$, the reduction relation on $\calR$:



\btl{T.leq.red.}
Let $\calR=(Ter, \ar,/)$ be a good SDRS. Then $\efcR=(\pfcR,\lleq)$ is
isomorphic to  $(Ter,\doar)$, where $\fcR$ is the set of all finite 
initial reductions in $\calR$, and $\ecR=(\pcR,\lleq)$ is isomorphic to
$\leq_\calR=IC(Ter,\doar)$, the ideal completion of $(Ter,\doar)$ (infinite
ideals of $\leq_\calR$ correspond to $\leeqv$-classes of infinite reductions
in $\calR$).

\bproof
By [AF], every term $t\in Ter$ uniquely determines exactly one element $\lclas{P_t}$
 of $\pfcR$, where $P_t$ is any initial reduction ending with $t$.
 Furthermore, $t\doar s$ iff $\lclas{P_t}\lleq \lclas{P_s}$: Indeed, if
 $N:t\doar s$, then by [AF] $P_s\leeqv P_t+N$, implying $P_t\lleq P_s$; and
 conversely, $P_t\lleq P_s$ implies $P_s\leeqv P_t+P_s/P_t$ and clearly
 $P_s/P_t:t\doar s$.
By \Lr{fin.el.}, $\pfcR$ coincides with the set of finite elements of $\ecR$, hence $\ecR$ is isomophic to $\leq_\calR$
(see e.g. \cite{[D.P.]}, pages 82-83).
\eproof
\et


Thus, we need to provide a domain-theoretic characterization of ideal completions of orderings $(Ter,\doar)$ for good SDRSs $\calR=(Ter, \ar,/)$, which are finitary $w$-algebraic complete lattices of a special form. It is standard (after~\cite{[K.P.]}) to associate with a partial order $\leq\,=(D,\leq_D)$ an ARS (or a transition system) $A_\leq=(Ter_\leq,\ar_\leq)$ such that $Ter_\leq=D$ and $t\ar_\leq s$ iff $t\crl_D s$ (in $D$), where $t\crl_D s$ iff $t<_D s \,\wedge \, \forall o\in D: (t\leq_D o\leq_D s \imply t=o \vee s=o)\}$. The relation $\crl_D$ is called \emph{covering}.
A sequence of the form $t\crl_D t_1 \crl_D \ldots$ is called a \john{\emph{covering
chain}, or a \emph{covering $(t,s)$-chain}} when $t_i \leq_D s$.

Since any algebraic cpo $\cal L$ is obtained as the ideal completion
of its subset of finite elements (noted $F({\cal L})$), it is enough to axiomatize properties of finite elements only. Therefore, following~\cite{[Cur]}, if in a pair $t\crl_D s$ in an algebraic cpo both $t$ and $s$ are finite, we write it as $[t,s]_D$ (or simply as $[t,s]$) and call it a \emph{prime interval}, although the definition of (prime) intervals $[t,s]$ say in~\cite{[K.P.],[Win]} does not require $t$ and $s$ to be finite.
Similarly, if all $t_i$ in a covering chain $t\crl_D t_1 \crl_D \ldots$ are finite, we write it also as $[t\crl_D t_1 \crl_D \ldots]$. Finally, we write
$t \crl_D s \ccrl_D s^*$ if, for any $o\in D$, $s^* \not\leq_D s
\sqcup_D o$ (if $D$ is a lattice with lub operation $\sqcup_D$), and we
write $[t \crl_D s \ccrl_D s^*]$ to indicate that $t,s$ and $s^*$ are finite.






\bdl{rel.stab.order.}
Let $\leq\,=(D,\leq_D,\sqcup_D,\sqcap_D)$ be a (finitary $\omega$-algebraic) complete lattice such that:

$\bullet$ [FB] (finite branching) For any $t\in F(D)$, there are only a finite number of $s\in D$ such that $t \crl_D s$ (such an $s$ must be finite).
\delete{
$\bullet$ [NT] (no-tringles) For any pair of different co-initial prime intervals $[t,s]$ and $[t,o]$ in $D$, $s,o< s\sqcup o$.
}

$\bullet$ [SD] (semi-distributivity) For any triple of co-initial prime intervals $[t,s]$, $[t,e]$, and $[t,o]$ in $D$, $s \sqcup_D (o \sqcap_D e)=
(s\sqcup_D o) \sqcap_D (s\sqcup_D e)$. (Note here that, by [NE],
$s \sqcup_D (o \sqcap_D e)=s$.)

$\bullet$ [FC] (finite chains) For any set of co-initial prime intervals $[t,s_i]$, any maximal covering $(t,\sqcup_D s_i)$-chain is finite and
ends with $\sqcup_D s_i$.

$\bullet$ [S] (stability) For any $t,s,s^*,e,e^* \in F(D)$ such that
$[t \crl_D s \ccrl_D s^*]$ and $[t \crl_D e \ccrl_D e^*]$, $(s \sqcup_D e^*)
\sqcap_D (e \sqcup_D s^*)= e \sqcup_D s$.


Then we call $\leq$ a \emph{complete regular domain} (CRD).
\ed


For the ordering $\leq_\calR$ generated by a good SDRS $\calR$, the fact
that $\calR$ is non-erasing can be expressed by the following property:
\emph{for any pair of co-initial prime intervals $[t,s]$ and $[t,o]$ in
$\leq_\calR$,  $s,o<_\calR s\sqcup o$ (strictly)}, and we can call any
prime interval $[s,e]$ such that $e\leq_\calR s\sqcup o$ a \emph{residual}
of $[t,o]$ by $[t,s]$. This is because in non-erasing SDRSs, the
$\leq_\calR$-lub of co-initial steps $u,v$ is exactly the endpoint of the
complete development of the non-empty set $u/v$. But if the SDRS was
erasing, there could be larger redex sets $U'$ in the target term of $v$
such that $U\leeqv U'$ (in which case the redexes in $U'\setminus U$ are
erased by $U$). Hence this definition of residuals \delete{would} may 
not work properly in `erasing' partial orders.


\bd
In a CRD $\leq\,=(D,\leq_D,\sqcup_D,\sqcap_D)$, we define a
residual relation $/_D$ as the reflexive and transitive closure
of the following relation:

$\bullet$ For any pair of co-initial prime intervals $u=[t,o],v=[t,s]$ in $D$, $u/_D v =\{[s,e] \,\vert\,e\leq s\sqcup o\}$.
\ed

Thus we may as well refer to an CRD as a triple $\leq\,=(D,\leq_D,/_D)$.
Using this definition, we can show that good SDRSs and
CRDs are equivalent models. We need two simple lemmas first:

\bll{L.no-erasu.}
Let $(D,\leq,\sqcup, \sqcap)$ be a CRD, and let $[t,s]$, $[t,s_i]$
$(0\leq i\leq m)$ be prime intervals such that $s\not= s_i$.
Then $s< s \sqcup (\sqcup s_i)$ and
$\sqcup s_i < s \sqcup (\sqcup s_i)$.
\delete{
\bproof
By induction on the length $n$ of a longest covering $(t,\sqcup s_i)$-chain $P$
($n$ is finite by [FB] and K\"{o}nig's Lemma). The case $n=1$ is trivial by
[NE]. Assume (without loss of generality) that $P$ starts with $t\crl s_1$,
 let $[s_1,e_j]$ $(1\leq j\leq k)$ e allresiduals of $[t,s_i]$ in $s_1$, and
let $[s_1,o_r]$ $(1\leq r\leq l)$. Clearly, $\sqcup s_i = \sqcup e_j$. (Indeed,
$e_j \leq s_1 \sqcup s_{i_j}$ for any $j$ and some $i_j$,
by definition of residuals, thus
$\sqcup e_j \leq \sqcup s_i$; conversly, $s_i \leq e_{j_i}$ for any $i$ and
some $j_i$, thus  $\sqcup s_i \leq \sqcup e_j$.) By [LD], $e_j$ and $o_r$ are
pairwise different. By the induction assumption, for any $r$,
$\sqcup e_j < o_r
\sqcup (\sqcup e_j)$, thus $\sqcup e_j < (\sqcup o_r) \sqcup
(\sqcup e_j)$. Hence, by [FD], $\sqcup s_i < (s\sqcup s_1) \sqcup
(\sqcup s_i) = s \sqcup (\sqcup s_i)$. Finally, $s< s \sqcup (\sqcup s_i)$
follows immediately from $s < s \sqcup s_1$ (which holds by [NE]).
\eproof
}
\el




\bll{L.red=cov.}
Let $\leq\,=(D,\leq_D,\sqcup_D,\sqcap_D)$ be a CRD, let
$e_0 \crl_D e_1 \crl_D\ldots\crl_D e_n$, and let $e_0 \crl e_0 ^*$.
Then $[e_m, e_m ^*]$ is a residual, w.r.t. $/_D$, of $[e_0,e_0 ^*]$
iff $e_m ^* \leq_D e_0 ^* \sqcup_D e_m$, and the lub of all
such $e_m ^*$ is $e_0 ^* \sqcup_D e_m$.

\delete{
\bproof
By induction on $n$.

\suf\ Let $[e_m, e_m ^*]$ be a residual of $[e_0,e_0 ^*]$. Then $[e_m, e_m ^*]$ is a residual of a residual $[e_{m-1}, e_{m-1} ^*]$ of $[e_m, e_m ^*]$ in $e_{m-1}$. By definition of $/_D$ and the induction assumption, $e_m ^* \leq_D e_m \sqcup_D e_{m-1} ^* \leq_D e_m \sqcup_D (e_0 ^* \sqcup_D e_{m-1}) =
e_m \sqcup_D e_0 ^*$.

\nec\ Let $e_m ^* \leq_D e_0 ^* \sqcup_D e_m$. Further, let $[e_{m-1}, e_{m-1} ^i]$ $(0\leq i \leq p)$ be all prime intervals such that
$e_{m-1} ^i \leq_D e_0 ^* \sqcup_D e_{m-1}$. By \suf\ and the induction assumption, $[e_{m-1}, e_{m-1} ^i]$ are
all residuals of $[e_{m-1}, e_{m-1} ^i]$.  If on the contrary $[e_m,e_m ^* ]$ is not a residual o any of $[e_{m-1}, e_{m-1} ^i]$, then $e_m ^* \not\leq_D e_m \sqcup_D e_{m-1} ^i$, for all $0\leq i \leq p$. Hence, by \Lr{L.no-erasu.},
$e_m ^* \not\leq_D e_m \sqcup_D (\sqcup_D e_{m-1} ^i)=$ (by induction assumpttion) $=e_m \sqcup_D (\sqcup_D (e_0 ^* \sqcup_D e_{m-1})) = e_0 ^* \sqcup_D e_m$.
\eproof
}
\el


\btl{T.eq.po.mod.}
Good SDRSs and complete regular domains are equivalent models: CRDs are
(up to isomorphism) the partial orders generated by good SDRSs. More precisely,

(1) For any good SDRS $\calR=(Ter,\ar,/)$, $IC(Ter,\doar)$ is a CRD
(where $\doar$ is the transitive reflexive closure of $\ar$).

(2) If $\leq=(D, \leq_D, /_D)$ is a CRD, then $\calR_\leq = (F(D), \crl_D, /_D)$
is a good SDRS and $\leq$ is isomorphic to $IC(F(D), \crl_D)$ (where $\crl_D, /_D$  in $\calR_\leq$ are restrictions, to $F(D)$, of these relations in $\leq$).

\bproof
\zurab{Complete the proof.}

(1) Let $(Ter,\ar,/)$ be a good SDRS, and let $\sqcup$ and $\sqcap$ be the
corresponding lub and glb operations. By Theorems~\ref{P.stab.lat.fin.},
\ref{T.isom.proj.} and \ref{T.leq.red.}, $(Ter,\doar)$ is a finitary
$w$-algebraic complete lattice (we denote by $\sqcup_\leq$ and $\sqcap_\leq$
 the corresponding lub and glb operatins). Then [FB] is immediate.
\delete{[NT] is immediate from [NE] (since for any $t,s \in Ter$, 
$t\sqcup_\leq s$ is the endpoint of $P\sqcup Q$ for
any co-initial reductions in $\calR$ ending with $t$ and $s$, respectively).}
To show [LD] (in its simpified form), let $[t,s]$, $[t,e]$, and $[t,o]$ 
be prime intervals in $\leq$. Then clearly $s\doar s\sqcup_\leq e$ and 
$s\doar s\sqcup_\leq o$, hence $s\doar (s\sqcup_\leq e) \sqcap_\leq 
(s\sqcup_\leq o)=s^*$. If on the contrary $s\doarp s^*$, then for any 
$s'$ such that
$s\ar s'\doar s^*$, we would have that the redex $[s,s']$ is a $[t,s]$-residual
of both redexes $[t,o]$ and $[t,e]$ in $\calR$ -- contradiction. To prove [FC],
let $[t_0,s_i]$ be prime intervals in $\leq$, and let $P:t_0\ar t_1 \ar\ldots$
be a $t_0, \sqcup_\leq$-chain. Then $P$ is a development of the set of redexes
$[t_0,s_i]$ in $\calR$: Indeed, if on the contrary $t_k \ar t_{k+1}$ is
the first step in $P$ that is not a residual of any of $[t_0,s_i]$
\eproof
\et



\section{Imposing more structure on $\sleq$}
\label{S.DFS-order}

In~\cite{[rndrs]}, \emph{Deterministic Family Structures} were introduced
on the top of DRSs, by imposing further axioms on \john{the residual relation, enabling us}
to infer important properties of \emph{redex-families}, such as the 
optimality theorem~\cite{[levy],[le80]}. Formally, a DFS is a pair 
$\calF_\stab=(\calR,\fami)$, where $\calR$ is a DRS and $\fami$ is 
a \emph{family} relation on redexes with histories $Pv$ ($v$ is a redex in 
the final term of $P$), satisfying a number of axioms not listed here.

The projection of pairs $(\calR,\stab)$ onto SDRSs $\calR_\stab$ induces a
projection of pairs $(\calF,\stab)$ onto $\calF_\stab=(\calR_\stab,
\fami_\stab)$, where $v'\fami_\stab w'$ iff $Pv\fami Qw$, and
$v'=(\sclas{P},\sclas{P+v})$ and $w'=(\sclas{Q},\sclas{Q+w})$. Note here
that, because of accident-freeness, in $\calR_\stab$ redexes determine
their histories uniquely up to $\leeqv$, thus $\fami_\stab$ can simply
be seen as a relation on redexes rather than redexes with histories;
and although there may be other $P^*v^*, Q^*w^*$ such that $v'=(\sclas{P^*},
\sclas{P^*+v^*})$ and $w'=(\sclas{Q^*},\sclas{Q^*+w^*})$, one has $Pv\fami
P^*v^*$ and $Qw\fami Q^*w^*$ (since $Pv$ and $P^*v^*$ must be the residuals
of the same redex in the final term of $\snp{P}$, by \Lr{P.cre.res.need.},
and similarly for $Qw$ and $Q^*w^*$), thus the definition of $\fami_\stab$
is correct. It is easy to show that:



\btl{L.proj.fam.}
For any DFS $\calF$ with a regular stable semantics $\stab$, $\calF_\stab$
is a DFS.
\et



Thus orderings $\sleq$ generated by pairs $(\calF,\stab)$ are generated by
\emph{good} DFSs, i.e., DFSs $\calF=(\calR,\fami)$ such that $\calR$ is good.
And furthermore the family relation $\fami$ induces an equivalence relation
on prime intervals in $\leq_\calR$ that is a family relation (when
considering $\leq_\calR$ as an SDRS). 
There may be more than one way to define a family relation on a (good)
SDRS,\footnote{This is related to the \emph{separability} problem: a redex
may create a number of redexes that may be put in different families, as well
as in the same family, without violating the family axioms~\cite{[ldrs]}.}
so in general the family axioms do add strength to complete regular domains. 
Furthermore, we can impose the \emph{minimality} property (the counterpart 
of superstability of \john{reduction} 
sets) on regular stable domains to obtain an even better behaved ordering. 





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



We have defined \emph{stable computational semantics} for deterministic
reduction systems based on very natural orderings $\sleq$ reflecting the
growth of information towards the value of an expression w.r.t. a semantics
$\stab$ specified by a set of computations. We showed that $\sleq$ are
finitary $\omega$-algebraic complete lattices of a special form (containing
$dI$-domains as substructures), and gave their equivalent domain-theoretic
 characterization. The proposed semantics unifies Boudol's computational
 approach to semantics~\cite{[Bou]} with Winskel's stable Event Structure
 Semantics~\cite{[Win89]} (in the conflict-free case).We have learned
 that the `finest' good domains to model functional calculi are actually the
 domains generated by the calculi themselves.


The importance of the concepts of stability and $dI$-domains for
construction of models of functional calculi (based on the \lc) and for
the full abstraction problem~\cite{[BCL],[Ong.chap.]}, as well as for
modeling polymorphism~\cite{[Gir86],[CGW89]}, is well understood, and we
hope that our results will contribute to progress in these areas.  The
interpretation of DFSs into non-duplicating ones proposed
in~\cite{[acoi-rep],[ldrs]} maps good DFSs into linear DFSs which
generate $dI$-domains, and we can readily get denotational models for
lambda-calculi with different stable semantics using Berry's
construction~\cite{[berry]}. However, more direct ways of using the
orderings $\sleq$ in the study of denotational models of $\lambda$- and
related calculi deserve further investigation. The precise relevance of 
family axioms and the minimality for regular stable
domains is presently unknown.

\delete{
Furthermore, we believe that
once the completeness requirement is relaxed to bounded completeness or
coherence, the regular domains (rather than $dI$-domains) can be used to
model for example higher-order process calculi, where processes can be
passed as arguments and therefore erased or duplicated. This is a non-trivial
task and is left for a future work. \delete{Finally, we mention that it may
be possible to give another alternative definition of orderings $\sleq$ via
Information Systems~\cite{[Sco]}, by relaxing the axioms for Prime
Information Systems (which are equivalent to Prime Event
Structures)~\cite{[Zha91]}.}
}


\begin{thebibliography}{99}

\bibitem[{AGM}]{[AGM]}
Abramsky S., Gabbay D., and Maibaum T., eds.  Handbook  of Logic in Computer Science, vol.~1-4, Oxford University Press, 1992-1995.


\suppress{
\bibitem[{AO93}]{[A.O.]}
Abramsky S., Ong C.-H. L. Full abstraction in the lazy lambda calculus. Information  and Computation, 105:159-267, 1993.


\bibitem[{AL93}]{[AL]}
Asperti A., Laneve C. Interaction Systems I: The
theory of optimal reductions.  MSCS 11:1-48,
\delete{Cambridge University Press,} 1993.
}

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


\bibitem[{Ber96}]{[Ber96]}
Berarducci A. Infinite lambda-calculus and non-sensible models. Logic and Algebra, Lecture Notes in Pure and Applied Mathematics 180, Marcel Dekker Inc., 1996, p.~339-378.

\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[{BL79}]{[B.L.]}
Berry G., L\'evy J.-J. Minimal and optimal computations of recursive
programs. JACM 26, 1979, p.~148-175.


\bibitem[{BCL85}]{[BCL]}
Berry G., Curien P.-L., L\'evy J.-J. Full abstraction for sequential languages: the state of the art. \delete{In: Algebraic methods in semantics. Nivat M., Reynolds J.C., eds. Cambridge Univ. Press, 1985,} In~\cite{[N.R.]}, p.~89-132.


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


\suppress{
\bibitem[{BC88}]{[B.C.]}
Boudol G., Castellani I. A non-interleaving semantics for CCS based on proved transitions. Fundamenta Informaticae, 11(4):433-452, 1988.


\bibitem[{CK96}]{[C.K.]}
Clark D., Kennaway R. Event structures and non-orthogonal term graph rewriting.
MSCS 6:545-578,~1996.
}


\bibitem[{CGW89}]{[CGW89]}
Coquand T., Gunter C.A., Winskel G. $dI$-domains as a model of polymorphism. In Proc. of \delete{the $3^{rd}$ Workshop on the Mathematical Foundations of Programming Language Semantics,} MFPLS'87, Springer LNCS, vol.~298, 1987, p.~344-363.


\bibitem[{CGM95}]{[CGM]}
Corradini A., Gadduchi F., Montanari U. Relating two categorical models of term rewriting. In: Proc. of RTA'95, springer LNCS, Vol.~914, 1995, p.~25-240.


\bibitem[{Cur86}]{[Cur]}
Curien P.-L. Categorical combinators, Sequential algorithms and functional programming. John Wiley \& Sons, 1986.


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

\bibitem[{DP90}]{[D.P.]}
Davey, B.A., Priestley H.A., Introduction to Lattices and Order
Cambridge University Press, 1990.


\bibitem[{DJ90}]{[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[{Gir86}]{[Gir86]}
Girard J.Y. The system $F$ of variable types:fifteen years later. TCS 45:159-192, 1986.


\bibitem[{Gir87}]{[Gir87]}
Girard J.Y. Linear logic. TCS 50:1-101, 1987.

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

\bibitem[{GKK00}]{[jlc2]}
J. R. W. Glauert, J. R. Kennaway and Z. Khasidashvili. Stable
results and relative normalization. Journal of Logic and Computation, 
vol.~10(3). Special Issue on Type Theory and Term Rewriting, 
F.~Kamareddine and J.W.~Klop, eds. Oxford University Press, 2000, p.~1-26.

\suppress{
\bibitem[{GK94}]{[morn]}
Glauert J.R.W., Khasidashvili Z. Minimal and optimal relative normalization in Orthogonal Expression Reduction Systems. Report SYS-C94-06, UEA, Norwich, 1994.
}


\bibitem[{GK96}]{[rndrs]}
Glauert J.R.W., Khasidashvili Z. Relative normalization in deterministic
residual structures. In: Proc. of
\delete{the $19^{th}$ International Colloquium on
Trees in Algebra and Programming,}
CAAP'96, Springer LNCS, vol.~1059,  H.~Kirchner, ed. 1996,  p.~180-195.


\bibitem[{GK96a}]{[fsttcs]}
Glauert J.R.W., Khasidashvili Z. Minimal relative normalization in orthogonal expression reduction systems. In: Proc. of FST\&TCS'96, Springer LNCS, vol.~1180, \excl{ V.~Chandru, ed.} 1996, p.~238-249.


\excl{
\bibitem[{GK98}]{[inf-com]}
Glauert J.R.W., Khasidashvili Z. Stable Results and Relative Normalization. Submitted to Inf.\& Comp. Available at http://www.sys.uea.ac.uk/\~{}zurab.


\bibitem[{GK96a}]{[rndrs-rep]}
Glauert J.R.W., Khasidashvili Z. Relative normalization in stable
deterministic
residual structures. Technical Report SYS-C96-01, UEA, Norwich, UK.
}


\bibitem[{GK02}]{[GK02]}
J. R. W. Glauert, Z. Khasidashvili. ``{\sl An abstract
B\"ohm-normalization}''. in: Proc. of Second International Workshop on 
Reduction Strategies in Rewriting and Programming, WRS'02, Electronic Notes 
in Computer Science, Elsevier Science B.V., 2002\john{\delete{(to appear)}}.


\bibitem[{GLM92}]{[GLM]}
Gonthier G., L\'evy J.-J., Melli\`es P.-A. An abstract Standardisation
theorem. In: Proc. of LICS'92,  1992,~ p.~72-81.

\bibitem[{Gun93}]{[Gun93]}
Gunter C.A. Semantics of programming languages: structures and techniques.
MIT Press, 1993.


\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. MIT Press, 1991.


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

\excl{
\bibitem[{Ken96}]{[Ken96]}
Kennaway J.R.  Transfinite rewriting, Int. School on Type Theory and Term
Rewriting, Glasgow, 1996. (Invited survey paper.)
}

\bibitem[{KKSV93}]{[KKSdV]}
Kennaway J. R., Klop J. W., Sleep M. R, de Vries F.-J. Event structures and
orthogonal term graph rewriting. In: Term Graph Rewriting: Theory and Practice. Sleep M.~R., Plasmeijer M.~J., van Eekelen M.~C.~J. D., eds. John Wiley,
1993, p.~141-156.

\delete{
\bibitem[{KOV97}]{[KOV]}
Kennaway J. R., van Oostrom V., de Vries F.-J. Meaningless terms in rewriting.
Journal of Functional and Logic Programming,  1999.
}

\excl{
\bibitem[{KG96}]{[dndrs]}
Khasidashvili Z.,  Glauert J. R. W. Discrete normalization and Standardization in Deterministic Residual Structures. In: Proc. of
\delete{the $5^{th}$ International Conference on Algebraic and Logic Programming,}
 ALP'96, Springer LNCS, vol.~1139,  M.~Hanus, M. Rodr\'{\i}guez-Artalejo, eds. 1996, p.~135-149.
}



\bibitem[{KG97}]{[ldrs]}
Khasidashvili Z., Glauert J.R.W. Zig-zag, extraction and separable families in
non-duplicating stable deterministic residual structures. Report IR-420, Free University, February~1997.


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


\excl{
\bibitem[{KG97a}]{[icalp]}
Khasidashvili Z,  Glauert J. R. W. The Geometry of Orthogonal Reduction Spaces. In Proc. of \delete{$24^{th}$ International Colloquium on Automata, Languages, and Programming,} ICALP'97, Springer LNCS, vol.~1256, 1997, 649-659.
}

\excl{
\bibitem[{KG97b}]{[mfcs]}
Khasidashvili Z., Glauert J. R. W. Relating conflict-free transition and event models. In Proc. of \delete{the $22^{nd}$ International Symposium on Mathematical Foundations of Computer Science,} MFCS'97, Springer LNCS, vol.~1295, 1997, 269-278.
}

\bibitem[{KG98}]{[mfcs-tcs]}
Khasidashvili Z., Glauert J.R.W.  Relating conflict-free stable transition
and event models.  Available on request.
(Conference version appears in Proc. of \excl{the $22^{nd}$ International
Symposium on Mathematical Foundations of Computer Science,} MFCS'97,
Springer LNCS, vol.~1295, 1997, p.~269-278.)


\delete{
\bibitem[{KG98a}]{[atoe-tcs]}
Khasidashvili Z., Glauert J.R.W.  An abstract theory of optimal evaluation.
Draft. Available on request.
}

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


\bibitem[{Klo92}]{[Klo92]}
Klop J. W. Term  Rewriting Systems.  In:~\cite{[AGM]}, vol.~2, 1992, p.~1-116.


\bibitem[{Lan94}]{[Lan94]}
Laneve C.  Distributive evaluations of $\lambda$-calculus,
Fundamenta Informaticae, 20(4):333 -- 352, 1994.


\bibitem[{LW93}]{[LW93]}
Larsen K., Winskel G. Using information systems to solve recursive domain equations effectively. In: Proc. of Int. Symposium on the Semantics of Data Types, Springer LNCS, vol.~173, 1984.


\bibitem[{L\'ev76}]{[le76]}
L\'evy J.-J. An algebraic interpretation of the
$\lambda\beta K$-calculus; and an
application of a labelled \lc. TCS 2(1):97-114, 1976.

\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[{Lon83}]{[Lon]}
Longo G. Set theoretic models of lambda calculus: theories, expansions
and isomorphisms. Annals of Pure and Applied Logic, 24:153-188, 1983.


\delete{
\bibitem[{Mar91}]{[Mar91]}
Maranget L. Optimal derivations in weak $\lambda$-calculi and in orthogonal
Term Rewriting Systems. In: Proc. of 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[{Mel96}]{[Mel]}
Melli\`es P.-A. Description Abstraite des Syst\`emes de R\'e\'ecriture.
Th\`ese de l'Uni\-versit\'e Paris 7, 1996.


\bibitem[{Mel97}]{[Mel97]}
Melli\`es P.-A. A factorization theorem in rewriting theory. In; Proc. of CTCS'97, Springer LNCS vol. 1290.


\bibitem[{Mel98}]{[Mel98]}
Melli\`es P.-A. A stability theorem in rewriting theory. In: Proc. of LICS'98, 1998.

\bibitem[{NPW81}]{[NPW]}
Nielsen M., Plotkin G., Winskel G. Petri nets, event structures and
domains. Part 1. TCS 13:85-108, 1981.

\bibitem[{NR85}]{[N.R.]}
Nivat M., Reynolds J.C., eds. Algebraic methods in semantics.
Cambridge Univ. Press, 1985.


\bibitem[{Ong95}]{[Ong.chap.]}
Ong C.-H. Correspondence between operational and denotational semantics: the full abstraction problem for PCF.  In:~\cite{[AGM]},  vol.~4, 1995, p.~269-356.


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


\bibitem[{Oos96}]{[Oos]}
Van Oostrom V. Higher order families. In: Proc. of
RTA'96, Springer LNCS, vol.~1103, Ganzinger, H., ed., 1996, p.~392--407.

\bibitem[{Oos97}]{[Oos97]}
Van Oostrom V. Finite family developments. In: Proc. of. RTA'97, Springer LNCS, vol.~1232, H. Common, ed., 1997, p.~308-322.
}


\bibitem[{Plo83}]{[Plo83]}
Plotkin G. Domains. University of Edinburgh, 1983 (Manuscript).

\delete{
\bibitem[{Raa96}]{[Raa.th]}
Van Raamsdonk F. Confluence and normalisation for higher-order rewriting.
Ph.D. Thesis, Free University, Amsterdam,~1996.
}


\bibitem[{Sco82}]{[Sco]}
Scott D. Domains for denotational semantics. In Proc. ICALP'82, Springer LNCS, vol.~140, pp.~577-613, 1982.

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


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


\bibitem[{Win86/89}]{[Win89]}
Winskel G. An introduction to Event Structures. \suppress{In proc. of School/Workshop on `Linear time, branching time and partial order in logics and models of concurrency'.} Springer LNCS, vol.~354, 1989, p.~364-397. Extended version appears as Cambr. Univ. Comp. Lab. Report n. 95, 1986.

\suppress{
\bibitem[WN95]{[WN]}
Winskel G., Nielsen M.  Models for concurrency.   In:  S.~Abramsky, D.~Gabbay,
and T.~Maibaum eds.  Handbook  of Logic in Computer Science, vol.~4, Oxford University Press, 1995, p.~1-148.


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

\end{thebibliography}



\section{Appendix A: Partial orders}




\bdl{D.fpad.}
%\bit
$\bullet$ A \emph{partial order} is a binary relation $\sqleq$ on a set $L$ which is \emph{reflexive}: $\forall x\in L: x\sqleq x$; \emph{transitive}: $\forall x,y,z\in L: x\sqleq y \wedge y\sqleq z \imply x\sqleq z$; and \emph{antisymmetric}: $\forall x,y\in L: x\sqleq y \wedge y\sqleq x \imply x=y$. \excl{Without the third axiom, ${\cal L}=(L,\sqleq)$ is called a \emph{preorder}.}


$\bullet$ A \emph{complete lattice} is a partial order ${\cal L}=(L,\sqleq)$ which has least upper bounds (or joins) $\sqcup X$ and greatest lower bounds (or meets) $\sqcap X$ of arbitrary subsets $X\ssq L$. (Actually, it is enough to require only existence of meets $\sqcap X$, or equivalently, existence of a top element $\top$ and of meets $\sqcap X$ for all non-empty $X$.) We write $x\sqcup y$ and $x\sqcap y$ for the join and meet respectively of two elements $x,y\in L$.

$\bullet$ A subset $X\ssq L$ of a partial order ${\cal L}=(L,\sqleq)$ is \emph{bounded} or \emph{consistent} if $X$ has an upper bound in $L$. Further, $X\ssq L$ is \emph{pairwise bounded} or \emph{compatible} if each pair of elements in $X$ is bounded. ${\cal L}$ is \emph{coherent} if any pairwise bounded subset $X\ssq L$ has least upper bound, and is \emph{bounded complete} or \emph{consistently complete} if any bounded subset $X\ssq L$ has least upper bound.


$\bullet$ A \emph{directed subset} of a partial order ${\cal L}$ is a subset $Y\ssq L$ with the property that for any finite set $X\ssq Y$ there is an element $y\in Y$ such that $\forall x\in X. x\sqleq y$.


$\bullet$ A \emph{complete partial order (cpo)} is a partial order ${\cal L}=(L,\sqleq)$ that has a least element $\bot$ and all least upper bounds of directed subsets of $L$.


$\bullet$ A \emph{finite element} (also called \emph{isolated} or \emph{compact}) of a cpo is an element $z$ with the property that, for all directed subsets $Y$, if $z\sqleq \sqcup Y$, then there is some $y\in Y$ for which $z\sqleq y$.


$\bullet$ A cpo is ${\cal L}$ is \emph{algebraic} if for any element $d\in L$ the set $\{x\sqleq d\,\vert\,x\,\,is\,\,finite\}$ is directed and has least upper bound~$d$. If moreover ${\cal L}$ has only a denumerable number of finite elements, then ${\cal L}$ is called $\omega$-algebraic.


$\bullet$ A \emph{computation domain} is a coherent and $\omega$-algebraic partial order. A \emph{Scott domain} is a consistently complete $\omega$-algebraic cpo.


$\bullet$ A \emph{complete prime} of a complete lattice $\cal L$ is an element $p\in L$ such that $p\sqleq\cup X\Rightarrow \exists x\in X. p\sqleq x$ for any subset $X\ssq L$. ${\cal L}$ is \emph{prime algebraic} if, for all $x\in L$, $x=\sqcup\{p\sqleq x\,\vert\,p\,\,is\,\,a\,\,complete\,\,prime\}$.

$\bullet$ An algebraic cpo is \emph{finitary} iff every finite element dominates only a finite number of elements, i.e., $\{x\,\vert\,x\sqleq d\}$ is finite for every finite element~$d$.

$\bullet$ A complete lattice ${\cal L}$ is \emph{distributive} if $x\sqcap (y\sqcup z)=(x\sqcap y)\sqcup (x\sqcap z)$, for all elements $x,y,z\in L$.
\delete{
$\bullet$ In a partial order $L$, if $x\sqleq y$, then $y$ \emph{covers} $x$, written $x\crl y$, iff $x< y \,\wedge \, \forall z\in L: (x\leq z\leq y \imply x=z \vee y=z)\}$. An \emph{interval} $[a,b]$ in $L$ is a set $[a,b]=\{x\,\vert\, a\sqleq x\sqleq b\}$, and $[a,b]$ is a \emph{prime} interval if $[a,b]=\{a,b\}$, i.e., if $a\crl b$. A \emph{covering chain} of an interval $[a,b]$ is a sequence of the form $a=a_1\crl a_2\crl\ldots \crl a_n=b$. For prime intervals $[a,b]$ and $[c,d]$, an order $\leq$ is defined by: $[a,b]\leq [c,d]$ iff $a=b\sqcap c$ and $d=b\sqcup c$.
}
%\eit
\ed

%\delete{


\section{Appendix B: Properties of Residuals}


\bdl{D.levy.str.}
A \emph{Deterministic Residual
Structure} (DRS) is a pair ${\cal R}=(A, /)$, where $A= (Ter,Red,\ar)$ 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$; and if moreover $v\not=u$,
then $u$ \emph{discards} $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 finite $P:t\doar o$ 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 if $P$ is finite and $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:
\delete{the following axiom is satisfied: (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 along $u/v$.
\ed


\bll{P.cre.res.need.} (\cite{[GK02]})
Let $\stab$ be a stable semantics of an SDRS, and let $P:t\red{u}s\doar\in\stab$. Further:

(1) Let $v'$ be a $u$-residual of $v\subt t$, and let $v$ be $\stab$-unneeded. Then so is $v'$.

(2) Let $u$ create  $v\subt s$, and let $u$ be $\stab$-unneeded. Then so is $v$.

(3) Let $\stab$ be regular, let $u\not=v\subt t$, and let
$v$ be $\stab$-needed. Then $v$ has at least one $\stab$-needed residual
in $s$.

(4) Let $\stab$ be regular. Then $\snp{P}$ is an $\stab$-needed
reduction whose length coincides with the number of $\stab$-needed steps in
$P$, and $P\seqv \snp{P}$.
\el


\begin{rem}
Note that without regularity $\snp{P}\sleq P$ need not hold in general:
Consider the DRS generated by the rewrite system $R=\{f(x)\ar
g(x,x),\,a\ar b\}$, restricted to the reduction graph of $t=f(a)$,
let $\stab_{ter}$ be the set of terms (in the reduction graph of $t$) not
containing occurrences of $a$, and let $\stab$ be the set of all
$\stab_{ter}$-normalizing reductions. Then $\stab$ is stable but not
regular since the $\stab$-unneeded step $f(a)\ar g(a,a)$ duplicates the
$\stab$-needed redex $a\subt t$, and we have for $P:f(a)\ar g(a,a)\ar
g(b,a)$ that $\snp{P}:f(a)\ar f(b)$, and $\snp{P}\not\sleq P$.
\end{rem}

\zurab{Need to include definition of DFSs as well, since it is used in the
proof of \Tr{L.proj.fam.} below.}

\section{Appendix C: Proofs}



\bproof \PLr{sleq.via.leq.}
\suf\ By \Dr{D.rel.ord.}, $P\sleq Q$ implies that $P/Q$ is $\stab$-unneeded. But $P\lleq Q+P/Q$, and we can take $P/Q$ for $Q'$.
\nec\ By \Dr{D.rel.ord.}, we need to show that $P/Q$ is $\stab$-unneeded. Suppose on the contrary that $P/Q=N'+v+N''$ where $N'$ is $\stab$-unneeded and $v$ is $\stab$-needed. By \Lr{P.cre.res.need.}.(1), $Q'/N'$ is $\stab$-unneeded, thus by \Lr{P.cre.res.need.}.(3) $v$ must have at least one ($\stab$-needed) residual under $Q'/N'$, contradicting $(P/Q)/Q'=P/(Q+Q')=\emp$.
\eproof  \\


\bproof \PLr{L.tra.fin.}
First assume that $P,Q$ and $N$ are finite. By \Lr{sleq.via.leq.}, $P\sleq Q\sleq N$ implies $P\lleq Q+Q'$ and $Q\lleq N+N'$ for some $\stab$-unneeded $Q'$ and $N'$. But $Q\lleq N+N'$ implies $Q+Q'\lleq N+N'+Q^*$ (see the figure), where $Q^*=Q'/((N+N')/Q)$ is $\stab$-unneeded. Thus $P\lleq N+N'+Q^*$ where $N'+Q^*$ is $\stab$-unneeded, and $P\sleq N$ by \Lr{sleq.via.leq.}. Thus the lemma is proved when $P,Q$ and $N$ are finite. Now let us consider the general case.  By \Dr{D.rel.ord.} and $P\sleq Q$, for any finite $P'\leq P$ there is a finite $Q'\leq Q$ such that $P'\sleq Q'$. Similarly, there is a finite $N'\leq N$ such that $Q'\sleq N'$, thus $P'\sleq N'$, implying again by \Dr{D.rel.ord.} that $P\sleq N$.
\begin{diagram}[height=1.6em,width=1.6em]
{}         & \rOnto^{N}    &  {}      &\rOnto^{N'}   &  {}  \\
\dOnto<{Q}   &          &\dOnto   &         & \dOnto_\emp     \\
{}     &\rOnto   & {}    & \rOnto  & {}   \\
\dOnto<{Q'}   &          &\dOnto  &             &  \dOnto_{Q^*}   \\
{}      &\rOnto       &  {}       & \rOnto      & {}   \\
\end{diagram}
\eproof  \\


\bproof \PLr{l.eq.sun.sun.}
Suppose on the contrary $P=P'+v+P''$, where $v$ is $\stab$-needed. Then By  \Lr{P.cre.res.need.}.(1) and \Lr{P.cre.res.need.}.(3), $Q/P'$ is $\stab$-unneeded and $v/(Q/P')$ contains at least one ($\stab$-needed) redex, contradicting $P\lleq Q$.
\eproof  \\

\bproof \PLr{L.sle.pr.res.}
It is enough to prove the lemma for finite $P,Q$. By \Lr{sleq.via.leq.}, $P\lleq Q+Q'$ for some $\stab$-unneeded $Q'$, implying that $P/N\lleq Q/N+Q^*$, where $Q^*=Q'/(N/Q)$ is  $\stab$-unneeded by \Lr{P.cre.res.need.}.(1). Hence $P/N\sleq Q/N$ again by \Lr{sleq.via.leq.}.
\eproof  \\


\bproof \PLr{L.dev.dom.fin.}
Suppose \john{in} contradiction that $w$ is the first step in $N$ that is not a residual of a redex in $U$, say $N=N'+w+N''$. Since $w$ is $\stab$-needed and $w/(U/N')$ is $\stab$-unneeded, $U/N'$ must contract a residual $w'$ of $w$, say $U/N'=P'+w'+Q'$. Thus $U=P+u'+Q$ where $P'=P/N'$ and $w'\in u'/(N'/P)\ssq u/(P\sqcup N')$ for some redex $u\in U$ (see the figure). But by the Cube Lemma, $w'\in u/(N'\sqcup P)$, thus $w'$ is a $P'$-residual of a redex in the final term of $N'$, and that latter redex must coincide with $w$ (since $w'\in w/P'$ and a redex can be a residual of at most one redex along a reduction in an SDRS) -- a contradiction.
\begin{diagram}[height=1.5em,width=1.5em]
t           &\rOnto^P  & &  \cdot       &\rTo^{u'}   & {} \\
\dOnto<{N'}  &            & &\dOnto<{N'/P}   &         &      \\
\cdot     &\rOnto^{P'}& & \cdot    & \rTo^{w'} & {}  \\
\dTo<{w}   &         & &\dTo<{w'}  &             &     \\
{}      &      & & {}      &       &  {}  \\
\end{diagram}
\eproof  \\


\bproof \PLr{L.finfin.}
By \Lr{P.cre.res.need.}.(4), we can assume that both $P$ and $Q$ are $\stab$-needed, and that $Q$ is finite, and we want to prove that $P$ is finite too. Suppose not. Since $P/Q$ is $\stab$-unneeded, there is a step $u$ of $Q$, say $Q=Q'+u+Q''$, such that $P/Q'$ contracts infinitely many $\stab$-needed redexes while $P/(Q'+u)$ contracts only a finite number of them. Let $P=P'+P''$, where $P''/((Q'+u)/P')$ is $\stab$-unneeded, let $N=P''/(Q'/P')$ and $U=u/(P'/Q')$ (see the figure). Thus we have $N\sleq U$. Hence $N'=\snp{N}\sleq U'$, where $U'$ is the set of $\stab$-needed redexes in $U$, and $N'$ is an infinite $\stab$-needed reduction by \Lr{P.cre.res.need.}.(4), contradicting \Lr{L.dev.dom.fin.}.
\begin{diagram}[height=1.5em,width=1.5em]
t           &\rOnto^{Q'}  & &  \cdot       &\rTo^{u}   & {} \\
\dOnto<{P'}  &            & &\dOnto    &         &      \\
\cdot     &\rOnto{Q'/P'} & & \cdot    & \rOnto^{U} & {}  \\
\dOnto<{P''}   &         & &\dOnto<{N}  &             &     \\
{}      &      & & {}      &       &  {}  \\
\end{diagram}
\eproof  \\


\bproof \PLr{fin.el.}
\suf\ Let $\sclas{P}$ be finite. We can assume by \Lr{L.finfin.} that $P$ is $\stab$-needed and finite. Now let $\sclas{\Phi}$ be directed and $\sclas{P}\sleq \sclas{\sjoin\Phi}$. Then $P\sleq \sjoin\Phi$, and by \Lr{L.jo.fin.joi.}, $P\sleq \sjoin\Phi[k]$ for some $k$, where $\Phi[k]\ssq\Phi$ is finite. Since $\sclas{\Phi}$ is directed, $\exists N\in\Phi.\sjoin\Phi[k]\sleq N$. Thus $\sclas{P}\sleq \sclas{N}\in \sclas{\Phi}$, which means that $\sclas{P}$ is finite in $\sefcR$.  \nec\ Let $\sclas{P}$ be finite in $\sefcR$, and let $P$ be infinite (otherwise $\sclas{P}$ is trivially finite). It is immediate from \Dr{D.mj.rel} that  $P= \sjoin \{\ip{P}{k}\vert k\in {\cal N}\}$, thus $P\sleq \sjoin \{\ip{P}{k}\vert k\in {\cal N}\}$, and clearly $\{\ip{P}{k}\vert k\in {\cal N}\}$ is directed. Hence by finiteness of $\sclas{P}$ in $\sefcR$, $P\sleq \ip{P}{n}$ for some $n$, which by definition of $\sleq$ means that $\fp{P}{n}$ is $\stab$-unneeded. Hence $\sclas{P}$ is finite.
\eproof  \\



\bproof \PLr{L.proj.lem.}
It is immediate from \Dr{D.stab.proj.} that for any redex $t\red{u}_\stab s$ in $\calR_\stab$, and redexes $v\in t$ and $w\in s$, $v/_\stab u$ is a set of redexes in $s$, and that $w$ can be the $u$-residual of at most one redex in $t$. Further, $\calR_\stab$ is non-erasing by \Lr{P.cre.res.need.}.(3), which immediately implies [weak acyclicity]. And [stability] for $\calR_\stab$ follows immediately from [stability] for $\calR$. Thus it remains to check [FD] and [AF].

[FD]: Let $U\subts t$ in $\calR_\stab$. Then $t=\sclas{P}$ for some finite initial reduction $P$ in $\calR$ ($P$ can be taken $\stab$-needed), and let $U'$ be the set of corresponding (to $U$) $\calR$-redexes in the final term of $P$. By [FD] for $\calR$, all complete $U'$-developments $Q$ end at the same term and generate the same residual relation $- / U'$. Hence any complete development of $U$ in $\calR_\stab$ ends at $\sclas{P+\snp{Q}}$. Further, since $Q\leeqv \snp{Q}+Q'$ for some $\stab$-unneeded $Q'$ in $\calR$, we have by the regularity of $\stab$ and \Lr{P.cre.res.need.} that any $\stab$-needed redex in the final term of $Q$ is the unique $Q'$-residual of exactly one $\stab$-needed redex in the final term of $\snp{Q}$ (the correspondence between the redexes in the final terms of $Q$ and $\snp{Q}$ is $1 - 1$). Hence any complete development of $U$ in $\calR_\stab$ generates the same residual relation $-/_\stab U$, and [FD] for $\calR_\stab$ follows.

[AF]: Let $P',Q'$ be initial reductions in $\calR_\stab$ ending at the same term. Then (by \Dr{D.stab.proj.}) there are $\stab$-needed reductions $P=h'(P'),Q=h'(Q')$ in $\calR$ such that $h(P)=P'$ and $h(Q)=Q'$, and $\sclas{P}=\sclas{Q}$ (since $P$ and $Q$ end at the same term). Thus it is enough to prove that for any reductions $P,Q$ in $\calR$, $P\staeq Q$ implies $h(P)\leeqv h(Q)$ in $\calR_\stab$. To this end, we first prove that:

 $(a)$ Let $P,Q$ be finite initial  reductions in $\calR$. Then $h(P/Q)=h(P)/h(Q)$.

\emph{Proof of} $(a)$: By induction on the number of multisteps in $P$ and $Q$ (it does not matter how do we group steps in $P$ and $Q$ into multi-steps). The case $P = \emp$ is trivial, so let $P=P_1+P_2$ be non-empty. Then
\begin{center}
\begin{tabular}{rcl}
$h(P/Q)$ &  $=$    & $h((P_1+P_2)/Q)$   \\
        &   $=$    & $h(P_1/Q+P_2/(Q/P_1))$   \\
        &   $=$    & $h(P_1/Q)+h(P_2/(Q/P_1))$  \\
        &   $=$    & $h(P_1)/_\stab h(Q)+ h(P_2)/_\stab (h(Q)/_\stab h(P_1))$ \\
        &   $=$    & $(h(P_1)+h(P_2))/_\stab h(Q)$  \\
        &   $=$    & $h(P_1+P_2)/_\stab h(Q)$  \\
        &   $=$    & $h(P)/_\stab h(Q)$.  \\
\end{tabular}
\end{center}
Now, by $(a)$, $P\sleq Q$ iff $P/Q$ is $\stab$-unneeded iff $h(P/Q)=\emp$ iff $h(P)/_\stab h(Q)=\emp$ iff  $h(P)\lleq h(Q)$ (in $\calR_\stab$), and the lemma follows.
\eproof \\


\bproof \PLr{L.no-erasu.}
By induction on the length $n$ of a longest covering $(t,\sqcup s_i)$-chain $P$
($n$ is finite by [FB] and K\"{o}nig's Lemma). The case $n=1$ is trivial by
[NE]. Assume (without loss of generality) that $P$ starts with $t\crl s_1$,
 let $[s_1,e_j]$ $(1\leq j\leq k)$ e allresiduals of $[t,s_i]$ in $s_1$, and
let $[s_1,o_r]$ $(1\leq r\leq l)$. Clearly, $\sqcup s_i = \sqcup e_j$. (Indeed,
$e_j \leq s_1 \sqcup s_{i_j}$ for any $j$ and some $i_j$,
by definition of residuals, thus
$\sqcup e_j \leq \sqcup s_i$; conversly, $s_i \leq e_{j_i}$ for any $i$ and
some $j_i$, thus  $\sqcup s_i \leq \sqcup e_j$.) By [LD], $e_j$ and $o_r$ are pairvise different. By the induction assumption, for any $r$, $\sqcup e_j < o_r
\sqcup (\sqcup e_j)$, thus $\sqcup e_j < (\sqcup o_r) \sqcup
(\sqcup e_j)$. Hence, by [FD], $\sqcup s_i < (s\sqcup s_1) \sqcup
(\sqcup s_i) = s \sqcup (\sqcup s_i)$. Finally, $s< s \sqcup (\sqcup s_i)$
follows immediately from $s < s \sqcup s_1$ (which holds by [NE]).
\eproof
\\




\bproof \PLr{L.red=cov.}
By indution on $n$.

\suf\ Let $[e_m, e_m ^*]$ be a residual of $[e_0,e_0 ^*]$. Then $[e_m, e_m ^*]$ is a residual of a residual $[e_{m-1}, e_{m-1} ^*]$ of $[e_m, e_m ^*]$ in $e_{m-1}$. By definition of $/_D$ and the induction \john{assumption}, $e_m ^* \leq_D e_m \sqcup_D e_{m-1} ^* \leq_D e_m \sqcup_D (e_0 ^* \sqcup_D e_{m-1}) =
e_m \sqcup_D e_0 ^*$.

\nec\ Let $e_m ^* \leq_D e_0 ^* \sqcup_D e_m$. Further, let $[e_{m-1}, e_{m-1} ^i]$ $(0\leq i \leq p)$ be all prime intervals such that
$e_{m-1} ^i \leq_D e_0 ^* \sqcup_D e_{m-1}$. By \suf\ and the induction assumption, $[e_{m-1}, e_{m-1} ^i]$ are
all residuals of $[e_{m-1}, e_{m-1} ^i]$.  If on the contrary $[e_m,e_m ^* ]$ is not a residual o any of $[e_{m-1}, e_{m-1} ^i]$, then $e_m ^* \not\leq_D e_m \sqcup_D e_{m-1} ^i$, for all $0\leq i \leq p$. Hence, by \Lr{L.no-erasu.},
$e_m ^* \not\leq_D e_m \sqcup_D (\sqcup_D e_{m-1} ^i)=$ (by \john{the induction assumption}) $=e_m \sqcup_D (\sqcup_D (e_0 ^* \sqcup_D e_{m-1})) = e_0 ^* \sqcup_D e_m$.
\eproof
%}
\\

\bproof \PTr{L.proj.fam.}
To prove that $\fami_\stab$ is a family relation on $\calR_\stab$, let us first show that $\zfami\ssq\fami_\stab$. So let $v'\zfami w'$ in $\calF_\stab$, where $v'=(\sclas{P},\sclas{P+v})$ and $w'=(\sclas{Q},\sclas{Q+w})$. Since $\fami_\stab$ is clearly an equivalence relation, it is enough to consider the case when say $w'$ is a copy of $v'$, i.e. $Q\leeqv P+N$ and $w\in v/N$ for some $N$. Then $Pv\zfami Qw$ in $\calF$, thus $Pv\fami Qw$, implying $v'\fami_\stab w'$ (by the definition of $\fami_\stab$). Now we need to check the family axioms for $\fami_\stab$.

[initial]: This is immediate by [initial] in $\calF$: any initial redexes $\emp u$ and $\emp v$ in $\calF_\stab$ are also initial redexes in $\calF$ and therefore $\emp u \not\fami \emp v$, implying $\emp u \not\fami_\stab \emp v$.

[contribution]: since we assume that the contribution relation $\contr_\stab$ of $\calF_\stab$ is defined from $\fami_\stab$ via [contribution], there is nothing to prove.

[creation]: Let $e\dored{P}_\stab t\red{u}_\stab s$ in $\calF_\stab$, let $u$ create $v\in s$, and let $P'v'\fami_\stab (P+u)v$. We need to show that $P'$ contracts a redex in the $\fami_\stab$-family of $Pu$. By the definition of $\fami_\stab$, $h'(P'v')\fami h'((P+u)v)$. By [creation] for $\calF$, $h'(P')$ contracts a redex $P''u''$ in the $\fami$-family of $h'(Pu)$, implying (by the definition of $\fami_\stab$) that $h(P''u'')\fami_\stab Pu$ (where $h(P''u'')$ is a redex contracted in $P'$), and we are done.
\eproof


\end{document}
