Publication:
Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories

Thumbnail Image
Files

Files

Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories.png (7.08 KB)
View Statistics
Reference Managers
Mendeley
Indexers
Google Scholar CORE
QR Code
QR Code
Authors

Authors

Rocha, Camilo
Meseguer, José
Abstract (Spanish)
Se ha estudiado a fondo la integridad suficiente para las especificaciones de ecuaciones, donde los símbolos de función se clasifican en constructores y símbolos definidos. Pero, ¿qué debería significar suficiente completitud para reescribir la teoría R=(Σ,E,R) con ecuaciones E y reglas no ecuacionales R que describen transiciones concurrentes en un sistema? Este trabajo argumenta que una teoría de reescritura tiene naturalmente dos nociones de constructor: la habitual para sus ecuaciones E, y otra diferente para sus reglas R. La suficiente completitud de constructores para las reglas R resulta estar íntimamente relacionada con la libertad de interbloqueo, es decir, R no tiene interbloqueos fuera de los constructores de R. La relación entre estas dos nociones se estudia en el marco de las teorías de reescritura ordenadas por orden incondicional. Se dan condiciones suficientes que permiten la comprobación automática de la integridad suficiente, la libertad de interbloqueo y otras propiedades relacionadas, mediante axiomas ecuacionales de módulos de autómatas proposicionales como la asociatividad, la conmutatividad y la identidad. Se utilizan para extender el verificador de integridad suficiente de Maude desde la verificación de teorías ecuacionales hasta la de teorías ecuacionales y de reescritura. Finalmente, se caracteriza e ilustra con un ejemplo la utilidad de la noción de constructores propuesta para probar teoremas inductivos sobre la relación de reescritura de alcanzabilidad →R asociada a una teoría de reescritura R (y también sobre la relación de capacidad de unión ↓R).
Abstract (English)
Sufficient completeness has been throughly studied for equational specifications, where function symbols are classified into constructors and defined symbols. But what should sufficient completeness mean for a rewrite theory R=(Σ,E,R) with equations E and non-equational rules R describing concurrent transitions in a system? This work argues that a rewrite theory naturally has two notions of constructor: the usual one for its equations E, and a different one for its rules R. The sufficient completeness of constructors for the rules R turns out to be intimately related with deadlock freedom, i.e., R has no deadlocks outside the constructors for R. The relation between these two notions is studied in the setting of unconditional order-sorted rewrite theories. Sufficient conditions are given allowing the automatic checking of sufficient completeness, deadlock freedom, and other related properties, by propositional tree automata modulo equational axioms such as associativity, commutativity, and identity. They are used to extend the Maude Sufficient Completeness Checker from the checking of equational theories to that of both equational and rewrite theories. Finally, the usefulness of the proposed notion of constructors in proving inductive theorems about the reachability rewrite relation →R associated to a rewrite theory R (and also about the joinability relation ↓R ) is both characterized and illustrated with an example.
Extent
16 páginas.
Rights

© Springer-Verlag Berlin Heidelberg 2010

URI: https://repositorio.escuelaing.edu.co/handle/001/1901
Collections

Collections

AD - CTG – Informática
References

Avenhaus, J., Hillenbrand, T., Löchner, B.: On using ground joinable equations in equational theorem proving. Journal of Symbolic Computation 36(1-2), 217–233 (2003)

Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. In: Kaci, A.H., Nivat, M. (eds.) Resolution of Equations in Algebraic Structures. Rewriting Techniques, vol. 2, pp. 1–30. Academic Press, New York (1989)

Becker, K.: Proving ground confluence and inductive validity in constructor based equational specifications. In: Gaudel, M.-C., Jouannaud, J.-P. (eds.) CAAP 1993, FASE 1993, and TAPSOFT 1993. LNCS, vol. 668, pp. 46–60. Springer, Heidelberg (1993) ISBN 3-540-56610-4

Bouhoula, A.: Using induction and rewriting to verify and complete parameterized specifications. Theoretical Computer Science 170(1-2), 245–276 (1996)

Bouhoula, A.: Simultaneous checking of completeness and ground confluence for algebraic specifications. ACM Transactions on Computational Logic 10(3) (2009)

Bouhoula, A., Jacquemard, F.: Automated induction with constrained tree automata. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 539–554. Springer, Heidelberg (2008)

Bouhoula, A., Jouannaud, J.-P., Meseguer, J.: Specification and proof in membership equational logic. Theoretical Computer Science 236(1-2), 35–132 (2000)

Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theoretical Computer Science 360(1-3), 386–414 (2006)

Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.: Maude: specification and programming in rewriting logic. Theoretical Computer Science 285, 187–243 (2002)

Comon, H.: Sufficient completness, term rewriting systems and “anti-unification”. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol. 230, pp. 3–540. Springer, Heidelberg (1986), ISBN 3-540-16780-3

Comon, H.: An effective method for handling initial algebras. In: Grabowski, J., Wechler, W., Lescanne, P. (eds.) ALP 1988. LNCS, vol. 343, pp. 108–118. Springer, Heidelberg (1989), ISBN 3-540-50667-5

Comon, H., Dauchet, M., Gilleron, R., Löding, C., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (2007)

Comon, H., Jacquemard, F.: Ground reducibility is EXPTIME-complete. Information and Computation 187(1), 123–153 (2003)

Gnaedig, I., Kirchner, H.: Computing constructor forms with non terminating rewrite programs. In: Bossi, A., Maher, M.J. (eds.) PPDP, pp. 121–132. ACM, New York (2006) ISBN 1-59593-388-3

Guttag, J.: The Specification and Application to Programming of Abstract Data Types. PhD thesis, University of Toronto, Computer Science Department (1975)

Guttag, J.V., Horning, J.J.: The algebraic specification of abstract data types. Acta Informatica 10, 27–52 (1978)

Hendrix, J.: Decision Procedures for Equationally Based Reasoning. PhD thesis, University of Illinois at Urbana-Champaign (April 2008)

Hendrix, J., Clavel, M., Meseguer, J.: A sufficient completeness reasoning tool for partial specifications. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 165–174. Springer, Heidelberg (2005), ISBN 3-540-25596-6

Hendrix, J., Meseguer, J.: On the completeness of context-sensitive order-sorted specifications. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 229–245. Springer, Heidelberg (2007), ISBN 978-3-540-73447-5

Hendrix, J., Ohsaki, H., Viswanathan, M.: Propositional tree automata. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 50–65. Springer, Heidelberg (2006), ISBN 3-540-36834-5

Huet, G.P., Hullot, J.-M.: Proofs by induction in equational theories with constructors. In: FOCS, pp. 96–107. IEEE, Los Alamitos (1980)

Jouannaud, J.-P., Kounalis, E.: Automatic proofs by induction in theories without constructors. Information and Computation 82(1), 1–33 (1989)

Kapur, D., Narendran, P., Otto, F.: On ground-confluence of term rewriting systems. Information and Computation 86(1), 14–31 (1990)

Kapur, D., Narendran, P., Rosenkrantz, D.J., Zhang, H.: Sufficient-completeness, ground-reducibility and their complexity. Acta Informatica 28(4), 311–350 (1991)

Kapur, D., Narendran, P., Zhang, H.: On sufficient-completeness and related properties of term rewriting systems. Acta Informatica 24(4), 395–415 (1987)

Kounalis, E.: Testing for the ground (co-)reducibility property in term-rewriting systems. Theoretical Computer Science 106(1), 87–117 (1992)

Lazrek, A., Lescanne, P., Thiel, J.-J.: Tools for proving inductive equalities, relative completeness, and omega-completeness. Information and Computation 84(1), 47–70 (1990)

Martin, U., Nipkow, T.: Ordered rewriting and confluence. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 366–380. Springer, Heidelberg (1990), ISBN 3-540-52885-7

Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992)

Nipkow, T., Weikum, G.: A decidability result about sufficient-completeness of axiomatically specified abstract data types. In: Cremers, A.B., Kriegel, H.-P. (eds.) GI-TCS 1983. LNCS, vol. 145, pp. 257–268. Springer, Heidelberg (1982), ISBN 3-540-11973-6

Plaisted, D.: Semantic confluence tests and completion methods. Information and Control 65, 182–215 (1985)

Rocha, C., Meseguer, J.: Constructors, sufficient completeness and deadlock freedom of generalized rewrite theories. Technical report, University of Illinois at Urbana-Champaign (2010)

Viry, P.: Equational rules for rewriting logic. Theoretical Computer Science 285, 487–517 (2002)