TAPLを読む会(~7章)
2章 数学的準備
用語の定義、もしくは集合とか関係とか列とかについて。二項関係について慣れていれば大丈夫そう。
3章 型無し算術式
boolっぽいやつとnatっぽいやつだけからなる言語を例にとって、今後の概念について説明する。
3.1
対象言語とかメタ言語とか項,式,値とかについて。
3.2
帰納的な項の定義,推論規則による項の定義(証明木みたいな感じ),を定義する。この時点では型とかは考えていないので意味的にやばい式も項となりうる。そしてこれらの等価性を示す。
3.3
項の(深さ|サイズ|構造)についての帰納法についての説明と、その正当性について。これから沢山出てきます。
3.4
(操作的|表示的|公理的)意味論について紹介しているのだけれど正直それらの違いがよく分からない。
3.5
この節から本編。
B
まず、{true,false,if_then_else} のみからなる言語を例に取って説明している。
構文 「項」と「値」に対応するメタ変数と、それらが何であるかが再帰的に定義されている。これによって
評価 項がどう評価(簡約)されていくかを示す。最終的に同じ項に評価されるものでも、評価戦略はいろいろあったりする。
将来、型を表すメタ変数や型付け規則が追加されたりするが、この時点ではまだ型はない。
この節における「定義」は後々においても使われるが、「定理」は今見ている言語についてのものであり一般的ではない(まあしかし大抵は後の言語でも満たされる性質ばかりであるが)
評価が行き詰まらず、全ての項の正規形が値であることは型付けの一つの目標である。(評価が有限回で停止することも可能ならば目指したいが、その場合は計算能力を犠牲にすることになる)
この言語では、
- 評価は決定的に行われる
- 値 ⇔ 正規形
- 正規形は一意
- 評価が有限回で停止する(強正規化性的な)
が成り立つ。
B + N
数値が入ってくる。この体系でも「評価は決定的に行われる」が、正規形だが値でないもの(行き詰り状態)が発生する。(errorなものを全てwrongに簡約していくのはHaskellのNothingっぽい)
後、小ステップスタイルと大ステップスタイルについて。この本は全体的に小ステップで評価規則を定めている。 (小ステップは証明木に似ていて、大ステップはシークエント計算に似ているなと思った)
4章 算術式のML実装
やってねぇ…
5章 型無しラムダ計算
みんな大好き型無しλ計算。
5.1
基礎。
とか。評価戦略は型システムにはあまり関係ないのでさらっと。この本では値呼びでいく。
5.2
λ計算でひととおり遊ぶ。多分誰しもやったことがあるはず。 まず、 bool -> pair -> nat -> add,sub,mul くらいまで定義する。
計算体系の拡張
プリミティブとしてnat,boolを加えて、それらの間の相互変換をする話。2つのλ式が等価であるかは決定不能だった(はず)なので、λ式→数字変換関数があると便利。
再帰
不動点、fixのはなし。この本ではfixとしてZコンビネータを示している。(値呼び評価なので)
5.3
3.4でやったように、型無しλ計算の体系の性質を示したりする。が深入りはしない。 構文、代入(β簡約)における変数名についての諸注意、値呼びを実現するための評価戦略について。
6章 項の名無し表現
de Bruijn インデックスについて。型理論をやるにあたっては必要ないが、実際に実装するときに大いに参考になる。(僕のpythonでの実装はこれを参考にした)
7章 ラムダ計算のML実装
やってねぇ…
