Term Rewriting with Conditionals and Priority Orderings

Conditional rewriting and priority rewriting are two recent generalizations of term rewriting systems. In the former, each rewrite rule is accompanied by an antecedent which must be shown to hold before rewriting can occur. In the latter, rewrite rules can be used only in a particular order. We compare these formalisms: neither formalism encompasses the other in a practical sense, but we give restrictions under which priority and conditional rewriting can be equivalent. We combine the two operational mechanisms, obtaining a natural and expressive formalism called Priority Conditional Rewriting Systems (PCRS). PCRS can be used to “fully-define” data type specifications and function specifications. Towards this goal, restrictions are given that encourage modularity of specifications and ensure properties of termination, confluence, and total reducibility of ground terms. A logical semantics for priority conditional rewriting is described, using equational formulas ε(R) obtained from the rules in the PCRS R; we give conditions under which rewriting with PCRS is sound and complete