%\documentstyle[11pt]{article}
\documentstyle{llncs}   
\def\english{0}
\input{BoxedEPS}
\HideDisplacementBoxes
\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
\newcommand{\john}[1]{\{{\bf John:~\sf #1}\}} % Highlight text.
\newcommand{\zurab}[1]{\{{\bf Zurab:~\sf #1}\}} % Highlight text.
\newcommand{\suppress}[1]{\{} % Omit text.
\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\lc{$\lambda$-calculus}
\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\lleq{\unlhd}
\def\lles{\lhd}
\def\leeqv{\approx_L}
\def\ind{\ddagger}
\def\hole{\circ}
\def\restr{\vert}
\def\exten{\updownarrow}
\def\lc{$\lambda$-calculus}
\def\ovl{\overline}
\def\unl{\underline}
\newarrow{Co}<--->
\def\zfami{\simeq_z}
\def\fami{\simeq}
\def\t{Theorem~\ref}
\def\p{Proposition~\ref}
\def\c{Corollary~\ref}
\def\l{Lemma~\ref}
\def\d{Definition~\ref}
\def\bd{\begin{deff}\em}
\def\bdl{\begin{deff}\em\label}
\def\bl{\begin{lem}\em}
\def\bll{\begin{lem}\em\label}
\def\bp{\begin{prop}\em}
\def\bpl{\begin{prop}\em\label}
\def\bt{\begin{thm}\em}
\def\btl{\begin{thm}\em\label}
\def\bel{\begin{ex}\em\label}
\def\bc{\begin{cor}\em}
\def\bcl{\begin{cor}\em\label}
\def\bproof{\begin{proof}}
\def\eproof{\end{proof}}
\def\ed{\end{deff}}
\def\el{\end{lem}}
\def\ep{\end{prop}}
\def\et{\end{thm}}
\def\ee{\end{ex}}
\def\ec{\end{cor}}
\def\setm{\setminus}
\def\crea{\vdash}
\def\emp{\emptyset}

%
%
\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
\thanks{This work was supported by the Science and Engineering Council of Great Britain under grant GR/H 41300}}
\maketitle
%
\begin{abstract}
We study reductions in orthogonal (left-linear and non-am\-bi\-guous) Expression Reduction Systems, a formalism for Term Rewriting Systems with bound variables and substitutions. To generalize the normalization theory of Huet and L\'evy, we introduce the notion of {\em neededness} with respect to a set of reductions $\Pi$ or a set of terms $M$ so that each existing notion of neededness can be given by specifying $\Pi$ or $M$.  We impose natural conditions on $M$, called {\em stability}, that are sufficient and necessary for each term not in $M$-normal form (i.e., not in $M$) to have at least one $M$-needed redex, and repeated contraction of $M$-needed redexes in a term $t$ to lead to an $M$-normal form of $t$ whenever there is one. Our relative neededness notion is based on tracing of {\em (open) components}, which are occurrences of contexts not containing {\em any} bound variable, rather than tracing of redexes or subterms.

\vspace{1cm}

The full paper will appear here within a few days. Please contact the authors by email.
\end{abstract}

\end{document}





