Operational Termination of Membership Equational Programs: the Order-Sorted Way

Salvador Lucas, José Meseguer

Research output: Contribution to journalArticlepeer-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) context-sensitive 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 unconditional, 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)207-225
Number of pages19
JournalElectronic Notes in Theoretical Computer Science
Issue number3
StatePublished - Jun 29 2009


  • Term rewriting
  • membership equational logic
  • operational termination
  • order-sorted equational logic
  • program analysis
  • rewriting logic

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Operational Termination of Membership Equational Programs: the Order-Sorted Way'. Together they form a unique fingerprint.

Cite this