TY - JOUR
T1 - Operational termination of conditional term rewriting systems
AU - Lucas, Salvador
AU - Marché, Claude
AU - Meseguer, José
N1 - Funding Information:
✩ This research was partly supported by bilateral CNRS-DSTIC/ UIUC research project “Rewriting calculi, logic and behavior”, and by ONR Grant N00014-02-1-0715 and NSF Grant CCR-0234524; Salvador Lucas was partially supported by the EU (FEDER) and the Spanish MEC, under grant TIN 2004-07943-C04-02. * Corresponding author. E-mail addresses: [email protected] (S. Lucas), [email protected] (C. Marché), [email protected] (J. Meseguer).
PY - 2005/8/31
Y1 - 2005/8/31
N2 - We describe conditional rewriting by means of an inference system and capture termination as the absence of infinite inference: that is, all proof attempts must either successfully terminate, or they must fail in finite time. We call this notion operational termination. Our notion of operational termination is parametric on the inference system. We prove that operational termination of CTRSs is, in fact, equivalent to a very general notion proposed for 3-CTRSs, namely the notion of quasi-decreasingness, which is currently the most general one which is intended to be checked by comparing parts of the CTRS by means of term orderings. Therefore, existing methods for proving quasi-decreasingness of CTRSs immediately apply to prove operational termination of CTRSs.
AB - We describe conditional rewriting by means of an inference system and capture termination as the absence of infinite inference: that is, all proof attempts must either successfully terminate, or they must fail in finite time. We call this notion operational termination. Our notion of operational termination is parametric on the inference system. We prove that operational termination of CTRSs is, in fact, equivalent to a very general notion proposed for 3-CTRSs, namely the notion of quasi-decreasingness, which is currently the most general one which is intended to be checked by comparing parts of the CTRS by means of term orderings. Therefore, existing methods for proving quasi-decreasingness of CTRSs immediately apply to prove operational termination of CTRSs.
KW - Conditional term rewriting
KW - Program analysis
KW - Programming languages
KW - Termination
UR - http://www.scopus.com/inward/record.url?scp=21344452839&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=21344452839&partnerID=8YFLogxK
U2 - 10.1016/j.ipl.2005.05.002
DO - 10.1016/j.ipl.2005.05.002
M3 - Article
AN - SCOPUS:21344452839
SN - 0020-0190
VL - 95
SP - 446
EP - 453
JO - Information Processing Letters
JF - Information Processing Letters
IS - 4
ER -