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

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.