正誤表

第1刷(第2刷で修正済)
  • 定理15.3.5 の証明(p. 148)の「T-Subの場合」における結論の「Γ ⊢ t : T」は、正しくは「Γ ⊢ t' : T」です(原著の該当箇所も同様)。 @ksknac さん、ご指摘ありがとうございました。
第2刷(第3刷で修正済)
  • 5.2 節、p. 46 の「この関数に第一引数としてmを渡し」は、正しくは「mに、第一引数としてこの関数を渡し」でした。
  • 18.11 節、p.186 の下から4行目「110ページ図 11-12 の E-Fix」は、正しくは「110ページ図 11-12 の E-FixBeta」です。田中さん、ご指摘ありがとうございました。
  • 演習21.3.4 (p. 225)の「μSfによって関連付けられているが、vSfによって関連付けられない」は、正しくは「vSfによって関連付けられているが、μSfによって関連付けられない」です。 甲斐宏味さん、ご指摘ありがとうございました。
  • 定理21.8.7の証明 (p. 238) で、「Sについて整合的である集合Q∈T✕T」は「Sについて整合的である集合Q⊆T✕T」が正しいです。
  • 21.11 節の(S-AMBER)規則(p.245)の直後「仮定(assumption)の集合Σ の下でμX.S がμY.Tであることを示すには」は、正しくは「仮定(assumption)の集合Σ の下でμX.S がμY.Tの部分型であることを示すには」です。 Shota Kawabuchi さん、ご指摘ありがとうございました。
  • 定義22.4.1 (p. 256) などで σ' = γ⚪σ などと書かれていますが、型代入に対する = の定義が不明確でした。一般に、任意の型Tに対してσ(T) = σ'(T)となるとき、σ=σ'と書くものとしています。(定義域も含めた有限写像としての = ではありません。)
  • 解答3.5.17 の命題 A.9 (p. 394) の証明は、t = succ t_1の場合、tの評価とt_1の評価が同じステップ数になるため、帰納法の仮定を適用できないという問題がありました。第3章の対象言語に限ればtの構造に関する帰納法で証明できますが、より一般的な対象言語では「t→t'かつt'⇓vならば、t⇓v」のような別の補題をt→t'の導出に関する帰納法で示す等が必要になります。
  • 解答17.3.1 (p. 417) のallFieldsの定義が誤っています(詳しくは報告を参照)。@ksknac さん、ご指摘ありがとうございました。
  • 23.6 節 (p. 278) の「これは型適用の引数を(部分的に)消去し、それ以外の型注釈をすべて残す。」は「これは型適用の引数とラムダ抽象の型注釈を(部分的に)消去する。」が正しいです。
  • 解答23.4.9 (p. 433) で pairNat の第一引数と第二引数が、問題文にかかれているヒントと逆になっていました。
Comments