Operational termination of membership equational programs: The order-sorted way

Salvador Lucas, José Meseguer

Research output: Contribution to journalConference articlepeer-review


Our main goal is automating termination proofs for programs in rewriting-based languages with features such as: (i) expressive type structures, (ii) conditional rules, (iii) matching modulo axioms, and (iv) contextsensitive rewriting. Specifically, we present a new operational termination method for membership equational programs with features (i)-(iv) that can be applied to programs in membership equational logic (MEL). The method first transforms a MEL program into a simpler, yet semantically equivalent, conditional order-sorted (OS) program. Subsequent trasformations make the OS-program unconditonal, and, finally, unsorted. In particular, we extend and generalize to this richer setting an order-sorted termination technique for unconditional OS programs proposed by Ölveczky and Lysne. An important advantage of our method is that it minimizes the use of conditional rules and produces simpler transformed programs whose termination is often easier to prove automatically.

Original languageEnglish (US)
Pages (from-to)189-205
Number of pages17
JournalElectronic Notes in Theoretical Computer Science
StatePublished - 2008
Event7th International Workshop on Rewriting Logic and its Applications, WRLA 2008 (European Joint Conference on Theory and Practice of Software, ETAPS 2008) - Budapest, Hungary
Duration: Mar 29 2008Mar 30 2008


  • Membership equational logic
  • Operational termination
  • Order-sorted equational logic
  • Program analysis
  • Rewriting logic
  • Term rewriting

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Operational termination of membership equational programs: The order-sorted way'. Together they form a unique fingerprint.

Cite this