Help Guide Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse




Conference Paper

How to realize LSE narrowing


Bockmayr,  Alexander
Programming Logics, MPI for Informatics, Max Planck Society;

There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available

Werner, A., Bockmayr, A., & Krischer, S. (1994). How to realize LSE narrowing. In G. Levi, & M. Rodríguez-Artalejo (Eds.), Proceedings of the 4th International Conference on Algebraic and Logic Programming (ALP'94) (pp. 59-76). Berlin, Germany: Springer.

Cite as:
Narrowing is a complete unification procedure for equational theories defined by canonical term rewriting systems. It is also the operational semantics of various logic and functional programming languages. In an earlier paper, we introduced the LSE narrowing strategy which is complete for arbitrary canonical rewriting systems and optimal in the sense that two different LSE narrowing derivations cannot generate the same narrowing substitution. LSE narrowing improves all previously known strategies for arbitrary systems. According to their definition, LSE narrowing steps seem to be very expensive, because a large number of subterms has to be checked for reducibility. In this paper, we first show that many of these subterms are identical. Then we describe how using left-to-right basic occurrences the number of subterms that have to be tested can be reduced drastically. Finally, based on these theoretical results, we develop an efficient implementation of LSE narrowing.