Operational Semantics of Term Rewriting with Priorities

We study the semantics of term rewriting systems with rule priorities (PRS), as introduced in [1]. Three open problems posed in that paper are solved, by giving counter examples. Moreover, a class of executable PRSs is identified. A translation of PRSs into transition system specifications (TSS) is given. This translation introduces negative premises. We prove that the translation preserves the operational semantics. Contents 1 Introduction 2 2 Term rewriting with rule priorities 3 2.1 Definition and semantics . . . . . . . . . . . . . . . . . . . . . . 3 2.2 Fixed points . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.3 An executable class of PRSs . . . . . . . . . . . . . . . . . . . . 8 2.4 Counter examples to open questions . . . . . . . . . . . . . . . . 11 3 Transition system specifications 14 3.1 Universal negative premises in TSSs . . . . . . . . . . . . . . . . 15 3.2 Translation of PRSs into TSSs . . . . . . . . . . . . . . . . . . . 18 4 Operational semant..