\documentstyle[11pt]{article}
\marginparwidth 0pt
\oddsidemargin  0pt
\evensidemargin  0pt
\marginparsep 0pt

\topmargin   0pt

\textwidth   6.5in
\textheight  8.5 in
%\def \dred {\mbox {$\,\ \rightarrow\kern-0.7em\rightarrow\ $}}
\def \doar{\mbox {$\,\ \rightarrow\kern-0.7em\rightarrow\ $}}
%\documentstyle[fullpage,11pt,amssymbols]{article}
%\input{diagrams} % Paul Taylor's Macro Package
\begin{document}
\newtheorem{thm}{Theorem}[section]
\newtheorem{lem}{Lemma}[section]
\newtheorem{cor}{Corollary}[section]
\newtheorem{ex}{Example}[section]
\newtheorem{rem}{Remark}[section]
\newtheorem{prop}{Proposition}[section]
%%%%\newtheorem{proof}{Proof}
%\newenvironment{proof}{{\it Proof:}}{{\it Q.e.d.}}
\newenvironment{akn}{\noindent{\bf Acknowledgments }}{}
\newenvironment{proof}{\noindent{\bf Proof }}{}
\newtheorem{deff}{Definition}[section]
\newcommand{\notation}{{\bf Notation }}
\newcommand{\note}{{\bf Note }}
\newcommand{\newl}{\mbox{ }\\}
\newcommand{\ar}{\rightarrow}
\newcommand{\undl}{\underline}
\newcommand{\impl}{\Rightarrow}
%\newcommand{\doar}{\twoheadrightarrow}
\newcommand{\trar}{\Rightarrow}
\newcommand{\red}[1]{\mbox{$\stackrel{#1}{\ar}$}}
\newenvironment{prsk}{\noindent{\bf Proof sketch }}{}
\newenvironment{altpr}{\noindent{\bf Alternative proof }}{}
\newcommand \inputpic[1] {\begin{center} \input{#1} \end{center}}
\newcommand{\ssq}{\subseteq}
\newcommand{\sset}{\subset}
\hyphenation{meta-var-ia-ble}
\newcommand{\vect}[1]{\mbox{$\overline{#1}$}}
\newcommand{\rpsim}{\mbox{$\stackrel{r}{\psim}$}}
\newcommand{\rpessim}{\mbox{$\stackrel{r}{\pessim}$}}
\newcommand{\ressim}{\mbox{$\stackrel{r}{\essim}$}}
\newcommand{\rsim}{\mbox{$\stackrel{r}{\sim}$}}
\newcommand{\muer}[1]{\mbox{$[{#1}]_{\mu}$}}
\newcommand{\lclas}[1]{\mbox{$[{#1}]_L$}}
\newcommand{\ines}[2]{\mbox{$\overbrace{#1}^{#2}$}}
\newcommand{\unin}[2]{\mbox{$\undl{#1}_{#2}$}}
\newcommand{\dist}[2]{\mbox{$\vert{#1},{#2}\vert$}}
\def\pessim{\prec\!\!\prec}
\def\steq{\approx_{st}}
\def\essim{\approx}
\def\psim{\prec}
\def\orth{\perp}
\def\esorth{\perp_{es}}
\def\subt{\subseteq}
%\def\lleq{\triangleleft}
%\def\lles{\triangleleft}
\def\lleq{\unlhd}
\def\lles{\lhd}
\def\leeqv{\approx_L}
\def\ind{\ddagger}
\def\hole{\circ}
\def\restr{\vert}
\def\exten{\updownarrow}
\def\zig{\simeq}




\begin{titlepage}



\thispagestyle{empty}

\title{Euclidean Reduction Spaces: Independence, Context Sharing, and
Modularity}
\author{John Glauert \hspace{.20in} Zurab Khasidashvili \\
University of East Anglia, UK }
\maketitle

\thispagestyle{empty}

\begin{abstract}
We define a {\em residual structure} or a {\em L\'evy-Klop structure} as an abstract reduction system where L\'evy's notion of strong equivalence and the zig-zag family relation is defined based on the notion of residual as primitive, using the method of commutative  diagrams due to Klop~\cite{[Kl.CRS]}. We further define the notion of {\em independence} of reductions and {\em distance} between reductions in any  L\'evy-Klop structure, which makes the latter a {\em Euclidean reduction space}. We show how a Euclidean basis at a term $t$ can be constructed so that each reduction starting from $t$ can be decomposed as a least upper bound of subreductions of directions of the basis in the corresponding upper semilattice.  We further investigate the Euclidean reduction spaces for Orthogonal Combinatory Reduction systems (OCRSs). This leads to a study of computations of components (i.e., contexts) of a term rather than subterms independently, i.e., in parallel; computations of different occurrences of a component whose corresponding subterms are not the same can also be shared. An elegant implementation of computations of terms with shared components is possible using {higher order} environments. The structure of terms in CRSs enables one to study more refined properties of the concept of independence, which cannot be captured by residual structures, using an extension of the residual notion, that of {\em descendant}. We demonstrate this by proving the {\em Essential Similarity Lemma}. Finally, we show how one can study modular properties of CRSs using concepts related to independence.
\end{abstract}


\bigskip
\subsection*{Correspondence Address}

\begin{tabbing}
John Glauert \\
School of Information Systems \\
University of East Anglia \\
Norwich NR4 7TJ England \\
\\
Email: jrwg@sys.uea.ac.uk \\
Tel: +44 603 592671 \\
Fax: +44 603 507720
\end{tabbing} 

\end{titlepage}



\section{Introduction}
 We study computation as an abstract reduction process. An {\em Abstract Reduction System (ARS)} consists of a set of {\em objects} $t,s,\ldots$, often called terms, and {\em labelled transitions} $t\red{u}s$ between objects, where $u$ is a label. Each transition is uniquely labelled. If $t\red{u}s$ and $t\red{u}s'$, then $s=s'$. Transitions between the same source and target terms may have different labels. When $t\red{u}s$, $u$ is said to be a {\em redex} of $t$, reduction of which gives $s$. A {\em reduction} is a sequence of transitions.

 A redex captures the computational notion of an atomic task. When one redex is reduced, other tasks may remain. If $t\red{u}s$, one can define a partial function, called the {\em residual} function, from redexes of $s$ to redexes of $t$. The {\em residual} concept formalises the relationship between redexes under reduction, capturing the idea of the same computation remaining to be done.  Redexes of $s$ in the domain of the function are {\em residuals} under $u$ while those not in the domain are {\em created} by $u$.
Redexes of $t$ not in the range of the function are {\em erased} by $u$. $u$ is always erased by $u$.

{\em L\'evy equivalence} formalizes the idea of reductions which do a same work. The {\em copy} relation generalies the residual concept by identifying L\'evy equivalent reductions.  The {\em family} relation is the symetric and transitive closure of the copy relation. It captures the idea of all copies of the same work. Any reduction that contracts all redexes of a given family at a time is therefore optimal, provided no {\em non-needed} families are contracted, since it avoids doing the same work twice; here {\em needed} means a step that cannot be omitted in a reduction leading to the normal form --- the value of the term.

 {\em L\'evy-Klop structures} are ARSs where all the above relations are defined using Klop's method of commutative diagrams~\cite{[Kl.CRS]}. The method is well described also in Barendregt~\cite{[Bar]} and we do not give any details here. We recall only that a {\em diagram} for co-initial reductions is constructed by joining all {\em elementary diagrams} emerging when attempting to find a common reduct of the reductions; an elementary diagram considers complete developments of pairs of redexes, reducing either redex, then all residuals of the other. 

 Our aim is to identify the conditions for independence of reduction sequences, thus identfying the potential for concurrent computation. Further, we aim for a Euclidean measure of distance between reductions, allowing us to characterise the amount of independent computation present between components of a computation before interaction is required. 


Formalization of the two notions yields a nice theory of {\em Euclidean Reduction Spaces}. It turns out that each term $t$ in a L\'evy-Klop structure has a {\em finest basis} consisting of {\em directions}, which are reductions starting from $t$; different directions do not contract needed redexes of the same family and therefore are {\em independent}; and any reduction starting from $t$ can be decomposed as a `disjoint sum' of some subreductions of the directions. The directions in a basis at $t$  contract residuals of redexes from some set of redexes in $t$ and created redexes in a way that each such redex is eventually contracted or erased.

Imposing a structure on terms in L\'evy-Klop structures yields a more refined notion of basis. In {\em Orthogonal Combinatory Reduction Systems (CRSs)}, directions are reductions {\em internal} to some {\em areas} of a term; areas consist of {\em components} which are occurrences of contexts together with corresponding bound variables. In OCRSs one can share computations of occurrences of the same components, i.e., share even {\em parts} of different but similar tasks, doing the common parts only once. This is possible using {\em higher order environments} where along with (object) variables one can assign values to {\em function} variables as well; to a function variable of arity $n$ one can assign a context (component) with $n$ holes.

In a (not necessarily orthogonal) CRS one can define also the notion of {\em projection} of a reduction starting from $t$ to an area ${\cal A}$ of $t$, whenever $P$ {\em respects} ${\cal A}$, i.e., roughly, only symbols of the area contribute to creation of redexes contracted in $P$. The projection can be defined using the notion of {\em descendants} of an area, which we introduce for this purpose. The notion captures and generalises the notion of modularity of rewrite systems (and programs). We illustrate this by proving that, similarly to TRSs \cite{[Rus]}, strong normalization is a modular property for CRSs.

The descendant relation is a generalization of the residual relation and it captures certain fine properties that the residual relation cannot. Using the descendant relation for subterms one can generalize the notion of neededness to that of {\em essentiality} which works for all subterms, not for redexes only~\cite{[rta]}. For example, as an application of the independence theory developed for OCRSs, we prove the {\em Essential Similarity Lemma}, which identifies which parts of the term will influence the `essentiality status' of its subterm --- only essential bindings in independent subterms matter.


The paper is organized as follows. In the next section, we introduce L\'evy-Klop structures and Euclidean Reduction Spaces and study their properties. In section~\ref{S.ind.crs.}, we study Euclidean Reduction Spaces of OCRSs and the descendant notion for components in CRSs. Finally, in section~\ref{S.apl.}, we apply obtained results to show that strong normalization is a modular property for CRSs with non-collapsing rules, to prove the Essential Similarity Lemma for OCRSs, and to implement context-sharing in higher order environments.






\section{Euclidean Reduction Spaces}

In this section we introduce L\'evy-Klop structures and Euclidean reduction Spaces and study its properties in an abstract setting. Note that L\'evy-Klop structures do not give an axiomatic definition of the residual relation. Such a definition that works for several (but not all)  L\'evy-Klop structures is given in Gonthier et al~\cite{[GLM]}.

The definition and some results about Abstract Reduction Systes (ARSs) can be found e.g., in \cite{[Kl.TRS]}. An ARS is a two-sorted set of objects: the set {\em Ter} of {\em terms} (ranged over by $t,s,o,e$) and the set {\em Red}  of {\em redexes} (ranged over by $u,v,w$), with two predicates $\subt: Red\times Ter$ and $\ar:Ter\times Red\times Ter$ such that for any $u\subt t$ there is exactly one $s$ such that $(t,u,s)\in\ar$ i.e., $t\red{u}s$. A {\em reduction} is a sequence $t\red{u_1}t_2\red{u_2}\ldots$. Reductions are denoted by $P,Q$. We write $P:t\doar s$ if $P$ denotes a reduction (sequence) from $t$ to $s$. $Pu$ denotes a redex $u$ in the final term of $P$. $\vert P\vert$ denotes the length of $P$.  $P+Q$ denotes the concatenation of $P$ and $Q$.

\begin{deff}\em
\label{D.levy.str.}
{\bf (L\'evy-Klop structure)}  A {\em residual structure} or a {\em L\'evy-Klop structure} is an abstract rewrite system $R$ with a {\em residual} relation for redexes (which are labels) under reductions, relations $+$ (concatenation), / (residual), $\sqcup$ (square sum), $\lleq$ (L\'evy embedding), $\leeqv$ (L\'evy equivalence or strong equivalence), and $\zig$ (zig-zag family) on reductions such that:

$\bullet$ If $t\red{u}t'\in R$ and $v$ is a redex in $t$, a set $v/u$ of {\em residuals of $v$ under $u$} is a set of redexes of $t'$ and $u/u=\emptyset$.
The set of residuals of a redex under any reduction is defined by transitivity. A {\em development} of a set $F$ of redexes in a term $t$ is a reduction $P:t\doar s$ that only contracts residuals of redexes from $F$; the development $P$ is {\em complete} if $F/P$, the set of residuals of redexes from $F$, is empty. 

$\bullet$ All developments are terminating; all  coinitial complete developments of the same set of redexes end at the same term; (that is, any {\em elementary diagram} is joinable independently of the order of contraction of residuals;) and residuals of a redex under all complete coinitial developments are the same.

$\bullet$ For any co-initial $P$ and $Q$, the {\em diagram} $D(P,Q)$ of $P$ and $Q$ can be completed by completing elementary diagrams in any order, and the constructed common reduct of $P$ and $Q$ (i.e., the right-bottom  term of $D(P,Q)$) does not depend on the particular completion. For any $D(P,Q)$, the reduction corresponding to the right side of $D(P,Q)$ is called the {\em residual of $P$ under $Q$} (the emply steps are omitted),  notation $P/Q$, and the reduction corresponding to the bottom side of $D(P,Q)$ is called the {\em residual of $Q$ under $P$}.

$\bullet$ $+$ is the {\em concatenation} relation on reductions; for any co-initial $P$ and $Q$ one defines $P\sqcup Q=P+Q/P$, $P\lleq Q$ iff $P/Q=\emptyset$, and $P\leeqv Q$ iff $P\lleq Q$ and $Q\lleq P$.

$\bullet$ Although $D(P,Q)$ is defined for finite reductions, $P/Q$ can be defined also if $P$ is infinite as a reduction whose initial parts are residuals of initial parts of $P$ under $Q$. If $P$ is a one step reduction $u$ and $Q$ is infinite, then we define $u/Q=\emptyset$ if $u/Q'=\emptyset$ for some initial part of $Q$. If at least one of $P$ and $Q$ is infinite, then we define $P\lleq Q$ or $P/Q=\emptyset$ if for any redex $v$ contracted in $P$, i.e., if $P=P_1+v+P_2$, $v/(Q/P_1)=\emptyset$.


$\bullet$ The following equations hold (they can easily be derived from the above items~\cite{[Bar]}): 
%(and $P\lleq P'$ and $Q\lleq Q'\Rightarrow P\sqcup Q\lleq P'\sqcup Q'$ ???).

 (1) $P+\emptyset=\emptyset+P=P,\,\,\,P+(Q+Q')=(P+Q)+Q'$; 

  (2) $(P_1+P_2)/Q\leeqv P_1/Q+P_2/Q,\,\,\,P/(Q_1+Q_2)\leeqv (P/Q_1)/Q_2$;

  (3) $P/\emptyset=P,\,\,\,\emptyset/P=\emptyset\,\,\,P/P=\emptyset$;

  (4) $P\leeqv P',Q\leeqv Q'\Rightarrow P+Q\leeqv P'+Q',\,\,P+Q\leeqv P+Q'\Rightarrow Q\leeqv Q',\,\,P\leeqv\emptyset\Rightarrow P=\emptyset$;

   (5) $P\sqcup Q\leeqv Q\sqcup P$.
 
$\bullet$ For any co-initial reductions $P$ and $Q$, the redex $Qv$ (read as $v$ {\em with history} $Q$), is called a {\em copy} of a redex $Pu$ if $P\lleq Q$, i.e.,  $P+Q/P\leeqv Q$, and $v$ is a $Q/P$-residual of $u$. The {\em zig-zag} relation $\zig$ is the symmetric and transitive closure of the copy relation. A {\em family} relation is an equivalence relation among redexes with histories containing the zig-zag relation. However, below by family we always mean the zig-zag family relation.
\end{deff}


In fact, a L\'evy-Klop structure is a {\em L\'evy spectrum} as pointed out briefly in \cite{[Kl.TRS]} defined using Klop's method of commutative diagrams, with an extra relation --- the family relation, due to L\'evy~\cite{[levy]}. We choose this way of defining L\'evy-Klop structures because it is clear and allows an easy definition of orthogonality of reductions in non-orthogonal systems. It is well known that the $\lambda$-calculus~\cite{[levy]}, orthogonal TRSs~\cite{[H.L.]}, OCRSs~\cite{[Kl.CRS]}, and Orthogonal Term Graph Rewriting Systems~\cite{[KKSdV]} form L\'evy-Klop structures (any set of co-initial reductions in the last is moreover an {\em event structure}~\cite{[Wsk]}). Examples of other  L\'evy-Klop structures are given in subsection~\ref{SS.ESL.}.







\begin{deff}\em
$\bullet$ Let $P=P'+u+P''$ be a reduction in a L\'evy-Klop structure. We call $u$ $P$-{\em needed} if there is no reduction strongly equivalent to $u+P''$ that does not contract residuals of $u$ and erases it. If $Q$ is co-initial with $P$, then we call $u$ {\em $Q$-needed} iff it is $Q/P'$-needed. We call $P$ {\em $Q$-needed} if each redex contracted in $P$ is. % We call a family contracted in $P$ (i.e., a family whose member is contracted in $P$) {\em $Q$-needed} iff at least one of its contracted members are $Q$-needed.


$\bullet$ We call $P$ and $Q$ {\em cross-needed} if $P$ is $Q$-needed and $Q$ is $P$-needed. We call $P$ {\em self-needed} if it is cross-needed to itself, i.e., if it is $P$-needed. We call a set of co-initial reductions {\em cross-needed} if the reductions are pairwise cross-needed. % We call any self-needed reduction strongly equivalent to $P$ a a self-needed variant of $P$.
\end{deff}



It is easy to see that if $P\leeqv Q$, $P$-neededness  coincides with $Q$-neededness. So one can speak about $\lclas{P}$-neededness, where $\lclas{P}$ is the L\'evy equivalence class of $P$. It is easy to see that standard reductions are self-needed. Note that a redex in a term $t$ is needed \cite{[levy],[Mar]} iff it is  $P$-needed for any reduction $P$ starting from  $t$. 

% An interesting fact about self-neededness is the following: if $Q:t\doar s$, then any {\em $Q$-needed strategy} (which contracts $Q$-needed redexes only) is correct for computation of $s$. For example, if $P$ is the lazy-reduction from a term $t$ to its head-normal form $s$, then all $P$-needed reductions are correct for computing $s$. Similarly, for any strategy $F$, one can define an $F$-needed strategy $G$ to be a strategy that constructs only (or all) reductions that are $P$-needed for some $P$ constructed by $F$. Then $G$ constructs the same normal forms (finite or infinite) as $F$. (Here as an infinite normal form one can consider the L\'evy equivalence class of an infinite reduction.)





\begin{deff}\em
{\bf (Euclidean reduction space)} Let $R$ be a L\'evy-Klop structure.


$\bullet$ We call a set $\{P_i\}$ of co-initial $R$-reductions {\em independent} if there is no $i$ such that $P_i\lleq\sqcup_{i\not= j} P_j$ and no $u\subt t$ whose $P_j$-needed residual is contracted in $P_j$ for at least two $j$'s.

$\bullet$  We call a set $\{P_i\,\vert\, i\in\Gamma\}$ of $R$-reductions starting from a term $t$ a {\em basis} of $R$ at $t$ if $P_i$ are independent and, for any reduction $Q:t\doar s$, one has $Q\lleq\sqcup P_i$.


$\bullet$  We call a basis ${\bf B_1}=\{P_i\}_{i\in I}$ {\em a refinement} of a basis ${\bf B_2}=\{P'_j\}_{j\in J}$ if $\forall i\exists M_i\ssq J:\,\,P_i=\sqcup_{j\in M_i}P'_j$ and there is at least one $i$ such that $M_i$ contains more than one element. We call a basis {\em finest} if it does not have a refinement.


$\bullet$ The {\em distance} $\dist{P}{Q}$ between co-initial reductions $P$ and $Q$ is the number of families whose member redexes are either contracted  in $P$ and are $P$-needed or are contracted in $Q$ and are $Q$-needed (but not in both).


$\bullet$ We call a L\'evy-Klop structure with a finest basis at each term  and the metric defined as above a {\em Euclidean reduction space}.
\end{deff}
 

For any $P:t\doar s$, let us call a {\em (self-needed) family-completion} $CP(P)$ ($CP_s(P)$) of $P$ a reduction obtained from $P$ by contracting residuals of ($P$-needed) redexes contracted in $P$. $P$ is {\em (self-neededly) family complete} if $P=CP(P)\,\,(P=CP_s(P))$. (The family-completion notion is due to L\'evy~\cite{[levy]}.)

In the above definition, we need to consider self-needed redexes to ensure that the distance between  reductions and the independence of reductions does not depend upon a choice of reductions in their strong equivalence classes or on the  self-essential completion of reductions. One might think that more appropriate would be to consider $P\sqcup Q$-needed redexes only. The following example shows that the distance would not be a metric. Indeed, take $t=Kx\omega, \, P:t\red{\omega}t\red{\omega}t\red{\omega}t\red{\omega}t,\, Q:t\red{\omega}t,$ and $P':t\red{\omega}t\red{\omega}t\red{\omega}t\red{\omega}t\red{K}x$. Then $\dist{P}{Q}=3$ and $\dist{P}{P'}=\dist{P'}{Q}=1$.


%For any element $l$ in an upper semilattice $L$, let the set $L'\,\vert\,l'\lleq l,l'\in L$ be the {\em cone} of $l$. It is easy to see that a subset $\{l_i\}\ssq L$ is independent iff the cones of $l_i$ do not overlap and there is no $i$ such that $l_i\lleq \sqcup_{i\not= j}l_j$. Further, if $l$ is the supremum of $L$ and $\{l_i\}\subseteq L$ is an independent subset such that $\sqcup_i l_i=l$, then $\{l_i\}$ is a basis of $L$. Moreover, if there is no $i$ and no $\{m_j^i\}\subseteq L$ such that $\sqcup_j m_j^i=l_i$ and $\{m_j^i\}$ contains more than one element at least for one $i$, then $\{l_i\}$ is a finest basis of $L$.




\begin{deff}\em
$\bullet$ We call co-initial reductions {\em family-disjoint} if they  do not contract redexes from a same family.

$\bullet$ We call finite reductions $P$ and $Q$ {\em quasi-independent} if all $P\sqcup Q$-needed new redexes in  terms of $D(P,Q)$ are residuals of  redexes from the  terms of $P$ and $Q$. Co-initial infinite reductions are quasi-independent if all their initial parts are so.
\end{deff}
%


Disjointness of co-initial reductions does not imply independence:  $u$ and $v=(\lambda x.y)u$ are disjoint, but $u\lleq v$. Independence does not imply disjointness either; consider for example the modified example from L\'evy~\cite{[le80]}: take $t=(\lambda x.K_a(xY))K_b$ where $K_a=\lambda x.a$, $K_b=\lambda x.b$, and $Y=(\lambda x.f(xx))(\lambda x.f(xx))$ and consider the reductions $t\ar K_a(K_bY)\ar K_a(K_b(fY))\ar K_ab$ and  $t\ar (\lambda x.K_a(x(fY)))K_b\ar (\lambda x.a)K_b$. However,  cross-needed co-initial reductions are independent iff they are disjoint. 
%In particular, reductions of a basis are cross-needed and family-complete, hence disjoint. 
Further, one can show that  the upper semi-lattice corresponding to any L\'evy-Klop structure of cross-needed reductions is a complete lattice.


\begin{deff}\em
\label{D.cov.red.}
Let $t$ be a term in a  L\'evy-Klop structure, let $P$ be a reduction starting from $t$,  and let $F$ be a set of redexes in $t$. 

$\bullet$ We call $P$ {\em internal} to $F$ or just an {\em $F$-reduction} if it does not contract residuals of redexes in $t$ that are not in $F$ (i.e., $P$ contracts only residuals of redexes from $F$ and created redexes).

$\bullet$ Let $P:t\ar t_1\ar\ldots$ and $u\subt t_i$. Then $u$ is called {\em secured} in $P$~\cite{[Kl.TRS]} if there is $j>i$ such that $u$ does not have residuals in $t_j$. We call an $F$-reduction $P$ {\em $F$-complete} if each redex from $F$ and each created redex in $P$ is secured.

$\bullet$ We call an $F$-reduction $P$ {\em strongly cofinal for $F$} or {\em strongly $F$-cofinal} if, for any $F$-reduction  $Q$ starting from $t$, $Q\lleq P$.

$\bullet$ We call $P$  a {\em direction} if it is $F$-cofinal for some set $F$ of redexes in $t$ and is quasi-independent from any reduction starting from $t$.

$\bullet$ We call $F$ {\em independent} if any strongly $F$-cofinal $F$-reduction is a direction for $F$.

$\bullet$ Let $F_i$ with $i\in I$ be nonempty sets of redexes in $t$ such that $\cup_iF_i$ contains each redex of $t$ and $F_i\cap F_j=\emptyset$ when $i\not= j$. Then we call the set $\Im=\{F_i\}_{i\in I}$ a {\em (redex-)covering} of $t$. We call $\Im$ an {\em independent covering} if each $F_i$ is independent.
\end{deff}




It is easy to see that if $F_1$ and $F_2$ are independent redex sets in $t$, in an ARS, then so are $F_1-F_2$, $F_2-F_1$, $F_1\cup F_2$, and $F_1\cap F_2$. Therefore there is exactly one finest covering of $t$, and any set of directions related to the elements of the finest covering (and only such a set of reductions starting from $t$) is a finest  basis at $t$. Further, one can show that an $F$-reduction $P$ is strongly $F$-cofinal iff it is $F$-complete. (Recall that if each redex in a reduction $P$ is secured then $P$ is cofinal, but not conversly~\cite{[Kl.CRS]}).



\begin{deff}\em
Let $t$ be a term in a L\'evy-Klop structure $R$, let $F$ and $F'$ be complimentary  sets of redexes in $t$, and let $P:t_0\red{u_0}t_1\red{u_1}\ldots$. The notions {\em $P$ self-neededly respects $F$}  and the {\em restriction of $P$ to $F$}, written $P\vert(F)$, are defined  by induction on $\vert P\vert$ as follows. If $\vert P\vert=0$, then $P$ respects $F$ and $P\vert(F)=\emptyset$. Now let $P=P'+u$ and let $P'$ respect $F$. Assume that  $P'\vert(F)$ and $P'\vert(F')$ are defined as family-complete reductions such that $CP(P')=P'\vert(F)\sqcup P'\vert(F')$. If $u$ does not have a residual in the final term of $CP(P)$, then we say that $P$ self-neededly respects $F$ and $F'$; and define $P\vert(F)=P'\vert(F)$ and $P\vert(F')=P'\vert(F')$. Otherwise, let $u'$ be a residual of $u$ in the final term of $CP(P')$. Then we say that $P$ self-neededly respects $F$ and $F'$ if $u'$ is a residual of such a redex $u''$ that is either in the final term of $P'\vert(F)$ and $P'\vert(F)+u''$ is still internal to $F$, or in the final term of $P'\vert(F')$ and $P'\vert(F')+u''$ is internal to $F'$. In the first case, we define $P\vert(F)=P'\vert(F)+Q$ and $P\vert(F')=P'\vert(F')$, there $Q$ is a complete development of the redexes (in the final term of $P'\vert(F)$) in the same family as $u''$, and likewise in the second case. So we have $CP(P)=P\vert(F)\sqcup P\vert(F')$ and $P\vert(F)$ and $P\vert(F')$ are family-complete reductions, hence the definition is correct.
\end{deff}




\begin{thm}\em
\label{T.dec.thm.}
{\bf (Decomposition Lemma)} Let $\Im=\{F_i\}_{i\in I}$ be a redex-covering of a term $t$ in a  L\'evy-Klop structure $R$.

$\bullet$ Let $P_i$ be internal to $F_i$. Then $P=\sqcup_iP_i$ respects $\Im$ and $P\vert(F_i)=P_i$.

$\bullet$ Let  $P$ be a reduction starting from $t$ that respects $\Im$. Then $CP(P)\leeqv\sqcup_iP\vert(F_i)$; if $\{F_i\}$ is an independent covering, then the latter equation is valid for any $P$.

$\bullet$ If $P_i$ is an $F_i$-direction for a covering  $\{F_i\}$ respected by $P$, then $CP(P)\lleq\sqcup_iP_i$. Moreover, there are reductions $P_i'\lleq P_i$ such that $CP(P)\leeqv\sqcup_iP_i'$; if $\{F_i\}$ is an independent covering, then $B=\{P_i\}_i$ is a basis at $t$ and the equations are valid for any $P$.

$\bullet$ Let $\Im$ be the finest and independent, and let $\Im'=\{F_i\}_{i\in J\ssq I}$ contain all $F_i$ that contain at least one needed redex. Then $P_i$ with $i\in J$ are optimal (with respect to the number of contracted families) $F_i$-complete reductions iff $P=\sqcup_iP_i$ is an optimal normalizing reduction starting from $t$.
\end{thm}



Note that, for any $P:t\doar s$ and any new redex $u\subt s$, the smallest reduction needed to create $u$ (the {\em extraction} of $Pu$~\cite{[le80]}) is internal to some finest independent set $F$ of redexes in $t$, since any redex created by $P$ is created by its restriction to $F$.









\section{Independence in Combinatory Reduction Systems}
\label{S.ind.crs.}


In this section, we study the independence notion in CRSs. The structure emposed on terms and reductions allow us to refine the results of the previous section. This study leads to a study of computations of components rather than subterms and of (higher order) substitutions for function as well as object variables.

{\em Combinatory Reduction Systems} have been introduced in Klop~\cite{[Kl.CRS]}
to provide a uniform framework for reductions with substitutions (referred to also as higher order rewriting) as in the $\lambda$-calculus and
its extensions~\cite{[Bar]}. Several other formalisms have been introduced later. We refer to  Klop et al.~\cite{[kor]} for further information. 


Our syntax \cite{[OCRS]} is closer to the syntax of $\lambda$-calculus and First Order Logic. The alphabet contains (object) variables, function and quantifier symbols, and function variables. Quantifiers may be {\em partial}, that is, they may bind variables only in some of the arguments. Patterns of left-hand and right-hand sides of rules in CRSs may have arbitrary shape, {\em object metavariables} must be bound, and right-hand sides may contain any number of, sometimes nasted, {\em metasubstitutions}. For example, the $\beta$-rule is written as $\beta: Ap(\lambda aA,B)\ar(B/a)A,$ where $a$ is an object metavariable to be instantiated by a variable and $A$ and $B$ are term-metavariables to be instantiated by terms.  The expression $(B/a)A$ is a metasubstitution, and its instance $(t/x)s$ denotes the result of
substitution of the term $t$ for $x$ in the term $s$.  To express ``pure''
substitutions we use $S$-reduction rules $S^{n+1}a_{1}\ldots a_{n}A_{1}\ldots A_{n}A_0\ar(A_{1}/a_{1},\ldots,A_{n}/a_{n})A_0,\,\,\,n=1,2,\ldots$,
where $S^{n+1}$ is an {\em operator sign of substitution}, which binds free variables only in the last argument. 

 We do not require that term metavariables in the right-hand sides of rules necessarily occur in the left-hand sides. If a rewrite step $u\ar s$, where $u$ is a redex, introduces fresh free variables in $s$, then the corresponding step in a context $C[\,\,]$ (which may bind free  occurrences of variables of $u$ in $C[u]$) requires renaming of binding variables in $C[\,\,]$ to avoid bindings of fresh variables of $s$ in $C[s]$. Below we ignore questions relating to renaming of bound variables.
%



Any CRS $R$ can be split into a ``first order part'' $R_f$, which delays substitutions as $\undl{S}$-redexes, and a ``substitution part'' $\undl{S}$, which makes substitutions (underlining is only used to distinguish created $S$-redexes from other ones). For example, a $\beta$-reduction step $Ap(\lambda x\,t,s)\ar (s/x)t$ expands to a $\beta_f$-reduction step $(\lambda x\,t)s\ar\undl{S}x\,s\,t$ and an $\undl{S}$-step $\undl{S}x\,s\,t\ar (s/x)t$. The notion of {\em expansion} generalizes by transitivity to reductions with $0$ or more steps.


Let $t\stackrel{u}{\ar} s$ be an $R_f$-reduction step and let $e$ be the contractum of $u$ in $s$.  For each argument $o$ of $u$ there are $0$ or more arguments of $e$. We call them ($u$-){\em descendants} of $o$. Correspondingly, subterms of $o$ have $0$ or more {\em descendants}.  By definition, the {\em descendant} of each pattern-subterm of $u$ is $e$. It is clear what is to be meant by {\em descendants} of a subterm that is not in $u$. In an $S$-reduction step $C[S^{n+1}x_1\ldots x_n\,t_1\ldots t_nt_0]\red{u}C[(t_1/x_1,\ldots,t_n/x_n)t_0]$, the argument $t_i$ and subterms in $t_i$ have the same number of descendants as the number of free occurrences of $x_i$ in $t_0$. All subterms of $t_0$, including free occurrences of
$x_1,\ldots,x_n$, have exactly one descendant. The descendant  of the contracted redex $u$ itself is its contractum. The notion of {\em descendant}  extends by transitivity  to arbitrary reductions. If $P$ is an $R$-reduction, then $P$ descendants are defined to be the descendants under the expansion of $P$.





We call the co-initial reductions $P:t\doar s$ and $Q:t\doar e$ {\em strictly
equivalent} (written $P\steq Q$) if $s=e$ and $P$-descendants and
$Q$-descendants of any subterm of $t$ are the same in~$s$ and~$e$.

%
The definition of {\em orthogonality} in CRSs is similar to the case of TRSs:  the rules do not introduce new term-metavariables, are left-linear, and in no term redex-patterns can overlap.


We call a {\em component} of a term an occurrence of a context, which is the {\em main part} of the component, together with the occurrences of variables bound by the (quantifiers occurring in the) context; call an {\em area} a set of occurrences comprising of disconnected non-overlapping components; call a(n {\em area-)covering} of a term $t$  a set of non-overlapping areas covering each occurrence of $t$. To define the notion of {\em descendant} of an area we again consider $R_f$ steps and $\undl{S}$-steps; the precise definition is subtle, and here we only give a rough idea. If $s=C[s_1,\ldots,s_n]$ is the corresponding subterm of the main part  $C$ of a component in $t$, then a {\em main descendant*} of $C$ is a descendant of $s$ with the `corresponding' descendants of $s_1,\ldots,s_n$ removed (the notion of `corresponding' descendants can be made precise by introducing {\em indexes} of descendants). The descendant* of a bound variable of a component is its descendant if no substitution for it happens during the step, and is the area corresponding to the subarea of the substituted argument otherwise. The {\em descendant} of an area ${\cal A}$ is the area comprising occurrences in descendants* of the main parts and bound variables of components of ${\cal A}$ (the descendants* of main arguments of different components may form the main part of a single component in the descendant area,  i.e., new connections can emerge).

Now the notions  $P$ {\em self-neededly respects} an area ${\cal A}$ and the {\em restriction} $P\vert({\cal A})$ of $P$ to ${\cal A}$ are defined in orthogonal CRSs (OCRSs) similarly to the abstract case; the counterparts of the notions introduced in Definition~\ref{D.cov.red.}  are also defined similarly.  Now the statement analogous to Theorem~\ref{T.dec.thm.} can be proved; we refer to it again as the Decomposition Lemma. 
%or be derived from it since one can show that, for any (independent) set $F$ of redexes in $t$ there is a component $C$ in $t$ such that a reduction $P$ starting from $t$ respectively respects, is internal, or is external to $F$ iff it is so to $C$. 


A more refined notion than the one of restriction, the notion of {\em projection} of a reduction $P$ to an area, can be defined for all CRSs. First, for any term $t=\ldots f(s_1,\ldots,s_n)\ldots$, containing an occurrence $f$ of an $n$-ary function variable,  and a context $C$ with $n$ holes, the {\em replacement} of $f$ by $C$ is the term $t'=\ldots C[s_1,\ldots,s_n]\ldots$. The result $t\theta$ of a replacement $\theta$ of several occurrences of function and variable occurrences in $t$ is defined similarly (different occurrences of a same variable may be replaced by different contexts).  We call a redex $u\subt t\theta$ {\em orthogonal} to $\theta$ (written $u\orth\theta$) if the pattern of $u$ does not overlap with the substituted components. We call $t$ and $\theta$ {\em orthogonal} if $\theta$ is orthogonal to any redex with the pattern not inside the substituted components. 

Further, if $t$ is a term in a CRS $R$ and ${\cal A}$ is an area in $t$, then the complement of ${\cal A}$ is itself an area, say ${\overline{\cal A}}$. One can replace in $t$ the main part of each component of ${\overline{\cal A}}$ with a subterm of the form $f(x_1,\ldots,x_n)$, where $f$ is a fresh function variable, and $x_1,\ldots,x_n$ is the multiset of variables representing the occurrences bound by the replaced component. We call such a term $t_{{\cal A}}$ a {\em completion} of ${\cal A}$ with respect to $t$. Now, for any reduction $P:t_1\red{u_1}t_2\red{u_2}\ldots$ one can define the notion $P$ {\em respects} ${\cal A}$ and the {\em projection}  $Q:s_1=t_{1{\cal A}}\red{v_1}s_2\red{v_2}\ldots$ of $P$ to ${\cal A}$ by induction on $\vert P\vert$ in such a way that  there are higher order replacements $\theta_i$ for occurrences of the fresh function variables in $s_i$ such that  $s_i\theta_i=t_i$, $u_i\orth\theta_i$, and $u_i$ and $v_i$ are the corresponding occurrences of $t_i$ and $s_i$. (The projection is defined uniquely up to renaming of occurrences of function variables.) 

% One can show that ${\cal A}$ is {\em independent} if it is respected by any reduction starting from $t$. Further, if the corresponding subterm $s=C[s_1,\ldots,s_n]\subt t$ of a component $C$ is independent in $t$ and $s_i$ are independent in $s$, then $C$ is independent in $t$. The convrse holds if $C$ is not collapsing or no collapsing creation is possible in $R$. So one can obtain splitting of a term into (finest) independent components by finding (all) its independent subterms. 












\section{Applications}
\label{S.apl.}

\subsection{Independence and modularity}
\label{SS.mod.}

In this subsection, we generalize a theorem of Rusinowitch~\cite{[Rus]}, stating that strong normalization is a modular property for non-collapsing TRSs. (Right-hand sides of collapsing rules in CRS do not contain function or quantifier symbols; for example, the $\beta$-rule is a collapsing rule.) We hope that the problems with collapsing rules can be settled similarly to the first order case.


\begin{thm}\em
Let $R_1$ and $R_2$ be strongly normalizing CRSs with no collapsing rules. Then the disjoint union $R=R_1\bigoplus R_2$ of $R_1$ and $R_2$ is strongly normalizing.

\begin{prsk}
Any term $t$ in $R$ can be decomposed into two areas ${\cal A}_1$ and ${\cal A}_2$ with symbols from $R_1$ and $R_2$, respectively. Then, since $R_1$ and $R_2$ are non-collapsing, any reduction starting from $t$ respects both ${\cal A}_1$ and ${\cal A}_2$. Therefore, if $t$ has an infinite $R$-reduction, then its projection on at least one of $t_{{\cal A}_1}$ and $t_{{\cal A}_2}$ is an infinite $R_1$ or $R_2$-reduction, respectively.
\end{prsk}
\end{thm}








\subsection{Essential Similarity Lemma}
\label{SS.ESL.}

In this subsection, we generalise the Essential Similarity Lemma~\cite{[pti]}, which identifies which parts of a term influence essentiality of its subterms, to all OCRSs.

Let us call redexes $u$ and $v$ in a term of a CRS {\em orthogonal} if their patterns do not overlap. Then the residual relation is defined similarly to the case of OCRSs and the elementary diagrams of $u$ and $v$  {\em strictly} commute. Now, we call co-initial reductions $P$ and $Q$ {\em orthogonal}, written $P\orth Q$, if the diagrams for $P$ and $Q$ are well defined, i.e., all the elementary diagrams to be joined are orthogonal, and construction of diagrams terminate independently from the order in which residuals are contracted in the elementary diagrams. Therefore one can prove the following {\em Strict} form of the  Church-Rosser theorem:  for any orthogonal $P$ and $Q$, $P+Q/P\steq Q+P/Q$.




 We call a subterm $s$ in $t$ {\em essential} (written $ES(s,t)$) if $s$ has at
least one descendant under any reduction starting from $t$ and call it {\em
inessential} (written $IE(s,t)$) otherwise \cite{[rta]}.
The notion of essentiality is a generalization of the notion of {\em
neededness} \cite{[levy],[Mar]} in a way that it works not only for redexes, but for all subterms, bound variables in particular. We call a subterm $s$ of a term $t$ {\em essentially independent} if the descendants of $s$ and its subterms under any reduction starting from $t$ never appear as pattern-subterms of essential new redexes.



It is easy to see that if $e\subt s\subt t$, then $ES(e,t)$ implies $ES(e,s)$ and $ES(s,t)$. One can show that the converse is also valid if $s$ is independent in $t$.

\notation  For any $s\subseteq t$, $BV(s)$ (resp. $EBV(s)$) denotes
the set of (essential) free occurrences of $s$ bound 
by quantifiers that are outside $s$.




%
\begin{lem}\em 
\label{L.ess.sim.lem.}  
({\bf Essential Similarity Lemma})
Let $s=C[s_1,\ldots,s_n]$, $t=C[t_1,\ldots ,t_n]$ and let $EBV(t_i)=EBV(s_i)\,(1\leq j\leq k)$, where 
$s_1,\ldots ,s_k$ are essential and essentially independent in $s$, subterms $s_{k+1},\ldots ,s_{n}$ are inessential in $s$, and $t_1,\ldots,t_k$ are essentially independent in $t$. If $s'$ and $t'$ are any corresponding subterms in $s$ and $t$  (that are outside of the replaced subterms), then $ES(s',s)$ iff $ES(t',t)$.

\begin{prsk}
Let $IE(s',s)$. Then there is a reduction $P'$ that erases $s',s_{k+1},\ldots ,s_{n}$. Since each redex whose pattern-subterm is a descendant of a subterm of some of $s',s_{k+1},\ldots ,s_{n}$ is inessential, there is a reduction $P$ that erases $s'$ and is external to $s_{k+1},\ldots ,s_{n}$, hence respects the decomposition $s=C[s_1,\ldots ,s_n]$. Further, let $P_i=P\vert(s_i)$, and $Q=P\vert (C)$. By the Decomposition Lemma, $CP(P)=(\sqcup_iP_i)\sqcup Q$. Let the $\sqcup_iP_i$-reduct of $s$ has the form $s^*=C[s^*_1,\ldots ,s^*_n]$. Then, by the strict Church-Rosser theorem, the corresponding subterm $s'^*$ of $s'$ (i.e., the $\sqcup_iP_i$-descendant of $s'$) does not have $Q^*=Q/(\sqcup_iP_i)$-descendants. Let $Q_i:t_i\doar t_i^*$ be reductions that erase all inessential variables in $t_i$ and hence $EBV(s_i)=EBV(s_i^*)=BV(s_i^*)$. Let $t^*=C[t^*_1,\ldots ,t^*_n]$ and let $t'^*$ be the corresponding subterm of $t'$ in $t^*$. Obviously, $t_1^*,\ldots,t_n^*$ are independent in $t^*$.  Let $R'=\{r_i:s^*_i\ar t^*_i\,\vert\,i=1,\ldots,n\}$, and let $Q':s^*\doar t^*$ be an $R'$-reduction that rewrites all the $s^*_i$'s to $t^*_i$'s using the rules $r_i\in R'$; such an $R'$ exists iff $BV(t^*_i)\ssq BV(s^*_i)$, and the latter is the case since $BV(t_i^*)=EBV(t_i)=EBV(s_i)=EBV(s_i^*)\ssq BV(s_i^*)$. Since $Q'$ is internal to $C$ and $Q^*$ is external to it, $Q'\orth Q^*$. Hence, by the strict Church-Rosser theorem, $Q'+Q^*/Q'\steq Q^*+Q'/Q^*$. Since $s'^*$ does not have $Q^*$-descendants, $t'^*$ does not have $Q'/Q^*$-descendants. Therefore, $IE(t',t)$.
\end{prsk}
\end{lem}

%
The lemma in particular allows us to define, for any OCRS $R$, the {\em essential substructure} $R_{es}$ of $R$ as an ARS whose terms are equivalence classes of terms of $R$ modulo replacement of inessential subterms and the reduction relation is the one induced by $R$. Then one can check that the latter is a L\'evy-Klop structure. (So are any set of orthogonal reductions closed under $+$ and $/$ (and hence $\sqcup$) and its essential substructure.) Further, one can define in an OCRS $R$ notions such as {\em essential distance} between co-initial reductions $P$ and $Q$, {\em essential independence} of a set of co-initial reductions $\{P_i\}$, {\em essential basis} at a term, etc. Then the essential distance between $P$ and $Q$ coincides with the distance between the corresponding reductions in $R_{es}$, $\{P_i\}$ are essentially independent iff the corresponding reductions in $R_{es}$ are independent, etc.




\subsection{Computations in higher order environments}

A term in an OCRS may contain occurrences of a component while the corresponding subterms of the different occurrences of the component may be different subterms; therefore sharing of the subterms is not possible. In this case one can compute some completion of the component and use the value for each occurrence. If ${\bf C}$ is an independent decomposition of $t$, then $t$ has a normal form iff the completion with respect to $t$ of each essential area of ${\bf C}$ has a normal form. Whether a component (an area) is independent is only decidable in {\em persistent} OCRSs where only restricted kinds of redex creation are possible, but persistent systems are Turing incomplete~\cite{[pti]}. Moreover,  shared components need not be independent. Therefore independent computation of shared subterms compute a term only to a certain extent, and unsharing is necessary from time to time; unsharing must be (in general) made randomly since a normalizing term may have a decomposition where none of the components are so (for example, take $t=Ap(\lambda y.Ap(\lambda z.Ap(z,\Omega),\lambda x.Ap(y,\Omega),\lambda x''.y'')$ and the decomposition $t=C[C']$, where $C[\,\,]=Ap(\lambda y.Ap(\lambda z.Ap(z,\Omega),[\,\,],\lambda x''.y'')$ and $C'=\lambda x.Ap(y,\Omega)$). In particular, the following {\em chaotic} strategy is normalizing: given a term in an OCRS $R$, split it into non-overlapping components without destroying redexes; compute each component independently using the parallel outermost strategy; stop occasionally; using the current values of the components restore the intermediate result of computation of $t$. Compute the obtained term in the same way and so on, as long as possible. Of course, it is better not to split subterms with high degrees of independence (when an analysis assessing the independence degrees of subterms can be made; methods for analyzing degrees of independence is a subject of future work).


This unpleasant situation can be resolved by formalizing sharing of components in {\em higher order environments} in a very much similar way as is done in the ordinary case: along with binding subterms to variables in an environment one can bind components to function variables. For example, the term $C[f(g((a),g'(b)),f(g(c),g'(d))]$, where the functions $f,g$ and $g'$ are subject to computation, can be represented as $C[F(a,b),F(c,d)]\{F(\circ_1,\circ_2)=f(g(\circ_1),g'(\circ_2))\}$. In strongly sequential systems, where one step normalizing strategies are feasible, the computation of a topmost component that looks in the environment while looking for a strongly needed (essential), i.e., an index, redex is feasible as well. Moreover, computations of the components bound to variables in the environment  can be run independently (in parallel) with the computation of the topmost component. Correctness of such an implementation follows from correctness of the index strategy, as well as from correctness of the chaotic strategy, since the computation does unsharing always when it is necessary to contract the counterpart of a needed (more precisely, an index) redex of the term which (on any given stage) the environment represents. For example, 


\begin{thm}\em
Lazy computations of $\lambda$-terms in higher order environments are correct for computing head-normal forms.
\end{thm}



\section{Conclusions and future work}



According to L\'evy's approach to optimality, a reduction is optimal if it contracts only needed redexs and shares computations of redexes in the same family. But all the redexes in the initial term are in different families, thus no `initial' sharing is made in it. Development of an optimality theory with initial component-sharing and its implementation, possibly using higher order environments, seems to be a promising, though difficult, direction for future research.

The Essential Similarity Lemma shows that the residual structure is not rich enough to capture finer properties of subterms and components. We expect that the {\em descendant} structure can be defined having the notion of {descendant} as a primitive, which will enable one to prove e.g., properies of
essential and independent components in an abstract way.

In subsection \ref{SS.mod.}, we only indicated how can one use the notions of decomposition and projection of reductions to study modular properties of rewrite systems. Much work is still to be done in that direction.

Finaly, an investigation of the geometry of Euclidean Reduction Spaces may reveal interesting properties of reductions not studied before.

\begin{akn} 
We thank  J. R. Kennaway and  M. R. Sleep for useful discussions and help in the preparation  of this paper.
\end{akn}
%



\begin{thebibliography}{99}

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


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

\bibitem{[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{[H.L.]} Huet G., L\'evy J.-J. Computations in Orthogonal Rewriting 
     Systems. In: Computational Logic, Essays in Honor of Alan Robinson,
     ed. by J.-L. Lassez and G. Plotkin, MIT Press, 1991.
 
\bibitem{[GLM]} Gonthier G., L\'evy J.-J., Melli\`es P.-A. An abstract Standardisation theorem. In: Proc. of LICS 1992, p. 72-81.

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


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


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

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


\bibitem{[pti]} 
Khasidashvili Z. Higher order recursive program schemes are Turing incomplete. Report CWI CS-R9348, Amsterdam, 1993. To appear in: Proc. of Colloquium on Trees in Algebra and Programming, Edinburgh, 1994.

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

\bibitem{[Kl.TRS]} 
Klop J. W. Term  Rewriting Systems.
     In:  S. Abramsky, D. Gabbay,  and T. Maibaum, eds.  Handbook  of Logic in
      Computer Science, vol. II, Oxford University Press, 1992, p. 1-116.
\bibitem{[kor]}
Klop J. W., van Oostrom V., van Raamsdonk F. Combinatory reduction Systems:
introduction and survey. In: To Corrado B\"ohm. To appear in J. of Theoretical
Computer Science. Available as Free University Report IR-327, 
Amsterdam, June 1993.

\bibitem{[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{[le80]}
L\'evy J.-J. Optimal reductions in the Lambda-calculuus. In: To H. B. Curry: Essays on Combinatory Logic, Lambda-calculus and Formalizm, Hindley J. R., Seldin J. P. eds, Academic Press, 1980, p. 159-192.

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

\bibitem{[Rus]} 
Rusinowitch M. On termination of the direct sum of term rewriting systems. Information Processing Letters 26, p. 65-70, 1987.

\bibitem{[Wsk]}
Winskel G. Events in Computation. Ph.D. thesis, Dept. of Computer Science, University of Edinburgh, 1980.
\end{thebibliography}
\end{document}





