Abstract
In this paper we analyze completeness results for basic narrowing. We show that basic narrowing is not complete with respect to normalizable solutions for equational theories defined by confluent term rewriting systems, contrary to what has been conjectured. By imposing syntactic restrictions on the rewrite rules we recover completeness. We refute a result of Hölldobler which states the completeness of basic conditional narrowing for complete (i.e. confluent and terminating) conditional term rewriting systems without extra variables in the conditions of the rewrite rules. We extend the completeness result of Giovannetti and Moiso for level-confluent and terminating conditional systems with extra variables in the conditions to systems that may also have extra variables in the right-hand sides of the rules.
Partially supported by ESPRIT Basic Research Action 3020, INTEGRATION.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
J.A. Bergstra and J.W. Klop, Conditional Rewrite Rules: Confluence and Termination. JCSS 32(3), pp. 323–362, 1986.
A. Bockmayr, Beiträge nur Theorie des Logisch-Funktionalen Programmierens, Ph.D. thesis, Universität Karlsruhe, 1990. (In German.)
P.G. Bosco, E. Giovannetti and C. Moiso, Refined Strategies for Semantic Unification, Proceedings TAPSOFT'87, Pisa, LNCS 250, pp. 276–290, 1987.
P.G. Bosco. E. Giovannetti and C. Moiso, Narrowing vs. SLD-Resolution, TCS 59, pp. 3–23, 1988.
J. Chabin and P. Réty, Narrowing Directed by a Graph of Terms, Proceedings RTA'91, Como, LNCS 488, pp. 112–123, 1991.
N. Dershowitz and J.-P. Jouannaud, Rewrite Systems, in: “Handbook of Theoretical Computer Science, Vol. B” (ed. J. van Leeuwen), North-Holland, pp. 243–320, 1990.
N. Dershowitz and M. Okada, A Rationale for Conditional Equational Programming, TCS 75, pp. 111–138, 1990.
N. Dershowitz, M. Okada and G. Sivakumar, Confluence of Conditional Rewrite Systems, Proceedings CTRS'87, Orsay, LNCS 308, pp. 31–44, 1987.
N. Dershowitz, M. Okada and G. Sivakumar, Canonical Conditional Rewrite Systems, Proceedings CADE'88, Argonne. LNCS 310, pp. 538–549, 1988.
N. Dershowitz and D.A. Plaisted, Logic Programming cum Applicative Programming, Proceedings SLP'85, Boston, pp. 54–66, 1985.
R. Echahed, On Completeness of Narrowing Strategies, TCS 72, pp. 133–146, 1990.
M. Fay, First-Order Unification in Equational Theories, Proceedings CADE'79, Austin, pp. 161–167, 1979.
L. Fribourg. SLOG: A Logic Programming Language Interpreter based on Clausal Superposition and Rewriting. Proceedings SLP'85, Boston, pp. 172–184, 1985.
E. Giovannetti, G. Levi, C. Moiso and C. Palamidessi, Kernel-LEAF: A Logic plus Functional Language, JCSS 42, pp. 139–185, 1991.
E. Giovannetti and C. Moiso, A Completeness Result for E-Unification Algorithms based on Conditional Narrowing, Proceedings of the Workshop on Foundations of Logic and Functional Programming, Trento, LNCS 306, pp. 157–167, 1986.
M. Hanus, Compiling Logic Programs with Equality, Proceedings of the International Workshop on Language Implementation and Logic Programming, Linköping, LNCS 456. pp. 387–401, 1990.
A. Herold, Combination of Unification Algorithms in Equational Theories, Ph.D. thesis, Universität Kaiserslautern, 1987.
G. Huet and J.J. Lévy, Call by Need Computations in Non-Ambiguous Linear Term Rewriting Systems, Report 359, INRIA, 1979.
S. Hölldobler, Foundations of Equational Logic Programming. LNAI 353, 1989.
J.-M. Hullot, Canonical Forms and Unification, Proceedings CADE'80, LNCS 87, pp. 318–334. 1980.
J.-M. Hullot, Compilation de Formes Canoniques dans les Théories Equationelles, Thèse de troisième cycle, Université de Paris Sud, Orsay, 1980. (In French).
H. Hußmann, Unification in Conditional-Equational Theories. Proceedings EUROCAL'85, LNCS 204, pp. 543–553, 1985.
S. Kaplan, Simplifying Conditional Term Rewriting Systems: Unification, Termination and Confluence, JSC 4(3), pp. 295–334. 1987.
C. Kirchner, Méthodes et Outils de Conception Systématique d'Algorithmes d'Unification dans les Théories Equationelles, Thèse de d'état, Université de Nancy I, 1985. (In French).
J.W. Klop, Term Rewriting Systems: from Church-Rosser to Knuth-Bendix and beyond, Proceedings ICALP'90, Warwick, LNCS 443, pp. 350–369, 1990.
J.W. Klop, Term Rewriting Systems, Report CS-R9073, CWI, Amsterdam. To appear in: “Handbook of Logic in Computer Science, Vol. I” (eds. S. Abramsky, D. Gabbay, T. Maibaum), Oxford University Press, 1991.
S. Krischer and A. Bockmayr, Detecting Redundant Narrowing Derivations by the LSE-SL Reducibility Test, Proceedings RTA'91, Como, LNCS 488, pp. 74–85,1991.
Corrado Moiso, personal communication, August 1991.
J.J. Moreno-Navarro and M. Rodríguez-Artalejo. BABEL: A Functional and Logic Programming Language based on Constructor Discipline and Narrowing, Proceedings ALP'89, Gaußig. LNCS 343, pp. 223–232, 1989.
W. Nutt, P. Réty and G. Smolka, Basic Narrowing Revisited, JSC 7, pp. 295–317, 1989.
Catuscia Palamidessi. personal communication, July 1991.
P. Réty, Improving Basic Narrowing Techniques, Proceedings RTA'87, Bordeaux, LNCS 256, pp. 228–241, 1987.
A. Yamamoto, Completeness of Extended Unification Based on Basic Narrowing, Proceedings LPC'88, Jerusalem, pp. 1–10, 1988.
Y.H. You, Enumerating Outer Narrowing Derivations for Constructor Based Term Rewriting Systems, JSC 7, pp. 319–343, 1989.
Author information
Authors and Affiliations
Corresponding author
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Middeldorp, A., Hamoen, E. (1992). Counterexamples to completeness results for basic narrowing (extended abstract). In: Kirchner, H., Levi, G. (eds) Algebraic and Logic Programming. ALP 1992. Lecture Notes in Computer Science, vol 632. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0013830
Download citation
DOI: https://doi.org/10.1007/BFb0013830
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55873-6
Online ISBN: 978-3-540-47302-2
eBook Packages: Springer Book Archive