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 [BKW93], 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.
The first author's work was supported by the Deutsche Forschungsgemeinschaft as part of the SFB 314 (project S2). The second author's work was supported by the German Ministry for Research and Technology (BMFT) (contract ITS 9103) and the ESPRIT Working Group CCL (contract EP 6028). The third author's work was supported by the Centre National de la Recherche Scientifique (CNRS), and the Conseil Régional de Lorraine.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
A. Bockmayr, S. Krischer and A. Werner. An Optimal Narrowing Strategy for General Canonical Systems. In Conditional Term Rewriting Systems, CTRS 1992, Pont-à-Mousson, France, LNCS 656, Springer-Verlag, 1993.
A. Bockmayr, S. Krischer and A. Werner. Narrowing Strategies for Arbitrary Canonical Systems. Interner Bericht 22/93, Fakultät für Informatik, University of Karlsruhe, 1993. To appear in Fundamenta Informaticae.
A. Bockmayr and A. Werner. LSE Narrowing for Decreasing Conditional Term Rewrite Systems. To appear in Conditional Term Rewriting Systems, CTRS 1994, Jerusalem, Israel, 1994.
M. Gollner and C. Scharnhorst. Integration logischer und funktionaler Sprachkonzepte mit dem normalisierenden Narrowing-System KANN. In Proc. Workshop ”Sprachen für KI-Anwendungen”, Bericht 12/92-I, Univ. Münster, 1992.
D. DeGroot and G. Lindstrom. Logic Programming. Functions, Relations, and Equations. Prentice Hall, 1986.
N. Dershowitz, J.P. Jouannaud. Rewrite Systems, in: Handbook of Theoretical Computer Science, Volume B, Chapter 6, pages 244–320, Elsevier Science Publishers North-Holland, 1990.
M. Gollner. Implicit, Explicit and Consistent-Explicit Basic-Indexing. In Implementation of Logical-Functional Languages. Interner Bericht 10/92, Fakultät für Informatik, Univ. Karlsruhe, 1993.
M. Hanus. Efficient Implementation of Narrowing and Rewriting. In Proc. International Workshop on Processing Declarative Knowledge, Kaiserslautern, LNAI 567, Springer-Verlag, 1991.
M. Hanus. Integration of Funtions into Logic Programming: A Survey. MPI-Report MPI-I-94-201, Max-Planck-Institut für Informatik, Saarbrücken, 1994. To appear in Journal of Logic Programming.
A. Herold. Narrowing Techniques Applied to Idempotent Unification. SEKI Report SR-86-16, Univ. Kaiserslautern, 1986.
G. Huet and D.C. Oppen. Equations and Rewrite Rules: A Survey. In R. Book, editor, Formal Languages: Perspectives and Open Problems, Academic Press, 1980.
J. M. Hullot. Canonical Forms and Unification, In Proc. 5th Conference on Automated Deduction, Les Arcs, France, 1980, LNCS 87, Springer-Verlag.
S. Krischer: Vergleich und Bewertung von Narrowing-Strategien. Diplomarbeit, Fakultät für Informatik, Univ. Karlsruhe, 1990.
S. Krischer and A. Bockmayr. Detecting Redundant Narrowing Derivations by the LSE-SL Reducibility Test. In Proc. 4th International Conference on Rewríting Techniques and Applications, RTA-91, Como, LNCS 488, Springer-Verlag, 1991.
P. Réty: Improving Basic Narrowing Techniques. In Proc. 2nd International Conference on Rewriting Techniques and Applications, RTA-87, Bordeaux, LNCS 256, Springer-Verlag, 1987.
D. H. Warren: An Abstract Prolog Instruction Set. Technical Report 309, Artificial Intelligence Center, SRI International, 1983.
A. Werner, A. Bockmayr and S. Krischer. How to Realize LSE Narrowing, Interner Bericht 6/93, Fakultät für Informatik, Univ. Karlsruhe, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag
About this paper
Cite this paper
Werner, A., Bockmayr, A., Krischer, S. (1994). How to realize LSE narrowing. In: Levi, G., Rodríguez-Artalejo, M. (eds) Algebraic and Logic Programming. ALP 1994. Lecture Notes in Computer Science, vol 850. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58431-5_7
Download citation
DOI: https://doi.org/10.1007/3-540-58431-5_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58431-5
Online ISBN: 978-3-540-48791-3
eBook Packages: Springer Book Archive