項書き換え
項書き換え(こうかきかえ、英: term rewriting)とは、数学・計算機科学・論理学において、式(数式、論理式)の項を別の項に置換する手法を総称する用語である。項書き換え系(英: term rewriting system、TRS)とは、項の集合とその置換規則から構成される。
項書き換えは非決定的になることがありうる。ある規則で書き換え可能な項が他の規則でも書き換え可能な場合がありえて、その場合は複数の規則が適用可能と言うことになる。項書き換え系では、項書き換えのためのアルゴリズムは提供されず、書き換え規則の集合のみが提供される。しかし、適当なアルゴリズムと組み合わせれば、項書き換え系はプログラムのような働きをし、実際いくつかの宣言型プログラミング言語は項書き換えに基づいている。
例
算術
一般的な算術の規則は、以下のような規則を含む項書き換え系とみなすことができる:
- Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite Systems (1990). Chapter 6 of Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pp.243–320.
- Term Rewriting Systems, Terese, Cambridge Tracts in Theoretical Computer Science, 2003
- Term Rewriting and All That, Franz Baader and Tobias Nipkow, Cambridge University Press, 1998
- 項書き換えのページへのリンク