$ \newcommand{\alert}[1]{\textcolor{brown}{#1}} \newcommand{\m}[1]{\mathsf{#1}} \newcommand{\mi}[1]{\mathit{#1}} \newcommand{\RR}{{\mathcal{R}}} \newcommand{\VV}{\mathcal{V}} \newcommand{\AA}{\mathcal{A}} \newcommand{\FF}{\mathcal{F}} \newcommand{\TT}{\mathcal{T}} \newcommand{\CC}{\mathcal{C}} \newcommand{\hole}{\square} \newcommand{\Var}{\mathcal{V}\mathsf{ar}} \newcommand{\Fun}{\mathcal{F}\mathsf{un}} \newcommand{\Dom}{\mathcal{D}\mathsf{om}} \newcommand{\Pos}{\mathcal{P}\mathsf{os}} \newcommand{\lpo}{{\mathsf{lpo}}} \newcommand{\NIL}{[\,]} \newcommand{\CONS}{:} \newcommand{\APPEND}{\mathbin{\texttt{+}\!\texttt{+}}} \newcommand{\LEQ}{\leq} $

項書換え

（筆・郭子玉）

1. 項書換えとは

項書換こうかきかえは宣言型プログラミング言語や定理自動証明の基礎として用いられている計算モデルです。この記事ではその定義を紹介するとともに、項書換えに基づく小さなプログラミング言語を実装します。

項書換え系は等式を一方向に向きづけた書換え規則からなる集合です。計算の方向を明示するため等号 $=$ の代わりに矢印 $\to$ を用います。例えばペアノ数の足し算を項書換え系で表すと次のようになります。 \[ \RR = \left\{ \begin{aligned} \m{add}(\m{0},y) & \to y \\ \m{add}(\m{s}(x),y) & \to \m{s}(\m{add}(x,y)) \end{aligned} \right\} \] $2 + 1$ に対応する $\m{add}(\m{s}(\m{s}(\m{0})),\m{s}(\m{0}))$ の計算は書換えによって行われます： \[ \underline{\m{add}(\m{s}(\m{s}(\m{0})),\m{s}(\m{0}))} \to_\RR \m{s}(\underline{\m{add}(\m{s}(\m{0}), \m{s}(\m{0}))}) \to_\RR \m{s}(\m{s}(\underline{\m{add}(\m{0},\m{s}(\m{0}))})) \to_\RR \m{s}(\m{s}(\m{s}(\m{0}))) \] 最後の項 $\m{s}(\m{s}(\m{s}(\m{0})))$ はこれ以上書換えることができませんので、これが計算結果になります。計算をこのように定義することにより、停止性や時間的計算量（ステップ数）、計算結果の一意性（合流性）など、様々な計算の性質を数学的に議論できるようになります。

2. 項書換えの定義

この節では項書換え系の定義について述べていきます。項書換えの「項」とは書換えの対象となる数式のことで、変数と関数記号から構成されます。

定義

関数記号の集合 $\FF$ をシグネチャと呼ぶ。各関数記号 $f \in \FF$ には引数の数を表す自然数 $n$ が紐付けられており、これをアリティと呼ぶ。アリティを明示したい場合 $f^{(n)}$ で表記する。アリティがゼロの関数記号は定数と呼ばれる。

定義

$\FF$ をシグネチャ、$\VV$ を $\FF \cap \VV = \varnothing$ であるような可算無限集合とする。 $\VV$ の要素を変数と呼ぶ。 $\FF$ と $\VV$ からなる項の集合 $\TT(\FF, \VV)$ を以下のように帰納的に定義する。

$x \in \VV$ のとき、$x \in \TT(\FF, \VV)$
$f \in \FF$ かつ $t_1, \ldots, t_n \in \TT(\FF, \VV)$ のとき、$f(t_1, \ldots, t_n) \in \TT(\FF, \VV)$

定数記号 $f^{(0)}$ からなる項 $f()$ に対しては、括弧を省略し $f$ で表す。

例

$\FF = \{\m{add}^{(2)}, \m{0}^{(0)}\}, \VV = \{x, \ldots\}$ とする。以下にこの $\FF$ と $\VV$ からなる項の例をいくつか挙げる。

$x$ は変数なので項である。
$\m{0}$ は定数なので項である。
$\m{add}$ はアリティ2の関数記号であり $x$ と $\m{0}$ は項であるから、 $\m{add}(x, \m{0})$ もまた項である。

項書換え系を定義します。

定義

$\ell$ が変数ではない項であり、$r$ に含まれる変数が $\ell$ に含まれるとき、項の対 $(\ell, r)$ を書換え規則と呼び、$\ell \to r$ で表す。書換え規則の集合を項書換え系と呼ぶ。

例

集合 $ \RR = \left\{ \begin{aligned} \m{add}(\m{0}, y) & \to y \\ \m{add}(\m{s}(x), y) & \to \m{s}(\m{add}(x,y)) \end{aligned} \right\} $ は項書換え系の一例である。

次に等式変形に相当する書換え関係 $\to_\RR$ を定義しますが、そのためには書換える場所を指定する位置、対応する部分項、部分項の置き換え、そして書換え規則の変数に項を割当てる代入の概念が必要になります。

定義

位置とは正の整数列である。空列をルート位置と呼び $\epsilon$ で表す。位置 $p$ と位置 $q$ の連接を $pq$ で表す。項 $t$ に現れる位置の集合 $\Pos(t)$ を以下のように定義する。 \[ \Pos(t) = \begin{cases} \{\epsilon\} & \text{$t$ が変数のとき}\\ \{\epsilon\} \cup \{ip \mid 1\leqslant i \leqslant n \text{ かつ } p \in \Pos(t_i)\} & \text{$t = f(t_1, \ldots, t_n)$ のとき} \end{cases} \] 項 $t$ における位置 $p$ の部分項 $t|_p$ は次の式で与えられる。 \[ t|_p = \begin{cases} t & \text{$p = \epsilon$ のとき} \\ t_i|_q & \text{$t = f(t_1, \ldots, t_n)$ かつ $p = iq$ のとき} \end{cases} \] 項 $t$ における位置 $p$ の部分項を項 $u$ に置き換えて得られる項を $t[u]_p$ で表す。正確な定義は以下の通り。 \[ t[u]_p = \begin{cases} u & \text{$p = \epsilon$ のとき} \\ f(t_1,\dots,t_i[u]_q,\dots,t_n) & \text{$t = f(t_1, \ldots, t_n)$ かつ $p = iq$ のとき} \end{cases} \]

例

項 $t = \m{s}(\m{add}(\m{0},\m{s}(\m{0})))$ を考える。 $\Pos(t) = \{ \epsilon, 1, 11, 12, 121 \}$ であり、 \begin{align*} t|_\epsilon & = \m{s}(\m{add}(x,y)) & t|_1 & = \m{add}(\m{0},\m{s}(\m{0})) & t|_{11} & = \m{0} & t|_{12} & = \m{s}(\m{0}) & t|_{121} & = \m{0} \end{align*} となる。また $t[\m{s}(\m{0})]_1 = \m{s}(\m{s}(\m{0}))$ となる。

定義

写像 $\sigma : \VV \to \TT(\FF, \VV)$ の定義域 $\Dom(\sigma)$ が有限であるとき、$\sigma$ を代入と呼ぶ。但し、$\Dom(\sigma)$ は $\{x \mid \sigma(x) \neq x\}$ で定義される。項 $t$ への代入 $\sigma$ の適用 $t\sigma$ は次のように再帰的に定義される。 \[ t\sigma = \begin{cases} \sigma(t) & \text{$t$ が変数のとき} \\ f(t_1\sigma, \ldots, t_n\sigma) & \text{$t = f(t_1, \ldots, t_n)$ のとき} \end{cases} \] 簡便のため $\{ x_1 \mapsto t_1, \dots, x_n \mapsto t_n \}$ で次の代入 $\sigma$ を表すものとする： \[ \sigma(x) = \begin{cases} t_i & \text{$x = x_i$ のとき} \\ x & \text{それ以外の場合} \end{cases} \]

例

項 $t = \m{add}(\m{s}(x), y)$ に対して代入 $\sigma = \{x \mapsto \m{0},\; y \mapsto \m{s}(\m{0})\}$ を適用すると \[ t\sigma = \m{add}(\m{s}(\sigma(x)), \sigma(y)) = \m{add}(\m{s}(\m{0}), \m{s}(\m{0})) \] となる。

準備が整いましたので書換え関係を定義します。

定義

$\RR$ を項書換え系、$s$, $t$ を項とする。書換え規則 $\ell \to r \in \RR$ と位置 $p \in \Pos(s)$、代入 $\sigma$ が存在して $s|_p = l\sigma$ かつ $t = s[r\sigma]_p$ を満たすとき $s \to_\RR t$ と記す。この関係 $\to_\RR$ を $\RR$ の書換え関係と言う。項 $s$ に対して $s \to_\RR t$ となる $t$ が存在しないとき、$s$ を正規形と呼ぶ。

例

項書換え系 $\RR$ \begin{align*} \m{add}(\m{0}, y) & \to y \\ \m{add}(\m{s}(x), y) & \to \m{s}(\m{add}(x, y)) \end{align*} は次の書換え列を持つ。 \[ \underline{\m{add}(\m{s}(\m{s}(\m{0})),\m{s}(\m{0}))} \to_\RR \m{s}(\underline{\m{add}(\m{s}(\m{0}), \m{s}(\m{0}))}) \to_\RR \m{s}(\m{s}(\underline{\m{add}(\m{0},\m{s}(\m{0}))})) \to_\RR \m{s}(\m{s}(\m{s}(\m{0}))) \] 例えば二番目の書換え関係 $ s = \m{s}(\m{add}(\m{s}(\m{0}), \m{s}(\m{0}))) \to_\RR \m{s}(\m{add}(\m{0},\m{s}(\m{0}))) = t $ は

書換え位置 $p = 1$,
書換え規則 $(\ell \to r) = (\m{add}(\m{s}(x),y) \to \m{s}(\m{add}(x, y)))$,
代入 $\sigma = \{ x \mapsto \m{0},\; y \mapsto \m{s}(\m{0}) \}$

によって行われる書換えである。実際、 $s|_p = \m{add}(\m{0}, \m{s}(\m{0})) = \ell\sigma$ となり、また $s[r\sigma] = \m{s}(\m{add}(\m{0},\m{s}(\m{0})))$ となるため、$s \to_\RR t$ の成立を確認できる。書換え列の最後の項 $\m{s}(\m{s}(\m{s}(\m{0})))$ はこれ以上書換えられない項であり、正規形である。

3. パターンマッチング

項書換えを自動化するには、書換え規則で書換えられるのかを調べる必要があります。

定義（パターンマッチアルゴリズム）

項の対の有限集合に関する二項関係 $\leadsto$ を次の規則により定める。 \[ \{(f(s_1, \ldots, s_n), f(t_1, \ldots, t_n)) \} \uplus P \leadsto \{ (s_1, t_1), \ldots, (s_n, t_n) \} \cup P \] ここで $\uplus$ は disjoint union を表す。次の二つの性質をともに満たす項の対の有限集合 $P$ を 解形式と呼ぶ。

全ての $(s,t) \in P$ に対して $s$ は変数である。
$(x,t), (x,u) \in P$ に対して $x$ が変数であれば $t = u$ が成立する。

$P = \{ (x_1, t_1), \dots, (x_n, t_n) \}$ が解形式であるとき、 $\{ x_1 \mapsto t_1, \dots, x_n \mapsto t_n \}$ は代入になる。これを $P$ から導出される代入と呼ぶ。

$\leadsto$ による導出は無限のステップをもちません。

定理（パターンマッチアルゴリズムの正しさ）

$\{ (s, t) \} \leadsto \cdots \leadsto P$ とし、$P$ に対して $\leadsto$ による導出をこれ以上行えないものとする。

$s\sigma = t$ となる代入 $\sigma$ が存在するならば $P$ は解形式である。
$P$ が解形式であるとき $P$ によって導出される代入 $\sigma$ は $s\sigma = t$ を満たす。

例（パターンマッチングの例）

項 $s = \m{add}(x, \m{s}(\m{add}(y, z)))$ と $t = \m{add}(\m{s}(y), \m{s}(\m{add}(\m{add}(x, 0), z)))$ に対して、$s\sigma = t$ となる代入 $\sigma$ を見つけるためパターンマッチングアルゴリズムを用いる。 \begin{align*} \{ (s, t) \} & \,\;=\; \left\{ \bigl( \alert{\m{add}}(x, \m{s}(\m{add}(y, z))), \alert{\m{add}}(\m{s}(y), \m{s}(\m{add}(\m{add}(x, 0), z))) \bigr) \right\} \\[1ex] & \;\leadsto\; \left\{ \bigl(x, \m{s}(y)\bigr),\; \bigl(\alert{\m{s}}(\m{add}(y, z)), \alert{\m{s}}(\m{add}(\m{add}(x, 0), z))\bigr) \right\} \\[1ex] & \;\leadsto\; \left\{ \bigr(x, \m{s}(y)\bigr),\; \bigr(\alert{\m{add}}(y, z), \alert{\m{add}}(\m{add}(x, 0), z)\bigr) \right\} \\[1ex] & \;\leadsto\; \left\{ \bigl(x, \m{s}(y)\bigr),\; \bigl(y, \m{add}(x, 0)\bigr),\; \bigl(z, z\bigr) \right\} \end{align*} 最後の集合は解形式であり、導出される代入 $ \sigma = \{\, x \mapsto \m{s}(y),\; y \mapsto \m{add}(x, 0),\; z \mapsto z \,\} $ は $s\sigma = t$ を満たす。

例（パターンマッチングの失敗例）

項 $s = \m{add}(\m{s}(x), \m{add}(x, y))$ と $t = \m{add}(\m{s}(\m{add}(\m{0}, x)), \m{add}(\m{add}(\m{0}, \m{0}), x))$ に対してパターンマッチングアルゴリズムを用いると次の導出列を得る。 \begin{align*} \{ (u, v) \} & \,\;=\; \left\{ \bigl(\alert{\m{add}}(\m{s}(x), \m{add}(x, y)), \alert{\m{add}}(\m{s}(\m{add}(\m{0}, x)), \m{add}(\m{add}(\m{0}, \m{0}), x))\bigr) \right\} \\[1ex] & \;\leadsto\; \left\{ \bigl(\m{s}(x), \m{s}(\m{add}(\m{0}, x))\bigr),\; \bigl(\m{add}(x, y), \m{add}(\m{add}(\m{0}, \m{0}), x)\bigr) \right\} \\[1ex] & \;\leadsto\; \left\{ \bigl(x, \m{add}(\m{0}, x)\bigr),\; \bigl(\alert{\m{add}}(x, y), \alert{\m{add}}(\m{add}(\m{0}, \m{0}), x)\bigr) \right\} \\[1ex] & \;\leadsto\; \left\{ \alert{\bigl(x, \m{add}(\m{0}, x)\bigr)}\; \alert{\bigl(x, \m{add}(\m{0}, \m{0})\bigr)}\; \bigl(y, x\bigr) \right\} \end{align*} 最後の集合からこれ以上 $\leadsto$ によって導出できず、また解形式ではない。よって $s\sigma = t$ となる代入 $\sigma$ は存在しない。

4. 項書換えの実装

項書換えを実装してみましょう。 TRS フォーマットで記述された項書換え系のファイルをコマンドラインから受け取り、 main の正規形を出力するプログラム RewritingTool を作成することが目標です。例えば、先述の足し算の項書換え系を記述したファイル add.trs

(VAR x y)
(RULES
add(0,y) -> y
add(s(x),y) -> s(add(x,y))
main -> add(s(s(0)),s(0))
)

が入力に与えられた場合は、

$ ./RewritingTool append.trs
s(s(0()))

と出力することが期待されます。以下では関数型言語 Haskell を用いて実装する手順を演習問題形式で提示します。

演習問題 1

項と位置のデータ型 Term, Position に基づいて、 $\Pos(t)$, $t|_p$ および $t[u]_p$ に対応する関数を実装せよ。

data Term = V String | F String [Term] deriving Eq
type Position = [Int]

instance Show Term where
  show (V x)    = x
  show (F f ts) = f ++ "(" ++ intercalate "," [ show t | t <- ts ] ++ ")"

-- Pos(t)
positions :: Term -> [Position]

-- subtermAt t p = t|_p
subtermAt :: Term -> Position -> Term

-- replace t u p = t[u]_p
replace :: Term -> Term -> Position -> Term

以下は動作例。

>> positions (F "add" [F "add" [V "x", V "y"], V "y"])
[[],[0],[0,0],[0,1],[1]]

>> subtermAt (F "add" [F "add" [V "x", V "y"], V "y"]) [0, 0]
x

>> replace (F "add" [F "add" [V "x", V "y"], V "y"]) (F "0" []) [0, 0]
F "add" [F "add" [F "0" [], V "y"], V "y"]

演習問題 2

代入とパターンマッチングを行う関数 substitute, match を実装せよ。

type Subst = [(String, Term)]

-- substitute t sigma = t sigma
substitute :: Term -> Subst -> Term

-- match l t = Just sigma, if l sigma = t for some sigma
-- match l t = Nothing, otherwise
match :: Term -> Term -> Maybe Subst

以下は動作例。


>> substitute (F "add" [F "add" [V "x", V "y"], V "y"]) [("x", F "0" [])]
F "add" [F "add" [F "0" [], V "y"], V "y"]

>> match (F "add" [F "add" [V "x", V "y"], V "y"]) (F "add" [V "x", V "y"])
Nothing

>> match (F "add" [V "x", V "y"]) (F "add" [F "add" [V "x", V "y"], V "y"])
Just [("y", V "y"),("x", F "add" [x, y])]

演習問題 3

項を一ステップ書換える関数 rewrite と、正規形 (normal form) まで書換える関数 nf を実装せよ。

type Rule  = (Term, Term)
type TRS = [Rule]

-- rewrite R t = Just u,  if t ->_R u for some term u
-- rewrite R t = Nothing, otherwise
rewrite :: TRS -> Term -> Maybe Term

-- nf R t = u  if t ->_R ... ->_R u for some normal form u.
nf :: TRS -> Term -> Term

以下は動作例。

-- trs = { add(0,y) -> y,  add(s(x),y) -> s(add(x,y)) }
>> rule1 = (F "add" [F "0" [], V "y"], V "y")
>> rule2 = (F "add" [F "s" [V "x"], V "y"], F "s" [F "add" [V "x", V "y"]])
>> trs = [rule1, rule2]

-- a normal form of add(s(0),s(s(0))):
>> nf trs (F "add" [F "s" [F "0" []], F "s" [F "s" [F "0" []]]])
s(s(s(0())))

-- which is identical to: F "s" [F "s" [F "s" [F "0" []]]]

演習問題 4

項書換え系のファイルを読み込み、定数 main の正規形を出力するプログラムを実装せよ。

雛形となるコードを用意しました。実装の参考にしてください。

TRS.hs: 項や代入を扱う関数群の雛形。
TRSParser.hs: TRS フォーマットの構文解析器。
RewritingTool.hs: 本体の実装。 ghc -o RewritingTool RewritingTool.hs でコンパイルすると RewritingTool という実行ファイルが生成されます。

演習問題 5

クイックソートを表した項書換え系（qsort.trs） \begin{align*} \NIL \APPEND \mi{ys} & \to \mi{ys} \\ (x \CONS \mi{xs}) \APPEND \mi{ys} & \to x \CONS (\mi{xs} \APPEND \mi{ys}) \\[1ex] \m{0} \LEQ y & \to \m{true} \\ \m{s}(x) \LEQ \m{0} & \to \m{false} \\ \m{s}(x) \LEQ \m{s}(y) & \to x \LEQ y \\[1ex] \m{qsort}(\NIL) & \to \NIL \\ \m{qsort}(x \CONS \mi{xs}) & \to \m{split}(x, \mi{xs}, \NIL, \NIL) \\ \m{split}(w, \NIL, \mi{ys}, \mi{zs}) & \to \m{qsort}(\mi{ys}) \APPEND (w \CONS \m{qsort}(\mi{zs}))) \\ \m{split}(w, x \CONS \mi{xs}, \mi{ys}, \mi{zs}) & \to \m{if\_split}(w \LEQ x, w, x, \mi{xs}, \mi{ys}, \mi{zs}) \\ \m{if\_split}(\m{true}, w, x, \mi{xs}, \mi{ys}, \mi{zs}) & \to \m{split}(w, \mi{xs}, \mi{ys}, x \CONS \mi{zs}) \\ \m{if\_split}(\m{false}, w, x, \mi{xs}, \mi{ys}, \mi{zs}) & \to \m{split}(w, \mi{xs}, x \CONS \mi{ys}, \mi{zs}) \\ \m{main} & \to \m{qsort}(\m{s}(\m{s}(\m{0})) \CONS (\m{0} \CONS (\m{s}(\m{s}(\m{s}(\m{s}(\m{0})))) \CONS (\m{s}(\m{0}) \CONS (\m{s}(\m{s}(\m{s}(\m{0}))) \CONS \NIL))))) \end{align*} に対して作成したプログラムを実行し、整列されたリストが出力されることを確認せよ。

5. 研究について

項書換え系を介して、次のような計算に関する性質や応用・技法が研究されています。

停止性（再帰関数の well-definedness やプログラムの停止性）
合流性（計算結果の一意性）
計算量（正規形までのステップ数）
戦略（遅延評価等、正規形を得る方法）
定理自動証明

参考文献

以下に挙げる二冊が項書換えの標準的な教科書です。

[BN98]: F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge Unniversity Press, 1998.
[T03]: Terese. Term Rewriting Systems. Cambridge University Press, 2003.