A Semantic Approach to Order-sorted Rewriting

Order-sorted rewriting builds a nice framework to handle partially defined functions and subtypes. To be able to prove a critical-pair lemma and Birkhoffʹs completeness theorem, order-sorted rewriting was restricted to sort decreasing term rewriting systems. However, natural examples show that this approach is too restrictive. To solve this problem, we generalize well-sorted terms to semantically well-sorted terms and well-sorted substitutions to a restricted form of semantically well-sorted substitutions. Semantically well-sorted terms with respect to a set of equationsEare terms that denote well-defined elements in every algebra satisfyingE. We prove a critical-pair lemma and Birkhoffʹs completeness theorem for so-called range-unique signatures and arbitrary order-sorted rewriting systems. A transformation is given which allows us to obtain an equivalent range-unique signature from each non-range-unique one. We also show decidability and undecidability results.