\documentclass{rtaloop}
\rtalabel{one-step}

\begin{document}
\begin{problem}{J. R. Kennaway}{}{April 1991}

\begin{abstract}
Has any full, finitely-generated and Church-Rosser
term-rewriting system (or system with bound variables)
a recursive, one-step, normalizing reduction strategy?
\end{abstract}

Let a term-rewriting system (or more generally, a system with bound variables
\cite{K92:ox}) have the following properties: it is ``finitely generated''
(has finitely many function symbols and rules), it is ``full'' (its terms are
all that can be formed from the function symbols), and it is Church-Rosser.
Does it follow that it has a recursive, one-step, normalizing reduction
strategy? (There are counterexamples if any of the three conditions is
dropped.) Kennaway \cite{K89:apal} showed that for ``weakly'' orthogonal
systems the answer is yes. So, any counterexample must come from the murky
world of non-orthogonal systems. See also \cite{AM96}.



\end{problem}
\end{document}