8章 型付け関係 NBに対して型をつけてみる。 型付け関係の逆転(逆転補題)(生成補題) 項を型付けるためのアルゴリズムを与える。(部分型とかが入ってくるとこれが大変になる…かな？) 進行性 項が正しく型付けられているなら、正規形->値(標準形)が成り立つ。 …

2章 数学的準備 用語の定義、もしくは集合とか関係とか列とかについて。二項関係について慣れていれば大丈夫そう。 3章 型無し算術式 boolっぽいやつとnatっぽいやつだけからなる言語を例にとって、今後の概念について説明する。 3.1 対象言語とかメタ言語と…