国立情報学研究所 ソフトウェア研究系 助教授／ E-mail: ichiro@nii.ac.jp 計算モデル特論 型付ラムダ計算 国立情報学研究所 ソフトウェア研究系 助教授／ 科学技術振興事業団 さきがけ研究21 研究員 佐藤一郎 E-mail: ichiro@nii.ac.jp

型とは プログラミングにおけるデータ型 Pascal: var x,y: integer, a:real

型の必要性 プログラム設計を明確化 プログラムの誤り防止 関数やモジュールの仕様 コンパイラ最適化への補助情報 プログラム停止性への補助保証 可読性の向上

プログラミング言語の型 基本データ型 整数、浮動小数点、文字、真偽値 構造データ型 配列、直積型、直和型、レコード型、ストラクチャ型 ユーザ定義型

型付プログラミング言語 プログラミング言語と型 型なしプログラミング言語 ○プロトタイピング、×インタープリタ実行 弱い型付プログラミング言語 ○手っ取り早く設計・記述、×信頼性が低い 強い型付プログラミング言語 ○安全なプログラム、×慎重な設計と冗長な記述 型検査 静的検査 動的検査

型推論 強い型付プログラミング言語を利用しながら簡潔な記述を実現するには 型は文面から推定可能 例： f(x) = if x == 0 then 1 else x * f(x-1) 推定により冗長な記述を現象 形式的な体型により型を厳密に決定

型推論の例 式要素の型と式全体の型 例： if e0 then e1 else e2 型推論の目的 与えられた式がある型を持つことを証明する 「もし e0 が真偽値型（bool型）で、e1とe2が T という型を持つことが示されれば、 if e0 then e1 else e2は T という型を持つ（ことがわかる）」 型推論の目的 与えられた式がある型を持つことを証明する 与えられた式がもつ型を求める 推論規則 e0: bool型 かつ e1:T型 かつ e2:T型 仮定 (if e0 then e1 else e2):T型 結論

型付ラムダ計算 型理論体系 項（term） 型（type） 判定（judgment） 推論規則（inference）

型付ラムダ式（基本） τ ::= b | (τ→τ) M ::= cτ | x | (λx:τ.M) | (M1 M2) BNF文法による型

型付ラムダ式 | (M1 ,...,M2) | M.i τ ::= b | (τ×・・・×τ) | (τ→τ) M ::= cτ | x | (λx:τ.M) | (M1 M2) | (M1 ,...,M2) | M.i

型付ラムダ式 基本型: b 直積型： (τ×・・・×τ) 関数型： (τ→τ) BNF文法による型 括弧の省略 型における矢印は右結合 直積型： (τ×・・・×τ) 関数型： (τ→τ) 括弧の省略 型における矢印は右結合 例: (t1→(t2 →(t3 →t4) = t1→t2 →t3 →t4

型付ラムダ式の直感的意味 (M1 M2) (λx:τ.M) 基本式： 関数M1に引数M2を与えたときの値

型付きラムダ式の例 f(x)=x+1なる関数fは lx:int.x+1 fに実引数3を与えた式f(3)は (lx:int.x+1)(3int)

自由変数 FV(c) = 0 FV(M1 M2) = FV(M1) È FV(M2) FV(lx:t.M) = FV(M) - {x} FV(x) = {x} FV(M1 M2) = FV(M1) È FV(M2) FV(lx:t.M) = FV(M) - {x} FV((M1 ,..,M2)) = FV(M1) È .. È FV(M2) FV(M.i) = FV(M) 自由変数でない変数を束縛変数と呼ぶ

型付ラムダの計算 [N/x]c = c [N/x](M1,...,Mn) = ([N/x]M1,...,[N/x]Mn) 簡約規則 [N/x]c = c [N/x](M1,...,Mn) = ([N/x]M1,...,[N/x]Mn) [N/x](M.i) = ([N/x]M).I (lx:t.M)=(ly:t.[y/x]M) ((lx:t.M) N:t) → [N/x]M

記法 e:t A ├ e:t A1├ M1:t1 ・・・・・ An├ Mn:tn A├ M:t 前提（assumption）： 判定（judgement）: A ├ e:t （０個以上の）前提A（型環境）から、ある式eが型tを持つことが示される 推論（inference）： 式Miがそれぞれの前提Aiにおいて型tを持つならば、結論が示される A1├ M1:t1 ・・・・・　 An├ Mn:tn A├ M:t

型推論規則 型推論規則 (app) (const) (prod) (var) (abs) (proj)

型推論規則の記法 G+{x:t} G(x)=t 前提への操作と表記

型推論規則（詳細） 型推論規則 関数lx:t1.Mが関数型t1→t2を持つ のは、仮引数の型t1と仮定したとき、 (const) (var) 関数lx:t1.Mが関数型t1→t2を持つ のは、仮引数の型t1と仮定したとき、 関数Mが型t2をもつときである。 (abs)

型推論規則（詳細） 型推論規則 関数は、関数がその定められた値 にのみ適用可能であり、その結果 は関数の値の型を持つこと (app) 関数の組(M1,...,M2)はM1,...,M2の 直積となる (prod) 関数の組(M1,...,M2)からI番目の 要素を取り出したときはM1の型 となる (proj)

型推論の例 型推論では推論規則により変形していく 型付ラムダ式 K=lx.(ly.x)

型推論の性質 健全性 型推論できるならば、その結果が正しい（型安全）ことを意味する 完全性 正しいことはすべての型において推論することができる 有用性 決定可能かつ効率がよいこと

多相型 プログラム中に現れる同一の式やデータが複数の型をもつこと L.CardelliとP.Wegnerによる分類 アドホックな多相型 文脈によって型を決定。例、等号、オーバーローディング演算子 系統的な多相型 共通の性質をもった型に作用。例：パラメトリック多相型 パラメトリック多相型の例： twice関数　(twice f(3)) = f(f(3)) fがint型ときのtwice関数の型: (int→int)→int→int fがfloat型ときのtwice関数の型: (float→float)→float→float