Detecting Redundant Narrowing Derivations by the LSE-SL Reducibility Test

Krischer, Stefan; Bockmayr, Alexander

doi:10.1007/3-540-53904-2_87

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Conference Paper

Detecting Redundant Narrowing Derivations by the LSE-SL Reducibility Test

MPS-Authors

/persons/resource/persons44149

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

External Resource

https://rdcu.be/ds6H6
(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

Krischer, S., & Bockmayr, A. (1991). Detecting Redundant Narrowing Derivations by the LSE-SL Reducibility Test. In R. Book (Ed.), Proceedings of the 4th International Conference on Rewriting Techniques and Applications (RTA '91) (pp. 74-85). Berlin, Germany: Springer.

Cite as: https://hdl.handle.net/11858/00-001M-0000-0014-AE39-4

Abstract

Rewriting and narrowing provide a nice theoretical framework for the
integration of logic and functional programming. For practical applications
however, narrowing is still much too inefficient. In this paper we show how
reducibility tests can be used to detect redundant narrowing derivations. We
introduce a new narrowing strategy, LSE-SL left-to-right basic normal
narrowing, prove its completeness for arbitrary canonical term rewriting
systems, and demonstrate how it increases the efficiency of the narrowing
process.