Skip to main content
SpringerLink
Log in

Analysis of Rewriting-Based Systems as First-Order Theories

  • Conference paper
  • First Online:
Logic-Based Program Synthesis and Transformation (LOPSTR 2017)

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

Abstract

Computational systems based on a first-order language that can be given a canonical model which captures provability in the corresponding calculus can often be seen as first-order theories \(\mathcal{S}\), and computational properties of such systems can be formulated as first-order sentences \(\varphi \) that hold in such a canonical model of \(\mathcal{S}\). In this setting, standard results regarding the preservation of satisfiability of different classes of first-order sentences yield a number of interesting applications in program analysis. In particular, properties expressed as existentially quantified boolean combinations of atoms (for instance, a set of unification problems) can then be disproved by just finding an arbitrary model of the considered theory plus the negation of such a sentence. We show that rewriting-based systems fit into this approach. Many computational properties (e.g., infeasibility and non-joinability of critical pairs in (conditional) rewriting, non-loopingness, or the secure access to protected pages of a web site) can be investigated in this way. Interestingly, this semantic approach succeeds when specific techniques developed to deal with the aforementioned problems fail.

Partially supported by the EU (FEDER), Spanish MINECO project TIN2015-69175-C4-1-R and GV project PROMETEOII/2015/013.

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.

    For instance, given terms s and t, \(s\rightarrow ^*_\mathcal{R}t\) is undecidable (Post’s correspondence problem is a particular case). Hence, is undecidable.

  2. 2.

    We follow the terminology and notation in [15].

  3. 3.

    Note that the joinability semantics can be rephrased into a reachability semantics: a joinability condition \(s\downarrow t\) is equivalent to a reachability condition \(s\rightarrow ^*x,t\rightarrow ^*x\) if x is a fresh variable not occurring elsewhere in the rule.

  4. 4.

    http://users.dsic.upv.es/workshops/wwv05/.

References

  1. Aoto, T.: Disproving confluence of term rewriting systems by interpretation and ordering. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS (LNAI), vol. 8152, pp. 311–326. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40885-4_22

    Chapter  MATH  Google Scholar 

  2. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)

    Book  Google Scholar 

  3. Bergstra, J.A., Klop, J.W.: Conditional rewrite rules: confluence and termination. J. Comput. Syst. Sci. 32, 323–362 (1986)

    Article  MathSciNet  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  5. Chang, C.L., Lee, R.C.: Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York (1973)

    MATH  Google Scholar 

  6. Clark, K.L.: Predicate logic as a computational formalism. Ph.D. thesis, Research Monograph 79/59 TOC, Department of Computing, Imperial College of Science, and Technology, University of London, December 1979

    Google Scholar 

  7. Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: 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 

  8. Clavel, M., Palomino, M., Riesco, A.: Introducing the ITP tool: a tutorial. J. Univ. Comput. Sci. 12(11), 1618–1650 (2006)

    Google Scholar 

  9. Dauchet, M., Tison, S.: The theory of ground rewrite systems is decidable. In: Proceedings of LICS 1990, pp. 242–248. IEEE Press (1990)

    Google Scholar 

  10. Dershowitz, N.: Termination of rewriting. J. Symb. Comput. 3, 69–115 (1987)

    Article  MathSciNet  Google Scholar 

  11. Dershowitz, N., Okada, M.: A rationale for conditional equational programming. Theor. Comput. Sci. 75, 111–138 (1990)

    Article  MathSciNet  Google Scholar 

  12. Gaillourdet, J.-M., Hillenbrand, T., Löchner, B., Spies, H.: The new WALDMEISTER loop at work. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 317–321. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45085-6_27

    Chapter  Google Scholar 

  13. Gallagher, J.P., Rosendahl, M.: Approximating term rewriting systems: a horn clause specification and its implementation. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 682–696. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-89439-1_47

    Chapter  MATH  Google Scholar 

  14. Giesl, J., Arts, T.: Verification of Erlang processes by dependency pairs. Appl. Algebra Eng. Commun. Comput. 12, 39–72 (2001)

    Article  MathSciNet  Google Scholar 

  15. Goguen, J.A., Meseguer, J.: Models and equality for logical programming. In: Ehrig, H., Kowalski, R., Levi, G., Montanari, U. (eds.) TAPSOFT 1987. LNCS, vol. 250, pp. 1–22. Springer, Heidelberg (1987). https://doi.org/10.1007/BFb0014969

    Chapter  Google Scholar 

  16. Gutiérrez, R., Lucas, S., Reinoso, P.: A tool for the automatic generation of logical models of order-sorted first-order theories. In: Proceedings of PROLE 2016, pp. 215–230 (2016). Tool http://zenon.dsic.upv.es/ages/

  17. Hodges, W.: A Shorter Model Theory. Cambridge University Press, Cambridge (1997)

    MATH  Google Scholar 

  18. Lucas, S., Gutiérrez, R.: A semantic criterion for proving infeasibility in conditional rewriting. In: Proceedings of IWC 2017, pp. 15–20 (2017)

    Google Scholar 

  19. Lucas, S., Gutiérrez, R.: Automatic synthesis of logical models for order-sorted first-order theories. J. Autom. Reason. 60(4), 465–501 (2018)

    Article  MathSciNet  Google Scholar 

  20. Lucas, S., Marché, C., Meseguer, J.: Operational termination of conditional term rewriting systems. Inf. Process. Lett. 95, 446–453 (2005)

    Article  MathSciNet  Google Scholar 

  21. Lucas, S., Meseguer, J.: Dependency pairs for proving termination properties of conditional term rewriting systems. J. Log. Algebraic Methods Program. 86, 236–268 (2017)

    Article  MathSciNet  Google Scholar 

  22. Lucas, S., Meseguer, J.: Models for logics and conditional constraints in automated proofs of termination. In: Aranda-Corral, G.A., Calmet, J., Martín-Mateos, F.J. (eds.) AISC 2014. LNCS (LNAI), vol. 8884, pp. 9–20. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-13770-4_3

    Chapter  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  24. Lucas, S., Meseguer, J., Gutiérrez, R.: Extending the 2D dependency pair framework for conditional term rewriting systems. In: Proietti, M., Seki, H. (eds.) LOPSTR 2014. LNCS, vol. 8981, pp. 113–130. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-17822-6_7

    Chapter  Google Scholar 

  25. Mendelson, E.: Introduction to Mathematical Logic, 4th edn. Chapman & Hall, Boca Raton (1997)

    MATH  Google Scholar 

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

  27. Meseguer, J.: Twenty years of rewriting logic. J. Logic Algebraic Program. 81, 721–781 (2012)

    Article  MathSciNet  Google Scholar 

  28. Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, New York (2002). https://doi.org/10.1007/978-1-4757-3661-8

    Book  MATH  Google Scholar 

  29. Prawitz, D.: Natural Deduction: A Proof-Theoretical Study. Dover, Mineola (2006)

    MATH  Google Scholar 

  30. Rapp, F., Middeldorp, A.: Automating the first-order theory of rewriting for left-linear right-ground rewrite systems. In: Proceedings of FSCD 2016, LIPIcs, vol. 52, pp. 36:1–36:12 (2016). Article No. 36

    Google Scholar 

  31. Smullyan, R.M.: Theory of Formal Systems. Princeton University Press, Princeton (1961)

    MATH  Google Scholar 

  32. Sternagel, T., Middeldorp, A.: Conditional confluence (system description). In: Dowek, G. (ed.) RTA 2014. LNCS, vol. 8560, pp. 456–465. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08918-8_31

    Chapter  Google Scholar 

  33. Sternagel, T., Middeldorp, A.: Infefasible conditional critical pairs. In: Proceedings of IWC 2015, pp. 13–18 (2015)

    Google Scholar 

  34. Sternagel, C., Sternagel, T.: Certifying confluence of almost orthogonal CTRSs via exact tree automata completion. In: Proceedings of FSCD 2016, LIPIcs, vol. 52, pp. 85:1–85:16 (2016). Article No. 85

    Google Scholar 

  35. Treinen, R.: The first-order theory of linear one-step rewriting is undecidable. Theor. Comput. Sci. 208, 179–190 (1998)

    Article  MathSciNet  Google Scholar 

  36. Wang, H.: Logic of many-sorted theories. J. Symb. Logic 17(2), 105–116 (1952)

    Article  MathSciNet  Google Scholar 

Download references

Acknowledgements

I thank María Alpuente and José Meseguer for many fruitful discussions. I also thank the anonymous referees for their comments.

Author information

Authors and Affiliations

  1. DSIC, Universitat Politècnica de València, Valencia, Spain

    Salvador Lucas

Authors
  1. Salvador Lucas
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Salvador Lucas .

Editor information

Editors and Affiliations

  1. University of Chieti-Pescara, Pescara, Italy

    Fabio Fioravanti

  2. Roskilde University, Roskilde, Denmark

    John P. Gallagher

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Lucas, S. (2018). Analysis of Rewriting-Based Systems as First-Order Theories. In: Fioravanti, F., Gallagher, J. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2017. Lecture Notes in Computer Science(), vol 10855. Springer, Cham. https://doi.org/10.1007/978-3-319-94460-9_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-94460-9_11

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-94459-3

  • Online ISBN: 978-3-319-94460-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation