[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
Originator: Jan Willem Klop
Date: April 1991
Summary: Which rewrite systems can be directly defined in lambda calculus?
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 [O’D85].)
Some progress has been made in [BB92].
[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |