計算モデルとアルゴリズム

計算モデル特論
MLの型推論
国立情報学研究所ソフトウェア研究系助教授／
科学技術振興事業団さきがけ研究21 研究員
佐藤一郎
E-mail: [email protected]
Ichiro Satoh
型付き言語の欠点


プログラムにおいて重要な型だけでなく、型を持つすべて
の式に型を記述する必要がある
Lispの関数のように、一つの関数を様々なデータに対し
て用いたい場合がある
Ichiro Satoh
例：型付き言語の欠点
階乗を計算するプログラム
f(x) := if x==0 then 1 then else x * f(x-1)
ここで x を int 型とするとき、プログラムを見ると下記がわかる
 x は int型
 f は int→int型
 x==0 は bool型
 * は int×int→int型
 - は int×int→int型
 if-then-else は bool×int×int→int型
Ichiro Satoh
例：型付き言語の欠点
Lispの関数mapcar(f, L)は、リストLの各要素に関数fを適用する
mapcar(odd, [3,4]) は
(int→bool)→(list(int)→list(bool))
Principe Type: (a→b)→(list(a)→list(b))
関数twice(f, x)は関数fにxを2回適用する
twice(inc 3) は (int→int)→(int→int)
Principe Type: (a→a)→(a→a)
Ichiro Satoh
Principle Type
主型（主たる型）
ある式に対する最も一般的な型付けをその式の主型と呼ぶ
例： lx.ly.x の型はたくさんの型をもつがその形はどれも
a→b
→ a である。よってlx.ly.x の主型はa → b → a
Ichiro Satoh
言語ML
ML式
e ::= x | n | true | false | lx.e | e1 e2 |
let x = e1 in e2 | fix x.e | if e1 then e2 else e3
型
 ::= a | int | bool | 1→2
aは型変数
Ichiro Satoh
プログラミング言語意味論
公理的意味論（Axiom Semantics）
 プログラムの動作毎に作用を定式化
表示意味論（Denotational Semantics）
 代数的構造にプログラムの表現（表示）を写像
操作的意味論（Operational Semantics）
 プログラムの動作を定式化
Ichiro Satoh
言語MLの操作的意味論
推論式による意味定義
├e  v [v / x├
] e'  v '
├ let x  e in e'  v
├b  true ├e  v1
├ if b then e1 else e2  v1
├b  false ├e  v2
├ if b then e1 else e2  v2
Ichiro Satoh
型推論規則
型推論規則
├e1 : bool ├e2 :  2 ├e3 :  3
├n : int
├if e1 then e2 else e3 :  3
├true : bool
, x : ├e : 
├false: bool
├fix x.e : 
├x :  (( x)   ,   )
  {x :  1├
} e : 2
├e1 :  1   2 ├e2 :  1 ├lx :  .e :   
1
1
2
├e1e2 :  2

├e1 :  1 {x : a . 1├
} e2 :  2
├let x  e1 in e2 :  2
Ichiro Satoh
let定義
(lx.e1)e2 は let x=e2 in e1に相当
型変数への型の代入（型の具体化）においてλ抽象とlet定義は相違
 λ抽象の場合はそのλ式の本体に現れるλ変数の型はすべて同一の
具体化を行う
 let定義の場合は関数適用ごとに別々に型付けが行える

 a . 1とは 1 に出現する自由な型変数のうち、前提Γの中に出現す
るものを省いたa1,...,anをすべて全称限量化すること
Ichiro Satoh
総称型
Generic type variable
型変数への型の代入（型の具体化）においてλ抽象とlet定義は相違
 λ抽象の場合はそのλ式の本体に現れるλ変数の型はすべて同一の
具体化を行う
 let定義の場合は関数適用ごとに別々に型付けが行える
 基本データ型
整数、浮動小数点、文字、真偽値
 構造データ型
配列、直積型、直和型、レコード型、ストラクチャ型
ユーザ定義型
Ichiro Satoh
型付プログラミング言語
プログラミング言語と型
 型なしプログラミング言語
○プロトタイピング、×インタープリタ実行
 弱い型付プログラミング言語
○手っ取り早く設計・記述、×信頼性が低い
 強い型付プログラミング言語
○安全なプログラム、×慎重な設計と冗長な記述
型検査
 静的検査
 動的検査
Ichiro Satoh
型推論
強い型付プログラミング言語を利用しながら簡潔な記述を実現するには
型は文面から推定可能
例： f(x) = if x == 0 then 1 else x * f(x-1)


推定により冗長な記述を現象
形式的な体型により型を厳密に決定
Ichiro Satoh
型推論の例
式要素の型と式全体の型
例： 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型
結論
Ichiro Satoh
型付ラムダ計算
型理論体系
 項（term）
 型（type）
 判定（judgment）
 推論規則（inference）
Ichiro Satoh
型付ラムダ式（基本）
BNF文法による型
τ ::=
b | (τ→τ)
ここで b は基底型、 τ×・・・×τは組、 τ→τは関数
BNF文法による型付ラムダ式
M ::=
cτ | x | (λx:τ.M) | (M1 M2)
Ichiro Satoh
型付ラムダ式
BNF文法による型



基本型:
直積型：
関数型：
b
(τ×・・・×τ)
(τ→τ)
括弧の省略
型における矢印は右結合
例:
(1→(2 →(3 →4) = 1→2 →3 →4
Ichiro Satoh
型付ラムダ式の直感的意味
基本式：
(M1 M2)
関数M1に引数M2を与えたときの値
(λx:τ.M)
型がτである仮引数 x をもつ、関数本体をMと定義される関数
Ichiro Satoh
型付きラムダ式の例

f(x)=x+1なる関数fは
lx:int.x+1

fに実引数3を与えた式f(3)は
(lx:int.x+1)(3int)
Ichiro Satoh
自由変数
ラムダ式Mに含まれる自由変数の集合FV(M)
FV(c) = 0
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)
自由変数でない変数を束縛変数と呼ぶ
Ichiro Satoh
型付ラムダの計算
簡約規則
[N/x]c = c
[N/x](M1,...,Mn) = ([N/x]M1,...,[N/x]Mn)
[N/x](M.i) = ([N/x]M).I
(lx:.M)=(ly:.[y/x]M)
((lx:.M) N:) → [N/x]M
Ichiro Satoh
記法
前提（assumption）：
e:t
ある式eが型tを持つこと
判定（judgement）:
A ├ e:t
（０個以上の）前提A（型環境）から、ある式eが型tを持つことが示される
推論（inference）：
A1├ M1:1 ・・・・・ An├ Mn:n
A├ M:
式Miがそれぞれの前提Aiにおいて型を持つならば、結論が示される
Ichiro Satoh
型推論規則の記法
前提への操作と表記
{x:}
前提に x: を追加、ただし、 に変数xに関する勝たし体があった場合
は、もっとも右側を優先する
(x)=
前提のもとで、定数あるいは変数xが型を持つことをあわす。
Ichiro Satoh
型推論規則（詳細）
型推論規則
(const)
 ├ c : 
(var)
├x : 
(abs)
  {x :  1├
} M : 2
├lx :  1.M :  1   2
( ( x )   )
関数lx:1.Mが関数型1→2を持つ
のは、仮引数の型1と仮定したとき、
関数Mが型2をもつときである。
Ichiro Satoh
型推論規則（詳細）
型推論規則
(app)
├M 1 :  1   2 ├M 2 :  1
├M 1M 2 :  2
関数は、関数がその定められた値
にのみ適用可能であり、その結果
は関数の値の型を持つこと
(prod)
├M 1 :  1  ├M n :  n
├ ( M 1 ,  , M n ) :  1     n
関数の組(M1,...,M2)はM1,...,M2の
直積となる
(proj)
├M :  1   n
(1  i  n)
├M .i :  i
関数の組(M1,...,M2)からI番目の
要素を取り出したときはM1の型
となる
Ichiro Satoh
型推論の例
型推論では推論規則により変形していく
型付ラムダ式 K=lx.(ly.x)
{x :  1├
} x :1
{x :  1├
} ly :  2 .x :  2   1
├lx :  1.(ly :  2 .x) :  1  ( 2   1 )
Ichiro Satoh
型推論の性質



健全性
型推論できるならば、その結果が正しい（型安全）ことを意味する
完全性
正しいことはすべての型において推論することができる
有用性
決定可能かつ効率がよいこと
Ichiro Satoh
多相型
プログラム中に現れる同一の式やデータが複数の型をもつこと
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
Ichiro Satoh

Download Report