Benjamin C. Pierce "Types and Programming Languages" の日本語版サポートサイトです。

ご質問・議論

書籍『型システム入門』（TAPL日本語版）の技術的内容や、型システム全般に関する、日本語での質問と議論は GitHub issues にお願いします（2023年9月以前の議論は Google グループ "taplkatasystem" を参照）。

正誤表

第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 の第一引数と第二引数が、問題文にかかれているヒントと逆になっていました。

第3刷（第4刷で修正済）

• 22章の最後の文: 「どちらの証明も(無制限の)半単一化問題の非決定性 (…) に依存している。」は、正しくは「決定不能性」です。

リンク

• オーム社の公式ページ（第1章がサンプルとしてダウンロードできます）
• 原著のサポートページ