Localized Operational Termination in General Logics

详细信息    查看全文

• 作者：Salvador Lucas (17) (18)
  Jos茅 Meseguer (17)
  
• 关键词：General Logics ; Operational Termination ; Program Termination
• 刊名：Lecture Notes in Computer Science
• 出版年：2015
• 出版时间：2015
• 年：2015
• 卷：8950
• 期：1
• 页码：91-114
• 全文大小：411 KB
• 参考文献：1. Aczel, P.: Schematic Consequence. In: Gabbay, D. (ed.) What is a Logical System, pp. 261鈥?72. Oxford University Press (1994)
  2. Alarc贸n, B., Guti茅rrez, R., Lucas, S., Navarro-Marset, R.: Proving Termination Properties with mu-term . In: Johnson, M., Pavlovic, D. (eds.) AMAST 2010. LNCS, vol.聽6486, pp. 201鈥?08. Springer, Heidelberg (2011) CrossRef
  3. Boronat, A., Knapp, A., Meseguer, J., Wirsing, M.: What Is a Multi-modeling Language? In: Corradini, A., Montanari, U. (eds.) WADT 2008. LNCS, vol.聽5486, pp. 71鈥?7. Springer, Heidelberg (2009) CrossRef
  4. Broy, M., Wirsing, M., Pepper, P.: On the Algebraic Definition of Programming Languages. ACM Transactions on Programming Languages and Systems聽9(1), 54鈥?9 (1987) CrossRef
  5. Codish, M., Taboch, C.: A semantic basis for the termination analysis of logic programs. Journal of Logic Programming聽41, 103鈥?23 (1999) CrossRef
  6. Cook, B., Rybalchenko, A., Podelski, A.: Proving Program Termination. Communications of the ACM聽54(5), 88鈥?8 (2011) CrossRef
  7. Dershowitz, N., Lindenstrauss, N., Sagiv, Y., Serebrenik, A.: A General Framework for Automatic Termination of Logic Programs. Applicable Algebra in Engineering, Communication and Computing聽12, 117鈥?56 (2001) CrossRef
  8. Dur谩n, F., Lucas, S., Meseguer, J.: MTT: The Maude Termination Tool (System Description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.聽5195, pp. 313鈥?19. Springer, Heidelberg (2008) CrossRef
  9. Dur谩n, F., Lucas, S., March茅, C., Meseguer, J., Urbain, X.: Proving Operational Termination of Membership Equational Programs. Higher-Order and Symbolic Computation聽21(1-2), 59鈥?8 (2008) CrossRef
  10. Endrullis, J., de Vrijer, R., Waldmann, J.: Local termination: theory and practice. Logical Methods in Computer Science聽6(3:20), 1鈥?7 (2010)
  11. Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and Improving Dependency Pairs. Journal of Automatic Reasoning聽37(3), 155鈥?03 (2006) CrossRef
  12. Giesl, J., Swiderski, P., Schneider-Kamp, P., Thiemann, R.: Automated Termination Proofs for Haskell by Term Rewriting. ACM Transactions on Programming languages and Systems聽33(2), Article 7 (2011)
  13. Lucas, S., Meseguer, J.: Strong and Weak Operational Termination of Order-Sorted Rewrite Theories. In: Escobar, S. (ed.) WRLA 2014. LNCS, vol.聽8663, pp. 178鈥?94. Springer, Heidelberg (2014) CrossRef
  14. Lucas, S., Meseguer, J.: Proving Operational Termination Of Declarative Programs In General Logics. In: Danvy, O. (ed.) Proc. of the 16th International Symposium on Principles and Practice of Declarative Programming, PPDP 2014. ACM Press (to appear, 2014)
  15. Lucas, S., March茅, C., Meseguer, J.: Operational termination of conditional term rewriting systems. Information Processing Letters聽95, 446鈥?53 (2005) CrossRef
  16. Meseguer, J.: General Logics. In: Ebbinghaus, H.-D., et al. (eds.) Logic Colloquium鈥?7, pp. 275鈥?29. North-Holland (1989)
  17. Meseguer, J.: A Logical Theory of Concurrent Objects and its realization in the Maude Language. In: Agha, G., Wegner, P., Yonezawa, A. (eds.) Research Directions in Concurrent Object-Oriented Programming, pp. 314鈥?90. The MIT Press (1993)
  18. Meseguer, J., Rosu, G.: The Rewriting Logic Semantics Project: A Progress Report. Information and Computation聽231, 38鈥?9 (2013) CrossRef
  19. Nguyen, M.T., Giesl, J., Schneider-Kamp, P., De Schreye, D.: Termination Analysis of Logic Programs Based on Dependency Graphs. In: King, A. (ed.) LOPSTR 2007. LNCS, vol.聽4915, pp. 8鈥?2. Springer, Heidelberg (2008) CrossRef
  20. de Scheye, D., Decorte, S.: Termination of Logic Programs: The Never-Ending Story. Journal of Logic Programming聽19, 199鈥?60 (1994) CrossRef
  21. Schneider-Kamp, P., Giesl, J., Nguyen, M.T.: The Dependency Triple Framework for Termination of Logic Programs. In: De Schreye, D. (ed.) LOPSTR 2009. LNCS, vol.聽6037, pp. 37鈥?1. Springer, Heidelberg (2010) CrossRef
  22. Winskel, G.: The Formal Semantics of Programming Languages. The MIT Press, Cambrige Massachusetts (1993)
  23. Wirsing, M.: Structured Algebraic Specifications: A Kernel Language. Theoretical Computer Science聽42, 123鈥?49 (1986) CrossRef
  24. Wirsing, M.: Algebraic Specification. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pp. 675鈥?88 (1990)
  25. Wirsing, M., Knapp, A.: A formal approach to object-oriented software engineering. Theoretical Computer Science聽285(2), 519鈥?60 (2002) CrossRef
  
• 作者单位：Salvador Lucas (17) (18)
  Jos茅 Meseguer (17)
  
  17. CS Dept., University of Illinois at Urbana-Champaign, IL, USA
  18. DSIC, Universitat Polit猫cnica de Val猫ncia, Spain
  
• 丛书名：Software, Services, and Systems
• ISBN：978-3-319-15545-6
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence and Robotics
  Computer Communication Networks
  Software Engineering
  Data Encryption
  Database Management
  Computation by Abstract Devices
  Algorithm Analysis and Problem Complexity
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1611-3349

文摘

Termination can be thought of as the property of programs ensuring that every input is given an answer in finite time. There are, however, many different (combinations of) programming paradigms and languages for these paradigms. Is a common formal definition of termination of programs in any (or most) of these programming languages possible? The notion of operational termination provides a general definition of termination which relies on the logic-based description of (the operational semantics of) a programming language. The key point is capturing termination as the absence of infinite inference, that is: all proof attempts must either successfully terminate, or they must fail in finite time. This global notion is well-suited for most declarative languages, where programs are theories in a logic whose inference system is specialized to each theory to characterize its computations. Other programming languages (e.g., imperative languages) and applications (e.g., the evaluation of specific expressions and goals in functional and logic programs) require a more specialized treatment which pays attention not just to theories, but to specific formulas to be proved within the given theory. For instance, the execution of an imperative program can be viewed as a proof of an specific formula (representing the program) within the computational logic describing the operational semantics of the programming language. In such cases, an appropriate definition of termination should focus on proving the absence of infinite proofs for computations localized to specific goals. In this paper we generalize the global notion of operational termination to this new setting and adapt the recently introduced OT-framework for mechanizing proofs of operational termination to support proofs of localized operational termination.