\documentclass{rtaloop}
\rtalabel{definability}

\begin{document}
\begin{problem}{Jan Willem Klop}{}{April 1991}

\begin{abstract}
Which rewrite systems can be directly defined in lambda calculus?
\end{abstract}

An important theme that is largely unexplored is definability (or
implementability, or interpretability) of rewrite systems in rewrite
systems.  Which rewrite systems can be directly defined in lambda
calculus?  Here ``directly defined'' means that one has to find lambda
terms representing the rewrite system operators, such that a rewrite
step in the rewrite system translates to a reduction in lambda
calculus.  For example, Combinatory Logic is directly lambda
definable.  On the other hand, not every orthogonal rewrite system can
be directly defined in lambda calculus.  Are there universal rewrite
systems, with respect to direct definability?  (For alternative
notions of definability, see \cite{O85:mit}.)


\begin{remark}
Some progress has been made in \cite{BB92:aquila}.
\end{remark}

\end{problem}
\end{document}