CoPL
2011/7/1
五十嵐淳 著
>第1部 導出システム入門
第１章 自然数の加算・乗算・比較
第２章 メタ定理と帰納法による証明
>第2部 ＭＬの操作的意味論
第３章 整数・真偽値式の評価
第４章 定義，変数束縛と環境
第５章 関数と再帰
第６章 静的有効範囲と名前無し表現
第７章 リストとパターンマッチング
>第3部 ＭＬの型システム
第８章 単純型システム
第9章 多相的型シスデム
p.145の下の方のツリーは、左上のy:'a\vdash y:'aの部分が良くないって意味だよな？
型安全性定理とその証明
最後の方わからなかったので再読したい
第10章 型推論
>#WIP
1章
算術式
ペアノ自然数と
+ や * を使って構成される式 + : P-Zero, P-Succ * : T-Zero, T-SuccT-Succが若干ややこしい
例としてn1=4, n2=3, n3=12, n4=15とか
算術式の計算
評価
式にその計算結果を与えるもの
式そのものは形式のみで、内容があっているとは限らないが、評価は内容的に正しいかも判断する
EvalNatExp
3項の式は左からまとめないといけない説がある(q.17)
e1 + e2 + e3 => (e1 + e2) + e3
簡約
式に対して、その計算を一歩進めて計算の途中経過とも考えられる単純化した別の式を与えるもの
形は違えど両辺は同じ意味を表す
1 + 5 ---> 2 + 3的な
操作的意味論
---> , -*-> e はexpression(式)決定的な簡約
-d-> + や * の左側が値になるまで簡約した結果のものになる + や * の左側から計算していく導出システムの「出来」を考察した理論のことを、メタ理論と呼ぶ
3章
OCamlのlet
静的有効範囲を持つ
inの中のみがscope(?)
let 変数名 = 式1 in 式2 変数(=式1)が生きているスコープは式2の中のみ
OCamlの関数
fun 変数 -> 式 関数閉包
E-Fun
「fun式を評価した結果」が「評価時の環境を含む関数閉包」になる
closure
関数の式に関する情報とパラメータ以外の変数の値を組にしたもの
(ε)[fun x → e] 8章
本章で示された規則が型安全性であることの具体的な証明法など
10章
型推論は大まかには以下の2つの操作
式と型環境から、型に関する方程式を立てる
型に関する方程式を解く
式と型環境から、型に関する方程式を立てる
pp.160-163
Extract :: (型環境Γ, 項e) -> ([方程式E], 型τ) 式を一周して方程式を積み上げていく感じ
型に関する方程式を解く
pp.164-167
Extractで作った方程式たちから解を求める
Unify :: [方程式E] -> [最汎単一化子τ] pp166-167のこの関数の説明はめちゃくちゃわかりやすい
CoPLでの型推論の作業は上2つが完全に2分されてる
全部の方程式を作ってから(Extract)→すべての方程式の解を求める(Unify)
p.167下のプログラムがそれを如実にあらわしている
mlPT(Γ, e) = let (E, τ) = Extract(Γ, e) in
let S = Unify(E) in
(S, Sτ) 型推論関数
PT :: (型環境Γ, 項e) -> (型代入S, 型Sτ) HaskellでTypeInferを作るでは、同時にやっている
同時にやるものについても少し触れられている pp.165-166