Order-sorted Term Rewriting

Citations Over TimeTop 10% of 1991 papers

Abstract

In this article we look at the motivation for order-sorted term rewriting by considering some of the very natural equational theories in which single-sorted (unsorted) and many-sorted rewriting lack sufficient expressiveness, for various reasons. However, order-sorted rewriting is not without problems of its own, and we consider some of these along with a brief description in each case of some current approaches to their solution.

Related Papers

• Higher-order rewriting with dependent types (lambda calculus)(1999)
• A Hierarchy of Semantics for Non-deterministic Term Rewriting(2008)
• → Equational Calculus and Term Rewriting(1985)