\documentstyle{article}

\begin{document}


\begin{titlepage}



\thispagestyle{empty}


\title{A uniform theory of normalization-by-neededness}
\author{Zurab Khasidashvili \\
University of East Anglia, Norwich}
\date{31 May 1994}
\maketitle

\thispagestyle{empty}

%\section{Abstract}


We study reductions in orthogonal (left-linear and non-ambiguous) Expression Reduction Systems, a formalism for Term Rewriting Systems with bound variables and substitutions. 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$. For example, {\em Huet\&L\'evy-neededness} is neededness w.r.t. the set of normal forms, {\em Maranget-neededness} is neededness w.r.t. all fair reductions, {\em head-neededness} is neededness w.r.t. the set of head-normal forms, etc. We impose natural conditions on $M$ 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. In this general setting, some properties of needed/unneeded redexes are different from the `standard' case of Huet and L\'evy neededness.

The above relative neededness notion is based on tracing {\em (open) components}, which are occurrences of contexts not containing any bound variable, rather than tracing redexes or subterms. We relate this notion to our earlier notion of {\em essentiality}, which is based on tracing subterms and proved to be a useful tool for reasoning about the neededness of subterms (in particular, bound variables) even if the term does not have a normal form. \\

\noindent The talk is based on recent joint work with John Glauert and some of my early work.


\end{titlepage}
\end{document}