rewrite の設計

設計目標

rewrite は局所的な規則、すなわち項をその根で書き換える部分関数を、大域的で監査可能な簡約に変える：選んだ位置での 1 ステップと、その位置と規則の記録、そしてそうしたステップの有界な繰り返しである。ライブラリのすべての操作的意味論（eval の戦略、lambda 計算、debruijn の De Bruijn 簡約器）はこの形の単一ステップ関数として定義されており、どの正規化器もステップごとに説明できる。

数学的背景

抽象書き換え系

抽象書き換え系とは、集合 $A$ と関係 $\to\ \subseteq A \times A$ の組である。¹1 Terese、Term Rewriting Systems、Cambridge University Press 2003、第 1 章。その反射推移閉包を $\to^{*}$ 、同値閉包を $\leftrightarrow^{*}$ と書く。

$a \to b$ となる $b$ が存在しないとき、 $a$ は正規形である。
無限列 $a_0 \to a_1 \to \cdots$ が存在しないとき $\to$ は停止的（強正規化的）であり、すべての要素がある正規形に簡約されるとき弱正規化的である。
$b \leftarrow^{*} a \to^{*} c$ ならばある $d$ について $b \to^{*} d \leftarrow^{*} c$ となるとき $\to$ は合流的であり、これが 1 ステップの分岐 $b \leftarrow a \to c$ について成り立つとき局所合流的である。

合流性により正規形は一意になる： $a \to^{*} n_1$ かつ $a \to^{*} n_2$ で両方が正規形ならば、共通の簡約結果 $d$ は両者に等しくなければならない。Newman の補題は、停止的かつ局所合流的な系は合流的であると述べる。項書き換え系の局所合流性は、その危険対の合流可能性から従う（Knuth–Bendix）。²2 M. H. A. Newman、“On theories with a combinatorial definition of equivalence”、Annals of Mathematics 43、1942。

位置と文脈

位置とは根からのフレームの経路 $p$ である：BinderBody は $\beta x.\,\Box$ に入り、ApplyHead は $\Box(\bar u)$ に入り、ApplyArgument(i) は $i$ 番目の引数に入る。 $p$ における部分項を $t|_p$ 、その部分項を $s$ で置き換えた $t$ を $t[s]_p$ と書く：

\begin{aligned} t|_{\varepsilon} &= t, & (\beta x.\,t)|_{\mathsf{B}\cdot p} &= t|_p, & t(\bar u)|_{\mathsf{H}\cdot p} &= t|_p, & t(u_0,\dots,u_n)|_{\mathsf{A}_i\cdot p} &= u_i|_p . \end{aligned}

規則の書き換え関係

規則とは部分関数 $r : \mathrm{Term} \rightharpoonup \mathrm{Term}$ である。 $r$ の簡約基とはその定義域に属する項である。 $r$ の書き換え関係は、文脈に関するその閉包である：

\frac{t|_p \in \operatorname{dom} r}{t \;\to_r\; t[\,r(t|_p)\,]_p}

戦略とは、定義されるときは常に $S(t) \in \{\, u \mid t \to_r u \,\}$ となる部分関数 $S$ であり、可能なステップの中から一つを選ぶ。このパッケージの走査関数は戦略であり、StepResult によってその選択が観測可能になる。

設計上の決定

単一ステップがプリミティブである

問題。 1 回の走査で「書き換えられるものすべて」を書き換える正規化器は高速だが、その振る舞いを仕様と比較できず、中間状態も失われる。

選択。 プリミティブは一つの位置での 1 ステップであり、Reduced(before, after, rule, path) または NoStep として返される。その契約は実装において構成的に保証されており、次のとおりである

\texttt{Reduced}(t, u, r, p) \implies t|_p \in \operatorname{dom} r \;\wedge\; u = t[\,r(t|_p)\,]_p ,

したがって報告される各ステップは、ちょうど報告された位置での $\to_r$ の 1 ステップである。走査は経路上のノードのみを再構築して after を作り、戻る途中で各レベルごとにフレームを一つ先頭に追加して path を作る。正規化器とトレースはこのプリミティブ上のループであり、意味的なものは何も追加しない。この設計のコストは、完全な正規化がステップごとに根から走査を繰り返すことである。利点は、すべての正規化器がトレースをもち、二つの実装をステップごとに比較できることである。

走査順序としての戦略

top_down_once はノードで規則を試してから子を試し、子の順序はヘッド、引数 0、引数 1、… である。前順で最初の簡約基を返し、これは最左最外の簡約基である：それを含む簡約基はなく、そのような簡約基の中で最も左にある。bottom_up_once は子を先に試し、後順で最初の簡約基、すなわち最左最内の簡約基を返す：それは他の簡約基を含まない。

補題（正規形）。 どちらの走査についても、 $t$ に対する NoStep は $t$ が $\to_r$ の正規形であることと同値である。

どちらの走査も $t$ のすべての位置（束縛子の本体、ヘッド、すべての引数）を訪れ、そこで $r$ を試す。すべての試行が None を返した後でのみ NoStep を返すので、どの位置も簡約基ではない。逆に、ある位置が簡約基ならば、走査は別のステップで先に返らない限りそこに到達する。 $\square$

したがって、いずれの走査を用いた normalize も、 $t$ が $\to_r$ 正規形であるときに限り NormalForm(t, n) を返す。eval の弱頭部簡約のような他の戦略は訪れる位置がより少なく、それらにとって NoStep は「戦略が考慮する位置に簡約基がない」ことのみを意味する。

正確なカウント付きの有界な繰り返し

normalize(t, step, k) は列 $t_0 = t$ 、 $t_{i+1} = \mathit{after}(\mathit{step}(t_i))$ を計算し、 $\mathit{step}(t_n) = \texttt{NoStep}$ となる最初の $n$ か、 $n = k$ で停止する：

\texttt{normalize}(t, \mathit{step}, k) = \begin{cases} \texttt{NormalForm}(t_n, n) & n \le k,\ \mathit{step}(t_n) = \texttt{NoStep},\\ \texttt{StepLimitReached}(t_k, k) & \mathit{step}(t_k) \ne \texttt{NoStep}. \end{cases}

$n = k$ での追加の呼び出しによって「ちょうど $k$ ステップ後に正規形」と「上限に到達」が区別されるので、結果が検査していない正規形を主張することはない。任意の規則に対して停止性は決定不能であり（型なしラムダ計算では成り立たない）、そのためステップ上限が必要である。これはパラメータであり、大域的な設定ではない。

規則は登録されるのではなく名前を付けられる

問題。 書き換え系は通常、複数の規則をもつ。

選択肢。 パッケージ内の規則レジストリ。呼び出しごとの規則のリスト。呼び出しごとに一つの規則関数。

選択。 呼び出しごとに一つの規則関数と一つの RuleName。複数の規則をもつ系は、一つの規則にまとめるか（lambda の beta_eta_rule のように、各位置で β を η より先に試す）、複数の単一規則走査を順に試すステップ関数として表現する。二つの選び方は異なる戦略を与える：前者はいずれかの規則が適用できる最も外側の位置を選び、後者は項全体のどこであれ最初の規則を優先する。この選択を呼び出し側に委ねることで、すべての言語に一つの優先順位方式を固定することを避ける。

ビューを介した汎用走査

generic_top_down_once は、パターンマッチに project を、再構築にトレイトのコンストラクタを用いる top_down_once である。ビュー法則以外に下流 AST についての知識を必要としないので、多項式や数値式の AST は位置とトレースを無償で得られる。汎用に提供されるのはトップダウン戦略のみである。下流の簡約器が使うのはこれであり、また正規形補題が利用可能になるからである。

正しさ / 不変条件

1 ステップは高々一つの位置を書き換え、報告される path は before におけるその位置を指す（上記の契約）。“structured step records rule and root path” と debruijn の経路テストで検査される。
top_down_once、bottom_up_once、generic_top_down_once からの NoStep は、項がその規則について正規形であることを意味する（正規形補題）。
normalize と trace は高々 max_steps ステップを実行し、step を高々 max_steps + 1 回呼ぶ。NormalForm(t, n) ならば step(t) = NoStep である。
ReductionTrace では steps[0].before = initial、steps[i].after = steps[i+1].before であり、result の最終項は最後の after（ステップがなければ initial）である。

検査されないこと。 このパッケージは規則の停止性や合流性を判定しない。規則が合流的であれば、停止するすべての戦略は同じ正規形に到達する。そうでなければ、異なる戦略が正当に異なる正規形を返すことがあり、トレースがその理由を示す。

コスト：サイズ $n$ の項に対して 1 ステップは $O(n)$ 回の規則試行と経路の再構築を要する。 $k$ ステップでの正規化は $O(k \cdot n)$ 回の規則試行を要する。

却下した代替案

その場書き換えまたはメモ化された書き換え。 より高速だが、before と経路が失われ、不変な項と相容れない。
固定された規則言語（変数付きパターン）。 パターン言語にはマッチングと出現検査が必要になる。MoonBit 関数としての規則は、ホスト言語のパターンマッチと任意の副条件を使える。
捕獲を考慮した走査。 走査は、開いた部分項を規則に渡す前に束縛子の名前替えを行うこともできる。束縛を考慮した振る舞いを必要とする規則は、すでに名前替えを行う代入を使う。走査の中で名前替えを行うと、規則の知らないところで束縛子名が変わってしまう。

境界

規則は束縛子の下の部分項を開いた項として見る。走査は名前替えを行わず、どの束縛子がスコープ内にあるかも報告しない。規則は開いた項に対して正しくなければならない。
結合律・可換律・α同値を法としたマッチングはない。規則は項をそのままの形で MoonBit のパターンによりマッチする。
停止性・合流性・危険対の解析は行わない。
汎用版はトップダウン戦略とトレースなしの正規化にのみ存在する。
上限 max_steps が数えるのはステップ数であり、時間やメモリではない。

Terese、Term Rewriting Systems、Cambridge University Press 2003、第 1 章。 ↩
M. H. A. Newman、“On theories with a combinatorial definition of equivalence”、Annals of Mathematics 43、1942。 ↩