Strict coherence of conditional rewriting modulo axioms. (English) Zbl 1386.68080
Summary: Conditional rewriting modulo axioms with rich types makes specifications and declarative programs very expressive and succinct and is used in all well-known rule-based languages. However, the current foundations of rewriting modulo axioms have focused for the most part on the unconditional and untyped case. The main purpose of this work is to generalize the foundations of rewriting modulo axioms to the conditional order-sorted case. A related goal is to simplify such foundations. In particular, even in the unconditional case, the notion of strict coherence proposed here makes rewriting modulo axioms simpler and easier to understand. Properties of strictly coherent conditional theories, like operational equi-termination of the \(\rightarrow_{R/B}\) and \(\rightarrow_{R,B}\) relations and general conditions for the conditional Church-Rosser property modulo \(B\) are also studied.
Keywords:
conditional rewriting modulo equations; coherence; order-sorted specifications; operational termination; Church-Rosser propertyReferences:
| [1] | Avenhaus, J.; Loría-Sáenz, C., On conditional rewrite systems with extra variables and deterministic logic programs, (Pfenning, F., Logic Programming and Automated Reasoning, 5th International Conference, LPAR 1994, Proceedings. Logic Programming and Automated Reasoning, 5th International Conference, LPAR 1994, Proceedings, LNCS, vol. 822 (1994), Springer), 215-229 |
| [2] | Baader, F.; Nipkow, T., Term Rewriting and All That (1998), Cambridge University Press |
| [3] | Bachmair, L.; Dershowitz, N., Completion for rewriting modulo a congruence, Theoret. Comput. Sci., 67, 2-3, 173-201 (1989) · Zbl 0686.68021 |
| [4] | Bergstra, J. A.; Klop, J. W., Conditional rewrite rules: confluence and termination, J. Comput. Syst. Sci., 32, 3, 323-362 (1986) · Zbl 0658.68031 |
| [5] | Bidoit, M.; Mosses, P. D., CASL User Manual—Introduction to Using the Common Algebraic Specification Language, Lecture Notes in Computer Science, vol. 2900 (2004), Springer · Zbl 1033.68025 |
| [6] | Bockmayr, A., Conditional narrowing modulo of set of equations, Appl. Algebra Engrg. Comm. Comput., 4, 147-168 (1993) · Zbl 0776.68068 |
| [7] | Borovanský, P.; Kirchner, C.; Kirchner, H.; Moreau, P.-E., ELAN from a rewriting logic point of view, Theoret. Comput. Sci., 285, 155-185 (2002) · Zbl 1001.68057 |
| [8] | Bouhoula, A.; Jouannaud, J.-P.; Meseguer, J., Specification and proof in membership equational logic, Theoret. Comput. Sci., 236, 35-132 (2000) · Zbl 0938.68057 |
| [9] | Bruni, R.; Meseguer, J., Semantic foundations for generalized rewrite theories, Theoret. Comput. Sci., 360, 1-3, 386-414 (2006) · Zbl 1097.68051 |
| [10] | Bürckert, H.-J., A Resolution Principle for a Logic with Restricted Quantifiers, Lecture Notes in Computer Science, vol. 568 (1991), Springer · Zbl 0985.03517 |
| [11] | Clavel, M.; Durán, F.; Eker, S.; Meseguer, J.; Lincoln, P.; Martí-Oliet, N.; Talcott, C., All About Maude—A High-Performance Logical Framework, LNCS, vol. 4350 (2007), Springer · Zbl 1115.68046 |
| [12] | Cohn, A. G., A more expressive formulation of many sorted logic, J. Automat. Reason., 3, 2, 113-200 (1987) · Zbl 0642.68166 |
| [13] | Cohn, A. G., Taxonomic reasoning with many-sorted logics, Artif. Intell. Rev., 3, 2-3, 89-128 (1989) |
| [14] | Comon, H., Completion of rewrite systems with membership constraints. Part I: deduction rules, J. Symbolic Comput., 25, 4, 397-419 (1998) · Zbl 0983.68091 |
| [15] | Comon, H., Completion of rewrite systems with membership constraints. Part II: constraint solving, J. Symbolic Comput., 25, 4, 421-453 (1998) · Zbl 0983.68092 |
| [16] | Dershowitz, N.; Jouannaud, J.-P., Rewrite systems, (van Leeuwen, J., Handbook of Theoretical Computer Science. Handbook of Theoretical Computer Science, Formal Models and Sematics (B) (1990), Elsevier), 244-320 · Zbl 0900.68283 |
| [17] | Dershowitz, N.; Plaisted, D., Rewriting, (Robinson, A.; Voronkov, A., Handbook of Automated Reasoning, vol. I (2001), Elsevier), 535-610, Chapter 9 · Zbl 0992.68123 |
| [18] | Durán, F.; Lucas, S.; Marché, C.; Meseguer, J.; Urbain, X., Proving operational termination of membership equational programs, High.-Order Symb. Comput., 21, 1-2, 59-88 (2008) · Zbl 1192.68154 |
| [19] | Durán, F.; Lucas, S.; Meseguer, J., Methods for proving termination of rewriting-based programming languages by transformation, Electron. Notes Theor. Comput. Sci., 248, 93-113 (2009) · Zbl 1337.68067 |
| [20] | Durán, F.; Lucas, S.; Meseguer, J., Termination modulo combinations of equational theories, (Frontiers of Combining Systems, 7th International Symposium, FroCoS 2009. Proceedings. Frontiers of Combining Systems, 7th International Symposium, FroCoS 2009. Proceedings, Trento, Italy, September 16-18, 2009. Frontiers of Combining Systems, 7th International Symposium, FroCoS 2009. Proceedings. Frontiers of Combining Systems, 7th International Symposium, FroCoS 2009. Proceedings, Trento, Italy, September 16-18, 2009, Lecture Notes in Computer Science, vol. 5749 (2009), Springer), 246-262 · Zbl 1193.68145 |
| [21] | Durán, F.; Meseguer, J., On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories, J. Algebr. Logic Program., 81, 816-850 (2012) · Zbl 1272.03139 |
| [22] | Eker, S., Associative-commutative rewriting on large terms, (Nieuwenhuis, R., RTA. RTA, Lecture Notes in Computer Science, vol. 2706 (2003), Springer), 14-29 · Zbl 1038.68560 |
| [23] | Escobar, S.; Sasse, R.; Meseguer, J., Folding variant narrowing and optimal variant termination, J. Algebr. Logic Program., 81, 898-928 (2012) · Zbl 1291.68217 |
| [24] | Frisch, A. M., The substitutional framework for sorted deduction: fundamental results on hybrid reasoning, Artif. Intell., 49, 1-3, 161-198 (1991) · Zbl 0736.68071 |
| [25] | Futatsugi, K.; Diaconescu, R., CafeOBJ Report (1998), World Scientific · Zbl 0962.68115 |
| [26] | Giesl, J.; Kapur, D., Dependency pairs for equational rewriting, (RTA 2001. RTA 2001, Lecture Notes in Computer Science, vol. 2051 (2001), Springer), 93-108 · Zbl 0981.68063 |
| [27] | Goguen, J.; Jouannaud, J.-P.; Meseguer, J., Operational semantics of order-sorted algebra, (Proc. ICALP 1985. Proc. ICALP 1985, LNCS, vol. 194 (1985), Springer), 221-231 · Zbl 0591.68041 |
| [28] | Goguen, J.; Meseguer, J., Equality, types, modules and (why not?) generics for logic programming, J. Logic Program., 1, 2, 179-210 (1984) · Zbl 0575.68091 |
| [29] | Goguen, J.; Meseguer, J., Completeness of many-sorted equational logic, Houston J. Math.. Houston J. Math., SIGPLAN Not., 16, 7, 24-37 (July 1981), Preliminary version in: |
| [30] | Goguen, J.; Meseguer, J., Unifying functional, object-oriented and relational programming with logical semantics, (Shriver, B.; Wegner, P., Research Directions in Object-Oriented Programming (1987), MIT Press), 417-477 |
| [31] | Goguen, J.; Meseguer, J., Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations, Theoret. Comput. Sci., 105, 217-273 (1992) · Zbl 0778.68056 |
| [32] | Goguen, J.; Winkler, T.; Meseguer, J.; Futatsugi, K.; Jouannaud, J.-P., Introducing OBJ, (Software Engineering with OBJ: Algebraic Specification in Action (2000), Kluwer), 3-167 |
| [33] | Haxthausen, A. E., Order-sorted algebraic specifications with higher-order functions, Theoret. Comput. Sci., 183, 2, 157-185 (1997) · Zbl 0901.68127 |
| [34] | Hendrix, J.; Meseguer, J., Order-sorted equational unification revisited, Electron. Notes Theor. Comput. Sci., 290, 37-50 (2012) · Zbl 1291.68220 |
| [35] | Hodges, W., A Shorter Model Theory (1997), Cambridge UP · Zbl 0873.03036 |
| [36] | Huet, G., Confluent reductions: abstract properties and applications to term rewriting systems, J. ACM, 27, 797-821 (1980) · Zbl 0458.68007 |
| [37] | Jouannaud, J.-P., Confluent and coherent equational term rewriting systems: application to proofs in abstract data types, (Ausiello, G.; Protasi, M., CAAP. CAAP, Lecture Notes in Computer Science, vol. 159 (1983), Springer), 269-283 · Zbl 0522.68013 |
| [38] | Jouannaud, J.-P.; Kirchner, H., Completion of a set of rules modulo a set of equations, SIAM J. Comput., 15, 1155-1194 (November 1986) · Zbl 0665.03005 |
| [39] | Jouannaud, J.-P.; Li, J., Church-Rosser properties of normal rewriting, (Cégielski, P.; Durand, A., CSL. CSL, LIPIcs, vol. 16 (2012), Schloss Dagstuhl—Leibniz-Zentrum fuer Informatik), 350-365 · Zbl 1252.68159 |
| [40] | Jouannaud, J.-P.; Muñoz, M., Termination of a set of rules modulo a set of equations, (CADE 1984. CADE 1984, Lecture Notes in Computer Science, vol. 170 (1984), Springer), 175-193 · Zbl 0546.68077 |
| [41] | Kaplan, S., Conditional rewrite rules, Theoret. Comput. Sci., 33, 175-193 (1984) · Zbl 0577.03013 |
| [42] | Kirchner, C., Order-Sorted Equational Unification (Dec. 1988), INRIA Lorraine & LORIA: INRIA Lorraine & LORIA Nancy, France, Technical report 954 |
| [43] | Kirchner, C.; Kirchner, H., Rewriting, Solving, Proving (2006), Unpublished book draft available online |
| [44] | Kirchner, C.; Kirchner, H.; Meseguer, J., Operational semantics of OBJ3, (Proc. ICALP 1988. Proc. ICALP 1988, LNCS, vol. 317 (1988), Springer), 287-301 · Zbl 0649.68028 |
| [45] | Lankford, D.; Ballantyne, A., Decision Procedures for Simple Equational Theories with a Commutative Axiom: Complete Sets of Commutative Reductions (1977), Department of Mathematics and Computer Science, Univ. of Texas: Department of Mathematics and Computer Science, Univ. of Texas Austin, Technical report ATP-35 |
| [46] | Lankford, D.; Ballantyne, A., Decision Procedures for Simple Equational Theories with Commutative-Associative Axioms: Complete Sets of Commutative-Associative Reductions (1977), Department of Mathematics and Computer Science, Univ. of Texas: Department of Mathematics and Computer Science, Univ. of Texas Austin, Technical report ATP-39 |
| [47] | Lankford, D.; Ballantyne, A., Decision Procedures for Simple Equational Theories with Permutative Axioms: Complete Sets of Permutative Reductions (1977), Department of Mathematics and Computer Science, Univ. of Texas: Department of Mathematics and Computer Science, Univ. of Texas Austin, Technical report ATP-37 |
| [48] | Lucas, S.; Marché, C.; Meseguer, J., Operational termination of conditional term rewriting systems, Inform. Process. Lett., 95, 4, 446-453 (2005) · Zbl 1185.68374 |
| [49] | Lucas, S.; Meseguer, J., Normal forms and normal theories in conditional rewriting, J. Log. Algebraic Methods Program., 85, 1, 67-97 (2016) · Zbl 1356.68124 |
| [50] | Marché, C., Normalised rewriting and normalised completion, (Proc. LICS’94 (1994), IEEE), 394-403 |
| [51] | Martí-Oliet, N.; Meseguer, J., Inclusions and subtypes II: higher-order case, J. Logic Comput., 6, 541-572 (1996) · Zbl 0931.03049 |
| [52] | Meseguer, J., General logics, (Ebbinghaus, E.-D.; etal., Logic Colloquium’87 (1989), North-Holland), 275-329 · Zbl 0691.03001 |
| [53] | Meseguer, J., Conditional rewriting logic as a unified model of concurrency, Theoret. Comput. Sci., 96, 1, 73-155 (1992) · Zbl 0758.68043 |
| [54] | Meseguer, J., Membership algebra as a logical framework for equational specification, (Proc. WADT’97. Proc. WADT’97, LNCS, vol. 1376 (1998), Springer), 18-61 · Zbl 0903.08009 |
| [55] | Meseguer, J., Twenty years of rewriting logic, J. Algebr. Logic Program., 81, 721-781 (2012) · Zbl 1267.03043 |
| [56] | Meseguer, J.; Goguen, J., Initiality, induction and computability, (Nivat, M.; Reynolds, J., Algebraic Methods in Semantics (1985), Cambridge University Press), 459-541 · Zbl 0571.68004 |
| [57] | Meseguer, J.; Goguen, J.; Smolka, G., Order-sorted unification, J. Symbolic Comput., 8, 383-413 (1989) · Zbl 0691.03002 |
| [58] | Mosses, P. D., CASL Reference Manual, the Complete Documentation of the Common Algebraic Specification Language, Lecture Notes in Computer Science, vol. 2960 (2004), Springer · Zbl 1046.68001 |
| [60] | Ohlebusch, E., Advanced Topics in Term Rewriting (2002), Springer-Verlag · Zbl 0999.68095 |
| [61] | Peterson, G. E.; Stickel, M. E., Complete sets of reductions for some equational theories, J. ACM, 28, 2, 233-264 (1981) · Zbl 0479.68092 |
| [62] | Plotkin, G. D., A Structural Approach to Operational Semantics, J. Log. Algebr. Program., 60-61, 17-139 (1981), Computer Science Department, Aarhus University, Previously published as technical report DAIMI FN-19 · Zbl 1082.68062 |
| [63] | Rocha, C.; Meseguer, J.; Muñoz, C., Rewriting modulo SMT and open system analysis, (Proc. WRLA 2014. Proc. WRLA 2014, LNCS, vol. 8663 (2014), Springer), 247-262 · Zbl 1367.68151 |
| [64] | Schmidt-Schauss, M., Computational aspects of order-sorted logic with term declarations, (LNCS, vol. 395 (1989), Springer) · Zbl 0689.68001 |
| [65] | Siekmann, J.; Szabó, P., A Noetherian and confluent rewrite system for idempotent semigroups, Semigroup Forum, 25, 83-110 (1982) · Zbl 0493.68087 |
| [66] | Smolka, G.; Aït-Kaci, H., Inheritance hierarchies: semantics and unification, J. Symbolic Comput., 7, 3/4, 343-370 (1989) · Zbl 0678.68009 |
| [67] | Smolka, G.; Nutt, W.; Goguen, J.; Meseguer, J., Order-sorted equational computation, (Nivat, M.; Aït-Kaci, H., Resolution of Equations in Algebraic Structures, vol. 2 (1989), Academic Press), 297-367 |
| [68] | TeReSe, Term Rewriting Systems (2003), Cambridge University Press · Zbl 1030.68053 |
| [69] | van Deursen, A.; Heering, J.; Klint, P., Language Prototyping: An Algebraic Specification Approach (1996), World Scientific · Zbl 0962.68114 |
| [70] | Viry, P., Equational rules for rewriting logic, Theoret. Comput. Sci., 285, 487-517 (2002) · Zbl 1001.68058 |
| [71] | Walther, C., A mechanical solution of Schubert’s steamroller by many-sorted resolution, Artif. Intell., 26, 2, 217-224 (1985) · Zbl 0569.68076 |
| [72] | Yamada, T.; Avenhaus, J.; Loría-Sáenz, C.; Middeldorp, A., Logicality of conditional rewrite systems, Theoret. Comput. Sci., 236, 1-2, 209-232 (2000) · Zbl 0938.68050 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
