Advertisement

Analysis of Rewriting-Based Systems as First-Order Theories

Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, 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.

Keywords

Logical models Program analysis Rewriting-based systems 

Notes

Acknowledgements

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

References

  1. 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_22CrossRefMATHGoogle Scholar
  2. 2.
    Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)CrossRefGoogle Scholar
  3. 3.
    Bergstra, J.A., Klop, J.W.: Conditional rewrite rules: confluence and termination. J. Comput. Syst. Sci. 32, 323–362 (1986)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theor. Comput. Sci. 351(1), 386–414 (2006)MathSciNetCrossRefGoogle Scholar
  5. 5.
    Chang, C.L., Lee, R.C.: Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York (1973)MATHGoogle Scholar
  6. 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 1979Google Scholar
  7. 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-1CrossRefMATHGoogle Scholar
  8. 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. 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. 10.
    Dershowitz, N.: Termination of rewriting. J. Symb. Comput. 3, 69–115 (1987)MathSciNetCrossRefGoogle Scholar
  11. 11.
    Dershowitz, N., Okada, M.: A rationale for conditional equational programming. Theor. Comput. Sci. 75, 111–138 (1990)MathSciNetCrossRefGoogle Scholar
  12. 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_27CrossRefGoogle Scholar
  13. 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_47CrossRefMATHGoogle Scholar
  14. 14.
    Giesl, J., Arts, T.: Verification of Erlang processes by dependency pairs. Appl. Algebra Eng. Commun. Comput. 12, 39–72 (2001)MathSciNetCrossRefGoogle Scholar
  15. 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/BFb0014969CrossRefGoogle Scholar
  16. 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. 17.
    Hodges, W.: A Shorter Model Theory. Cambridge University Press, Cambridge (1997)MATHGoogle Scholar
  18. 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. 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)MathSciNetCrossRefGoogle Scholar
  20. 20.
    Lucas, S., Marché, C., Meseguer, J.: Operational termination of conditional term rewriting systems. Inf. Process. Lett. 95, 446–453 (2005)MathSciNetCrossRefGoogle Scholar
  21. 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)MathSciNetCrossRefGoogle Scholar
  22. 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_3CrossRefGoogle Scholar
  23. 23.
    Lucas, S., Meseguer, J.: Normal forms and normal theories in conditional rewriting. J. Log. Algebraic Methods Program. 85(1), 67–97 (2016)MathSciNetCrossRefGoogle Scholar
  24. 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_7CrossRefGoogle Scholar
  25. 25.
    Mendelson, E.: Introduction to Mathematical Logic, 4th edn. Chapman & Hall, Boca Raton (1997)MATHGoogle Scholar
  26. 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_26CrossRefGoogle Scholar
  27. 27.
    Meseguer, J.: Twenty years of rewriting logic. J. Logic Algebraic Program. 81, 721–781 (2012)MathSciNetCrossRefGoogle Scholar
  28. 28.
    Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, New York (2002).  https://doi.org/10.1007/978-1-4757-3661-8CrossRefMATHGoogle Scholar
  29. 29.
    Prawitz, D.: Natural Deduction: A Proof-Theoretical Study. Dover, Mineola (2006)MATHGoogle Scholar
  30. 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. 36Google Scholar
  31. 31.
    Smullyan, R.M.: Theory of Formal Systems. Princeton University Press, Princeton (1961)MATHGoogle Scholar
  32. 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_31CrossRefGoogle Scholar
  33. 33.
    Sternagel, T., Middeldorp, A.: Infefasible conditional critical pairs. In: Proceedings of IWC 2015, pp. 13–18 (2015)Google Scholar
  34. 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. 85Google Scholar
  35. 35.
    Treinen, R.: The first-order theory of linear one-step rewriting is undecidable. Theor. Comput. Sci. 208, 179–190 (1998)MathSciNetCrossRefGoogle Scholar
  36. 36.
    Wang, H.: Logic of many-sorted theories. J. Symb. Logic 17(2), 105–116 (1952)MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.DSICUniversitat Politècnica de ValènciaValenciaSpain

Personalised recommendations