%\documentstyle[11pt]{article}
\documentstyle{llncs}   
\def\english{0}
\input{BoxedEPS}
\HideReservedBoxes
\SetOzTeXEPSFSpecial  
%\SetRokickiEPSFSpecial
%\marginparwidth 0pt
%\oddsidemargin  0pt
%\evensidemargin  0pt
%\marginparsep 0pt

%\topmargin   0pt

%\textwidth   6.5in
%\textheight  8.5in
%\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}$}}
\newcommand{\dored}[1]{\mbox{$\stackrel{#1}{\doar}$}}
\newenvironment{prsk}{\noindent{\bf Proof sketch }}{}
\newenvironment{altpr}{\noindent{\bf Alternative proof }}{}
\newcommand \inputpic[1] {\begin{center} \input{#1} \end{center}}
\newcommand{\ssq}{\subseteq}
\newcommand{\sset}{\subset}
\hyphenation{meta-var-ia-ble}
\newcommand{\vect}[1]{\mbox{$\overline{#1}$}}
\newcommand{\rpsim}{\mbox{$\stackrel{r}{\psim}$}}
\newcommand{\rpessim}{\mbox{$\stackrel{r}{\pessim}$}}
\newcommand{\ressim}{\mbox{$\stackrel{r}{\essim}$}}
\newcommand{\rsim}{\mbox{$\stackrel{r}{\sim}$}}
\newcommand{\muer}[1]{\mbox{$[{#1}]_{\mu}$}}
\newcommand{\lclas}[1]{\mbox{$\langle{#1}\rangle_L$}}
\newcommand{\eclas}[1]{\mbox{$\langle{#1}\rangleÄ$}}
\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\steqc{\approx_{st}^*}
\def\hyeq{\approx_{H}}
\def\kleq{\approx_{K}}
\def\eq{\approx}
\def\essim{\approx}
\def\psim{\prec}
\def\orth{\perp}
\def\esorth{\perp_{es}}
\def\subt{\subseteq}
\def\subpc{\sqsubseteq}
\def\lleq{\triangleleft}
\def\lles{\triangleleft}
\def\leeqv{\approx_L}
\def\ind{\ddagger}
\def\hole{\circ}
\def\restr{\vert}
\def\exten{\updownarrow}
\def\zig{\simeq}
\newarrow{Co}<--->
%
%
\title{On Relative Normalization in Orthogonal Expression Reduction Systems}
\author{John Glauert and Zurab Khasidashvili}
\institute{School of Information Systems, UEA\\
Norwich NR4 7TJ England \\ 
jrwg@sys.uea.ac.uk, zurab@sys.uea.ac.uk\\
DRAFT (CTRS'94)\thanks{This work was supported by the Science and Engineering Council of Great Britain under grant GR/H 41300}}
\maketitle
\date{}

\section{Introduction}

\begin{deff}\em
\label{D.desc.comp.}
Let $R$ be an ERS, $C$ be a component of a term $t$ in $R_{fS}$, $s=C[s_1,\ldots,s_n]$ be the corresponding subterm of $C$ in $t$, and let $t\red{u}s$ in $R_{fS}$. We define {\em $u$-descendants} of $C$ by considering all relative positions of $u$ and $C$.

(1) $C\cap u=\emptyset$ (if $C$ is an empty component, then its corresponding occurrence is outside $u$). Then the $(u,*)$-descendant of $C$ is the $(u,*)$-descendant of $s$ with the $(u,*)$-descendants of $s_i$ removed (see figure~\ref{P.ctrs1}).
 
(2) $u$ is an $R_f$-redex and $C$ is in an argument of $u$. Then the $(u,i)$-descendant of $C$ is the $(u,i)$-descendant of $s$ with the $(u,i)$-descendants of $s_i$ removed $(i\geq 1)$ (see figure~\ref{P.ctrs2}).
 
(3) $u$ is an $S$-redex (or an $\undl{S}$-redex) and $C$ is in an argument of $u$. Then the $(u,i)$-descendant of $C$ is the $(u,i)$-descendant of $s$ with the $(u,i)$-descendants of $s_i$ removed $(i\geq 0)$ (see figure~\ref{P.ctrs3}).
 

(4) $u$ is an $R_f$-redex and $pat(u)$ is in $C$. If $pat(u)=C$ and $cpat(u)=\empty[\,]$, then we say that $C$ is {\em collapsed} and its descendant is the empty component occurring at the top the the contractum of $u$. Otherwise, the {\em $(u,*)$-descendant} of $C$ is the $(u,*)$-descendant of $s$ with the descendants of $s_i$ removed (see figure~\ref{P.ctrs4}).

\begin{figure}[htbp]
\begin{center}
\BoxedEPSF{ctrs4.ps scaled 600}
\end{center}
\caption {}
\label{P.ctrs4}
\end{figure}

% (5) $u$ is an $S$-redex with the top in $C$, i.e., $u=Sx_1\ldots x_kC_1[\vect{e_1}]\ldots C_k[\vect{e_k}]C_0[\vect{e_0}]$ and $C=C'[u]$. If $C=pat(u)$, then $C$ is {\em collapsed} and it does not have descendants. Otherwise, the {\em $(u,*)$-descendants} of $C$ are  the $(u,*)$-descendant of $s$ with the descendants of the subterms $s_i$ that are outside $u$ and the descendants of $\vect{e_j}$ (which are inside the descendants of $\vect{e_0}$) removed; and the descendants of $C_i$, as defined in (3).

(5) $u$ is an $S$-redex, say with two arguments (for simplicity) $u=S^2x\,e\,o$, with the top in $C$, and let $s=C'[s_1,\ldots, S^2x\,C_e[s_i,\ldots,s_j]\,C_o[s_{j+1},\ldots, s_k],\ldots,s_n]$, where $C=C'[\ldots, S^2x\,C_e[\,\,]\,C_o[\,\,],\ldots]$, $e=C_e[s_i,\ldots,s_j]$, and $o=C_o[s_{j+1},\ldots, s_k]$. If $C=pat(u)$, then $C$ is {\em collapsed} and its descendant is the empty component occurring at the top the the contractum of $u$. Otherwise, the {\em $(u,*)$-descendants} of $C$ are  the $(u,*)$-descendant of $s$ with the descendants of the subterms $s_i$ removed, and the descendants of $C_e$, as defined in (3)  (see figure~\ref{P.ctrs5}). (Note that all $u$-descendants of $s_i,\ldots,s_j$ are inside the $u$-descendants of $s_{j+1},\ldots,s_k$.)

\begin{figure}[htbp]
\begin{center}
\BoxedEPSF{ctrs5.ps scaled 500}
\end{center}
\caption {}
\label{P.ctrs5}
\end{figure}

(6) $u$ is an $R_f$-redex, $pat(u)$ and $C$ partially ovarlap (i.e., neither contains another), and the top of $u$ is below the top of $C$. Then the $(u,*)$-descendant of $C$ is the $(u,*)$-descendant of $s$ with the arguments of $u$ and the descendants of $s_i$ that are disjoint from $u$ removed (see figure~\ref{P.ctrs6}).

\begin{figure}[htbp]
\begin{center}
\BoxedEPSF{ctrs6.ps scaled 600}
\end{center}
\caption {}
\label{P.ctrs6}
\end{figure}

(7) $u$ is an $R_f$-redex, $pat(u)$ and $C$ partially ovarlap, and the top of $C$ is below the top of $u$. Then the $(u,@)$-descendant of $C$ is the $(u,@)$-descendant of $s$ with the descendants of $s_i$ and the descendants of the arguments of $u$ that are disjoint from $C$ removed (see figure~\ref{P.ctrs7}).

\begin{figure}[htbp]
\begin{center}
\BoxedEPSF{ctrs7.ps scaled 600}
\end{center}
\caption {}
\label{P.ctrs7}
\end{figure}


(8) $u$ is an $R_f$-redex and $pat(u)$ contains $C$ ($C$ may be an empty component). Then the $(u,*)$-descendant of $C$ is the contractum-pattern of $u$ (the latter may also be empty) (see figure~\ref{P.ctrs8}).

\begin{figure}[htbp]
\begin{center}
\BoxedEPSF{ctrs8.ps scaled 600}
\end{center}
\caption {}
\label{P.ctrs8}
\end{figure}

The notion of descendant for components generalises by transitivity to all $R_{fS}$ reductions and to all $R$-reductions. 
\end{deff}



\end{document}






