Skip to main content
SpringerLink
Log in

Conditional narrowing modulo a set of equations

  • Published:
Applicable Algebra in Engineering, Communication and Computing Aims and scope

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Bachmair, L.: Associative-commutative reduction orderings. Technical Report MPI-1-91-209, Max-Planck-Institut für Informatik, Saarbrücken 1991

    Google Scholar 

  2. Ben Cherifa, A., Lescanne, P.: Termination of rewriting systems by polynomial interpretations and its implementation. Sci. Comput. Programming9, 137–159 (1987)

    Google Scholar 

  3. Brand, D., Darringer, J. A., Joyner, W. H.: Completeness of conditional reductions. Research report RC 7404, IBM, 1978

  4. 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

    Google Scholar 

  5. Boyer, R. S., Moore, J. S.: A computational logic. New York: Academic Press 1979

    Google Scholar 

  6. 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

  7. 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

    Google Scholar 

  8. Bockmayr, A.: Contributions to the Theory of Logic-Functional Programming. PhD thesis, Fakultät für Informatik, Univ. Karlsruhe, 1990. (in German)

  9. 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

    Google Scholar 

  10. Bachmair, L., Plaisted, D. A.: Termination orderings for associative-commutative rewriting systems. J. Symb. Comput.1, 329–349 (1985)

    Google Scholar 

  11. Colmerauer, A.: Introduction to PROLOG III. In: 4th Annual ESPRIT Conference, Bruxelles. Amsterdam: North Holland, 1987

    Google Scholar 

  12. Darlington, J., Guo, Y., Paul, H.: A new perspective on integrating functional and logic languages. Imperial College, London, September 1991

    Google Scholar 

  13. DeGroot, D., Lindstrom, G. (eds.): Logic Programming. Functions, Relations and Equations. Englewood: Prentice Hall 1986

    Google Scholar 

  14. Dershowitz, N., Manna, Z.: Providing termination with multiset orderings. Comm. ACM22, 465–476 (1979)

    Google Scholar 

  15. Dershowitz, N., Okada, M.: A rationale for conditional equational programming. Theoretical Comput. Sci.75, 111–138 (1990)

    Google Scholar 

  16. Dershowitz, N., Plaisted, D. A.: Logic programming cum applicative programming. In: Proc. Intern. Symposium on Logic Programming, Boston. IEEE, 1985

    Google Scholar 

  17. 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

  18. Fay, M.: First-order unification in an equational theory. In: 4th Workshop on Automated Deduction, Austin, Texas, 1979

  19. 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

    Google Scholar 

  20. Geser, A.: Termination Relative. PhD thesis, Univ. Passau, 1990

  21. 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

    Google Scholar 

  22. Gnaedig, I.: Investigations on termination of equational rewriting. Technical Report 732, INRIA, 1987

  23. Huet, G., Oppen, D. C.: Equations and rewrite rules, A survey. In: Book, R. V. (ed.) Formal Language Theory. New York: Academic Press 1980

    Google Scholar 

  24. Hölldobler, S.: Foundations of Equational Logic Programming. Lecture Notes in Computing Science, vol. 353. Berlin, Heidelberg, New York: Springer 1989

    Google Scholar 

  25. 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

    Google Scholar 

  26. 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

    Google Scholar 

  27. Hussmann, H.: Corrigenda to MIP-8502 “Unification in conditional equational theories”. Univ. Passau, April/October, 1988

  28. Jouannaud, J. P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput.15(4), 1155–1194 (1986)

    Google Scholar 

  29. 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

    Google Scholar 

  30. Jaffar, J., Lassez, J.-L.: Constraint logic programming. In: Proc. 14th ACM Symp. Principles of Programming Languages, Munich, 1987

  31. 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

    Google Scholar 

  32. 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

    Google Scholar 

  33. Kaplan, S.: Conditional rewrite rules. Theoret. Comput. Sci.33, 175–193 (1984)

    Google Scholar 

  34. Kaplan, S.: Fair conditional term rewriting systems: Unification, termination and confluence. Technical Report 194, L. R. I., Univ. Paris-Sud, 1984

    Google Scholar 

  35. Kaplan, S.: Simplifying conditional term rewriting systems: Unification, termination and confluence. J. Symb. Comput.4, 295–334 (1987)

    Google Scholar 

  36. 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

    Google Scholar 

  37. 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

  38. 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

    Google Scholar 

  39. Middeldorp, A., Hamoen, E.: Counterexamples to completeness results for basic narrowing. Technical Report CS-R9154, CWI Amsterdam, December 1991

    Google Scholar 

  40. 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

    Google Scholar 

  41. Padawitz, P.: Computing in Horn Clause Theories, vol. 16 of EATCS Monograph. Berlin, Heidelberg, New York: Springer 1988

    Google Scholar 

  42. 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

    Google Scholar 

  43. Peterson, G. E., Stickel, M.: Complete sets of reductions for some equational theories. J. Assoc. Comput. Machinery28, 182–215 (1981)

    Google Scholar 

  44. 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

    Google Scholar 

  45. 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

    Google Scholar 

  46. Werner, A.: Termersetzung und Narrowing mit geordneten Sorten. Diplomarbeit, Fakultät für Informatik, Univ. Karlsruhe, 1991

    Google Scholar 

  47. 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

  48. 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

    Google Scholar 

  49. 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

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Max-Planck-Institut für Informatik, Im Stadtwald, W-6600, Saarbrücken, Germany

    Alexander Bockmayr

Authors
  1. Alexander Bockmayr
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints 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

Download citation

  • Received:

  • Revised:

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF01202035

Keywords

Search

Navigation