Operational Termination of Conditional Term Rewriting Systems
Authors
Salvador Lucas, Claude Marché, José Meseguer
Abstract
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.
Keywords
Conditional term rewriting, program analysis, termination.