Operational termination of conditional term rewriting systems

Salvador Lucas, Claude Marché, José Meseguer

Research output: Contribution to journalArticlepeer-review


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.

Original languageEnglish (US)
Pages (from-to)446-453
Number of pages8
JournalInformation Processing Letters
Issue number4
StatePublished - Aug 31 2005


  • Conditional term rewriting
  • Program analysis
  • Programming languages
  • Termination

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Signal Processing
  • Information Systems
  • Computer Science Applications


Dive into the research topics of 'Operational termination of conditional term rewriting systems'. Together they form a unique fingerprint.

Cite this