Priority Rewriting: Semantics, Confluence, and Conditionals

Priority rewrite systems (PRS) [BBK] are partially ordered finite sets of rewrite rules; in this paper, two possible alternative definitions for rewriting with PRS are examined. A logical semantics for priority rewriting is described, using equational formulas obtained from the rules, and inequations which must be assumed to permit rewriting with rules with lower priority. Towards the goal of using PRS to define data type and functions specifications, restrictions are given that ensure confluence and encourage modularity. Finally, the relation between priority and conditional rewriting is studied, and a natural combination of these concepts is proposed