de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch
 
Hilfe Wegweiser Impressum Kontakt Einloggen
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Konferenzbeitrag

How to realize LSE narrowing

MPG-Autoren
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44149

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

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

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.


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