Advertisement

Using Well-Founded Relations for Proving Operational Termination

  • Salvador LucasEmail author
Article

Abstract

In this paper, we study operational termination, a proof theoretical notion for capturing the termination behavior of computational systems. We prove that operational termination can be characterized at different levels by means of well-founded relations on specific formulas which can be obtained from the considered system. We show how to obtain such well-founded relations from logical models which can be automatically generated using existing tools.

Keywords

Declarative languages Logical models Operational termination Program analysis Well-foundedness 

Notes

Acknowledgements

I thank the anonymous referees for their comments and suggestions, leading to many improvements in the paper.

Supplementary material

References

  1. 1.
    Alarcón, B., Gutiérrez, R., Lucas, S., Navarro-Marset, R.: Proving termination properties with MU-TERM. In: Proceedings of AMAST’10, LNCS, vol. 6486, pp. 201–208, Springer (2011)Google Scholar
  2. 2.
    Aguirre, L., Martí-Oliet, N., Palomino, M., Pita, I.: Sentence-normalized conditional narrowing modulo in rewriting logic and Maude. J. Automat. Reason. 60(4), 421–463 (2018)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Arts, T., Giesl, J.: Proving innermost normalisation automatically. In: Proceedings of RTA’97, LNCS, vol. 1232, pp. 157–171, Springer, Berlin (1997)Google Scholar
  4. 4.
    Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236(1–2), 133–178 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)CrossRefzbMATHGoogle Scholar
  6. 6.
    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 (2007)Google Scholar
  7. 7.
    Durán, F., Lucas, S., Meseguer, J.: Methods for proving termination of rewriting-based programming languages by transformation. Electron. Notes Theor. Comput. Sci. 248, 93–113 (2009)CrossRefzbMATHGoogle Scholar
  8. 8.
    Durán, F., Lucas, S., Marché, C., Meseguer, J., Urbain, X.: Proving operational termination of membership equational programs. High. Order Symb. Comput. 21(1–2), 59–88 (2008)CrossRefzbMATHGoogle Scholar
  9. 9.
    Falke, S., Kapur, D.: Operational termination of conditional rewriting with built-in numbers and semantic data structures. Electron. Notes Theor. Comput. Sci. 237, 75–90 (2009)CrossRefzbMATHGoogle Scholar
  10. 10.
    Floyd, R.W.: Assigning meanings to programs. Math. Asp. Comput. Sci. 19, 19–32 (1967)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Giesl, J., Arts, T.: Verification of Erlang processes by dependency pairs. Appl. Algebra Eng. Commun. Comput. 12, 39–72 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. J. Autom. Reason. 37(3), 155–203 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Giesl, J., Thiemann, R., Schneider-Kamp, P.: The dependency pair framework: combining techniques for automated termination proofs. In: Proceedings of LPAR’04, LNAI, vol. 3452, pp. 301–331 (2004)Google Scholar
  14. 14.
    Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: automatic termination proofs in the dependency pair framework. In: Proceedings of IJCAR’06, LNAI, vol. 4130, pp. 281–286 (2006)Google Scholar
  15. 15.
    Goguen, J., Meseguer, J.: Models and equality for logical programming. In: Proceedings of TAPSOFT’87, LNCS, vol. 250, pp. 1–22 (1987)Google Scholar
  16. 16.
    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)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    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’16, pp. 215–230 (2016)Google Scholar
  18. 18.
    Hodges, W.: Model Theory. Cambridge University Press, Cambridge (1993)CrossRefzbMATHGoogle Scholar
  19. 19.
    Korp, M., Sternagel, C., Zankl, H., Middeldorp, A.: Tyrolean termination tool 2. In: Proceedings of RTA 2009, LNCS, vol. 5595, pp. 295–304 (2009)Google Scholar
  20. 20.
    Lalement, R.: Computation as Logic. Masson-Prentice Hall International, Paris (1993)zbMATHGoogle Scholar
  21. 21.
    Lucas, S.: Context-sensitive rewriting strategies. Inf. Comput. 178(1), 294–343 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    Lucas, S.: Use of logical models for proving operational termination in general logics. In: Selected Papers from WRLA’16, LNCS, vol. 9942, pp. 1–21 (2016)Google Scholar
  23. 23.
    Lucas, S.: Directions of operational termination. In: Proceedings of PROLE’18. http://hdl.handle.net/11705/PROLE/2018/009 (2018). Accessed 9 Feb 2019
  24. 24.
    Lucas, S., Gutiérrez, R.: Automatic synthesis of logical models for order-sorted first-order theories. J. Autom. Reason. 60(4), 465–501 (2018)MathSciNetCrossRefzbMATHGoogle Scholar
  25. 25.
    Lucas, S., Gutiérrez, R.: Use of logical models for proving infeasibility in term rewriting. Inf. Process. Lett. 136, 90–95 (2018)MathSciNetCrossRefzbMATHGoogle Scholar
  26. 26.
    Lucas, S., Marché, C., Meseguer, J.: Operational termination of conditional term rewriting systems. Inf. Process. Lett. 95, 446–453 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  27. 27.
    Lucas, S., Meseguer, J.: Dependency pairs for proving termination properties of conditional term rewriting systems. J. Log. Algebr. Methods Program. 86, 236–268 (2017)MathSciNetCrossRefzbMATHGoogle Scholar
  28. 28.
    Lucas, S., Meseguer, J.: Proving operational termination of declarative programs in general logics. In: Proceedings of PPDP’14, pp. 111–122. ACM Digital Library (2014)Google Scholar
  29. 29.
    McCune, W.: Prover9 & Mace4. http://www.cs.unm.edu/~mccune/prover9/ (2005–2010). Accessed 9 Feb 2019
  30. 30.
    Mendelson, E.: Introduction to Mathematical Logic, 4th edn. Chapman & Hall, London (1997)zbMATHGoogle Scholar
  31. 31.
    Meseguer, J.: General logics. In: Logic Colloquium’87, pp. 275–329 (1989)Google Scholar
  32. 32.
    O’Donnell, M.J.: Equational Logic as a Programming Language. The MIT Press, Cambridge (1985)zbMATHGoogle Scholar
  33. 33.
    Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, Berlin (2002)CrossRefzbMATHGoogle Scholar
  34. 34.
    Prawitz, D.: Natural Deduction. A Proof Theoretical Study. Almqvist & Wiksell, 1965. Reprinted by Dover Publications (2006)Google Scholar
  35. 35.
    Rosu, G., Stefanescu, A., Ciobaca, S., Moore, B.M.: One-path reachability logic. In: Proceedings of LICS 2013, pp. 358–367. IEEE Press (2013)Google Scholar
  36. 36.
    Shapiro, S.: Foundations Without Foundationalism: A Case for Second-Order Logic. Clarendon Press, Oxford (1991)zbMATHGoogle Scholar
  37. 37.
    Schernhammer, F., Gramlich, B.: Characterizing and proving operational termination of deterministic conditional term rewriting systems. J. Log. Algebr. Program. 79, 659–688 (2010)MathSciNetCrossRefzbMATHGoogle Scholar
  38. 38.
    Serbanuta, T., Rosu, G.: Computationally equivalent elimination of conditions. In: Proceedings of RTA’06, LNCS, vol. 4098, pp. 19–34. Springer, Berlin (2006)Google Scholar
  39. 39.
    Turing, A.M.: Checking a large routine. In: Report of a Conference on High Speed Automatic Calculating Machines, Univ. Math. Lab., Cambridge, pp. 67–69 (1949)Google Scholar

Copyright information

© Springer Nature B.V. 2019

Authors and Affiliations

  1. 1.DSIC, Universitat Politècnica de ValènciaValenciaSpain

Personalised recommendations