目次

はじめに

帰納的閉包のさらなる理解のために、

• 自由に生成された集合
• 再帰的関数定義

について理解するのが良いので概要のみ紹介する。

自由に生成された集合

帰納的閉包 X = Ind(C, F)が以下の条件を満たすとき、「自由に生成された集合である」と言う。

1. 任意の異なる関数f^r(n),g^r(m) ∈ Fに対して、f^r(n)(X) ∩ g^r(m)(X) = ∅ である。
   1.1 つまり異なる関数を適用した結果の共通集合はなく、すなわち異なる関数を適用した結果はそれぞれ異なることを意味する
2. 任意の関数f^r(n) ∈ Fについて、f^r(n)(X) ∩ C = ∅ である
   2.1 つまり関数を適用した場合、定数Cを生成することはないことを意味する
3. 任意の関数f^r(n) ∈ Fについて、f^r(n)|_xⁿ は単射関数である
   3.1 fのXへの制限すなわち定義域をXに制限した集合{(a, b) | (a, b) ∈ f, a ∈ X}で表される関数を、f|_xと表記するのであった
   3.2 _xⁿはn次の直積を表す
   3.3 上記はf自身が同じものを生成することはない、つまり引数が異なれば必ず異なる結果を生成することを意味する

上記は直感的に「Fで生成される要素は既存のものとは異なる新しい要素である」ことを示している。

以降は帰納的閉包を、自由に生成された集合の定義とみなす。
つまり上記3つの条件を満たすこととし、別の言い方をすれば以下の2つだとも言える。

• BNF等の文法規則は、文字列ではなく構文木の集合を定義する規則である
• 証明規則は、正しい論理式やシーケンスのみでなく、その証明過程を含む証明木の集合を定義する規則である

※ みなす、と言われているのでしょうがないが…

関数の再帰的定義

Aを任意の集合とする。
また、X = Ind(C, F)は帰納的閉包であるが、ここでは自由に生成された集合（つまり前述の3つの条件を満たす）とする。

Cの要素をcとし各cに対してAの要素_cが与えられるとする。
各f^r(n)に対して関数f^r(n) ∈ Aⁿ → Aが与えられたとき、以下の条件を満たす関数ψ ∈ X → Aが唯一存在する。

• 任意の定数cに対して、ψ© = _c
• Xの要素f^r(n)(x₁, … , x_n)について、ψ(f^r(n)(x₁, … , x_n)) = _f^r(n)(ψ(x₁,…,ψ(x_n)))

つまり、上記の2つの条件を与えることができれば、関数の再帰的定義が可能と言える。

この関数ψを、関数λc ∈ C._{_c}の _f^r(n)に関する唯一の準同型拡張と呼ぶ。

型無しラムダ式

型推論の対象は以下のBNFで定義される型無しラムダ式である。

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

カッコが不要になるため、省略するのが慣例となっている。
ただし以下のルールを仮定する。

• 必要に応じてカッコを用いて良い
• λx.eにおけるeはできる限り大きくとる
  • (λx₁.λx₂…(λx_n.e)…)はλx₁.λx₂…λx_n.e と表記できる
• 関数適用は左結合とする
  • ((e₁ e₂) … e_n)はe₁ e₂ … e_nと表記できる

ラムダ式の意味（おさらい）

• λx.eは、xを仮引数として値eを計算する関数を表す
• e₁ e₂は、関数e₁に対して関数e₂を適用した結果を表す

この直感的な意味は、ラムダ式の簡約関係 (λx.e₁) e₂ ⇒ [e₂/x]e₁ である。

型の集合と型の直感的意味

基底型（これ以上型を持たない）の集合をb,tとする（BaseTypeが由来）。
また加算無限個の型変数の集合のメタ変数をTVarとする。

型の集合Typeを以下のように定義する。

τ ::= t | b | τ → τ

上記の意味は、

• t : 集合Typeの変数
• b : intやstring等の与えられた基底型
• τ₁ → τ₂ : τ₁ から τ₂ への関数の型

型表記のおさらい

• 関数型構成子→は右結合とする
  • 例えば、b → b → b のとき、b → (b → b) と解釈する

型システムの考え方

型システムとは、以下の関係を含む式の整合性を記述するものと考えることができる。

• 変数の定義と参照関係
• 関数と引数の適用関係

ここで変数が定義される文脈を表現する型環境をΓする。
このとき型システムは以下のように、型判定の導出システム（証明システム）として定義できる。

Γ :> e : τ

つまり式eは何らかの型集合τにマッピングできる（これを判定する）システムだと言っている。

なお、型環境Γは変数の有限集合から型への関数であり {x₁ : τ₁, …, x_n : τ_n} と記述できる。

型判定

例えば、式(f x)（関数fが引数xに適用された形）の変数f及びxは、
この式を囲む文脈（例えば λf. … λx. … のようなもの）で参照される。

このとき、この式は以下の型判定を持つ。

{ f : τ₁ → τ₂, x : τ₂} :> f x : τ₂

上記の意味は、

• fが型(τ₁ → τ₂)の変数であり、xが型τ₁の変数であると定義された環境の下で、
• 式(f x)は型τ₂を持つ

である。

すなわち、この型判定は上記の意味を主張する**文（シーケント）**である。

型推論規則（型付け規則）

構造を持たない式（変数と定数）に対して、以下の2つの規則を導入する。

• (var) Γ {x : τ} :> x : τ
• (const) Γ :> c^b : b
  • bはcの基底型を表すのであった

(var),(const)は規則名である。
これらの規則はすべて導出可能である。

次に部分式を持つ式に対して、以下の2つの規則を導入する。

• (abs) Γ {x : τ₁} :> e : τ₂ が導出できれば Γ :> λx.e : τ₁ → τ₂ が導出できる
  • これは{x : τ₁}を仮定できる環境下でeがτ₂の型を持てば、ある環境Γの下でλx.eは(τ₁ → τ₂)という関数型を持つ、と言っている
• (app) Γ :> e₁ : τ₁ → τ₂ 及び Γ :> e₂ : τ₁ が導出できれば Γ :> e₁ e₂ : τ₂ が導出できる
  • 規則(abs)から意味は容易に想像できるため割愛

ワンポイント： ある式が与えられ「それに対する型判定の導出をせよ」と言われたら、一番下に式を書き導出規則を逆に適用する（つまり下から上の式を導く）形で行おう！

Ref: 型判定導出の例

暗黙に型付けられたラムダ計算

型なしラムダ計算と型推論規則の集合は**「暗黙に型付けられたラムダ計算」**と呼ぶ型付きの計算系を意味する。
この計算系を λ と書く。

λ の項は型無しラムダ式eではなく、型導出を持つ型判定である。

なるほど！つまり λ において型が合わないような計算は存在し得ないということ。

型判定 Γ :> e : τ （実際には型推論規則でもあるが）に対して型導出（D(Γ :> e : τ) ∈ Typing(Γ :> τ)）が存在するとき（すなわち導出木が形成できる場合）、 λ |- Γ :> e : τ と書く。

つまり型システムの推論対象は λ |- Γ :> e : τ で表される Γ :> e : τ と言える。

参考

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