syntax の設計

設計目標

syntax は Luna Flow に「束縛子を持つ構文」の単一の定義を与える。これは任意の記号的 AST が採用できるほど小さく、しかも自由変数、α同値、名前替えに関する通常の法則を証明できるほど厳密である。対象は二つある。具体的な Term[T] を使うラムダ計算パッケージと、独自の型を保ちつつ BindingSyntax を通じて同じアルゴリズムを利用する下流の AST である。

数学的背景

項

core の設計 の名前の集合 $\mathcal{N}$ とドメイン値の集合 $V$ を固定する。項は次で生成される。

$$t, u \;::=\; v \;\mid\; x \;\mid\; t(u_1, \dots, u_n) \;\mid\; \beta x.\, t \qquad (v \in V,\ x \in \mathcal{N},\ n \ge 0),$$

これは構成子 Value、Variable、Apply、Bind に対応する。束縛子 $\beta x.\,t$ はジェネリックであり、ラムダ計算はこれを $\lambda x.\,t$ と読み、多項式ライブラリは局所スコープと読むことができる。値はアトムであり、名前を含まない。

自由変数と名前

$$\begin{aligned} \mathrm{FV}(v) &= \varnothing, & \mathrm{FV}(x) &= \{x\}, \\ \mathrm{FV}(t(u_1,\dots,u_n)) &= \mathrm{FV}(t) \cup \textstyle\bigcup_i \mathrm{FV}(u_i), & \mathrm{FV}(\beta x.\,t) &= \mathrm{FV}(t) \setminus \{x\}. \end{aligned}$$

$\mathrm{names}(t)$ は $\mathrm{names}(\beta x.\,t) = \mathrm{names}(t) \cup \{x\}$ を除いて同じ等式で定義される。これは all_names が返す集合であり、$\mathrm{FV}(t) \subseteq \mathrm{names}(t)$ である。

α同値

$y \notin \mathrm{names}(t)$ に対して、$t$ における $x$ の自由な出現をすべて $y$ で置き換えたものを $t\{x \mapsto y\}$ と書く。$y$ は $t$ のどこにも現れないので、どの出現も捕獲されない。α同値 $=_\alpha$ は、項上の合同関係のうち次を満たす最小のものである。

$$\beta x.\, t \;=_\alpha\; \beta y.\, t\{x \mapsto y\} \qquad \text{whenever } y \notin \mathrm{names}(t).$$

このライブラリのすべての操作は $=_\alpha$ のもとで不変であり、ラムダ計算は α同値類の上で定義される。¹1 H. P. Barendregt, The Lambda Calculus: Its Syntax and Semantics, North-Holland 1984, §2.1. このライブラリは同書の「変数規約」に依存しない。各操作は必要に応じて明示的に名前替えを行う。

設計上の決定

不透明なペイロードを持つ単一のジェネリックな項型

問題。 どの記号的パッケージも変数と束縛子を必要とするが、それぞれ独自の定数（数値、演算子、型付き定数）を持つ。

選択肢。 拡張可能な定数型を持つ固定のラムダ計算、パッケージごとに別々の項型、定数でパラメータ化された単一の項型。

選択。 Term[T] はその定数でパラメータ化され、T は不透明である。アルゴリズムは Value の内部を決して見ない。これが健全なのは定数が変数を含まない場合に限られ、それが明示された契約である（“T is a closed atom”）。定数が変数を含む AST は、代わりに BindingSyntax を実装しなければならない（次節）。適用は n 項である。ほとんどの記号的 AST は演算子を複数の引数に適用するからである。ラムダ計算はこれをカリー化されたスパインとして読む。

固定の AST の代わりにビュートレイト

問題。 下流のリポジトリはすでに AST を持っている。代入のたびにそれを Term[T] に変換して戻すのは時間がかかり、構造も失われる。

選択。 BindingSyntax は一層のビューを通じてノードを記述する。圏論の言葉では、シグネチャ関手を次のように定義する。

$$F(X) = 1 \;+\; \mathcal{N} \;+\; X \times X^{*} \;+\; \mathcal{N} \times X .$$

BindingView[N] は $F(N)$ であり、project は余代数 $N \to F(N)$、variable、apply、bind は三つの不透明でない直和成分上の代数をなす。すべてのジェネリックなアルゴリズムは構造的再帰であり、project を呼び、子に対して処理を行い、構成子で再構築する。実装が満たすべき法則は adapter の設計 に列挙されている。Term[T] については構成上成り立つ。project が Value でない項と Opaque でないビューの間の全単射だからである。

帰結。 Term[T] に対して、各ジェネリック関数はその特殊化版と同じ結果を計算する。

$$\texttt{generic\_free\_variables}(t) = \mathrm{FV}(t), \qquad \texttt{generic\_all\_names}(t) = \mathrm{names}(t),$$

また generic_alpha_rename_bound は Term::alpha_rename_bound と一致する。証明は直接的な帰納法である。各場合で二つの関数は同じ等式を持つ。project は構成子のフィールドをそのまま返すからである。

束縛レベルによる α同値の判定

問題。 定義から直接 $=_\alpha$ を判定するには名前替えの探索が必要になる。

選択。 alpha_equal は二つの項を歩調を合わせて走査し、二つの束縛環境 $E_L, E_R$ を保持する。これは各束縛名を、それが束縛されたレベル（根から数えた束縛の深さ）に写す。同じ名前の後の束縛は前の束縛をシャドーイングする。$E$ における $x$ の最後の束縛のレベルを $E(x)$、現在の深さを $d$ と書くと、

$$\begin{aligned} E_L, E_R \vdash_d v \sim v' &\iff v = v', \\ E_L, E_R \vdash_d x \sim y &\iff \begin{cases} E_L(x) = E_R(y) & \text{if both are bound},\\ x = y & \text{if both are free},\\ \text{false} & \text{otherwise}, \end{cases}\\ E_L, E_R \vdash_d t(\bar u) \sim t'(\bar u') &\iff |\bar u| = |\bar u'| \wedge t \sim t' \wedge \textstyle\bigwedge_i u_i \sim u'_i, \\ E_L, E_R \vdash_d \beta x.\,t \sim \beta y.\,t' &\iff E_L[x \mapsto d], E_R[y \mapsto d] \vdash_{d+1} t \sim t'. \end{aligned}$$

定理. alpha_equal(t, u) が成り立つのは $t =_\alpha u$ のとき、かつそのときに限る。

証明の概略。 $\ulcorner t \urcorner$ を debruijn の設計 の De Bruijn 変換とする。これは深さ $d$ にあり束縛子がレベル $\ell$ にある束縛された出現をインデックス $i = d - 1 - \ell$ で置き換え、自由な名前はそのまま残す。二つの走査は同じ深さ $d$ で同じ位置を訪れるので、束縛された出現について

$$\ell_L = \ell_R \iff d - 1 - \ell_L = d - 1 - \ell_R \iff i_L = i_R ,$$

であり、自由な出現はどちらでも名前で比較される。したがって alpha_equal(t, u) であることと $\ulcorner t \urcorner = \ulcorner u \urcorner$ であることは同値である。二つの名前付き項が α同値であるのはその De Bruijn 変換が一致するとき、かつそのときに限るという古典的定理²2 N. G. de Bruijn, “Lambda calculus notation with nameless dummies”, Indagationes Mathematicae 34, 1972. により証明が完了する。$\square$

このアルゴリズムの実行時間は項のサイズに線形であり、これに環境の参照コスト（束縛の深さに線形）が加わる。

自由変数の捕獲回避的な名前替え

問題。 束縛子の下で名前替え $\rho$ を適用すると捕獲が起こりうる。$\beta y.\,x$ で素朴に $x \mapsto y$ と名前替えすると $\beta y.\,y$ になる。

選択。 rename_free は次を実装する。

$$\begin{aligned} x\rho &= \rho(x), \qquad v\rho = v, \qquad t(\bar u)\rho = (t\rho)(\overline{u\rho}),\\ (\beta x.\,t)\rho &= \begin{cases} \beta x.\; t(\rho \setminus x) & \text{if } x \notin \operatorname{tgt}(\rho \setminus x),\\ \beta x'.\; \big(t\{x \mapsto x'\}\big)(\rho \setminus x) & \text{otherwise,} \end{cases} \end{aligned}$$

ここで $x' = \operatorname{fresh}(x,\ \mathrm{names}(t) \cup \operatorname{supp}(\rho \setminus x) \cup \{x\})$ である。

補題（名前替えの自由変数）。 $\mathrm{FV}(t\rho) = \rho(\mathrm{FV}(t))$。

興味深いのは新しい名前にしない束縛子の場合だけである。$\rho' = \rho \setminus x$ とし、$x \notin \operatorname{tgt}\rho'$ とする。帰納法により $\mathrm{FV}(t\rho') = \rho'(\mathrm{FV}(t))$ なので、

$$\begin{aligned} \mathrm{FV}\big((\beta x.\,t)\rho\big) &= \{\rho'(n) \mid n \in \mathrm{FV}(t)\} \setminus \{x\} \\ &= \{\rho(n) \mid n \in \mathrm{FV}(t),\ n \ne x\} && \rho'(x) = x,\ \rho'(n) = \rho(n) \ne x \text{ for } n \ne x \\ &= \rho(\mathrm{FV}(\beta x.\,t)). \end{aligned}$$

二番目のステップでは $n \ne x$ に対して $\rho(n) \ne x$ であることを用いる。実際、$n \in \operatorname{dom}\rho'$ かつ $\rho(n) \in \operatorname{tgt}\rho'$ であって $x$ は除外されるか、または $\rho(n) = n \ne x$ である。新しい名前にする場合も同じ計算が $t\{x \mapsto x'\}$ と $x'$ に適用できる。$x'$ は $\operatorname{supp}\rho'$ の外にあり、したがって写す元でも写す先でもないからである。この補題はまさに、どの自由変数も捕獲されなかったことを述べている。

判定 $x \notin \operatorname{tgt}(\rho \setminus x)$ は保守的である。問題となるエントリの元が $t$ に現れない場合にも束縛子を名前替えする。それでも結果は最小のものと α同値である。

検査付きの束縛名の名前替え

alpha_rename_bound(t, x, y) は上記の α ステップの本体である $t\{x \mapsto y\}$ を計算し、$y \notin \mathrm{names}(t)$（または $x = y$）でない限り None を返す。この付帯条件のもとで、α公理から直接次が得られる。

$$\beta x.\, t \;=_\alpha\; \beta y.\, t\{x \mapsto y\}.$$

この検査は必要以上に強い（内側の $y$ の束縛子の下にある $y$ の出現は無害である）が、安価であり、代入アルゴリズムが必要とするのはこれだけである。代入アルゴリズムは常に本体に対して新しく選んだ名前でこれを呼び出すからである。

正しさ / 不変条件

• $\mathrm{FV}(t) \subseteq \mathrm{names}(t)$ であり、map_values は両者を保存する。
• alpha_equal は反射的、対称的、推移的であり、$=_\alpha$ と一致する（上記の定理）。反射性は src/syntax/syntax_wbtest.mbt の QuickCheck プロパティでも検査されている。
• rename_free は $\mathrm{FV}(t\rho) = \rho(\mathrm{FV}(t))$ を満たし、$=_\alpha$ のもとで不変である。α同値な入力は α同値な出力を与える。
• alpha_rename_bound(t, x, y) = Some(t') ならば $\beta x.\,t =_\alpha \beta y.\,t'$ である。
• Term[T] 上では、各 generic_* 関数はその特殊化版と等しい。

コスト：free_variables と all_names は項のサイズに線形である（ハッシュ集合操作の回数で）。rename_free と alpha_rename_bound は束縛子が名前替えされなければ線形であり、新しい名前にされる束縛子ごとに本体の走査が一回加わる。

却下した代替案

• 値の内部の変数。 T に名前を含めることを許すと、T にも走査用のトレイトが必要になる。そのような AST は BindingSyntax を直接実装すればよく、一つのトレイトで同じ要求を満たせる。
• 多変数の束縛子。 複数の名前を一度に束縛する束縛子は、入れ子の Bind ノードとして表現する。これによりビューは小さく保たれ、証明も束縛子ごとに行える。
• 検査なしの束縛名の名前替え。 None の場合をなくした版では捕獲が黙って起こる。検査付きの形にすると事前条件が型に現れる。
• 変換による α同値。 両方の項を De Bruijn 形式に変換して比較すると新しい項を二つ割り当てることになる。歩調を合わせるアルゴリズムは割り当てなしで同じ比較を行う。

境界

• Value ペイロードは決して調べられない。変数を含むペイロードは契約の範囲外である。
• 項に対する == は構造的な等価性であり、α同値ではない。
• ソート、スコープ、型はない。すべての名前は同じ種類の項変数である。
• このパッケージは BindingSyntax の実装がその法則に従っているかを検査しない。その検査方法は adapter で説明されている。
• 代入は substitution に、走査と書き換えは rewrite にある。

Footnotes

1. H. P. Barendregt, The Lambda Calculus: Its Syntax and Semantics, North-Holland 1984, §2.1. このライブラリは同書の「変数規約」に依存しない。各操作は必要に応じて明示的に名前替えを行う。 ↩

2. N. G. de Bruijn, “Lambda calculus notation with nameless dummies”, Indagationes Mathematicae 34, 1972. ↩