debruijn の設計

設計目標

名前付き構文では、束縛子をまたぐすべての操作で新鮮な名前とリネーミングが必要になる。debruijn は alpha 同値が構文的な等しさになり、beta 簡約にリネーミングがまったく要らない表現を、名前付き構文との間の正確な変換とともに提供する。これは utlc/nbe の型なし NbE のカーネル表現であり、utlc/lambda の名前付き計算をテストする際の参照簡約器でもある。

数学的背景

インデックス

名前のない束縛子を持つ項では、束縛された出現は数 $i$、すなわちその De Bruijn インデックスであり、出現とそれが参照する束縛子の間にある束縛子の数である。¹1 N. G. de Bruijn, “Lambda calculus notation with nameless dummies”, Indagationes Mathematicae 34, 1972. Bind を $\lambda$、Apply を並置で表すと：

$$\lambda x.\,\lambda y.\,x\,y \;\rightsquigarrow\; \lambda.\,\lambda.\,1\;0 , \qquad \lambda x.\,x\,(\lambda y.\,x\,y) \;\rightsquigarrow\; \lambda.\,0\,(\lambda.\,1\,0).$$

同じ変数でも深さが異なればインデックスも異なる（ここでは $x$ は $0$、次に $1$）。自由変数は名前のまま（Free(x)）であり、これは自由な部分についての「locally nameless」な選択で、変換を単純に保つ。

$k$ 個の束縛子の下にあるすべてのインデックスが $n + k$ より小さいとき、項は深さ $n$ でスコープが正しいという。深さ $0$ でスコープが正しいとき、単にスコープが正しいという。validate はこれを判定する。

レベル

束縛子のレベルとは、根から数えた深さである。$n$ 個の束縛子の下にあるインデックス $i$ の出現は、次のレベルの束縛子を参照する。

$$\ell = n - 1 - i, \qquad\text{equivalently}\qquad i = n - 1 - \ell .$$

項を束縛子 1 つ分深く移すとき（弱化：文脈が内側の端で伸びる）、その自由変数のインデックスは 1 だけシフトしなければならないが、レベルは変わらない。そのため NbE 評価器は束縛子の下に入る際に導入する変数にレベルを使い、意味値をシフトせずに深い位置へ移せるようにし、quote の際に $i = n - 1 - \ell$ で変換し戻す。

シフト

$\uparrow^{d}_{c}\,t$ は、カットオフ $c$ に関して自由な $t$ のすべてのインデックスに $d$ を加える。

$$\begin{aligned} \uparrow^{d}_{c}\,i &= \begin{cases} i & i < c \\ i + d & i \ge c \end{cases}, & \uparrow^{d}_{c}\,(\lambda.\,t) &= \lambda.\,\uparrow^{d}_{c+1} t, \\ \uparrow^{d}_{c}\,(t\,\bar u) &= (\uparrow^{d}_{c} t)\,(\overline{\uparrow^{d}_{c} u}), & \uparrow^{d}_{c}\,v &= v, \quad \uparrow^{d}_{c}\,x = x \ (x \text{ free}). \end{aligned}$$

shift(t, d, c) は束縛子の深さ $k$ を持ち回り $i \ge c + k$ を判定することでこれを実装する。これは $c$ に関する再帰を展開したものである。

インデックスの代入

$[j \mapsto s]\,t$ は自由インデックス $j$ を $s$ で置き換える。

$$[j \mapsto s]\,i = \begin{cases} s & i = j \\ i & i \ne j \end{cases}, \qquad [j \mapsto s]\,(\lambda.\,t) = \lambda.\,[\,j+1 \mapsto \uparrow^{1}_{0} s\,]\,t .$$

substitute_bound は束縛子の場合を展開する。$k$ 個の束縛子の下では、インデックス $j + k$ を $\uparrow^{k}_{0} s$ で置き換える。カットオフが同じシフトは合成できる（後述の補題 1）ので、両者は一致する：$\uparrow^{1}_{0}\cdots\uparrow^{1}_{0} s = \uparrow^{k}_{0} s$。

Beta 簡約

$$(\lambda.\,t)\;s \;\to_\beta\; \uparrow^{-1}_{0}\big(\,[\,0 \mapsto \uparrow^{1}_{0} s\,]\;t\,\big) .$$

引数は $t$ の束縛子の下に移るので上方にシフトされる。代入の後でその束縛子は取り除かれるので、本体に残るすべての自由インデックスは下方にシフトされる。これが instantiate(t, s) である。²2 B. C. Pierce, Types and Programming Languages, MIT Press 2002, §6.2–6.3.

設計上の決定

シフトは仮定せず検査する

問題。 不正な項に負のシフトを行うと負のインデックスが生じ、それは黙って何も参照しない。

選択。 代わりに shift は Err(NegativeShift) を返し、すべての操作は負の入力に対して NegativeIndex を報告する。以下の補題は、スコープの正しい入力からはエラーの場合に到達しないことを示すので、Result は正しい呼び出し側には何のコストもなく、誤った呼び出し側に対しては黙った破損をデータに変える。これは、公開境界で想定される失敗は構造化された値であるというライブラリの規則に従う。

スコープの正しい入力では具体化は失敗しない

補題 1（シフトの合成）。 $a, b \ge 0$ について $\uparrow^{a}_{c}\uparrow^{b}_{c} t = \uparrow^{a+b}_{c} t$ であり、$\uparrow^{0}_{c} t = t$ である。

現在のカットオフに対する添字 $i$ について：$i < c$ ならば両辺ともそのまま残し、$i \ge c$ ならば $i + b \ge c$ であるので

$$\uparrow^{a}_{c}\uparrow^{b}_{c}\, i = (i + b) + a = \uparrow^{a+b}_{c}\, i .$$

束縛子の場合は両辺で同様にカットオフを引き上げる。$\square$

補題 2（下方向シフトの安全性）。 $\lambda.\,t$ と $s$ が深さ $n$ でスコープ整合であるとする。このとき $u = [\,0 \mapsto \uparrow^{1}_{0} s\,]\,t$ のすべての自由添字は $\{1, \dots, n\}$ に属するので、$\uparrow^{-1}_{0} u$ は成功し、深さ $n$ でスコープ整合である。

本体 $t$ は深さ $n + 1$ でスコープ整合であるので、その自由添字は $\{0, \dots, n\}$ に属する。$t$ 内で $k$ 個の内側の束縛子の下にある自由な出現を追う：

$$\begin{aligned} i = k + 0 &: \text{replaced by } \uparrow^{k}_{0}\uparrow^{1}_{0} s = \uparrow^{k+1}_{0} s \text{ (Lemma 1)}, \\ &\quad\text{whose free indices relative to the root are } j + 1 \in \{1, \dots, n\} \text{ for } j \in \mathrm{fi}(s) \subseteq \{0, \dots, n-1\}, \\ i = k + m,\ m \ge 1 &: \text{kept, with root-relative index } m \in \{1, \dots, n\}. \end{aligned}$$

自由添字 $0$ はもはや残らないので、$-1$ によるシフトは負の結果を生じることなく $\{1, \dots, n\} \to \{0, \dots, n - 1\}$ と写す。$\square$

したがって instantiate と reduce_once はスコープ整合な入力に対して ScopeError を返さず、スコープ整合な項の簡約結果はスコープ整合である（スコープに関する主部簡約性）。ゆえに normalize からの ScopeFailure は常に入力がスコープ不整合であったことを意味する。

異なるカットオフをもつシフトの可換性や De Bruijn 代入補題を含む詳細な証明は、添付資料にある：

De Bruijn 項の添字に関する補題

厳密な相互変換

from_named は束縛子名のスタックを保持し、$x$ の出現を最も近い $x$ の束縛子までの距離に変換する。そのような束縛子がなければ Free(x) に変換する。to_named は fresh_name("x", U) で束縛子名を生成する。ここで $U$ は項の自由な名前と外側の束縛子の名前を含む。

定理（往復変換）。

1. すべての名前付き項 $t$ について $\texttt{to\_named}(\texttt{from\_named}(t)) =_\alpha t$。
2. すべてのスコープ整合な $d$ について $\texttt{from\_named}(\texttt{to\_named}(d)) = d$。
3. $\texttt{from\_named}(t) = \texttt{from\_named}(u) \iff t =_\alpha u$.

(2) について：根からの任意の経路に沿って、to_named が選ぶ名前は互いに異なり、かつすべての自由な名前とも異なる。各名前は、自由な名前と外側のすべての束縛子名を含む集合に対して新しく選ばれるからである。$n$ 個の束縛子の下にある添字 $i$ の出現は、レベル $n - 1 - i$ の束縛子の名前になる。逆変換すると、その名前をもつ最も近い束縛子はまさにその束縛子であり（外側の他の束縛子はその名前をもたない）、距離は $i$ である。Free(x) は $x$ になり、これは経路上のどの束縛子の名前でもないので、Free(x) に戻る。(3) は de Bruijn の定理であり、(1) は (2) と (3) から従う。$\texttt{from\_named}(\texttt{to\_named}(\texttt{from\_named}(t))) = \texttt{from\_named}(t)$ だからである。

名前付きと名前なしの β 簡約の一致

名前付き項に対して、β 簡約は $(\lambda x.\,b)\,a \to b[x := a]$ であり、代入 の捕獲回避代入を用いる。$x$ を最も内側の束縛子としたときの $b$ の変換を $\ulcorner b \urcorner_{x}$ と書く。このとき

$$\ulcorner b[x := a] \urcorner \;=\; \texttt{instantiate}\big(\ulcorner b \urcorner_{x},\ \ulcorner a \urcorner\big),$$

$b$ に関する帰納法による：$k$ 個の内側の束縛子の下にある $x$ の出現は添字 $k$ をもち、$\uparrow^{k}_{0}\ulcorner a \urcorner$ を受け取る。これはそれら $k$ 個の束縛子の下に置かれた $a$ の変換である。名前付き代入による束縛子の名前替えは、(3) により変換後には見えない。変換は項の形も保つので、二つの簡約器は同じ最左最外の簡約基を選び、1 ステップは $=_\alpha$ を除いて変換と可換である。テスト “named and debruijn beta reduction agree modulo alpha” は、名前付き側で名前替えが必要となる例を検査する。

スパインと簡約順序

Apply(head, args) はカリー化されたスパインである：Apply(Bind(t), [a, ..rest]) は rest に適用された簡約基 $(\lambda.\,t)\,a$ であり、1 ステップは最初の引数のみを縮約する。reduce_once は根、ヘッド、引数を探索し、束縛子の中にも入る：これは名前なし項上の eval の設計 の正規順序戦略であり、したがって正規化定理が normalize に適用される。

正しさ / 不変条件

• すべての名前付き項 $t$ について validate(from_named(t)) == Ok(())。
• 上記の往復変換 (1)–(3)。スコープ整合な DbTerm 上の == は α同値である。
• 補題 2：スコープ整合な入力に対して instantiate は成功しスコープを保つ。reduce_once は決して ScopeFailure を返さず、すべての簡約結果はスコープ整合である。
• reduce_once は rewrite の単一簡約基契約を満たし、規則名は "beta" である。
• shift(t, 0, c) == Ok(t) であり、同じカットオフのシフトは合成できる（補題 1）。

コスト：shift と validate は項のサイズに対して線形である。添字が $m$ 回出現する場合、挿入される各コピーがシフトされるため、substitute_bound のコストは $O(|t| + m \cdot |s|)$ である。reduce_once の 1 ステップのコストは探索 1 回と instantiate 1 回である。

却下した代替案

• 構文で添字の代わりにレベルを使う。 レベルを使うと弱化はコストなしになるが、束縛子の下での代入が複雑になる。構文には添字が標準であり、レベルは役立つ場面（NbE）で用いる。
• 完全に名前なしの自由変数。 自由変数は名前のまま保持される。これにより、ユーザーや下流の AST からの開いた項に大域的な変数番号付けが不要となり、to_named がそれらを正確に復元できる。
• 明示的代入。 保留された代入をもつ計算体系は繰り返しのシフトを避けられるが、すべての利用側を複雑にする。代わりに効率的な経路は NbE パッケージが提供する。

境界

• 束縛子名は保存されない：to_named は x、x_1、… を選ぶ。
• substitute_bound と reduce_once は束縛されていない添字を検出しない。信頼できない入力には validate を呼ぶこと。
• 実装されているのは β のみであり、De Bruijn 項に対する η 規則はない。
• 値は不透明であり、その内容がシフトされることはない。

Footnotes

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

2. B. C. Pierce, Types and Programming Languages, MIT Press 2002, §6.2–6.3. ↩