Which rewrite systems can be directly defined in lambda calculus?
The source page states the original problem together with its recorded qualifications and progress updates as follows.
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 [Klop, 1991].)
Recorded progress.
Some progress has been made in [Klop, 1991].
