Proving Termination of Context-Sensitive Rewriting With MU-TERM

Authors

Beatriz Alarcón, Raúl Gutiérrez, José Iborra, and Salvador Lucas

Abstract

Context-sensitive rewriting (CSR) is a restriction of rewriting which forbids reductions on selected arguments of functions. Proving termination of CSR is an interesting problem with several applications in the fields of term rewriting and programming languages. Several methods have been developed for proving termination of CSR. The new version of MU-TERM which we present here implements all currently known techniques. In this paper we describe the recently introduced techniques and provide a first experimental evaluation of their performance.