A SEMANTIC APPROACH TO ORDER-SORTED REWRITING

Order-sorted rewriting builds a nice framework to handle partially def ined functions and subtypes. To be able to prove a critical-pair lemma and Birkhoff's completeness theorem, order-sorted rewriting was restr icted to sort decreasing term rewriting systems. However, natural exam ples show that this approach is too restrictive. To solve this problem , we generalize well-sorted terms to semantically well-sorted terms an d well-sorted substitutions to a restricted form of semantically well- sorted substitutions. Semantically well-sorted terms with respect to a set of equations E are terms that denote well-defined elements in eve ry algebra satisfying E. We prove a critical-pair lemma and Birkhoff's completeness theorem for so-called range-unique signatures and arbitr ary order-sorted rewriting systems. A transformation is given which al lows us to obtain an equivalent range-unique signature from each non-r ange-unique one. We also show decidability and undecidability results. (C) 1998 Academic Press Limited.