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

\topmargin   0pt

\textwidth   6.5in
\textheight  8.5 in

\input{diagrams} % Paul Taylor's Macro Package
\newarrow{Co}<--->
\begin{document}


\title{Relative Normalization in Deterministic Residual Structures}
\author{John Glauert and Zurab Khasidashvili \\ School of Information Systems, UEA\\
Norwich NR4 7TJ England \\ 
\sf{jrwg@sys.uea.ac.uk, zurab@sys.uea.ac.uk}}
\maketitle
\begin{abstract}
We define {\em Stable Deterministic Residual Structures} (SDRS) and {\em Family Structures} by axiomatizing some properties of the residual relation and the family relation on redexes. We present two proofs of the {\em Relative Normalization Theorem}, one for SRDRs for {\em regular stable} sets, and another for DRSs for all {\em stable} sets of desirable `normal forms'. We further prove the {\em Relative Optimality Theorem}. Finally, we give several applications of our results.
\end{abstract}


\section{Introduction}

\begin{figure}
\begin{diagram}[height=1.5em,width=1em]
  &        &      &        &      &        & &        & & P      \\
  & \cdot  &      & \rTo   &      & \cdot  & & \rTo   & & \cdot &      & \rTo   &      & \cdot  & & \rOnto & & \cdot  \\
  &        &      &        &      &        & &        & & \dTo  &      &        &      & \dOnto & &        & & \\
  & \dTo   &      &        &      & \dTo   & &        & & \cdot & \rTo & \cdot  & \rTo & \cdot  & &        & & \dOnto \\
  &        &      &        &      &        & &        & & \dTo  &      &        &      &        & &        & & \\
  & \cdot  &      & \rTo   &      & \cdot  & & \rTo   & & \cdot &      &        &      &        & &        & & \cdot  \\
  &        &      &        &      &        & &        & &       &      &        &      &        & &        & & \\
Q & \dTo   &      &        &      & \dOnto & &        & &       &      &        &      &        & &        & & \dOnto \\
  &        &      &        &      &        & &        & &       &      &        &      &        & &        & & \\
  & \cdot  & \rTo & \cdot  & \rTo & \cdot  & &        & &       &      &        &      &        & &        & & \cdot  \\
  &        &      &        &      &        & &        & &       &      &        &      &        & &        & & \\
  & \dOnto &      &        &      &        & &        & &       &      &        &      &        & &        & & \dOnto \\
  &        &      &        &      &        & &        & &       &      &        &      &        & &        & & \\
  & \cdot  &      & \rOnto &      & \cdot  & & \rOnto & & \cdot &      & \rOnto &      & \cdot  & & \rOnto & & \cdot  \\
\end{diagram}
\caption{Klop Tiling Diagram}\label{tiling-diag}
\end{figure}


\begin{figure}
\begin{diagram}[height=2em,width=2em]
& \rTo^x & \cdot  & & \rTo^v     &              & \cdot &              & \\
&        &        & &            & \ldTo_{u_2}  &       & \rdTo_{u_1}  & \\
&        & \dTo^u & & \cdot      &              &       &              & \cdot & \pile{\rTo^w \\ \lTo_{u_{21}'}} &             & \cdot \\    
&        &        & &            & \rdTo^{u_1'} &       & \ldTo^{u_2'} &        &         & \ldTo_{u_{22}'} \\
&        & \cdot  & & \rTo_{v_1} &              & \cdot &              & \pile{\rTo^{w'} \\ \lTo_{u^*_{21}}}  & \cdot \\      
\end{diagram}
\caption{The Necessity of Stability}\label{non-hyper}
\end{figure}

\begin{figure}
\begin{diagram}
 \bullet  & \rTo^v & \bullet     \\
 \dTo^u &     &  \dOnto_{u/v}  \\
\bullet  & \rOnto_{v/u} & \bullet    \\
\end{diagram}
\caption{An Elementary Diagram}\label{elem-diag}
\end{figure}

\begin{figure}
\begin{diagram}
 t      & \rTo^u       & e             & \rTo^w           & {}  \\
 \dTo^v &              &  \dOnto_{v/u}  &                 &      \\
s       & \rOnto_{u/v} & o              & \rOnto^{w/(v/u)}   & {}  \\
\end{diagram}
\caption{Berry's Stability}\label{berry-stab}
\end{figure}



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


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


\begin{figure}
\begin{diagram}
{} & &\rOnto^{P_1} & & {}       &\rTo^{u}       & {} \\
{} & &             & &\dTo<{v'} &               &\dTo>{v} \\
{} & &             & & {}       & \rOnto_{u/v'} & {} & &\rOnto_{P_2} & & {} \\
\end{diagram} 
\caption{Constructing Semi-needed Reductions}\label{moving-needed}
\end{figure}
 
 
\begin{figure}
\begin{diagram}
t_0    &   \rTo^{u_0}  &   t_1   &   \rTo^{u_1}  &   t_2    &  \rOnto  &   {} \\
 \dTo^{u=F_0}  &     & \dOnto^{F_1} &          & \dOnto^{F_2}&         &      \\
s_0    &   \rOnto^{u_0/F_0}  &   s_1   &   \rOnto^{u_1/F_1}  &   s_2    &  \rOnto  &   {} \\
\end{diagram} 
\caption{Preservation of Infinite Needed Reductions}\label{Di.ess.}
\end{figure}


\begin{figure}
\begin{diagram}[height=2em,width=3em]
f(a)     &\rTo  &             &       & g(a,a)  &        &        \\
\dCo     &      &             & \ldCo &         &  \rdCo &         \\
         &      & {\bf g(a,b)}&       &         &        & g(b,a) \\    
         &      &             & \rdCo &         & \ldCo  &         \\
f(b)     &\rTo  &             &       & g(b,b)  &        &        \\      
\end{diagram}
\caption{Need for Closure under Permutation}\label{clos-perm}
\end{figure}


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

\end{document}





