Formal Lab

第1〜3章で、式を型・項・入力・出力に分けて読む習慣を作ります。第5〜9章では、命題、量化、等式の 背後にある型と束縛をLeanで確かめます。第20〜22章の集合・関数・関係で通常の数学へ戻り、第31・32章で 添字や「値に依存する型」まで同じ読み方を広げます。

第1〜3章でLeanの式を読む最小限の基礎を得た後、第6〜10章で仮定と結論、量化、等式、推論規則を学びます。 第20〜23章では、集合・関数・関係・帰納法の証明を、紙の上の議論とLeanの証明項の両方で組み立てます。 まず演習まで自力で進みたい読者の基本経路です。

第2〜4章で関数、データ、ラムダ計算を確認し、第6・10・11章で命題、推論、型判断との対応を見ます。 第12〜14章では代入、評価、再帰型を通じて「項を実行すること」と「項を証明として読むこと」を分けて 接続します。第31〜33章へ進むと、依存型と構成計算までを一つの型体系として見渡せます。

第3章の構成子と再帰、第23章の帰納法から始めます。第27〜30章で最小・最大不動点、第36・37章で一般の 帰納族とW型を学ぶと、有限データと無限の振舞いを区別できます。さらに第54〜57・66〜69・82章へ進めば、 始代数・終余代数と再帰型の意味論が、同じ原理を別の側から説明することを確かめられます。

第20〜22章の集合・関数・関係を具体例として、第42〜44章で「対象そのもの」ではなく、それを特徴づける 写像の条件を読みます。第45〜47章で圏・関手・自然変換という比較の言葉を導入し、第48〜53章で同値、 極限、表現可能性、米田、随伴、モナドへ進みます。分野ごとの記号の奥にある共通の形を探す経路です。

第31〜33章で依存型側の見取り図を得て、第42〜52章で普遍性から圏論を組み立てます。第70〜74章では 関数型・単純型・依存型を圏の中で解釈し、第75〜78章では資源、計算効果、内部論理まで同じ視点を広げます。 個々の専門語を先に選ぶのではなく、本書の後半が前半をどう説明し直すかを追う総合経路です。