PowerPoint

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

Download Report