Strong and weak operational termination of order-sorted rewrite theories

This paper presents several new results on conditional term rewriting within the general framework of order-sorted rewrite theories (OSRTs) which contains the more restricted framework of conditional term rewriting systems (CTRSs) as a special case. The results uncover some subtle issues about conditional termination. We first of all generalize a previous known result characterizing the operational termination of a CTRS by the quasi-decreasing ordering notion to a similar result for OSRTs. Second, we point out that the notions of irreducible term and of normal form, which coincide for unsorted rewriting are totally different for conditional rewriting and formally characterize that difference. We then define the notion of a weakly operationally terminating (or weakly normalizing) OSRT, give several evaluation mechanisms to compute normal forms in such theories, and investigate general conditions under which the rewriting-based operational semantics and the initial algebra semantics of a confluent OSRT coincide thanks to a notion of canonical term algebra. Finally, we investigate appropriate conditions and proof methods to ensure good executability properties of an OSRT for computing normal forms.