Skip to main content
SpringerLink
Log in
Book cover

International Conference on Logic for Programming Artificial Intelligence and Reasoning

LPAR 2010: Logic for Programming, Artificial Intelligence, and Reasoning pp 594–609Cite as

Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6397))

Abstract

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 \(\mathcal{R} = (\Sigma,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., \(\mathcal{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 \(\rightarrow_\mathcal{R}\) associated to a rewrite theory \(\mathcal{R}\) (and also about the joinability relation \(\downarrow_\mathcal{R}\)) is both characterized and illustrated with an example.

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

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

    Chapter  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

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

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

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

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

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

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Chapter  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Chapter  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Illinois at Urbana-Champaign, USA

    Camilo Rocha & José Meseguer

Authors
  1. Camilo Rocha
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. José Meseguer
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institut für Computersprachen 185.2, Theory and Logic Group, TU Wien, Favoritenstraße 9-11, A-1040, Vienna, Austria

    Christian G. Fermüller

  2. School of Computer Science, University of Manchester, Oxford Road, Kilburn Building, M13 9PL, Manchester, United Kingdom

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Rocha, C., Meseguer, J. (2010). Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories. In: Fermüller, C.G., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2010. Lecture Notes in Computer Science, vol 6397. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16242-8_42

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-16242-8_42

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-16241-1

  • Online ISBN: 978-3-642-16242-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation