[Back]

F. Schernhammer, B. Gramlich:
"On Proving and Characterizing Operational Termination of Deterministic Conditional Rewrite Systems";
Talk: 9th International Workshop on Termination (WST 2007), Paris, France; 2007-06-29; in: "Proc. 9th International Workshop on Termination", D. Hofbauer, A. Serebrenik (ed.); (2007), 82 - 85.

Conditional term rewriting systems (CTRSs) are a natural extension of unconditional such systems (TRSs) allowing rules to be guarded by conditions. Conditional rules tend to be very intuitive and easy to formulate and are therefore used in several programming and specification languages, such as Maude or ELAN. Besides, the particular class of deterministic (oriented) CTRSs (DCTRSs) has been used for instance in proofs of termination of (well-moded) logic programs, [Ganzinger/Waldmann'92]. Recently, the notion of operational termination of DCTRSs was defined in [Lucas/Marché/Meseguer'05], which guarantees finite reductions in existing rewrite engines. In [Ohlebusch'02], based on the idea of unravelings of [Marchiori'96], a transformation from DCTRSs into TRSs was proposed, such that termination of the transformed TRS implies quasi-reductivity of the DCTRS. In this extended abstract we provide an alternative definition of quasi-reductivity, which allows us to prove the property for strictly more DCTRSs than Ohlebusch's transformation was able to handle, while preserving the important implications of quasi-reductivity. The key concept used is context-sensitive rewriting [Lucas'01]. We define a transformation from DCTRSs into context-sensitive (unconditional) TRSs such that termination of the transformed context-sensitive TRS implies context-sensitive quasi-reductivity of the DCTRS. Furthermore we relate the latter notion to other known ones and give equivalent characterizations of operational termination.

Conditional term rewriting systems (CTRSs), deterministic CTRSs, operational termination, quasi-reductivity, context-sensitivity, elimination of conditions.

http://publik.tuwien.ac.at/files/pub-inf_4990.pdf