第1部　形式化の基礎

コロンの左右だけでなく、判断を成立させる文脈を明示します。加算規則の二つの前提が、同じ型を要求することに 注目してください。

式は形式言語の構文に従う記号列、型は式の使用法を分類する式、項はある型に分類された式です。判断は 「その分類が規則から成立する」という体系上の主張です。Nat : Type は型を宇宙へ、two : Nat は項を 自然数型へ分類します。文脈を $\Gamma=(n:\mathsf{Nat})$ とすると、変数規則と数値規則から $\Gamma\vdash n:\mathsf{Nat}$ と $\Gamma\vdash1:\mathsf{Nat}$ を得ます。加算規則により $\Gamma\vdash n+1:\mathsf{Nat}$ です。導出木として書けば

となります。横線の上は規則の前提、下はその前提から得る結論です。true へ替えると、第二前提 $\Gamma\vdash\mathsf{true}:\mathsf{Nat}$ を作れません。

新しい構文を読むときも、構文、形成規則、導入規則、除去規則を分けます。エラーは「値が変」ではなく、 導出木のどの前提が欠けたかとして診断できます。

型検査の出力は型、評価の出力は値です。両方が同じ式を入力にしても、答える問いは異なります。

def triple (n : Nat) : Nat := n + n + n と定義します。#check triple 4 の結果は triple 4 : Nat、#eval triple 4 の結果は 12 です。前者は式を自然数として使用できることを保証しますが、 値が12であるとは述べません。後者は閉じた式を計算しますが、全入力についての定理を証明しません。 2 : Nat と 3 : Nat は同じ型を持ちますが、2 = 3 は偽です。

抽象的な関数では型検査できても値を表示できない場合があります。その場合も、具体例の評価と一般定理の証明を 混同せず、必要な保証に対応するコマンドを選びます。

宣言が要求する型と、本体から推論される型を別々に書きます。

def bad : Nat := true の期待型は Nat、本体 true の推論型は Bool です。成立させたい判断は true : Nat ですが、その導出規則はありません。def goodBool : Bool := true は期待型を本体へ合わせます。 def goodNat : Nat := 0 は本体を期待型へ合わせます。どちらも宣言全体の型整合性を回復します。

関数本体のエラーでも、期待される出力型と各分岐の推論型を表にすると同じ診断ができます。最初に現れた エラー文だけでなく、要求された判断まで戻ることが重要です。

合成の中央の型が一致するように、右側の関数から入力を流します。

$f:A\to B$ と $g:B\to C$ から作れる合成は $g\circ f:A\to C$ です。入力 $a:A$ をまず $f$ へ渡して $f(a):B$ を得て、それを $g$ へ渡します。逆向きの $f\circ g$ には、一般には $g$ の出力 C を $f$ の入力 A として使う根拠がありません。Leanの compose g f x := g (f x) も同じ順序です。

関手の合成や自然変換の垂直合成でも、中央の始域・終域を照合すれば向きを復元できます。記号の読み順より 先に型を並べます。

A → B → C を右結合で読み、一引数を与えた後に残る型を書きます。

カリー化された関数の型は $A\to(B\to C)$ です。multiply : Nat → Nat → Nat へ 2 を与えると、 multiply 2 : Nat → Nat という新しい関数が残ります。これが部分適用です。カリー化は多引数関数を一引数関数の 連鎖として表す変換、部分適用はその表現へ実際に一部の引数を与える操作です。

定理の暗黙引数や型クラス引数も、適用後に残る関数型を見れば同じ方法で追えます。どの引数が既に固定され、 どれがまだ量化されているかを区別します。

関数等式を直接示す代わりに、任意の入力へ適用した値を比較します。

任意の $f:A\to B$ と $x:A$ について、$(\mathrm{id}_B\circ f)(x)=\mathrm{id}_B(f(x))=f(x)$ です。 同様に $(f\circ\mathrm{id}_A)(x)=f(\mathrm{id}_A(x))=f(x)$ です。点ごとの等式から関数外延性により $\mathrm{id}_B\circ f=f$ と $f\circ\mathrm{id}_A=f$ が従います。

結合則も三つの関数を任意の入力へ適用し、両辺が h (g (f x)) へ簡約されることを示せます。 圏論ではこの点ごとの証明が射の単位則・結合則の原型になります。

値を作る規則、全ての値を使う規則、値を計算へ渡す規則、構成子上の計算規則を分けます。

形成規則は $\mathsf{TrafficLight}:\mathsf{Type}$、導入規則は $\mathsf{red},\mathsf{yellow},\mathsf{green}:\mathsf{TrafficLight}$ です。任意の型 $C$ と $c_r,c_y,c_g:C$ から、全ての $t:\mathsf{TrafficLight}$ に対する値を作れるのが除去規則です。 各構成子へ適用した結果が対応する分岐へ簡約される三式が計算規則になります。

列挙型の構成子を増やす場合も、各構成子に一つの分岐と計算規則を対応させます。再帰的な構成子を加えると、 除去規則には再帰結果または帰納仮定も現れます。

右辺が元の関数を小さい部分構造へ再び呼び出しているかを調べます。

toggle は入力の最上位構成子だけを見て値を返すため場合分けです。factorial (n+1) は factorial n を使い、listLength (x :: xs) は listLength xs を使うため構造再帰です。 どちらも構成子ごとに分岐しますが、再帰では構成子の引数に含まれる小さいデータへ呼出し辺があります。

木の高さや式の評価器でも、各再帰呼出しが直下の部分木へ向くかを確認します。単に match があるかではなく、 呼出し関係で分類します。

「値の個数が無限」と「一つの値を無限に観察できる」を別の量化として書きます。

自然数型は有限個の構成子 zero と succ から生成されますが、succ を任意の有限回使えるため値の集合は 無限です。ただし各自然数値は有限の構成木です。ストリームは一つの値から先頭と次の状態を何度でも観察でき、 有限構成木として全体を展開し終えません。前者は基数の無限、後者は観察の非終端性です。

無限木や状態機械でも、状態数、生成される有限値の個数、一つの振舞いの観察長を別々に記述します。

変数名ではなく、その変数を束縛するラムダまで何個の束縛を越えるかを数えます。

$\lambda x.x$ は lam (var 0)、$\lambda x.\lambda y.x$ は lam (lam (var 1)) です。内側で y は 直近の束縛なので0、x は一つ外側なので1です。逆変換では束縛子へ新しい名前を割り当て、添字0から外側へ 環境を参照します。自由変数は現在の束縛深さ以上の添字として別に管理します。

型変数と項変数を同時に持つ体系では、二種類の束縛深さを分けます。名前を消す目的は捕獲をなくすことではなく、 捕獲回避を添字操作へ変換することです。

ラムダの下へ入るとき、cutoffと代入対象の添字がともに一つ増える理由を追います。

自由変数を持つ項をラムダの下へ移す前に、cutoff以上の添字を1増やします。代入 $[j:=s]t$ でラムダの下へ入る場合は、対象を $j+1$ とし、置換項を shift s に替えます。 これにより、外側で自由だった変数が新しい束縛子の var 0 に誤って捕獲されません。束縛変数はcutoff未満なので シフトされず、同じ束縛先を保ちます。

型代入や文脈への弱化でも、保ちたい不変条件を「各添字が同じ束縛を指す」と書けば、必要なシフト量を導けます。

どの局所変形が許されるかと、複数の候補からどれを選ぶかを分けます。

β簡約規則は $(\lambda x.t)\,s\to t[x:=s]$ という局所変形を許します。これは項のどこを先に探すかを 指定しません。contractHead? は先頭がredexのときだけ縮約する関数です。完全な値呼び評価器なら関数位置、 次に引数を値まで評価し、その後にβ簡約します。名前呼びなら引数を先に評価せず代入します。

書換え系、証明簡約、最適化でも、関係を仕様、探索戦略を実装として分離します。完全性や決定性は別の定理です。

Nat : Type : Type 1 を一つの三項関係として読まず、隣接する二つの判断へ分けます。

第一の判断は Nat : Type で、自然数型を宇宙 Type の項として分類します。第二の判断は Type : Type 1 で、その宇宙自身を一段上の宇宙へ分類します。項 0 : Nat を加えると、 0 : Nat、Nat : Type、Type : Type 1 の三判断になります。Type : Type とはしないため、 自己包含に由来する不整合を避けます。

依存型の型を読むときも、項、型、型の属するsortを別の判断へ展開します。エラーが値の型か宇宙制約かを 切り分けられます。

二つの入力型が同じ宇宙に属する必要が本当にあるかを考えます。

定数関数や合成は、入力型と出力型が異なる宇宙にあっても構成できます。α : Type u と β : Type v を 一つの u に固定すると、定義に不要な同宇宙制約を課します。polymorphicConstant では u と v、 polymorphicCompose では u,v,w を独立に量化するのが一般的です。

圏の対象・射や型族でも、独立に選べる層には独立な宇宙変数を置きます。等しさが必要な制約だけを共有します。

直積型と依存関数型について、どの成分が Prop のとき宇宙が縮むかを比較します。

積 α × β は両方のデータを保持するため、α : Type u と β : Type v から α × β : Type (max u v) になります。依存関数型 (x : α) → β x の宇宙は通常 imax u v です。 終域が Prop、すなわち v=0 のとき、全称命題も Prop に留まります。これが imax u 0 = 0 の役割です。

宇宙式は暗記せず、構成がデータを保持するか、証明だけを要求するかから予測します。予測後にLeanの表示で 制約が解けることを確かめます。