Luna Flow
日本語

substitution の設計

設計目標

代入はライブラリの他のすべての部分の土台となる操作である。β簡約は引数をパラメータに代入し、書き換え規則はその変数をインスタンス化し、下流パッケージの部分評価は既知の変数を値で置き換える。substitution は Term[T] に対する捕獲回避的な同時代入を一つ提供し、任意の BindingSyntax AST に対しても同じアルゴリズムを提供する。その法則は α同値を除いて成り立つ。

数学的背景

項、FV\mathrm{FV}、names\mathrm{names}、=α=_\alpha は syntax の設計 のものである。

代入

代入とは名前から項への写像 σ\sigma で、有限の定義域 dom⁡σ\operatorname{dom}\sigma の外では恒等 σ(x)=x\sigma(x) = x であるものである。その台は supp⁡σ=dom⁡σ∪⋃x∈dom⁡σnames(σ(x))\operatorname{supp}\sigma = \operatorname{dom}\sigma \cup \bigcup_{x \in \operatorname{dom}\sigma} \mathrm{names}(\sigma(x)) であり、σ∖x\sigma \setminus x は定義域から xx を取り除く。名前の集合 SS に対して、SS 上の σ\sigma の関連値域は次のとおりである。

Rσ(S)=⋃z∈S∩dom⁡σFV(σ(z)).R_\sigma(S) = \bigcup_{z \in S \cap \operatorname{dom}\sigma} \mathrm{FV}(\sigma(z)).

捕獲回避的な同時代入

Substitution::apply は tσt\sigma を次のように計算する。

vσ=v,xσ=σ(x),t(u1,…,un)σ=(tσ)(u1σ,…,unσ),(βx. t)σ={βx.  tσ′if x∉Rσ′(FV(t)),βx′.  (t{x↦x′})σ′otherwise,σ′=σ∖x,\begin{aligned} v\sigma &= v, \qquad x\sigma = \sigma(x), \qquad t(u_1, \dots, u_n)\sigma = (t\sigma)(u_1\sigma, \dots, u_n\sigma),\\ (\beta x.\, t)\sigma &= \begin{cases} \beta x.\; t\sigma' & \text{if } x \notin R_{\sigma'}(\mathrm{FV}(t)),\\[2pt] \beta x'.\; \big(t\{x \mapsto x'\}\big)\sigma' & \text{otherwise,} \end{cases} \qquad \sigma' = \sigma \setminus x, \end{aligned}

ここで x′=fresh⁡(x, supp⁡σ′∪names(t)∪{x})x' = \operatorname{fresh}(x,\ \operatorname{supp}\sigma' \cup \mathrm{names}(t) \cup \{x\}) であり、t{x↦x′}t\{x \mapsto x'\} は syntax の設計における検査付きの束縛名の名前替えである。場合分けは厳密である。束縛子が名前替えされるのは、実際に tt に挿入される置換項が xx を自由に含む場合に限る。

設計上の決定

同時に、一回で

問題。 {x↦y, y↦2}\{x \mapsto y,\ y \mapsto 2\} を x+yx + y に適用したとき、y+2y + 2 と 2+22 + 2 のどちらを返すべきか。

選択肢。 逐次代入（各エントリを順に適用する）、反復代入（変化がなくなるまで繰り返す）、または同時代入（各変数を元の項で一度だけ参照する）。

選択。 同時代入。変数の場合 xσ=σ(x)x\sigma = \sigma(x) は xx を一度だけ参照し、挿入された項を再び訪れることはない。

(x+y){x↦y, y↦2}=x{… }+y{… }=y+2.\begin{aligned} (x + y)\{x \mapsto y,\ y \mapsto 2\} &= x\{\dots\} + y\{\dots\} \\ &= y + 2 . \end{aligned}

同時代入は代数構造を持つ方式であり（後述の合成）、常に停止し、{x↦y, y↦x}\{x \mapsto y,\ y \mapsto x\} のような入れ替えを直接表現できる。逐次適用は then による合成として引き続き利用でき、不動点までの反復は呼び出し側の方針である。ジェネリック版はこれを明示するために apply_once と名付けられている。

必要なときだけ束縛子を名前替えする

問題。 束縛子 βx\beta x が、xx を自由に含む挿入された置換項の上にあるとき、捕獲が起こる。すべての束縛子を名前替えすれば回避できるが、結果が読みにくくなる。

選択。 x∈Rσ′(FV(t))x \in R_{\sigma'}(\mathrm{FV}(t)) のときだけ名前替えし、そのとき新しい名前をヒント xx のもとで選ぶ。新しい名前は三つの集合を避けなければならず、それぞれに理由がある。

  • 関連する置換項の FV\mathrm{FV}。さもないと名前替えされた束縛子がそれらを再び捕獲してしまう。
  • dom⁡σ′\operatorname{dom}\sigma'。さもないと xx から x′x' に名前替えされた出現自体が代入されてしまう（回帰テスト “fresh binders avoid the substitution domain”）。
  • names(t)\mathrm{names}(t)。これにより検査付きの束縛名の名前替え t{x↦x′}t\{x \mapsto x'\} が失敗せず、名前替えされた変数が同名の内側の束縛子と混同されることもない。

supp⁡σ′\operatorname{supp}\sigma' は最初の二つの集合を含む。したがって実装中の abort には到達しない。新しさの補題より x′∉names(t)x' \notin \mathrm{names}(t) であり、これはちょうど alpha_rename_bound の付帯条件である。

第一級の操作としての合成

then は次のように σ;τ\sigma \mathbin{;} \tau を構成する。

(σ;τ)(x)={σ(x) τx∈dom⁡σ,τ(x)x∈dom⁡τ∖dom⁡σ,xotherwise,(\sigma \mathbin{;} \tau)(x) = \begin{cases} \sigma(x)\,\tau & x \in \operatorname{dom}\sigma,\\ \tau(x) & x \in \operatorname{dom}\tau \setminus \operatorname{dom}\sigma,\\ x & \text{otherwise,} \end{cases}

これにより逐次適用を一つの同時代入として表現でき、その方が安価であり（走査は一回）、以下の法則を満たす。

正しさ / 不変条件

自由変数

補題 1. FV(tσ)=⋃z∈FV(t)FV(σ(z))\mathrm{FV}(t\sigma) = \bigcup_{z \in \mathrm{FV}(t)} \mathrm{FV}(\sigma(z))。

tt に関する帰納法による。変数、値、適用の場合は自明である。名前替えのない βx. t\beta x.\,t について、σ′=σ∖x\sigma' = \sigma \setminus x とし、x∉Rσ′(FV(t))x \notin R_{\sigma'}(\mathrm{FV}(t)) と仮定する。

FV((βx. t)σ)=FV(tσ′)∖{x}=(⋃z∈FV(t)FV(σ′(z)))∖{x}induction=⋃z∈FV(t), z≠xFV(σ(z))(∗)=⋃z∈FV(βx. t)FV(σ(z)).\begin{aligned} \mathrm{FV}\big((\beta x.\,t)\sigma\big) &= \mathrm{FV}(t\sigma') \setminus \{x\} \\ &= \Big(\textstyle\bigcup_{z \in \mathrm{FV}(t)} \mathrm{FV}(\sigma'(z))\Big) \setminus \{x\} && \text{induction} \\ &= \textstyle\bigcup_{z \in \mathrm{FV}(t),\, z \ne x} \mathrm{FV}(\sigma(z)) && (*) \\ &= \textstyle\bigcup_{z \in \mathrm{FV}(\beta x.\,t)} \mathrm{FV}(\sigma(z)). \end{aligned}

ステップ (∗)(*)：z=xz = x のとき、σ′(x)=x\sigma'(x) = x は {x}\{x\} を寄与するが、これは取り除かれる。z≠xz \ne x のとき、σ′(z)=σ(z)\sigma'(z) = \sigma(z) かつ x∉FV(σ(z))x \notin \mathrm{FV}(\sigma(z)) である。実際、z∈dom⁡σ′z \in \operatorname{dom}\sigma' かつ FV(σ(z))⊆Rσ′(FV(t))∌x\mathrm{FV}(\sigma(z)) \subseteq R_{\sigma'}(\mathrm{FV}(t)) \not\ni x であるか、または σ(z)=z≠x\sigma(z) = z \ne x である。名前替えがある場合も同じ計算が x′x' と t{x↦x′}t\{x \mapsto x'\} に適用でき、x′∉supp⁡σ′x' \notin \operatorname{supp}\sigma' により付帯条件が成り立つ。□\square

系（捕獲なし）。 挿入された置換項 σ(z)\sigma(z)（z∈FV(t)z \in \mathrm{FV}(t)）で自由な変数は、tσt\sigma においても自由である。

自由変数だけが重要である

補題 2. tσ=αt (σ∣FV(t))t\sigma =_\alpha t\,(\sigma|_{\mathrm{FV}(t)})。ここで σ∣S\sigma|_S は restrict(S) である。

変数の場合は定義そのものである。束縛子の場合、名前替えの判定はすでに Rσ′(FV(t))R_{\sigma'}(\mathrm{FV}(t)) に制限されているので、両辺は同じ束縛子を名前替えし、参照されるのは FV(t)∖{x}\mathrm{FV}(t) \setminus \{x\} の変数だけである。新しい名前は異なる代入の台を避けるため異なりうるので、等しさは =α=_\alpha を除いてのものとなる。

α不変性

補題 3. t=αt′t =_\alpha t' ならば tσ=αt′σt\sigma =_\alpha t'\sigma である。

一回の α ステップ βx. t=αβy. t{x↦y}\beta x.\,t =_\alpha \beta y.\,t\{x \mapsto y\}（ただし y∉names(t)y \notin \mathrm{names}(t)）を確認すれば十分である。両辺は束縛名を除いて同じ本体を持つ束縛子となり、補題 1 よりその本体は束縛子の外で同じ自由変数を持つので、α同値である。その結果、代入は α同値類の上で well-defined であり、新しい名前の選び方が意味的に影響することはない。

合成

補題 4. t(σ;τ)=α(tσ)τt(\sigma \mathbin{;} \tau) =_\alpha (t\sigma)\tau。

補題 3 により、tt の代表元として、どの束縛子も supp⁡σ∪supp⁡τ\operatorname{supp}\sigma \cup \operatorname{supp}\tau に属さないものを選べる。すると両辺とも束縛子は名前替えされず、二つの代入はそのまま束縛子の下に入る。変数の場合は σ;τ\sigma \mathbin{;} \tau の定義と同様に場合分けする。

x∈dom⁡σ:x(σ;τ)=σ(x)τ=(xσ)τ,x∈dom⁡τ∖dom⁡σ:x(σ;τ)=τ(x)=xτ=(xσ)τ,otherwise:x(σ;τ)=x=(xσ)τ.\begin{aligned} x \in \operatorname{dom}\sigma:&\quad x(\sigma;\tau) = \sigma(x)\tau = (x\sigma)\tau,\\ x \in \operatorname{dom}\tau \setminus \operatorname{dom}\sigma:&\quad x(\sigma;\tau) = \tau(x) = x\tau = (x\sigma)\tau,\\ \text{otherwise}:&\quad x(\sigma;\tau) = x = (x\sigma)\tau . \end{aligned}

適用と値の場合は帰納法から従う。□\square

系（代入補題）。 x≠yx \ne y かつ x∉FV(r)x \notin \mathrm{FV}(r) のとき、

t[x:=s][y:=r]  =α  t[y:=r][x:=s[y:=r]].t[x := s][y := r] \;=_\alpha\; t[y := r]\big[x := s[y := r]\big].

補題 4 により、両辺はそれぞれ一つの同時代入である。左辺は {x↦s[y:=r], y↦r}\{x \mapsto s[y := r],\ y \mapsto r\} である。右辺は {y↦r[x:=s[y:=r]], x↦s[y:=r]}\{y \mapsto r[x := s[y := r]],\ x \mapsto s[y := r]\} であり、x∉FV(r)x \notin \mathrm{FV}(r) なので r[x:=… ]=rr[x := \dots] = r である（補題 1）。二つの写像は等しいので、結果は α同値である。11 Barendregt, The Lambda Calculus, 補題 2.1.16。 これがラムダ計算パッケージにおいて β簡約を代入と両立させる補題である。

名前替えは代入に埋め込まれる

名前替え ρ\rho と名前のリスト L⊇FV(t)L \supseteq \mathrm{FV}(t) に対して、from_renaming(L, ρ) は σρ={x↦ρ(x)∣x∈L, ρ(x)≠x}\sigma_\rho = \{x \mapsto \rho(x) \mid x \in L,\ \rho(x) \ne x\}（変数として）であり、tσρ=αtρt\sigma_\rho =_\alpha t\rho が成り立つ。どちらも各自由な xx を変数 ρ(x)\rho(x) で置き換え、どちらも捕獲が起こる場合にちょうど束縛子を新しい名前にする。

コスト

各束縛子はその本体の自由変数を計算するので、サイズ nn、束縛の深さ dd の項に対して apply のコストは O(n⋅d)O(n \cdot d) 回のハッシュ集合操作であり、名前替えされる束縛子ごとに本体の走査が一回加わる。then のコストは self のエントリごとに apply 一回である。

ジェネリックな代入

GenericSubstitution::apply_once は、各構成子を対応する BindingSyntax のものに置き換えた同じ定義であり、したがって補題 1–3 は adapter の設計 のビュー法則を満たす任意の実装について成り立つ。Term[T] 上では二つのアルゴリズムは一致する。

却下した代替案

  • Barendregt の変数規約。 束縛名がすべての自由名と異なると仮定すれば名前替えの場合をなくせるが、項は利用者や他のアルゴリズムから来るものであり、この規約は簡約で保存されない。そのためライブラリは明示的に名前替えを行う。
  • De Bruijn 項のみでの代入。 インデックスによる代入は名前替えを必要とせず debruijn で提供されているが、下流の AST 向けの共有インターフェースは名前付きなので、名前付き代入はそれ自体で正しくなければならない。
  • 反復代入。 定義域の変数が現れなくなるまで繰り返すと発散しうるし（x↦f(x)x \mapsto f(x)）、合成の法則もない。不動点を必要とする呼び出し側は明示的に反復する。

境界

  • 単一化、マッチング、出現検査（occurs check）はない。代入は与えられるものであり、解かれるものではない。
  • GenericSubstitution には then も restrict もない。ジェネリックな代入は順に適用することで合成する。
  • 結果が教科書の定義と等しいのは =α=_\alpha を除いてのみである。比較には @syntax.alpha_equal を使う。
  • 値の内部には決して入らないので、変数を含む Value ペイロードに対して代入は行われない。

Footnotes

  1. Barendregt, The Lambda Calculus, 補題 2.1.16。 ↩