目次

はじめに

Twitterにてこのようなツイートを見かけたので、内容を確認してみた。

これまでインターネットや書籍で軽く触れられてきた内容に切り込んでいくものだったので、理解を深めることができた。

その内容をまとめていく。

概要

言語は文法で定義される。

例えば、MLの一部の式は以下のように定義される。

<exp> ::= <id>                     // 変数
      |   <n> | <S> | true | false // 自然数(n), 文字列(S) その他定数
      |   fn <id> => <exp>         // 関数式
      |   <exp> <exp>              // 関数適用
      |   ...

プログラミング言語の理論ではより抽象的な定義を行うため、変数や定数を「与えられた集合」とし、これを代表するものをメタ変数と呼ぶ。

ラムダ式では以下の集合とメタ変数を導入する。

• 変数(Var)に対するメタ変数をxとする
• 定数(Const)に対するメタ変数をc^b(c of b)とする
  • ※ b はint等の型を明示するためのもの

構文自体に対してもメタ変数を導入できる。

• ラムダ式の集合(lambda)に対するメタ変数をeとする
  • ML式における非終端記号<exp>に相当する

BNF記法では以下のように表される。

e ::= x | c^b | (lambda x.e) | (e e)

これはMLの一部の式に示した定義と同等であることが分かる。
このような定義を抽象構文(abstract syntax)の定義と呼ぶ。
ここで抽象とは、語彙解析や構文解析の詳細について了解されていることを示す。

なぜ抽象構文を用いるか。
言語の型等の性質の理論的な分析を行うため、と言える。
また分析の対象となるのは、機能法等で分析可能な集合である、と言える。

ここで以下のBNFを思い出そう。

e ::= x | c^b | (lambda x.e) | (e e)

上記eはラムダ式の集合とみなせる。この集合をΛとする。

するとラムダ式の集合e（またはΛと表現）の条件が見えてくる。

• Λはxが代表する集合Varを含む
• Λはcが代表する集合Constを含む
• もしΛにeが含まれるのであれば、eを使った式もΛに含まれる
• もしe₁及びe₂がΛに含まれるのであれば、(e1, e2)もΛに含まれる
• Λは以上の要素のみを含む

またBNFから、Λを生成する以下の規則も見えてくる。
つまり先程のBNFは、Λの要素を生成する以下の操作であると言える。

• xと書いた場合、xが代表する集合VarをΛの要素に加える操作である
• c^bと書いた場合、c^bが代表する集合ConstをΛの要素に加える操作である
• もしeが集合lambdaに含まれるなら、(lambda x.e)と書いた場合、これをΛに加える操作である
• もしe₁,e₂が集合lambdaに含まれるなら、(e₁ e₂)と書いた場合、これをΛに加える操作である

また以上のことから、ラムダ式の集合は以上の要素生成を（無限に）繰り返して得られる集合であると言える。

集合の帰納的定義

動画ではここからスタートする内容である。

さて、前述したラムダ式の集合における条件や規則について、それらが数学的に定義可能かを見ていく。

まず、数学的定義を行うために必要な道具（集合に関する記法）を整理する。

• A,A₁…,A_n を集合とする
• 集合に対して以下の集合演算が可能である
  • A₁ ⊗ …A_x = {(a₁,…,a_n) | a_i ∈ A_i (1 ≤ i ≤ n)}
    • これはA₁,…A_nの直積を表す
  • Aⁿ = A ⊗ … ⊗ A
    • これは集合Aのn次の直積を表す
• 関数を代表するメタ変数fに対して、その定義域を dom(f) と表記する
• Xがdom(f)の部分集合である時（すなわちX ⊆ dom(f)の時）、集合{f(x) | x ∈ X}をf(X) と表記する
• fのXへの制限すなわち定義域をXに制限した集合{(a, b) | (a, b) ∈ f, a ∈ X}で表される関数を、f|_xと表記する
• f|_dom(f){x}すなわちXへの制限を取り除いたものをf|¬xと表記する
• 変数x₁〜x_nと対応する値v₁〜v_n (x_i ≠ x_j, 1 ≤ i ≤ j ≤ n)に対して、f{x₁:v₁,…,x_n:v_n}は新たな関数f’を表す
  • f’の定義域dom(f’)について、dom(f’) = dom(f) ∪ {x₁,…,x_n} となり
  • 且つf’の値について、f’(y) = f(y) (y ≠ x_i, 1 ≤ i ≤ n) または v_i (y = x_i)となる
    • x_iはdom(f)の定義であっても良い、そうでなければv_iとなるという意味

次に、全体集合Uを置き、集合Fを f ∈ Uⁿ → U つまり、Uのn次の直積からUへの関数の集合と定義する。

この時nをfのランクと言いrank(f)と書く。
また、ランクがnであるFの要素をf^r(n)と書く。

ここで、Uに対する部分集合X（X ⊆ U）に対して、{f^r(n) (x₁,…,x_n) | x_i ∈ X, f^r(n) ∈ F} となる集合をF(X)と書く。
つまりF(X)は、関数集合Fに属するfについて、ランクnにx₁〜x_n（xはXの要素）を与えfに適用した結果を集めた集合である。
さらにF(X) ⊆ X の時、すなわちXの要素(x_i等)をfに適用した際にその結果がXの範囲に留まる時、「XはFに関して閉じている(Closed under F)」と言う。

帰納的閉包

部分集合C（C ⊆ U）を与えられた集合とし、CのFに関する帰納的閉包を「集合Cを含みFに関して閉じている集合の最小のもの」と定義する。またこれを Ind(C, F)と書くことにする。

ここで最小とは、集合の包含関係（例えば A ⊆ B）に関して最小のもの、という意味である。

この講義で言いたいことは「BNFを含む再帰的な規則で定義される集合は、帰納的閉包である（帰納的閉包で表される）」ということである。

帰納的閉包の性質1

そもそもInd(C, F)つまり集合Cを含み関数集合Fに関して閉じている最小の集合というものは存在するのだろうか（直感的には存在するとは思うが、確認することが大事だ）。

そこでXを 空でない集合の集まり（集合）とし、以下の演算を定義する。

∩ X = {a | Xの要素（実体は集合）である全てのY（∀Y ∈ X）について a ∈ Y}

つまり上記の演算は、Xの全ての部分集合における共通集合を得ることになるため、必然的に最小の集合を得る演算となっている。

さて、Uの部分集合C（C ⊆ U）且つ F(U) ⊆ U から、U自身はCを含み且つFに関して閉じた集合全体の集合はUの要素を含み空ではないことが分かる。
また、空ではない集合の集合Xについて ∩ X の演算を定義したことから、F(X)すなわちXがFに関して閉じている場合、∩ X においてもFに関して閉じていると言える。

したがって Ind(C, F)は確かに存在し以下のように定義できる。

Ind(C, F) = ∩{V | V ⊆ U, C ⊆ V, F(V) ⊆ V}

つまり Uの部分集合V（V ⊆ U）は、Uの部分集合Cが含まれ且つFに関して閉じている全てのものの集まりであり、これに対して ∩ をとったものである。∩ をとるというのは、Vにおける最小の集合を得ることであり、ここではCが最小の集合であるため、Ind(C, F)は確かに存在することが分かる。

帰納的閉包の性質2

ここでは、Ind(C, F)にどのような要素が含まれているかを確かめていく。

自然数で添字付けられた無限列（集合系列） {X_n | n = 0,1,…,n} を以下のとおり定義する。

X₀ = C
X_i+1 = X_i ∪ F(X) (0 ≤ i)

上記のX₀は定数Cを表す。
X_i+1は、1つ前の値であるX_iとF(X_i)（つまり関数集合Fに属するfにX_iを適用して得られる全ての値）の和集合を表す。
つまり、上記の漸化式で表される集合系列は、添字の数を大きくなる毎にその集合自体も大きくなる。

この集合系列のもとで、Ind(C, F)は以下のように定義できる。

Ind(C, F) = ∪ {X_i | 0 ≤ i}

（それはそうか、という感じもするが、証明が必要だ）

性質2の証明

性質2を証明するにはどのようにすれば良いか。以下の2つを証明すれば良い。

1. Ind(C, F) ⊆ ∪ {X_i | 0 ≤ i}
2. ∪ {X_i | 0 ≤ i} ⊆ Ind(C, F)

1.については、次のステップで証明できる。

1. ∪ {X_i | 0 ≤ i}がFに閉じていることを示す
2. f^r(n)をFの任意の要素とし、∪ {X_i | 0 ≤ i}ⁿ （n次の直積）の任意の要素（
   実際はX_iで表される要素の組）をxとする
3. そのようなxをとった時、あるkが存在して x ∈ (X_k)ⁿであることを示す
4. するとf^r(n) ∈ X_k+1 ⊆ ∪ {X_i | 0 ≤ i}である
5. 同様にF(∪ {X_i | 0 ≤ i}) ⊆ ∪ {X_i | 0 ≤ i}である
6. よってInd(C, F) ⊆ ∪ {X_i | 0 ≤ i}である

※ 2,3のステップが微妙に整理できていないかも？

2.については、次のステップで説明できる。

1. 定義よりX₀ = C ⊆ Ind(C, F)である
2. X_i ⊆ Ind(C, F)と仮定する
3. Ind(C, F)はFに閉じているのだから、F(X_i) ⊆ Ind(C, F)である
4. 定義よりX_i+1 = X_i ∪ F(X_i)であるから、X_i+1 ⊆ Ind(C, F)である
5. よって∪ {X_i | 0 ≤ i} ⊆ Ind(C, F)である

帰納的閉包によるラムダ式の理解

この講義で言いたいことは「BNFを含む再帰的な規則で定義される集合は、帰納的閉包である（帰納的閉包で表される）」ということであった。早速見ていこう。

全体集合U（例えば構文木全体からなる集合等）を置き、ラムダ式の集合Λを帰納的閉包として定義する。
なおこの時Λは全体集合Uの部分集合になっている、

さて集合Varに対するメタ変数x（x ∈ Var）について、e（ラムダ式の集合Λに対するメタ変数）から (lambda x.e)を作る関数をf¹_{lambda x}、e₁及びe₂から(e₁ e₂)を作る関数をf²_appとすると、関数集合Fは以下のように定義できる。

F_Λ = {f¹_{lambda x} | x ∈ Var} ∪ {f²_app}

するとラムダ式の集合Λは、以下のとおり定義できる。

Λ = Ind(Var ∪ Const, F_Λ)

つまりX₀に相当するVar及びConstの和集合から始まり、それらを用いて作成できる関数を要素に持つ集合Fに関して閉じている最小の集合を示している。

BNFを帰納的閉包の文脈で見直してみる

Λ = Ind(Var ∪ Const, F_Λ) = ∩ {V | V ⊆ U, (Var ∪ Const) ⊆ V, F_Λ(V) ⊆ V}

と考えると、Λは次の制約を満たすものであると定義できる。

• (Var ∪ Const) ⊆ V よりΛは集合Varと集合Constを含む = (Var ∪ Const) ⊆ Λ
• F_Λ(V) ⊆ V よりF_Λ(Λ) ⊆ Λつまりf¹_{lambda x}及びf²_appに関して閉じた集合である
• 上記を満たす最小の集合である

つまり、

• Λはxが代表する集合Varを含む = Var ⊆ Λ である
• Λはcが代表する集合Constを含む = Const ⊆ Λ である
• もしΛにeが含まれるのであれば、eを使った式もΛに含まれる = もし e ⊆ Λ ならば (lambda x.e) ⊆ Λ である
• もしe₁及びe₂がΛに含まれるのであれば、(e₁ e₂)もΛに含まれる = もしe₁ ⊆ Λ 且つ e₂ ⊆ Λ ならば (e₁ e₂) ⊆ Λ である
• Λは以上の要素のみを含む ← これがはっきりとした！

と言える。

同様にΛの要素を生成する操作という文脈においても別の見方ができる。

Λ = Ind(Var ∪ Const, F_Λ) = ∪ {X_i | 0 ≤ i}

• (Var ∪ Const)の要素を追加する
• 全てのx, y ⊆ Λ に対して、f¹_{lambda x}及びf²_appを追加する

つまり

• xと書いた場合、xが代表する集合VarをΛの要素に加える操作である
• c^bと書いた場合、c^bが代表する集合ConstをΛの要素に加える操作である
• もしeが集合lambdaに含まれるなら、(lambda x.e)と書いた場合、これをΛに加える操作である
• もしe₁,e₂が集合lambdaに含まれるなら、(e₁ e₂)と書いた場合、これをΛに加える操作である
• Λは異常の要素の生成を（無限に）繰り返して得られる集合である ← これがはっきりした！

と言える。

参考

• 「型推論」特別講義 第２回 （プログラミング言語の基礎理論シリーズ）