Proving operational termination of membership equational programs

Francisco Durán, Salvador Lucas, Claude Marché, José Meseguer, Xavier Urbain

Research output: Contribution to journalArticlepeer-review

Abstract

Reasoning about the termination of equational programs in sophisticated equational languages such as Elan, Maude, OBJ, CafeOBJ, Haskell, and so on, requires support for advanced features such as evaluation strategies, rewriting modulo, use of extra variables in conditions, partiality, and expressive type systems (possibly including polymorphism and higher-order). However, many of those features are, at best, only partially supported by current term rewriting termination tools (for instance mu-term, C i ME, AProVE, TTT, Termptation, etc.) while they may be essential to ensure termination. We present a sequence of theory transformations that can be used to bridge the gap between expressive membership equational programs and such termination tools, and prove the correctness of such transformations. We also discuss a prototype tool performing the transformations on Maude equational programs and sending the resulting transformed theories to some of the aforementioned standard termination tools.

Original languageEnglish (US)
Pages (from-to)59-88
Number of pages30
JournalHigher-Order and Symbolic Computation
Volume21
Issue number1-2
DOIs
StatePublished - Jun 2008

Keywords

  • Conditional term rewriting
  • Declarative rule-based languages
  • Membership equational logic
  • Operational termination
  • Program transformation

ASJC Scopus subject areas

  • Software
  • Computer Science Applications

Fingerprint Dive into the research topics of 'Proving operational termination of membership equational programs'. Together they form a unique fingerprint.

Cite this