Abstract
Narrowing is a universal unification procedure for equational theories given by a canonical term rewrite system. In this paper we introduce conditional narrowing modulo a set of conditional equations and give a full proof of its correctness and completeness for equational conditional rewrite systemsR, E without extravariables whereE is regular andR, E is Church-Rosser moduloE and decreasing moduloE. This result can be seen as the theoretical foundation of a special form of constraint logic and functional programming.
Similar content being viewed by others
References
Bachmair, L.: Associative-commutative reduction orderings. Technical Report MPI-1-91-209, Max-Planck-Institut für Informatik, Saarbrücken 1991
Ben Cherifa, A., Lescanne, P.: Termination of rewriting systems by polynomial interpretations and its implementation. Sci. Comput. Programming9, 137–159 (1987)
Brand, D., Darringer, J. A., Joyner, W. H.: Completeness of conditional reductions. Research report RC 7404, IBM, 1978
Bertling, H., Ganzinger, H.: Completion-time optimization of rewrite-time goal solving. In: Proc. Rewriting Techniques and Applications, Chapel Hill. Lecture Notes in Computing Science, vol. 355. Berlin, Heidelberg, New York: Springer 1989
Boyer, R. S., Moore, J. S.: A computational logic. New York: Academic Press 1979
Bockmayr, A.: Conditional rewriting and narrowing as a theoretical framework for logic-functional programming: A survey. Technical Report 10/86, Fakultät für Informatik, Univ. Karlsruhe, 1986
Bockmayr, A.: Narrowing with built-in theories. In: First Int. Workshop Algebraic and Logic Programming, Gaußig. Lecture Notes in Computing Science, vol. 343. Berlin, Heidelberg, New York: Springer 1988
Bockmayr, A.: Contributions to the Theory of Logic-Functional Programming. PhD thesis, Fakultät für Informatik, Univ. Karlsruhe, 1990. (in German)
Boudet, A.: Unification in a combination of equational theories: an efficient algorithm. In: Proc. 10th CADE, Kaiserslautern. Lecture Notes in Computing Science, vol. 449. Berlin, Heidelberg, New York: Springer 1990
Bachmair, L., Plaisted, D. A.: Termination orderings for associative-commutative rewriting systems. J. Symb. Comput.1, 329–349 (1985)
Colmerauer, A.: Introduction to PROLOG III. In: 4th Annual ESPRIT Conference, Bruxelles. Amsterdam: North Holland, 1987
Darlington, J., Guo, Y., Paul, H.: A new perspective on integrating functional and logic languages. Imperial College, London, September 1991
DeGroot, D., Lindstrom, G. (eds.): Logic Programming. Functions, Relations and Equations. Englewood: Prentice Hall 1986
Dershowitz, N., Manna, Z.: Providing termination with multiset orderings. Comm. ACM22, 465–476 (1979)
Dershowitz, N., Okada, M.: A rationale for conditional equational programming. Theoretical Comput. Sci.75, 111–138 (1990)
Dershowitz, N., Plaisted, D. A.: Logic programming cum applicative programming. In: Proc. Intern. Symposium on Logic Programming, Boston. IEEE, 1985
López Fraguas, F. J., Rodriguez Artalejo, M.: An approach to constraint functional logic programming. Technical Report DIA 91/4, Univ. Compl. Madrid, October 1991
Fay, M.: First-order unification in an equational theory. In: 4th Workshop on Automated Deduction, Austin, Texas, 1979
Ganzinger, H.: Ground term confluence in parametric conditional equational specifications. In: Proc. STACS'87. Lecture Notes in Computing Science, vol. 247. Berlin, Heidelberg, New York: Springer 1987
Geser, A.: Termination Relative. PhD thesis, Univ. Passau, 1990
Giovannetti, E., Moiso, C.: A completeness result forE-unification algorithms based on conditional narrowing. In: Foundations of Logic and Functional Programming, Trento. Lecture Notes in Computing Science, vol. 306. Berlin, Heidelberg, New York: Springer 1986
Gnaedig, I.: Investigations on termination of equational rewriting. Technical Report 732, INRIA, 1987
Huet, G., Oppen, D. C.: Equations and rewrite rules, A survey. In: Book, R. V. (ed.) Formal Language Theory. New York: Academic Press 1980
Hölldobler, S.: Foundations of Equational Logic Programming. Lecture Notes in Computing Science, vol. 353. Berlin, Heidelberg, New York: Springer 1989
Hullot, J. M.: Canonical forms and unification. In: Proc. 5th Conference on Automated Deduction, Les Arcs. Lecture Notes in Computing Science, vol. 87. Berlin, Heidelberg, New York: Springer 1980
Hussmann, H.: Unification in conditional-equational theories. Technical Report MIP-8502, Univ. Passau, Jan. 1985. Short version: EUROCAL 85, Linz, Lecture Notes in Computing Science, vol. 204. Berlin, Heidelberg, New York: Springer 1985
Hussmann, H.: Corrigenda to MIP-8502 “Unification in conditional equational theories”. Univ. Passau, April/October, 1988
Jouannaud, J. P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput.15(4), 1155–1194 (1986)
Jouannaud, J. P., Kirchner, C., Kirchner, H.: Incremental construction of unification algorithms in equational theories. In: Proc. 10th ICALP, Barcelona. Lecture Notes in Computing Science, vol. 154. Berlin, Heidelberg, New York: Springer 1983
Jaffar, J., Lassez, J.-L.: Constraint logic programming. In: Proc. 14th ACM Symp. Principles of Programming Languages, Munich, 1987
Jouannaud, J. P., Munoz, M.: Termination of a set of rules modulo a set of equations. In: Proc. 7th Conference on Automated Deduction, Napa Valley. Lecture Notes in Computing Science, vol. 154. Berlin, Heidelberg, New York: Springer 1984
Jouannaud, J. P.: Church-Rosser computations with equational term rewriting systems. In: Proc. 8th CAAP, L'Aquila. Lecture Notes in Computing Science, vol. 159. Berlin, Heidelberg, New York: Springer 1983
Kaplan, S.: Conditional rewrite rules. Theoret. Comput. Sci.33, 175–193 (1984)
Kaplan, S.: Fair conditional term rewriting systems: Unification, termination and confluence. Technical Report 194, L. R. I., Univ. Paris-Sud, 1984
Kaplan, S.: Simplifying conditional term rewriting systems: Unification, termination and confluence. J. Symb. Comput.4, 295–334 (1987)
Krischer, S., Bockmayr, A.: Detecting redundant narrowing derivations by the LSE-SL reducibility test. In: Proc. Rewriting Techniques and Applications, Como. Lecture Notes in Computing Science, vol. 488. Berlin, Heidelberg, New York: Springer 1991
Kirchner, G.: Methodes et outils de conception systématique d'algorithmes d'unification dans les théories equationnelles, 1985. Thèse d'Etat, Univ. Nancy
Kapur, D., Sivakumar, G., Zhang, H.: A new method for proving termination of AC-rewrite systems. In: Foundations of Software Technology and Theoretical Computer Science, New Delhi. Lecture Notes in Computing Science, vol. 472. Berlin, Heidelberg, New York: Springer 1990
Middeldorp, A., Hamoen, E.: Counterexamples to completeness results for basic narrowing. Technical Report CS-R9154, CWI Amsterdam, December 1991
Narendran, P., Rusinowitsch, M.: A ground associative-commutative theory has a finite canonical system. In: Proc. Rewriting Techniques and Applications, Como. Lecture Notes in Computing Science, vol. 488. Berlin, Heidelberg, New York: Springer 1991
Padawitz, P.: Computing in Horn Clause Theories, vol. 16 of EATCS Monograph. Berlin, Heidelberg, New York: Springer 1988
Porat, S., Francez, N.: Full-commutation and fair-termination in equational and combined term rewriting systems. In: Proc. 8th Conference on Automated Deduction, Oxford. Lecture Notes in Computing Science, vol. 230. Berlin, Heidelberg, New York: Springer 1986
Peterson, G. E., Stickel, M.: Complete sets of reductions for some equational theories. J. Assoc. Comput. Machinery28, 182–215 (1981)
Remy, J. L.: Etude des systèmes de réécriture conditionnels et applications. Thèse de Doctorat d'Etat, Institut National de Polytechnique de Lorraine, Nancy, 1982
Steinbach, J.: AC-termination of rewrite systems: a modified Knuth-Bendix-ordering. In: Proc. Algebraic and Logic Programming, Nancy. Lecture Notes in Computing Science, vol. 463. Berlin, Heidelberg, New York: Springer 1990
Werner, A.: Termersetzung und Narrowing mit geordneten Sorten. Diplomarbeit, Fakultät für Informatik, Univ. Karlsruhe, 1991
Zhang, H.: REVEUR 4: Etude et mise en oeuvre de la réécriture conditionnelle. Thèse de Doctorat de 3ème cycle, Univ. de Nancy, CRIN, 1984
Zhang, H., Kapur, D.: First-order theorem proving using conditional rewriting rules. In: Proc. 9th CADE, Oxford. Lecture Notes in Computing Science, vol. 310. Berlin, Heidelberg, New York: Springer 1988
Zhang, H., Rémy, J. L.: Contextual rewriting. In: Proc. Rewriting Techniques and Applications, Dijon. Lecture Notes in Computing Science, vol. 202. Berlin, Heidelberg, New York: Springer 1985
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Bockmayr, A. Conditional narrowing modulo a set of equations. AAECC 4, 147–168 (1993). https://doi.org/10.1007/BF01202035
Received:
Revised:
Issue Date:
DOI: https://doi.org/10.1007/BF01202035