×

Ground confluence of order-sorted conditional specifications modulo axioms. (English) Zbl 1498.68073

Summary: Terminating functional programs should be deterministic, i.e., should evaluate to a unique result, regardless of the evaluation order. For equational functional programs such determinism is exactly captured by the ground confluence property. For operationally terminating conditional equations this is equivalent to ground local confluence, which follows from local confluence. Checking local confluence by computing critical pairs is the standard way to check ground confluence [M. Bezem (ed.) et al., Terese. Term rewriting systems. Cambridge: Cambridge University Press (2003; Zbl 1030.68053)]. The problem is that some perfectly reasonable equational programs are not locally confluent and it can be very hard or even impossible to make them so by adding more equations. We propose three methods, called Methods 1-3, that can be synergistically combined to prove an order-sorted conditional specification modulo axioms \(B\) ground locally confluent. Method 1 applies the strategy proposed in [F. Durán and J. Meseguer, J. Log. Algebr. Program. 81, No. 7–8, 816–850 (2012; Zbl 1272.03139)] to use non-joinable critical pairs as completion hints to either achieve local confluence or reduce the number of critical pairs. Method 2 uses the inductive joinability inference system proposed in this paper to try to prove the critical pairs remaining after applying Method 1 ground joinable. It can furthermore show ground local confluence of the original specification. Method 3 is hierarchical in nature: it can be used to prove the ground local confluence of a conditional equational specification whose conditions belong to a subspecification that has already been proved ground confluent and operationally terminating, and that is conservatively extended by the overall specification in an appropriate sense. These methods apply to order-sorted and possibly conditional equational programs modulo axioms such as, e.g., Maude functional modules. We show their effectiveness in proving the ground confluence of non-trivial examples that have eluded previous proof attempts.

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68N18 Functional programming and lambda calculus
68Q42 Grammars and rewriting systems
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

MTT; OBJ3; CSI; CRC 3; Maude; CafeOBJ
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Aoto, T.; Yoshida, J.; Toyama, Y., Proving confluence of term rewriting systems automatically, (Treinen, R., Rewriting Techniques and Applications, 20th International Conference. Rewriting Techniques and Applications, 20th International Conference, RTA. Rewriting Techniques and Applications, 20th International Conference. Rewriting Techniques and Applications, 20th International Conference, RTA, Lecture Notes in Computer Science, vol. 5595 (2009), Springer), 93-102 · Zbl 1242.68125
[2] 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, Proc. 5th International Conference. Logic Programming and Automated Reasoning, Proc. 5th International Conference, LPAR 1994. Logic Programming and Automated Reasoning, Proc. 5th International Conference. Logic Programming and Automated Reasoning, Proc. 5th International Conference, LPAR 1994, Lecture Notes in Computer Science, vol. 822 (1994), Springer), 215-229
[3] Bouhoula, A., Simultaneous checking of completeness and ground confluence for algebraic specifications, ACM Trans. Comput. Log., 10, 3, 1-33 (2009) · Zbl 1351.68171
[4] Bouhoula, A.; Jouannaud, J. P.; Meseguer, J., Specification and proof in membership equational logic, Theor. Comput. Sci., 236, 35-132 (2000) · Zbl 0938.68057
[5] Bruni, R.; Meseguer, J., Semantic foundations for generalized rewrite theories, Theor. Comput. Sci., 360, 1-3, 386-414 (2006) · Zbl 1097.68051
[6] 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
[7] Cohen, P., Set Theory and the Continuum Hypothesis (1966), W.A. Benjamin · Zbl 0182.01301
[8] Comon-Lundh, H.; Delaune, S., The finite variant property: how to get rid of some algebraic properties, (Term Rewriting and Applications, 16th International Conference. Term Rewriting and Applications, 16th International Conference, RTA. Term Rewriting and Applications, 16th International Conference. Term Rewriting and Applications, 16th International Conference, RTA, Lecture Notes in Computer Science, vol. 3467 (2005), Springer), 294-307 · Zbl 1078.68059
[9] Dershowitz, N.; Jouannaud, J. P., Rewrite systems, (van Leeuwen, J., Handbook of Theoretical Computer Science, vol. B (1990), North-Holland), 243-320 · Zbl 0900.68283
[10] 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
[11] Durán, F.; Lucas, S.; Meseguer, J., MTT: the Maude termination tool (system description), (Automated Reasoning, 4th International Joint Conference. Automated Reasoning, 4th International Joint Conference, IJCAR. Automated Reasoning, 4th International Joint Conference. Automated Reasoning, 4th International Joint Conference, IJCAR, Lecture Notes in Computer Science, vol. 5195 (2008), Springer), 313-319 · Zbl 1165.68360
[12] Durán, F.; Lucas, S.; Meseguer, J., Termination modulo combinations of equational theories, (Ghilardi, S.; Sebastiani, R., Frontiers of Combining Systems, 7th International Symposium. Frontiers of Combining Systems, 7th International Symposium, FroCoS. Frontiers of Combining Systems, 7th International Symposium. Frontiers of Combining Systems, 7th International Symposium, FroCoS, Lecture Notes in Computer Science, vol. 5749 (2009), Springer), 246-262 · Zbl 1193.68145
[13] Durán, F.; Meseguer, J., A Church-Rosser checker tool for conditional order-sorted equational Maude specifications (long version) (2010), available at · Zbl 1306.68065
[14] Durán, F.; Meseguer, J., On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories, J. Log. Algebraic Program., 81, 7-8, 816-850 (2012) · Zbl 1272.03139
[15] Durán, F.; Meseguer, J.; Rocha, C., Proving ground confluence of equational specifications modulo axioms, (Rewriting Logic and Its Applications - 12th International Workshop. Rewriting Logic and Its Applications - 12th International Workshop, WRLA. Rewriting Logic and Its Applications - 12th International Workshop. Rewriting Logic and Its Applications - 12th International Workshop, WRLA, Lecture Notes in Computer Science, vol. 11152 (2018), Springer), 184-204 · Zbl 1517.68159
[16] Durán, F.; Rocha, C.; Álvarez, J. M., Towards a Maude formal environment, (Formal Modeling: Actors, Open Systems, Biological Systems. Formal Modeling: Actors, Open Systems, Biological Systems, Lecture Notes in Computer Science, vol. 7000 (2011), Springer), 329-351
[17] Escobar, S.; Sasse, R.; Meseguer, J., Folding variant narrowing and optimal variant termination, J. Log. Algebraic Program., 81, 898-928 (2012) · Zbl 1291.68217
[18] Futatsugi, K.; Diaconescu, R., CafeOBJ Report (1998), World Scientific · Zbl 0962.68115
[19] 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
[20] Goguen, J. A.; Meseguer, J., Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations, Theor. Comput. Sci., 105, 2, 217-273 (1992) · Zbl 0778.68056
[21] Hendrix, J.; Meseguer, J.; Ohsaki, H., A sufficient completeness checker for linear order-sorted specifications modulo axioms, (Automated Reasoning (2006), Springer), 151-155
[22] Hrbacek, K.; Jech, T. J., Introduction to Set Theory, Monographs and Textbooks in Pure and Applied Mathematics, vol. 45 (1999), M. Dekker · Zbl 1045.03521
[23] Lucas, S.; Marché, C.; Meseguer, J., Operational termination of conditional term rewriting systems, Inf. Process. Lett., 95, 4, 446-453 (2005) · Zbl 1185.68374
[24] 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
[25] 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
[26] Meseguer, J., Membership algebra as a logical framework for equational specification, (Recent Trends in Algebraic Development Techniques, vol. 1376 (1998), Springer), 18-61 · Zbl 0903.08009
[27] Meseguer, J., Strict coherence of conditional rewriting modulo axioms, Theor. Comput. Sci., 672, 1-35 (2017) · Zbl 1386.68080
[28] Meseguer, J., Variant-based satisfiability in initial algebras, Sci. Comput. Program., 154, 3-41 (2018) · Zbl 1396.68074
[29] Nagele, J.; Felgenhauer, B.; Middeldorp, A., CSI: new evidence – a progress report, (de Moura, L., Automated Deduction, 26th International Conference on Automated Deduction, CADE. Automated Deduction, 26th International Conference on Automated Deduction, CADE, Lecture Notes in Computer Science, vol. 10395 (2017), Springer), 385-397 · Zbl 1494.68291
[30] Nakamura, M.; Ogata, K.; Futatsugi, K., Incremental proofs of termination, confluence and sufficient completeness of OBJ specifications, (Specification, Algebra, and Software. Specification, Algebra, and Software, Lecture Notes in Computer Science, vol. 8373 (2014), Springer), 92-109 · Zbl 1407.68312
[31] Rocha, C.; Meseguer, J., Constructors, sufficient completeness, and deadlock freedom of rewrite theories, (Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference. Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17. Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference. Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Lecture Notes in Computer Science, vol. 6397 (2010), Springer), 594-609 · Zbl 1306.68087
[32] Skeirik, S.; Meseguer, J., Metalevel algorithms for variant satisfiability, J. Log. Algebraic Methods Program., 96, 81-110 (2018) · Zbl 1430.68423
[33] (Term Rewriting Systems. Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science, vol. 55 (2003), Cambridge University Press) · Zbl 1030.68053
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.