Operational Termination of
Membership Equational Programs: the Order-Sorted Way
Authors
Salvador Lucas and José Meseguer
Abstract
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 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.
Keywords
Term rewriting, program analysis, operational termination, membership equational
logic, order-sorted equational logic, rewriting logic.