Skip to main content
SpringerLink
Log in

Generalized Rewrite Theories and Coherence Completion

  • Conference paper
  • First Online:
Rewriting Logic and Its Applications (WRLA 2018)

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

Included in the following conference series:

Abstract

A new notion of generalized rewrite theory suitable for symbolic reasoning and generalizing the standard notion in [3] is motivated and defined. Also, new requirements for symbolic executability of generalized rewrite theories that extend those in [8] for standard rewrite theories, including a generalized notion of coherence, are given. Finally, symbolic executability, including coherence, is both ensured and made available for a wide class of such theories by automatable theory transformations.

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

Access this chapter

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 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

Institutional subscriptions

Notes

  1. 1.

    If \(B = B_{0} \uplus U\), with \(B_{0}\) associativity and/or commutativity axioms, and U identity axioms, the B-preregularity notion can be broadened by requiring only that: (i) \(\varSigma \) is \(B_{0}\)-preregular in the standard sense, so that \( ls (u\rho )= ls (v\rho )\) for all \(u=v \in B_{0}\) and substitutions \(\rho \); and (ii) the axioms U oriented as rules \(\vec {U}\) are sort-decreasing in the sense that \(u=v \in U \Rightarrow ls (u\rho ) \geqslant ls (v\rho )\) for each \(\rho \). Maude automatically checks B-preregularity of an OS signature \(\varSigma \) in this broader sense [4].

  2. 2.

    See [24] for the more general definition of both convergence and the relation \(\rightarrow _{\vec {E},B}\) when \(\varSigma \) is B-preregular in the broader sense of Footnote 1.

  3. 3.

    This is supported in Maude by the frozen operator attribute, which forbids rewrites below the specified argument positions. For example, when giving a rewriting semantics to a CCS-like process calculus, the process concatenation operator \(\_{\cdot }\_\), appearing in process expressions like \(a \cdot P\), will typically be frozen in its second argument.

  4. 4.

    By definition this means that there is no function symbol f and position q such that: (i) \(p=q \cdot i \cdot q'\), (ii) \(u'|_{q}=f(u_{1},\ldots ,u_{n})\), and (iii) \(i \in \phi (f_{[s]}^{[s_{1}]\ldots [s_{n}]})\). Intuitively this means that the frozenness restrictions \(\phi \) do not block rewriting at position p in \(u'\).

  5. 5.

    Admittedly, it is possible to allow more general rules with additional “rewrite conditions” of the form \(l \rightarrow r \; if \; \varphi \wedge \bigwedge _{i=1\ldots n} u_{i} \rightarrow v_{i}\) in a generalized rewrite theory. Then, generalized rewrite theories would specialize to standard rewrite theories whose rules also allow rewrite conditions. I leave this further generalization as future work.

  6. 6.

    Recall that the strongly deterministic and convergent rules \(\vec {E}\) may be conditional. We are therefore using Definition 3 in its straightforward generalization to the conditional case.

References

  1. Arusoaie, A., Lucanu, D., Rusu, V.: Symbolic execution based on language transformation. Comput. Lang. Syst. Struct. 44, 48–71 (2015)

    MATH  Google Scholar 

  2. Bae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: Rewriting Techniques and Applications (RTA 2013). LIPIcs, vol. 21, pp. 81–96. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2013)

    Google Scholar 

  3. Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theor. Comput. Sci. 360(1–3), 386–414 (2006)

    Article  MathSciNet  Google Scholar 

  4. Clavel, M., et al.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71999-1

    Book  MATH  Google Scholar 

  5. Comon-Lundh, H., Delaune, S.: The finite variant property: how to get rid of some algebraic properties. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 294–307. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-32033-3_22

    Chapter  Google Scholar 

  6. Dershowitz, N., Jouannaud, J.P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 243–320. North-Holland, Amsterdam (1990)

    Google Scholar 

  7. Durán, F., Lucas, S., Meseguer, J.: Termination modulo combinations of equational theories. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS (LNAI), vol. 5749, pp. 246–262. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04222-5_15

    Chapter  MATH  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  9. Ehrig, H., Mahr, B.: Fundamentals of Algebraic Specification 1. Springer, Heidelberg (1985). https://doi.org/10.1007/978-3-642-69962-7

    Book  MATH  Google Scholar 

  10. Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: cryptographic protocol analysis modulo equational properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007–2009. LNCS, vol. 5705, pp. 1–50. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03829-7_1

    Chapter  MATH  Google Scholar 

  11. Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. J. Algebr. Logic Program. 81, 898–928 (2012)

    Article  MathSciNet  Google Scholar 

  12. Falke, S., Kapur, D.: Rewriting induction + Linear arithmetic = Decision procedure. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 241–255. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31365-3_20

    Chapter  Google Scholar 

  13. Futatsugi, K.: Fostering proof scores in CafeOBJ. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 1–20. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16901-4_1

    Chapter  Google Scholar 

  14. Goguen, J., Meseguer, J.: Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theor. Comput. Sci. 105, 217–273 (1992)

    Article  MathSciNet  Google Scholar 

  15. Jouannaud, J.P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput. 15, 1155–1194 (1986)

    Article  MathSciNet  Google Scholar 

  16. Kop, C., Nishida, N.: Automatic constrained rewriting induction towards verifying procedural programs. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 334–353. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-12736-1_18

    Chapter  Google Scholar 

  17. Lucanu, D., Rusu, V., Arusoaie, A., Nowak, D.: Verifying reachability-logic properties on rewriting-logic specifications. In: Martí-Oliet, N., Ölveczky, P.C., Talcott, C. (eds.) Logic, Rewriting, and Concurrency - Essays Dedicated to José Meseguer on the Occasion of His 65th Birthday. LNCS, vol. 9200, pp. 451–474. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23165-5_21

    Chapter  MATH  Google Scholar 

  18. Lucas, S., Meseguer, J.: Normal forms and normal theories in conditional rewriting. J. Log. Algebr. Methods Program. 85(1), 67–97 (2016)

    Article  MathSciNet  Google Scholar 

  19. Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Presicce, F.P. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998). https://doi.org/10.1007/3-540-64299-4_26

    Chapter  Google Scholar 

  20. Meseguer, J.: Generalized rewrite theories and coherence completion. Technical report, University of Illinois Computer Science Department, March 2018. http://hdl.handle.net/2142/99546

  21. Meseguer, J.: Variant-based satisfiability in initial algebras. Sci. Comput. Program. 154, 3–41 (2018)

    Article  Google Scholar 

  22. Meseguer, J., Palomino, M., Martí-Oliet, N.: Equational abstractions. Theor. Comput. Sci. 403(2–3), 239–264 (2008)

    Article  MathSciNet  Google Scholar 

  23. Rocha, C., Meseguer, J., Muñoz, C.A.: Rewriting modulo SMT and open system analysis. J. Log. Algebr. Methods Program. 86, 269–297 (2017)

    Article  MathSciNet  Google Scholar 

  24. Skeirik, S., Meseguer, J.: Metalevel algorithms for variant satisfiability. J. Log. Algebr. Methods Program. 96, 81–110 (2018)

    Article  MathSciNet  Google Scholar 

  25. Skeirik, S., Stefanescu, A., Meseguer, J.: A constructor-based reachability logic for rewrite theories. In: Fioravanti, F., Gallagher, J. (eds.) LOPSTR 2017. LNCS, vol. 10855, pp. 207–217. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94460-9_12. Technical report, University of Illinois Computer Science Department, March 2017. http://hdl.handle.net/2142/95770

    Chapter  MATH  Google Scholar 

  26. Ştefănescu, A., Ciobâcă, Ş., Mereuta, R., Moore, B.M., Şerbănută, T.F., Roşu, G.: All-path reachability logic. In: Dowek, G. (ed.) RTA 2014. LNCS, vol. 8560, pp. 425–440. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08918-8_29

    Chapter  Google Scholar 

  27. Thati, P., Meseguer, J.: Symbolic reachability analysis using narrowing and its application to the verification of cryptographic protocols. J. High. Order Symb. Comput. 20(1–2), 123–160 (2007)

    MATH  Google Scholar 

  28. Viry, P.: Equational rules for rewriting logic. Theor. Comput. Sci. 285, 487–517 (2002)

    Article  MathSciNet  Google Scholar 

Download references

Acknowledgments

I thank the referees for their constructive criticism and valuable suggestions to improve the paper. This work has been partially supported by NRL under contract number N00173-17-1-G002.

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Illinois at Urbana-Champaign, Urbana, IL, 61801, USA

    José Meseguer

Authors
  1. José Meseguer
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to José Meseguer .

Editor information

Editors and Affiliations

  1. Inria, Lille, France

    Vlad Rusu

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Meseguer, J. (2018). Generalized Rewrite Theories and Coherence Completion. In: Rusu, V. (eds) Rewriting Logic and Its Applications. WRLA 2018. Lecture Notes in Computer Science(), vol 11152. Springer, Cham. https://doi.org/10.1007/978-3-319-99840-4_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-99840-4_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-99839-8

  • Online ISBN: 978-3-319-99840-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation