How to realize LSE narrowing

Werner, Andreas; Bockmayr, Alexander; Krischer, Stefan

doi:10.1007/3-540-58431-5_7

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Conference Paper

How to realize LSE narrowing

MPS-Authors

/persons/resource/persons44149

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

External Resource

https://rdcu.be/dtoQ7
(Publisher version)

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

There are no public fulltexts stored in PuRe

Supplementary Material (public)

There is no public supplementary material available

Citation

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: https://hdl.handle.net/11858/00-001M-0000-0014-AD84-2

Abstract

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.