Term Rewriting with Variable Binding: An Initial Algebra Approach

摘要

We present an extension of first-order term rewriting systems, which involves variable binding in the term language. We develop the systems called binding term rewriting systems (BTRSs) in a step-wise manner; firstly we present the term language, then formulate equational logic, and finally define rewrite systems by two styles: rewrite logic and pattern matching styles. The novelty of this development is that we follow an initial algebra approach in an extended notion of ∑-algebras in various functor categories. These are based on Fiore-Plotkin-Turi's presheaf semantics of variable binding and Lueth-Ghani's monadic semantics of term rewriting systems. We characterise the terms, equational logic and rewrite systems for BTRSs are initial algebras in suitable categories. Finally, we discuss our design choice of BTRSs from a semantic perspective.