Advertisement

Equational completion in order-sorted algebras extended abstract

  • Isabelle Gnaedig
  • Claude Kirchner
  • Hélène Kirchner
Algebraic Specifications
Part of the Lecture Notes in Computer Science book series (LNCS, volume 299)

Abstract

We describe and prove completion procedures for equational term rewriting systems in order-sorted algebras. Problems specific to order-sorted equational logic are emphasized.

Keywords

Inference Rule Operational Semantic Critical Pair Equational Logic Equational Term 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    P. Arnold, D. Coleman, C. Dollin, R. Gallimore, H. Gilchrist, and T. Rush. An introduction to the Axis specification language. Technical Report HPL-BRC-TM-87-034, HP Laboratories, Bristol research centre, 1987.Google Scholar
  2. [2]
    L. Bachmair and N. Dershowitz. Completion for rewriting modulo a congruence. In Proceedings Second Conference on Rewriting Techniques and Applications, Springer Verlag, Bordeaux (France), May 1987.Google Scholar
  3. [3]
    L. Bachmair, N. Dershowitz, and J. Hsiang. Orderings for equational proofs. In Proceeding of the first symposium on Logic In Computer Science, Boston (USA), 1986.Google Scholar
  4. [4]
    G. Bernot, M. Bidoit, and C. Choppy. Abstract data types with exception handling: an initial approach based on a distinction between exceptions and errors. Theoretical Computer Science, 46:13–45, 1986.Google Scholar
  5. [5]
    R.M. Burstall, D.B. MacQueen, and D.T. Sannella. Hope: an experimental applicative language, In Conference Record of the 1980 LISP Conference, pages 136–143. Stanford (Californie, USA), 1980.Google Scholar
  6. [6]
    R.J. Cunningham and A.J.J. Dick. Rewrite Systems on a Lattice of Types. Technical Report, Imperial College, Department of Computing, 1983.Google Scholar
  7. [7]
    N. Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17:279–301, 1982.Google Scholar
  8. [8]
    N. Dershowitz. Termination. In Proceedings 1st Conference on Rewriting Techniques and Applications, pages 180–224, Springer Verlag, Dijon (France), May 1985.Google Scholar
  9. [9]
    N. Dershowitz and D.A. Plaisted. Equational programming. to appear in Machine Intelligence 11, 1985.Google Scholar
  10. [10]
    A.J.J. Dick. Eril equational reasoning: an interactive laboratory. In B. Buchberger, editor, Proceedings of the EUROCAL conference, Springer-Verlag, Linz (Austria), 1985.Google Scholar
  11. [11]
    K. Futatsugi, J.A. Goguen, J.P. Jouannaud, and J. Meseguer. Principles of OBJ2. In Proceedings of 12th ACM Symposium on Principles of Programming Languages Conference, 1985.Google Scholar
  12. [12]
    I. Gnaedig. Order-sorted equational termination. in preparation, 1987.Google Scholar
  13. [13]
    I. Gnaedig, C. Kirchner, and H. Kirchner. Equational Completion in Order-sorted Algebras. Technical Report 87R086, Centre de Recherche en Informatique de Nancy, 1987.Google Scholar
  14. [14]
    J.A. Goguen, J.P. Jouannaud, and J. Meseguer. Operational semantics for order-sorted algebra. In Proceeding of the 12th ICALP, Nafplion (Greece), pages 221–231, 1985.Google Scholar
  15. [15]
    J.A. Goguen and J. Meseguer, Completeness of many-sorted equational logic. Technical Report CSLI-84-15, Center for the Study of Language and Information, Stanford University, 1984.Google Scholar
  16. [16]
    J.A. Goguen and J. Meseguer. Order-sorted algebra I: partial and overloaded operators, errors and inheritance. 1986.Google Scholar
  17. [17]
    J.A. Goguen and J. Meseguer. Order-sorted algebra solves the constructor-selector, multiple representation and coercion problem. In Proceeding of the second symposium on Logic In Computer Science, 1987.Google Scholar
  18. [18]
    J.A. Goguen and J. Meseguer. Remarks on remarks on many-sorted equational logic. Bulletin of EATCS, (30):66–73, October 1986.Google Scholar
  19. [19]
    J.A. Goguen, J. Meseguer, and D. Plaisted. Programming with parameterized abstract objects in OBJ. Theory And Practice of Software Technology, 163–193, 1982.Google Scholar
  20. [20]
    C.M. Hoffmann and M.J. O'Donnell. Programming with equations. Transactions on Programming Languages and Systems, 4(1), 1982.Google Scholar
  21. [21]
    J. Hsiang and N. Dershowitz. Rewrite methods for clausal and non-clausal theorem proving. In Proceedings of 10th ICALP, pages 331–346, Springer-Verlag, Barcelona (Spain), 1983.Google Scholar
  22. [22]
    G. Huet. A complete proof of correctness of the Knuth and Bendix completion algorithm. Journal of Computer Systems and Sciences, 23:11–21, 1981.Google Scholar
  23. [23]
    G. Huet. Confluent reductions: abstract properties and applications to term rewriting systems. Journal of the Association for Computing Machinery, 27(4):797–821, 1980. Preliminary version in 18th Symposium on Foundations Of Computer Science, IEEE, 1977.Google Scholar
  24. [24]
    G. Huet and J.M. Hullot. Proofs by induction in equational theories with constructors. Journal of the Association for Computing Machinery, 25(2):239–266, 1982. Preliminary version in Proceedings 21st Symposium on Foundations of Computer Science, IEEE, 1980.Google Scholar
  25. [25]
    G. Huet and D. Oppen. Equations and rewrite rules: a survey. In R. Book, editor, Formal Language Theory: Perspectives and Open Problems. Academic Press, 1980.Google Scholar
  26. [26]
    J.P. Jouannaud. Church-rosser computations with equational term rewriting systems. In G. Ausiello and M. Protasi, editors, Proceedings of the 4th Conference on Automata, Algebra and Programming, Lecture Notes in Computer Science, Volume 159, Springer-Verlag, 1983.Google Scholar
  27. [27]
    J-P. Jouannaud. Proof algebras. Invited conference to the second Rewriting Techniques and Applications conference, Bordeaux (France), 1987.Google Scholar
  28. [28]
    J.P. Jouannaud and H. Kirchner. Completion of a set of rules modulo a set of equations. SIAM Journal of Computing, 15(4), 1986. Preliminary version in Proceedings 11th ACM Symposium on Principles of Programming Languages, Salt Lake City, 1984.Google Scholar
  29. [29]
    J.P. Jouannaud and H. Kirchner. Completion of a set of rules modulo a set of equations. Proceedings 11th ACM Symposium on Principles Of Programming Languages, Salt Lake City, 1984.Google Scholar
  30. [30]
    J.P. Jouannaud and M. Munoz. Termination of a set of rules modulo a set of equations. In Proceedings of the 7th Conference on Automated Deduction, Springer-Verlag, Napa Valley (California, USA), 1984.Google Scholar
  31. [31]
    C. Kirchner. Méthodes et outils de conception systématique d'algorithmes d'unification dans les théories équationnelles. Thèse d'état de l'Université de Nancy I, 1985.Google Scholar
  32. [32]
    C. Kirchner. Methods and tools for equational unification. In Proceedings of the Colloquium on Resolution of Equations in Algebraic Structures, May 1987.Google Scholar
  33. [33]
    C. Kirchner. Order sorted equational matching. In preparation, 1987.Google Scholar
  34. [34]
    C. Kirchner. Order sorted equational unification. In preparation, 1987.Google Scholar
  35. [35]
    C. Kirchner and H. Kirchner. Reveur-3: implementation of a general completion procedure parametrized by built-in theories and strategies. Science of Computer Programming, (8), 1987.Google Scholar
  36. [36]
    C. Kirchner, H. Kirchner, and J. Meseguer. Operational semantics of OBJ3. Technical Report 87-R-87, Centre de Recherche en Informatique de Nancy, 1987.Google Scholar
  37. [37]
    H. Kirchner. A general inductive completion algorithm and application to abstract data types. In R. Shostak, editor, Proceedings 7th international Conference on Automated Deduction, Springer-Verlag, Napa Valley (California, USA), 1984.Google Scholar
  38. [38]
    H. Kirchner. Preuves par complétion dans les variétés d'algèbres. Thèse d'état de l'Université de Nancy I, 1985.Google Scholar
  39. [39]
    D. Knuth and P. Bendix. Simple word problems in universal algebra. In J. Leech, editor, Computational Problems in Abstract Algebra, Pergamon Press, 1970.Google Scholar
  40. [40]
    D. Lankford and A. Ballantyne. Decision procedures for simple equational theories with associative commutative axioms: complete sets of associative commutative reductions. Technical Report, Univ. of Texas at Austin, Dept. of Mathematics and Computer Science, 1977.Google Scholar
  41. [41]
    D. Lankford and A. Ballantyne. Decision Procedures for Simple Equational Theories with Commutative Axioms: Complete Sets of Commutative Reductions. Technical Report, University of Texas at Austin, Dept. of Mathematics and Computer Science, 1977.Google Scholar
  42. [42]
    D. Lankford and A. Ballantyne. Decision procedures for simple equational theories with permutative axioms: complete sets of permutative reductions. Technical Report, Univ. of Texas at Austin, Dept. of Mathematics and Computer Science, 1977.Google Scholar
  43. [43]
    J. Meseguer and J.A. Goguen. Initiality, induction and computability. In M. Nivat and J. Reynolds, editors, Algebraic Methods in Semantics, Cambridge University Press, 1985.Google Scholar
  44. [44]
    J. Meseguer, J.A. Goguen, and G. Smolka. Order sorted unification. In Proceedings of the Colloquium on Resolution of Equations in Algebraic Structures, May 1987.Google Scholar
  45. [45]
    M. H. A. Newman. On theories with a combinatorial definition of Equivalence. Annals of Math, 43(2):223–243, 1942.Google Scholar
  46. [46]
    W. Nutt, G. Smolka, J.A. Goguen, and J. Meseguer. Order sorted computation. In Proceedings of the Colloquium on Resolution of Equations in Algebraic Structures, May 1987.Google Scholar
  47. [47]
    G. Peterson and M. Stickel. Complete sets of reductions for some equational theories. Journal of the Association for Computing Machinery, 28:233–264, 1981.Google Scholar
  48. [48]
    M. Schmidt-Schauss. Unification in many sorted equational theories. In J. Siekmann, editor, Proceedings 8th Conference on Automated Deduction, Oxford, Springer Verlag, Oxford (England). 1986.Google Scholar
  49. [49]
    Y. Toyama. Term rewriting systems with membership conditions. In Proceedings of the first international workshop on conditional term rewriting systems, Orsay (France), July 1987.Google Scholar
  50. [50]
    D.A. Turner. Miranda: a non-strict functional language with polymorphic types. In Proc. 2nd Conf. on Functional Programming Languages and Computer Architecture, pages 1–16, Springer Verlag, Nancy (France), 1985.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1988

Authors and Affiliations

  • Isabelle Gnaedig
    • 1
  • Claude Kirchner
    • 1
  • Hélène Kirchner
    • 1
  1. 1.CRIN/INRIAVandoeuvre les NancyFrance

Personalised recommendations