正誤表

p.12, 脚注4:
- 誤）関わったことで知らせる
- 正）関わったことで知られる
p.17, 練習問題 1.7 (2):
- 行末の閉じ括弧を削除
p.42, 練習問題 2.5:
- 誤) 定義2.4
- 正) 定義2.35
p. 43，定理2.36
- 誤) がならば
- 正) ならば
p. 45，原理2.38(CompareNat1 における判断 n₁ is less than n₂ の導出に関する帰納法(バージョン2))
- 誤) 「任意のペアノ自然数 n₁, n₂ に対して，P(n₁,n₂)」
- 正) 「任意のペアノ自然数 n₁, n₂ に対して，n₁ is less than n₂ ならば P(n₁,n₂)」
p. 46 の原理2.39, 2.40 も同様．
p. 52，定義3.1の2行目:
- 誤) Exp
- 正) Value
p. 64，練習問題3.6の最下行:
- 誤) のように
- 正) ように
p. 63, l.-10: 「ε」を太字体にする．
p. 63, l.-8:
- 誤) e₂ evalto vの評価
- 正) e₂ の評価
p. 73, 中段の導出の evalto (下向き矢印)の後，二箇所とも:
- 誤) 2
- 正) 1
p.77, l.13
- 誤) 記述されてよう
- 正) 記述されよう
p. 89，原理5.1
- 誤) 「任意の環境 E, 式 e, 値 v に対して，P(E, e, v)」
- 正) 「任意の環境 E, 式 e, 値 v に対して，E┣e evalto v ならば P(E, e, v)」
p. 90, 定理 5.2
- 誤) ML2
- 正) ML3
p. 91, (m): 証明が不十分でした．導出 D については，書かれている E-App で終わる場合だけでなく， E-AppRec で終わる可能性を検討しなければなりません．ただし，後者の場合はありえない(矛盾が導ける)ことが
1. E-AppRec から v'₁が再帰関数閉包である．
2. 帰納法の仮定からは v'₁ ≡ v₁，すなわち(再帰でない)関数閉包である
の二点からわかります．
p. 92, 導出 D, D' 中に現れる規則名:
- 誤) E-App
- 正) E-AppRec
p.110，関数 length の定義:
- 誤) x'
- 正) xs
p.130, 規則 E-IfErr3の結論:
- 誤) v
- 正) error
p.137, 下から5行目:
- 誤) e₂ : τ
- 正) e₁ : bool
p.150, 練習問題9.1(9)の3行目
- 誤) l1
- 正) l
p.153, 10行目:
- 誤) τ
- 正) Sτ
p.154，定義9.4の一行目:
- 誤) σ
- 正) τ
p.160, 10.3節1行目:
- 誤) アリゴリズム
- 正) アルゴリズム
p.164, 定義 10.2:
- 誤) τ_n/α_n
- 正) τ_m/α_m
p.168, 10.6節1行目:
- 誤) アリゴリズム
- 正) アルゴリズム
p.168, 練習問題10.4: TypingML5 は教科書中で言及されていない導出システムでした．意図としては第7章の ML5 に対する型システム，ということですので，それを定義した上で，型推論を考えてみてください．
p.170, l.5:
- 誤) アリゴリズム
- 正) アルゴリズム
p.170, l.7:
- 誤) α₂
- 正) α_n

Updated on $Date:: 2018-08-22 16:54:58 +0900#$