PowerPoint

プログラム理論特論
第6回
亀山幸義
[email protected]
http://logic.is.tsukuba.ac.jp/~kam/progtheory
前回

型付きラムダ計算に対する型推論アルゴリズ
ムの構成
型の拡張;型変数の導入
 型に対する代入
 型の単一化、最も一般的な単一化(mgu)
 型の単一化アルゴリズム
 型推論アルゴリズム


型推論の過程を「下から上へ」構成する
資料の訂正


型の代入に対する「より一般的」という関係の定義
(資料通り)
資料の定義は正しかったが例1,2が誤り


この例で、
は誤り。
定義通り計算すると、
おいても、
とはならない。
と
資料の訂正

正しい例

他の誤植



3ページ下から8行目と3行目
でなく
でなく
単一化の具体例
単一化の具体例
型推論の具体例
拡張

これまでの型付きラムダ計算の体系


単純型付きラムダ計算 (simply typed lambda calculus)
これから考えること

単純型付きラムダ計算をどのように拡張すれば、現実の
プログラム言語を表現することができるか?





C言語:直積型、リスト型、配列型 etc.
ML:多相型
Java:レコード型、Subtyping
そのような拡張をしたとき、単純型付きラムダ計算の持っ
ていた良い性質は保たれるのか、失われるのか?
そもそも、何が「良い性質」だったのか?
「良い」性質

型システムの健全性


型付けできるプログラムを計算して得られたものは、型付
け可能であり、もとのプログラムと同じ型をもつ
型付けできるプログラムで、「値」になっていないものはま
だ計算できる(計算の途中で、止まってしまわない)
「良い」性質

停止性(正規化可能性)


型付けできるプログラムの計算は、有限時間で必ず停止
する。
証明はかなり難しい(項の構成に関する帰納法ではうまく
いかない)
「良い」性質の応用

型システムの健全性


プログラムの実行前に型付けしておくと(型検査または型推論)、プロ
グラムが実行中に悪い振舞いをしないことが保証できる
プログラムの悪い振舞いの例

実行時に型エラーを起こす


char型の変数(1バイト)に、int型の値(4バイト以上)を代入しようとする。
char x = 12345;
ポインタ型でない変数をポインタと思って参照する。
int x = -135; ...(*x) + 1;
型システムをさらに強力にすることにより、以下の性質も保証できる
配列のサイズを超えた添え字でアクセスをしないこと
int data[100]; ...data[110]*2+1 ...;
ある種のSecurity(秘密度の高いデータが漏洩しないこと)

静的解析(static analysis)によるSafety Propertyの保証の一種



Safety(安全性) ... ずっと○○をしない (○○は悪い振舞い)
Liveness(活性)... いつか必ず△△をする (△△は良い振舞い)
静的解析...プログラムを実行する前に(実行せずに)プログラムの性質を
解析する
「良い」性質の応用

停止性

Liveness の一種



(どんなに下手なプログラムでも)プログラムの実行は必ず有限
時間で停止する。
ただし、普通のプログラム言語は、whileループや再帰呼
出しを含むので、停止性は成立しない
一般的なプログラムではなく、(並行)プロトコルの検証な
どで有用
型システムの拡張1-直積

直積型 etc. の導入

集合の直積 (cartesian product, product)



型Aと型Bの直積 A×B





bool×nat= {(true,0),(true,1),(true,2),...,(false,0),(false,1),...}
「対(pair)」の集合
(true,3) : bool×int
λxint. (x,x) : int→(int×int)
left (false, 30) ⇒ false
right (false,30) ⇒ 30
直積型に対する型推論規則はどうなるか?
型システムの拡張1-直積

直積型に対する規則
型システムの拡張1-直積

直積型の項の例
問題

直積型を加えたことにより、以下の2つのアルゴリズ
ムはどう変更する必要があるか?


単一化アルゴリズム
型推論アルゴリズム
型システムの拡張1ーリスト
問題

リスト型を加えたことにより、以下の2つのアルゴリ
ズムはどう変更する必要があるか?



単一化アルゴリズム
型推論アルゴリズム
他の型構成子についても同様に型推論規則を示し、
単一化と型推論アルゴリズムを考えよ。



配列型
組(tuple, n個の型の直積)
C言語の struct型 (レコード型、名前のある組)
型システムの拡張2-多相型

1つのプログラムがいろいろな型を持ち得る



型推論アルゴリズムでは、これらの型を1つの表現であらわすため型変
数を導入した




λx.x は int→int でも bool→bool でもよい
λf.λx. fx は (int→int)→(int→int) でも、(bool→int)→(bool→int)でもよい
λx.x : α→α
λf.λx. fx: (α→β)→(α→β)
λf.λx. f(fx): (α→α)→(α→α)
しかし、ここまでの話では、1つのプログラムを同時に異なる型に適用す
ることはできなかった
型システムの拡張2-多相型

1つのプログラムが多数の型に対して適用できる現
象を(型推論だけでなく)プログラムの中で使えない
か?




多相型(polymorphic type, polymorphism)
λx.x 「すべてのαに対して、α→αという型をもつ」
λf.λx.f(x) 「すべてのα、βに対して、(α→β)→(α→β)という
型をもつ」
型 A,B ::= ... | ∀α.A
型システムの拡張2-多相型

話はそう簡単ではない!



∀という型を許すと型検査ですら決定不能 (undecidable)で
ある
型検査、型推論ができなければ、プログラム言語の型シ
ステムとしては使えない (論理としては使える)
ML言語の多相型

∀の記号は、型の一番外側だけに許す




∀のない型 A,B ::= α | K | A→B
∀を含むかもしれない一般の型 T ::= A | ∀α. T
例: ∀α.∀β.(α→β→α)
1つのプログラムを複数の型で使うときは let 構文を使う。
型システムの拡張2-多相型

ML言語はCurry流(型をプログラムは書く必要がな
い)
型システムの拡張2-多相型

実は、ML言語の多相型を導入しても、型推論アル
ゴリズム(単一化アルゴリズムも)は変更の必要がな
い。


型変数を導入したときに、すでに多相型の考え方がは
いっていた
型推論アルゴリズムで、Γ|-M:Aであると推論できれば、M
Lでは、M:∀α∀β。。。A ができたことになる。 (ここでα、β
はAに含まれる型変数)
問題

次のプログラムの型付けを考えよ。
次週

Java の型システムを考えます。