TaPLを買ったので、誤解があった場合に指摘を受けたりできるように、読書ノートを公開します。 暇な人は間違いを見つけたら教えて下さい。
(このノートの目的上、自信が無いことも言っているので、このノートに書いてあることはあまり信じないように)
###序文
必要な背景知識
"本書はプログラミング言語理論の予備知識は前提としないが、読者は数学、特に離散数学、アルゴリズム、初等的な論理学に関する、学部レベルの論理的に正確な授業の内容に、ある程度習熟している必要がある。 読者は少なくとも一つの高階関数型プログラミング言語（Scheme、ML、Haskellなど）と、プログラミング言語およびコンパイラの基礎的な概念（抽象構文、BNF文法、評価、抽象機械など）に慣れている必要がある。" (p.ix)
離散数学・アルゴリズム・と「プログラミング言語およびコンパイラの基礎的な概念」とがちょっと心配ですが、頑張ります。
###第1章 はじめに
実行時型エラー(runtime type error)が難しい
"与えられた言語において型システムによって除去できる不正な振る舞いのことをしばしば実行時型エラーと呼ぶ。……各型システムの安全性（あるいは健全性）は、それぞれの実行時エラーの定義に照らし合わせて判断されねばならない。" (p.2)
動的型付き言語でのような実行時に起きる型エラー表示のことではないんですね。 できるというからには、(仕様通りなら?)実際に起こるものではないんですかね。 それとも、型システムを理想通りにすれば…ということですかね? その場合、依存型で扱えるなら配列の不正インデックスアクセスは実行時型エラー?
###第2章 数学的準備
####p.13の演習3つ (番号は節ごと。定義・定理・演習・などの環境ごとではなく一律)
演習2.2.6. R'= R ∪ {(s, s) | s ∈ S}がRの反射的閉包(Rを部分とする最小の反射的関係)であることの証明。
Rと{(s, s) | s ∈ S}との合併とは、Rと{(s, s) | s ∈ S}とをともに部分とする集合の中で、最小なもののことであり、反射性はまさに{(s, s) | s ∈ S}を部分とすることだから、R'はそのような関係の中で最小。 証明終わり。□
演習2.2.7. R[0] = R; R[i+1] = R[i] ∪ {(s, u) | ∃t. (s, t) ∈ R[i] & (t, u) ∈ R[i]}とする。R^{+}=∪[i ∈ ℕ] R[i](\bigcup記法のつもり)はRの推移閉包(関係Rを部分とする最小の推移的関係)であることの証明。
R⊆R^{+}は明らか。
(推移性) (x, y) ∈ R^{+}そして (y, z) ∈ R^{+}とする。 R^{+}のどんな要素についても、xを十分に大きく取れば、それはR[x]の要素でもあるから、どんなiについても、jを十分大きく取れば、(x,y)∈R[i]&(y,z)∈R[i]ならば、(x, z)∈R[j]であることを示せばよい((x,z)∈R^{+}となる)が、R[x+1]の定義から、i+1がそのようなjである。
(最小性) R'を、Rを部分とする推移的関係とする。 (x, y)∈R^{+}とする。 ∪[i ∈ ℕ]R[i]は任意のiについてR[i]を部分とする最小の関係だから、R'も任意のiについてR[i]を部分とすることを示せば、R^{+}⊆R'が分かる。 iに関する帰納法で示す。 i=0の場合、すでにRを部分とすると仮定したから、満たされる。 iについて示されたとして、R[i+1] ⊆ R'を示そう。 (x, y)∈R[i+1]なら、(x, y)∈R[i]か、(x, y)∈{(s, u) | ∃t. (s, t) ∈ R[i] & (t, u) ∈ R[i]}かに限るが、帰納法の仮定により第1の場合は(x, y)∈R'であり、R'の推移性により第2の場合もtの存在と帰納法の仮定から(x, y)∈R'。 したがって、R[i+1]⊆R'。 R'は任意だから、最小性が示された。
証明終わり。□
演習 2.2.8 Rを関係、PをRに対して保存的な述語として、PがR^{*}(Rの反射推移閉包)に対しても保存されることの証明
(x, y) ∈ R^{*} & P(x)とする。 反射推移閉包だから、
- (x, y)∈Rか、
- x=yか、
- (演習2.2.7の定義を流用すれば)何らかのiについて(x, y)∈R[i] が成り立つか、
のいずれかが成り立つ。 場合分けで、P(y)を示す。
第1の場合は、すでにRのPに対する保存性を仮定してるから、P(y)。
第2の場合は、自明にP(y)。
第3の場合については、iに関する帰納法でiが何であっても(x, y)∈R[i] ⇒ P(y)なことを示す。 i=0の場合は明らかなので、iについて示されたと仮定して、i+1について示そう。 (x, y)∈R[i+1]ならば、(x, y)∈R[i]か、何らかのzについて(x, z)∈R[i] & (z, y)∈R[i]かだが、前者は帰納法の仮定からP(y)が分かるので、後者について考える。 帰納法の仮定と(x, z)∈R[i]から、P(z)。 それにふたたび帰納法の仮定を適用すれば、P(y)が示された。 (これでzが何であってもP(y)なことが分かった)
x, yは任意だから、証明終わり。□
###第3章 型なし算術式
- ここでは、BNFがメタ言語、BNFの変数がメタ変数で、BNFによって記述している言語(形無し算術式)が、対象言語ですね (p. 17)
- メタ変数って対象言語の変数を表すメタ言語の変数のこと限定なのか、単にメタ言語の変数ならメタ変数なのか分からなくなってたけど、後者が正しい
###第6章 内から外へインデックスを振るのが、de Brujin インデックス(外から内へはde Brujinレベル)
##第二部 単純型システム ###第8章
"†3 我々がこれから考えるほとんどの型システムでは、評価は正しく型付けできるかどうかだけを保存するのではなく、その項の型自体も 保存する。しかし、型が評価の過程で変わりうる型システムもある。例えば部分型付けを持つ体系（第 15 章）では、型は評価の過程 でより小さくなる（多くの情報を持つようになる）ことがある。" (p. 72)
###第9章 演習 9.3.2. Γ |- x x : T となるような文脈Γと型Tはあるか。例か反駁を与える。
以下のような観察をいくつかやると存在しないと推測できる
Prelude> :t (\x -> x x)id
<interactive>:1:10:
Occurs check: cannot construct the infinite type: a ~ a -> a
Relevant bindings include x :: a -> a (bound at <interactive>:1:3)
In the first argument of ‘x’, namely ‘x’
In the expression: x x証明 単純型付きラムダ計算における型とは、
-
- 基本型
- n+1.n以前の型と型との間の関数型
なる型の族 Ts : ℕ → Types の和として考えられるから、帰納法が使える。