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


\title{Euclidean Reduction Spaces: Independence, Context Sharing, and Modularity}
\author{John Glauert and 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 equevalence and the zig-zag family relation is defined based on the notion of residual and elementary diagrams as primitives. We furrher 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 investigate the metric for the  L\'evy-Klop structure of Orthogonal Combinatory Reduction systems (OCRSs), finding how a Euclidean bases 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 bases in the corresponding upper semilattice. This leads to a study of computations of components (i.e., contexts) of a term rather than subterms independently, i.e., in parallel; computatitions of different occurrences of a component whose corresponding subterms are not the same can also be ahared. Since the independent computations are feasible only in OCRSs where restricted kinds of redex-creation is possible, one is forced to consider probabilistic strategies that do independent computations in components with higher digrees of independence. However, an elegant implimentation of terms with shared components is possible using {higher order} invironments.
\end{abstract}

\bigskip

\subsection*{Correspondence Address}

\begin{tabbing}
Dr. Zurab Khasidashvili \\
School of Information Systems \\
University of East Anglia \\
Norwich NR4 7TJ England \\
\\
Email: zurab@sys.uea.ac.uk \\
Tel: +44 603 592607 \\
Fax: +44 603 507720
\end{tabbing} 

\end{titlepage}

\section{Introduction}

The Essential similarity Lemma establishes which components of a term
detarmine essentiality (inessentiality) of a given subterm -- only
essential bindings in independant subterms are importent for essentiality
of a subterm.

For the sake of optimality, one can share independent contexts (not whole independent subterms) in the following way: represent a term $t$ as $t=C[C_1^1[C_2^1[\ldots],\ldots, C_2^{k_2}[\ldots ].\ldots, C_1^n[\ldots]]$, replace into a context $C_i^j$ immediate subcontexts $C_{i+1}^l$ by asubterms $f_{i+1}^l(x_1,\ldots,x_k$, where $f_{i+1}^l$ is a fresh function symbol and 
$x_1,\ldots,x_k$ is the set of (wessential) free variables of the subterm corresponding to the replaced context. Then one can compute all the independent ``context-terms'' independently and rewrite functions $f_i^j$ to the results of computations in all ``context-terms''. The result of rewriting the top-most ``context-term'' in that they is the normal form of $t$ (if the reasults of computations of all ``context-terms'' are normal formas). Computations of inessential context-subterms are redundent. Whether a context-subterm is inessentila or not reveals after computation of upper context-subterms --- corresponding $f$-symbol must desappear.






\section{Euclidean Reduction Spaces}


\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 $+$ (concatination), / (residual), $\sqcup$ (square sum), $\lleq$ (L\'evy embedding), $\leeqv$ (L\'evy equivalence or the strong equivalence), and $\zig$ (zig-zag family) on reductions such that:

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

(*) All developments are terminating; all  coinitial developments 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.

(*) 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 a 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$}.

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

(*) $+$ is the {\em concatination} 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$.

(*) The following equations hold (actually, they can easily be derived from the above items): 
%(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$.
 
(*) For any co-initial reductions $P+u$ and $Q+v$ (read as $u$ {\em with history} $P$ and $v$ {\em with history} $Q$), $u$ is called a {\em copy} of $v$ 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 stracture is a {\em L\'evy spectrum} as pointed out breifly 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 stractures because it clear and allows an easy difinition 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 (the latest is moreover an {\em evant structure}). Examples of other  L\'evy-Klop structures are given in subsection~\ref{[SS.ESL.]}.







\begin{deff}\em
(*) Let $P$ be a reduction in a L\'evy-Klop structure. The {\em canonical form} of $P$, written $CF(P)$, is defined by induction on $\vert P\vert$ as follows. 

(a) If $\vert P\vert\leq 1$, then $CF(P)=P$. 

(b) Let $P:t\red{u}s\red{v}o$. If $v$ is a new redex, then $CF(P)=P$. Otherwise, let $v$ be a residual of $v\subt t$. Then $CF(P)=P$ if $v'\sqcup u\geq 2$ and $CF(P)=v'\sqcup u=v'$ otherwise. In the latter case, we say that $u$  is {\em omited} in $CF(P)$.

(c) Let $P=P'+u$, where $P':t\doar s$ and $s\red{v}o$. Further, let $CF(P'):t\red{u_0}t_1\red{u_1}\ldots\red{u_{n-1}}t_n=s$, $P'_{n-1}=t\red{u_0}t_1\red{u_1}\ldots\red{u_{n-2}}t_{n-1}$, and $Q:t_{n-1}\red{u_{n-1}}s\red{v}o$. Then $CF(P)=CF(P_{n-1})+CF(Q))$  if $\vert Q\vert=1$, and $CF(P)=CF(P')+v$ otherwise.

 We say that a redex $w$ contracted in $P$ is {\em omited} in $CF(P)$ if $w$ is omited in $P'$ or $w=v$ and is omited in $Q$. We call a redex contracted in $P$ {\em $P$-needed} if it is not omited in $CF(P)$.

(*) Let $P:t\doar s$, $Q:t\doar o$, and $P=P'+u+P''$. We call $u$ {\em $Q$-needed} iff it is $Q/P'$-needed. We call $P$ {\em $Q$-needed} if if each redex contracted in $P$ is so. % 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.


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



It is easy to see that $u$ is not $P$-needed iff there is a $Q\leeqv P$ that  does not contract residuals of $u$ and erases $u$. Therefore, if $P\leeqv Q$, $P$-neededness (of subterms and reductions) 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 needed redexes in a term $t$ are $P$-needed for any reduction starting from $t$. 

An interesting fact about self-neededness is the followimg: 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.


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

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

(*) We call a bases ${\bf B_1=\{P_i\}}$ at a term $t$ {\em finer} than the bases ${\bf B_2=\{Q_j\}}$ at a term $t$ if, for any $P_i$, there is no $Q_j$ such that $Q_j\lles P_i$ (and not $P_i\lles Q_j$). The bases ${\bf B_1=\{P_i\}}$ is a {\em finest} or is an {\em Euclid bases} of $R$ at $t$ if it is finer than any over bases of $R$ at $t$ (such a bases exists); the reductions $P_i$ are called {\em directions} at $t$. (Note that  an Euclidean bases at a term is determined uniquely up to strong equevalence of directions.)

(*)  We call a bases ${\bf B_1}=\{P_i\}_{i\in I}$ {\em a refinment} of a bases ${\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 bases {\em finest} if it does not have a refinment.


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


(*) We call a L\'evy-Klop structure with an Euclidean bases at each term  and the metric defined as above a {\em Euclidean reduction space}.
\end{deff}
 

In the above definition, we need to consider self-needed reductions to ensure that the distance betveen strongly equevalent reductions is $0$. One might think that more appropriate would be to consider $P\sqcup Q$-needed families 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 $R:t\red{\omega}t\red{\omega}t\red{\omega}t\red{\omega}t\red{K}x$. Then $\dist{P}{Q}=3$ and $\dist{P}{R}=\dist{R}{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 bases 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 bases of $L$.




\begin{deff}\em
(*) We call co-initial reductions {\em disjoint} if they  contract redexes from different families.

(*) We call finite reductions $P$ and $Q$ {\em quasi-independant} 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}
%

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$. A reduction is {\em family-complete} if ech redex of a contracted family (i.e., a family whose at least one redex is contracted) is secured.


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: $w=(\lambda x.xx)u\red{w}uu\red{u}ou$ and $u$ are independent, but not disjoint. However, if both reductions are family-complete, then independence implies disjointness, and if the reductions are cros-needed, then disjointness implies independence. In particular, reductions of a bases are cros-needed and family-complete, hence disjoint. Further, cros-needed co-initial reductions are independent iff they are disjoint.



\begin{deff}\em
Le t $t$ be a term in an ARS, let $P$ be a reduction out of $t$,  and let $F$ be a set of redexes in $t$. 

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

(*) We call an $F$-reduction $P$ {\em $F$-complete} if each redex from $F$ and each created redex is secured.

(*) We call an $F$-reduction $P$ {\em strongly cofinal for $F$} if, for any $F$-reduction  $Q$ out of $t$, $Q\lleq P$.

(*) We call $P$  a {\em direction} if it is $F$-complete for some set $F$ of redxes in $t$ and is quasi-independent from any reduction starting from $t$.

(*) We call a set of redexes in $t$ {\em independent} if any strongly $F$-cofinal $F$-reduction is a direction for $F$.

(*) Let $F_i$ with $i\in I$ be sets of redexes in $t$ such that $\cup_iF_I$ contains each redex of $t$ and $F_i\cap F_j=\emptyset$. Then we call the set $\Im=\{F_i\}_{i\in I}$ a {\em 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 fineswt covering (and only such sets of reductions out of $t$) is a finest  bases at $t$. Further one can show that an $F$-reduction $P$ is strongly $F$-cofinal iff it is $F$-complete.



\begin{deff}\em
Let $t$ be a term in an ARS $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 notion {\em $P$ respects $F$}  and the {\em restriction of $P$ to $F$}, written $P\vert(F)$, is 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$ 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$ respect $F$ and $F'$ if $u'$ is a residual of a redex $u''$ either from the final term of $P'\vert(F)$ or the final term of $P'\vert(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 and are quasi-independent, 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 an ARS $R$.

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

(*) Let  $P$ be a reduction out of $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$.

(*) 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 bases at $t$ and the equations are valid for any $P$; the bases $B$ is a finest one iff each direction is so.

(*) 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 essential redex. Then $P_i$ with $i\in J$ are optimal (with respect to the number of contracted redexes) $F_i$-complete reductions iff $P=\sqcup_iP_i$ is an optimal normalizing reduction out of $t$.
\end{thm}



For any $P:t\doar s$ and any new redex $u\subt s$, the smolest reduction needed to create $u$ (the extraction of $Pu$) is internal to some finest independent component of $t$, since any redex created by $P$ is created by its projection to some direction.










\section{Independence in Combinatory Reduction Systems}



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, spacified by {\em scope indicators}. 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 syntactically 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} with arity $(n,n+1)$
and scope indicator $(n+1)$; i.e., it binds free variables only in the last argument. 

Each rule $r:t\ar s$ has a set of {\em admissible assignments} and for any admissible assignment $\theta$, the $\theta$-instance $t\theta$ of $t$ is an $r$-{\em redex}, and $s\theta$ is the {\em contractum} of $t\theta$. Redexes that are instances of the left-hand side of the same rule are called {\em weakly similar}. We do not require that term metavariables in the right-hand sides of rules necesserily occur in the left-hand sides. If a CRS is not regular, and 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 $u$ in $C[u]$) requres renaming of binding variables in $C[\,\,]$ to avoid bindings of fresh variables of $s$ in $C[s]$. Below we ignore questions related to renaming of bound variables.
%

\notation
We use  $c,d$ for constants, $t,s,e,o$ for terms and metaterms, $u,v,w$ for redexes, and $P,Q$ for reductions.  We write $s\ssq t$
if $s$ is a subterm of $t$.  A one-step reduction in which a redex $u$ in a
term $t$ is contracted is written as $t\stackrel{u}{\ar} s$ or $t\ar s$.  We
write $P:t\doar s$ if $P$ denotes a reduction (sequence) from $t$ to $s$. $\vert P\vert$ denotes the length of $P$.  $P+Q$ denotes the concatenation
of $P$ and $Q$.


Any CRS $R$ can be splitted into a ``first order part'' $R_f$, which delays substitutions as $\undl{S}$-redexes, and a ``substitution part'' $\undl{S}$, which makes substitutions from the right to left order (undrlining is only used to distinguish created $S$-redexes from other ones). For example, a $\beta$-reduction step $(\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}  extend 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$. The {\em ancestor} relation is converse to the decsendant relation.





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 CRS must be regular, all the rules must be left-linear, and in no term an overlap of redex-patterns can be possible; since the rules may be conditional, one must requare that descendants of non-contrated redexes be redexes weakly similar to their ancestors.







\begin{deff}\em
\label{D.free.} 
 We call a subterm $s$ in $t$ {\em free}, written $F(s,t)$, (resp. {\em essentially free}, written $F_{es}(s,t)$), if $s$ is not a
proper pattern-subterm of a redex (resp. an essential redex) in $t$. 
\end{deff}







\begin{deff}\em
Let $t$ be a term in a CRS $R$ and $\theta$ be a higher order substitution. We call a redex $u\subt t\theta$ {\em orthogonal} to $\theta$ (written $u\orth\theta$) if $p(u)$ (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. \end{deff}



\begin{deff}\em
\label{D.dec.comp.}



(*) If ${\bf D}=\{D_i\}$ is a set of non-overlapping components of $t_0$, then  $P$ and $P'$ {\em respect} ${\bf D}$ if they respect each $D_i$. We call ${\bf D}$ a {\em decomposition} of $t_0$ if the components are non-overlapping and each occurrence of $t_0$ is in some component. We call ${\bf D}$ an {\em independent decomposition} of $t_0$ (written $i.d.(t_0)$) if each component $D_i$ is independent, i.e., if ${\bf D}$ is respected by any reduction starting from $t_0$. The i.d. ${\bf D}$ is {\em finest} if no proper subcomponents of $D_i$ are independent.


(*) A set of components of $t_0$ is the {\em compliment} of another set ${\bf C}$ of components of $t$  (notation ${\bf\overline{C}}$) if ${\bf C}\cup{\bf\overline{C}}$ is a decomposition of $t_0$ and contains a smallest number of components. If $P$ and $P'$ respect $C_0$, then we call a redex executed in $P$ and $P'$ {\em internal} to the descendant sequence $(C)_n$ if the corresponding step in $P\restr(C_n)$ is not empty, and call {\em internal} to $C_0$ if it is internal to all descendant sequences of $C_0$. We call $P$ and $P'$ {\em external} to $C_0$ if it is internal to the complement of $\{C_0\}$. We call $P$ and $P'$ {\em internal} (resp. {\em external}) to ${\bf C}$ if they respect ${\bf C}$ and all their steps are internal to some (resp. external to all) element(s) of ${\bf C}$. (Obviously, $P$ is external to ${\bf C}$ iff it is internal to its compliment.)


(*)  The  {\em independense degree} of a component $C$ in $t$ is the length of a shortest reduction $P$ internal to $C$ such that there exists a reduction $Q$ external to $C$ that is quasi-independent from $P$.

\end{deff}







Let $t$ be a term in an OCRS $R$. Then one can show that 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. Note however that the independence of $C$ does not emply either  independence of $s$ or independence of $s_i$. Indeed, let $R=\{f(x)\ar x,\,\,g(a)\ar b\}$. Then the component $f[\,\,]$ in the term $g(f(a))$ is independent, while neither $f(a)$ nor $a$ are so. 





The statement analogous to Theorem~\ref{T.dec.thm.} is valid for OCRSs if instead of (independent) coverings one considers (independent) decompositions of terms. For example, one defines a reduction $P:t\doar s$ to be {\em cofinal for a component} $C$ of $t$ if $P$ is internal to $C$ and for any $Q:t\doar e$ internal to $C$ one has $Q\lleq P$. {\em $C$-completeness} of a reduction internal to $C$ is defioned similarly to $F$-completeness. Now the statement analogous to the above theorem  can be proved using Definition~\ref{D.desc.comp.} or be derived from the above theorem 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$ out of $t$ respectively respects, is internal, or is external to $F$ iff it is so to $C$.




\begin{lem}\em
Let ${\bf D}=\{D_i\}$ be a decomposition of a term $t$, in an OCRS $R$, respected by $P:t\doar s$. Then $C(P))=\sqcup_i(C(P\vert(D_i)))$
\end{lem}



\begin{lem}\em
\label{L.indep.decompos.}
(1) Let ${\bf C}=\cup C_i$ be a set of non-overlapping components of a term $t$ in an OCRS $R$ (???), $o_i$ be a complition of $C_i$ with respect to $t$, $P_i'$ be a reduction starting from $o_i$, and let $P_i=P_i'\exten(t)$. Then $P=\sqcup P_i$ respects ${\bf C}$ and $P\restr(C_i)=P_i'$.


(3) If ${\bf C}$ is a maximal set of independent essential components of $t$  (i.e., all subterms headed at the components are essential) and $P_i'$ are normalizing reductions of $o_i$, then $P=\sqcup P_i$ is an optimal reduction (with respect to the number of families whose redexes are contracted in the reduction) iff $P_i'$ are optimal normalizing reductions starting from $o_i$. Moreover, the destance between $P$ and any optimal normalizing reduction starting from $t$ is $0$.
\end{lem}






\section{Applications}

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

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$  '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$.


\notation  Below $EFV_{R}(t)$ denotes the set of
variables having $R$-essential free occurrences in~$t$ and $FV(s)$ denotes the
set of variables having free occurrences in~$s$.  For any $s\subseteq t$, $BV_R(s)$ (resp. $EBV_R(s)$) denotes
the set of free occurrences (resp. $R$-essential free occurrences)  of $s$ bound 
by quantifiers belonging to patterns of $R$-redexes that are outside $s$.




 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 using the above definition that the converse is also valid if $s$ is independent in $t$.


%
\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 $t\essim s$, 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, it can be omited. Therefore, there is a reduction $P$ that erases $s'$ and is external to $s',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$ be the restriction of $P$ to $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 $EFV(s_i)=EFV(s_i^*)=FV(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 in $s$ (in any order) 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 $FV(t_i^*)=EFV(t_i)=EFV(s_i)=EFV(s_i^*)\ssq FV(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 theorem 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; one can take for $R_{es}$ also some conditional 'context-sensitive' OCRS where contraction of redexes may only be allowed only in some contexts.) Further, one can define in an OCRS $R$ notions such as {\em essential destence} between co-initial reductions $P$ and $Q$, {\em essential independence} of a set of co-initial reductions $\{P_i\}$, {\em essential bases} at a term, etc. Then the essential distance between $P$ and $Q$ coincides with the distence between the corresponding redictions in $R_{es}$, $\{P_i\}$ are essentially independent iff the corresponding reductions in $R_{es}$ are independent, etc.




\subsection{Computations in higher order invironments}

A term in an OCRS may contain occurrences of a component while the corresponding subterms of the different ocurrences 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 component of ${\bf C}$ has a normal form; and the normal form of $t$ is obtained from the decomposition of $t$ by rewriting, upside down, all the components to their values. Whither a component 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 extand, 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. 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 occisionally; using the current values of the components restore the intermadiate result of computation of $t$. Compute the obtained term in the same way and so on, as long as possible. Of cource, it is batter not to split subterms with high degrees of independence (when an analises assesing the independence degrees of subterms can be made; methods for analizing degrees of independence is a subject of future work).


This unpleasent situation can be resolved by formalizing sharing of components in {\em higher order environments} a very much similar way as it is done in the ordinary case: along with bounding subterms to variables in an invironment one can bound 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 feasiable, the computation of a topmost component that looks in the invironment while looking for a strongly needed (essential), i.e., an index, redex is feasible as well. Moreover, computatins 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 sas from correctness of the chaotic strategy, since the computaion does unsharing always when it is necessary to contract the contrapart of a needed (more precisely, an index) redex of the term which (on any given stage) the invironment represents. For example, 


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



\section{Conclusions and future work}

We open the following directions for future investigation:

Context graph rewriting theory;

Implimentation in higher order invironments;

Investigate the geometry of Euclidean Reduction Spaces;

Define descendant structure which will be a refinment of the residual structure.

Dvelop optimality theory like L\'evy-Lamping-Gonthier and Asperti-Laneve. Corresponding sharing theory and path-theory.
%


\begin{akn} 
We thank  J. R. Kennaway and R. M. 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{[K.S.]} Kennaway J. R., Sleep M. R. Neededness is hypernormalizing in regular combinatory reduction systems. Preprint, School of Information Systems, University of East Anglia, Norwich, 1989.

\bibitem{[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.

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

\end{thebibliography}

\end{document}
