An initial algebra approach to term rewriting systems with variable binders |
| |
Authors: | Makoto Hamana |
| |
Affiliation: | (1) Department of Computer Science, Gunma University, Japan |
| |
Abstract: | We present an extension of first-order term rewriting systems. It involves variable binding in the term language. We develop
systems called binding term rewriting systems (BTRSs) in a stepwise manner. First we present the term language, then formulate
equational logic. Finally, we define rewriting systems. This development is novel because we follow the 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 Lüth-Ghani’s monadic semantics of term rewriting systems. We characterise the terms, equational logic
and rewrite systems for BTRSs as initial algebras in suitable categories. Then, we show an important rewriting property of
BTRSs: orthogonal BTRSs are confluent. Moreover, by using the initial algebra semantics, we give a complete characterisation
of termination of BTRSs. Finally, we discuss our design choice of BTRSs from a semantic perspective.
An erlier version appeared in Proc. Fifth ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP2003). |
| |
Keywords: | Term rewriting systems Abstract syntax with variable binding Higher-order abstract syntax Initial algebra semantics |
本文献已被 SpringerLink 等数据库收录! |
|