PowerPoint

プログラム理論特論
第４回
亀山幸義
[email protected]
http://logic.is.tsukuba.ac.jp/~kam/progtheory
ソフトウェアの
安全性、堅牢性、高信頼性

安全な(safe)ソフトウェア


堅牢な（robust)ソフトウェア


授業と関係のな
い寄り道です
Fault-tolerance, fail-safe：部分的に失敗しても全体としてはおかしくなら
ない
信頼性(reliable, trustful)の高いソフトウェア



Security：（悪意のある）攻撃者に対する安全性
上の２つを含む？
Verified: 正しさに関する保障がある
用語は定まっていない


プログラム言語の安全性、堅牢性：強い型システム等により
実現
Java言語の byte-code verifier：外付けの信頼性向上の手段
復習
プログラム言語の型システムの構造を深く観
察するために、非常に単純なプログラム言語
(型付きラムダ計算 Church流）を導入した
 型付きラムダ計算の構文、計算規則を定義し
た

例題
Δ|- f : α→α Δ|- x : α
Δ|- f : α→α
Δ|- f x : α
Δ|- f (f x) : α
Γ|- λx. f (f x) : α→α
{}|- λf. λx. f (f x) : (α→α) →(α→α)
Γ={fα→α}
Δ={fα→α, xα}
Curry流の体系：構文

項の構成規則
Γ|- M : B
具体例

(自然数の）階乗を計算する関数fact
型検査 (type-checking)

問題：Γ、M、Aが与えられたとき、
となるかどうか検査する（YES か NO か答え
る）
型推論 (type-inference)

問題：Mが与えられたとき、
となるΓとAがあるかどうか判定する。YES/NOだけでな
く、YESの場合は具体的に与える
今日の目標

Church流の型付きラムダ計算の体系に対する型推
論アルゴリズムを学ぶ。



型推論ができれば、型検査も容易
Curry流の体系に対する型推論アルゴリズムも基本的に
は同じ
型推論ができてしまえば、Church流もCurry流も差はない
階乗関数の例題 (revisited)

まず、具体的なラムダ計算の体系を定めよう
上記の例題を記述できるミニ言語を、型付きラム
ダ計算の一種として定式化しよう。
 型定数は何だろうか？
 定数とその型は何だろうか？

ミニ言語

型定数


int (整数）、bool (真理値）
定数とその型




*: int の引数を２つもらってintを返す関数
（これまでに学習した)型付きラムダ計算の体系では、関数の引数は
１つだけであった。
では、どうやって、２引数関数を表現するか？
方法１：２引数関数を新たに導入する



方法２：直積型を導入する



*: (int, int) → int
*(2,3) ⇒ 6
*: （int × int) → int
*(<2,3>) ⇒ 6
方法３：高階関数を使う（Currying)



*: int → (int → int)
*(2)(3) ⇒ 6
ここでは、方法３を採用、*(2)(3) を *(2,3) と書くこともある
ミニ言語

型定数


int (整数）、bool (真理値）
定数とその型

==: int の引数を２つもらってboolを返す関数



if: bool型の値１つと int型の値２つをもらってint型の値を
返す関数


if: bool→(int→(int→int))
そのほか


==: int→(int→bool)
=と紛らわしいので以下では eq と表記する
*: int→(int→int), -: int→(int→int), 0:int, 1:int
これで全てだろうか？
ミニ言語


まだ＝を定式化していない
定式化１


＝：ある型Aをもつ値２つをもらって、なにか（？）を返す関数
定式化２



＝：定義の導入
factを定義したいのだが、右辺にも出てくるので定義になって
いない
再帰呼び出しを表す定数を導入する
ミニ言語

R はなんだろうか？



Recursor (再帰呼出しを生成するもの）
型は (関数→関数)→関数という形をしている
計算規則： RM ⇒ M(RM)



すなわち
f = M f という形の｢方程式｣の解 f が RM である
一般には、R: （（A→A)→(A→A))→（A→A) という型をもつものを
recursor とよぶ。上記のRは一般的なrecursorの一例
上のようにすると = は単なる定義(右辺のプログラムに名前をつ
けているだけ）なので、＝の型付けを考える必要はない

右辺に型がつけば、それでおしまい
ミニ言語のまとめ

ミニ言語：型付きラムダ計算の体系で、型定
数、定数を以下のように定めたもの

型定数


int、bool
定数とその型





A→B→C は、
A→(B→C)のこと
eq: int→int→bool
if: bool→int→int→int
*: int→int→int, -: int→int→int
0:int, 1:int
R: ((int→int)→（int→int))→（int→int)
階乗プログラムの型付け

どのようにしたら、このプログラムの型が整合的かどう
か判定できるか？また、このプログラム(全体)の型は
何であるか？

top-down approach



プログラム全体から部分を見ていく
型推論図を、下から上へ作っていく
bottom-up approach

top-downの逆
その他の例
自由変数がある例
Church流でも、いきなり難しくなる
Curry流と同等な難しさ
休憩
再開後は、型推論アルゴリズム
について
型推論の準備

問題：１つのMに対してΓ|- M:A が成立するΓ、
Aが多数（しかも無限に多く）存在する可能性
があるため、これらをどう表現すればよい
か？
f(ｘ)というプログラムは
 f: int→int, x:int でも、
 f:bool→int, x:bool でも型がつく

型推論の準備

問題に対する答え：｢最も一般的な型付け」が
一意的に存在することが知られている
[Principal Typing Theorem]

f(x) は




f: A→B
x: A
f(x): B
という型付けがもっとも一般的
型変数、代入

型変数





型は、型定数と→から構成されていた。
型推論を行うため、「型をあらわす変数｣が必要になる。
ここでは、α、β 等を使う(以後では、型定数には K1, K2, ..を使う）
以下では、型といえば、型変数を含んでもよいものとする。一般的な型を
A,B,C 等であらわす
型に対する代入






[A/α, B/β, ...] の形のもの
意味としては、型変数αに型Aを代入する、等を同時に行った代入を表す
型の世界は、項の世界と違ってλがないので、代入は単純に定義できる
K [A/α,...] = K
α[A/α...] = A
(B→C)[A/α...] = （B[A/α,...]) (C[A/α,...])
単一化 (unification)

2つの型A,Bに対して、


Aτ = Bτ となる最も一般的な代入(mgu)を見つけ
るアルゴリズム
型推論問題の再定式化

Γ|- Ｍ：Ａとなる、Γ,A (型変数をふくんでいるか
もしれない）のうち、代入に関してもっとも一般的
なものを見つける
次回
単一化アルゴリズム
 型推論アルゴリズム
 簡単なレポート出題

訂正

型推論規則におけるΓ-{xA} という表記につ
いて
型推論規則の説明ではすっとばしてしまったが、
きちんと型推論するためには、以下の条件が必
要。
 Γに、xB という要素が含まれているとき（ＡとＢは
異なる型）、Γー{xA}は定義されない、と定める。
 また、同じΓの中に同時に、xA, xB （AとBは異な
る）という２つの要素はふくまれないとする。
int
bool}は文脈ではない
 たとえば、｛x , x
 Ｃｕｒｒｙ流の文脈でも同様の条件が必要


Download Report