TY - JOUR

T1 - Localized operational termination in general logics

AU - Lucas, Salvador

AU - Meseguer, José

N1 - Funding Information:
Partially supported by NSF grant CNS 13-19109. Salvador Lucas’ research, developed during a sabbatical year at the UIUC, was also supported by the EU (FEDER), MECD grant PRX12/00214, MINECO projects TIN2010-21062-C02-02 and TIN 2013-45732-C4-1-P, and GV projects BEST/2014/026 and PROMETEO/2011/052.
Publisher Copyright:
© Springer International Publishing Switzerland 2015.

PY - 2015

Y1 - 2015

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

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

KW - General logics

KW - Operational termination

KW - Program termination

UR - http://www.scopus.com/inward/record.url?scp=84924401845&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84924401845&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-15545-6_9

DO - 10.1007/978-3-319-15545-6_9

M3 - Article

AN - SCOPUS:84924401845

SN - 0302-9743

VL - 8950

SP - 91

EP - 114

JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

ER -