型システムを勉強するための1stステップとして、「プログラミング言語の基礎概念」の第１章を読み終えた話

要約

作者:五十嵐淳
サイエンス社

を読んでいます。
第1章だけでも「自然数の加算・乗算・比較の導出システム入門」という構成でしたが、想像よりずっとハイカロリーでした。
ただ、とても楽しい。
演習システムを使って練習までできるのも理解が深まって非常に良いです。

第1章を読み終えた記録として残すとともに、手元の演習に集中しすぎて視点が近視眼的になっていたので、整理も兼ねて頭から読み返すつもりで記事化しました。

背景

第2子が産まれ、ありがたいことに育児休暇を取得させていただいています。妻の体調・体力がまだ戻りきっておらず、昼夜逆転気味の新生児の夜のお世話を担当することになり、21:00〜翌 9:00 までは比較的まとまった時間を確保できる状態になりました。

せっかくならこの時間を活かそうと思い、積読の中でも腰の重かった本を読むことにしました。テーマとしては、第2子の出産待ち時間に ChatGPT と壁打ちしながら興味が高まっていた「関数型プログラミングの背景」「型システム」を深掘りしたいと考え、TaPL（型システム入門）を読もうとしました。

……が、まったく歯が立たず、基礎からやり直そうと思い、「プログラミング言語の基礎概念」にたどり着きました。

紹介元も以下の通りです。

筑波大学・プログラミング論理研究室で「最初に読むべき文献」に記載
www.logic.cs.tsukuba.ac.jp

エンジニア界隈でも有名な「きしだのはてな」にて紹介（2011年の記事）
nowokay.hatenablog.com

第1章について

「自然数の加算・乗算・比較」の導出システムに関する章でした。

プログラミング言語の意味論や型システムを記述するための枠組みとして、導出システムを用い、説明と演習問題を進めていく構成です。

導出システムは、数理論理学で形式的証明を記述するために用いられる自然演算やシーケント計算といった体系を一般化した汎用的な枠組みであり、論理式、プログラム、型などといった議論の対象に対する様々な判断を推論規則に従って導く、導出するための記述体系である。
具体的な導出システムは、判断の形式とそれに対する推論規則群を与えることによって定めることができる。「プログラミング言語の基礎概念」 P2

書籍ではペアノ自然数を題材に、導出システムを定義し、それに従って導出木（推論木）を組み立てていきます。

加算・乗算の推論規則は以下のようなものです（本を持っていない方には伝わりづらいと思いますが……）。

上記の推論規則を使って、例えば以下の問題の導出木を導く感じです。
S(S(S(Z))) plus S(S(Z)) is S(S(S(S(S(Z)))))

これは単に
3 + 2 = 5
を推論規則を使って証明する、というイメージです。

最初は抽象的すぎて「何を言っているのかさっぱり」でしたが、演習システムのおかげで徐々に理解が深まりました。

演習システムはこちらから登録すれば利用できます。
www.fos.kuis.kyoto-u.ac.jp

他の参考リンクはこちらです。

演習システムの使い方の資料

https://www.fos.kuis.kyoto-u.ac.jp/~igarashi/CoPL/guide.pdf

推論規則集

https://www.fos.kuis.kyoto-u.ac.jp/~igarashi/CoPL/rulebook.pdf

答えは用意されていないので、第1章で実際に解いたものは自分の GitHub にまとめました。
github.com

今の理解度について

算術式の簡約については、まだ理解が曖昧です。

R：簡約 1 ステップ
MR：簡約の連続
ER（決定的簡約）：簡約結果が一意になるもの

という理解ではいるものの、演習問題をこなしても、直感的にまだ腑に落ちていない部分があります。

ちなみにChatGPTに聞くと、以下の説明でしたので、理解度はまだまだでした。

R：1ステップ簡約（部分的・非決定的）
- 1回だけ簡約する関係
- 数学的には「原始的簡約関係」
MR（→＊） … 0回以上の簡約（R の反射推移閉包）
- 0回以上の簡約の繰り返し
- 数学的には「反射推移閉包」
ER（⇒） … 決定的簡約（evaluation / big-step reduction）
- 決定的（deterministic）な簡約
- 数学的には「部分関数」