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

計算モデル特論
型付ラムダ計算
国立情報学研究所ソフトウェア研究系助教授／
科学技術振興事業団さきがけ研究21 研究員
佐藤一郎
E-mail: [email protected]
Ichiro Satoh
型とは
プログラミングにおけるデータ型
Pascal:
var x,y: integer, a:real
Ichiro Satoh
型の必要性






プログラム設計を明確化
プログラムの誤り防止
関数やモジュールの仕様
コンパイラ最適化への補助情報
プログラム停止性への補助保証
可読性の向上
Ichiro Satoh
プログラミング言語の型
基本データ型
整数、浮動小数点、文字、真偽値
 構造データ型
配列、直積型、直和型、レコード型、ストラクチャ型
ユーザ定義型

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
型付ラムダ式
型
τ ::=
b | (τ×・・・×τ) | (τ→τ)
ここで b は基底型、 τ×・・・×τは組、 τ→τは関数
型付ラムダ式
M ::=
|
cτ | x | (λx:τ.M) | (M1 M2)
(M1 ,...,M2) | M.i
Ichiro Satoh
型付ラムダ式
BNF文法による型



基本型:
直積型：
関数型：
b
(τ×・・・×τ)
(τ→τ)
括弧の省略
型における矢印は右結合
例:
(t1→(t2 →(t3 →t4) = t1→t2 →t3 →t4
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:t.M)=(ly:t.[y/x]M)
((lx:t.M) N:t) → [N/x]M
Ichiro Satoh
記法
前提（assumption）：
e:t
ある式eが型tを持つこと
判定（judgement）:
A ├ e:t
（０個以上の）前提A（型環境）から、ある式eが型tを持つことが示される
推論（inference）：
A1├ M1:t1 ・・・・・ An├ Mn:tn
A├ M:t
式Miがそれぞれの前提Aiにおいて型tを持つならば、結論が示される
Ichiro Satoh
型推論規則
型推論規則
(app)
(const)
 ├ ct : t
├M 1 : t 1  t 2 ├M 2 : t 1
├M 1M 2 : t 2
(prod)
(var)
├x : t
(abs)
( ( x )  t )
  {x : t 1├
} M :t 2
├lx : t 1.M : t 1  t 2
├M 1 : t 1  ├M n : t n
├ ( M 1 ,  , M n ) : t 1    t n
(proj)
├M : t 1  t n
(1  i  n)
├M .i : t i
Ichiro Satoh
型推論規則の記法
前提への操作と表記
{x:t}
前提に x:t を追加、ただし、 に変数xに関する勝たし体があった場合
は、もっとも右側を優先する
(x)=t
前提のもとで、定数あるいは変数xが型tを持つことをあわす。
Ichiro Satoh
型推論規則（詳細）
型推論規則
(const)
 ├ ct : t
(var)
├x : t
(abs)
  {x : t 1├
} M :t 2
├lx : t 1.M : t 1  t 2
( ( x )  t )
関数lx:t1.Mが関数型t1→t2を持つ
のは、仮引数の型t1と仮定したとき、
関数Mが型t2をもつときである。
Ichiro Satoh
型推論規則（詳細）
型推論規則
(app)
├M 1 : t 1  t 2 ├M 2 : t 1
├M 1M 2 : t 2
関数は、関数がその定められた値
にのみ適用可能であり、その結果
は関数の値の型を持つこと
(prod)
├M 1 : t 1  ├M n : t n
├ ( M 1 ,  , M n ) : t 1    t n
関数の組(M1,...,M2)はM1,...,M2の
直積となる
(proj)
├M : t 1  t n
(1  i  n)
├M .i : t i
関数の組(M1,...,M2)からI番目の
要素を取り出したときはM1の型
となる
Ichiro Satoh
型推論の例
型推論では推論規則により変形していく
型付ラムダ式 K=lx.(ly.x)
{x : t 1├
} x :t1
{x : t 1├
} ly : t 2 .x : t 2  t 1
├lx : t 1.(ly : t 2 .x) : t 1  (t 2  t 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