第6部　依存型と型システム

型族 B : A→Type を B a=C という定数族にします。

依存関数型 (a:A)→B a でBが定数Cなら、返り値型は入力に依存せず通常の A→C です。依存対型 (a:A)×B a も通常の積 A×C になります。従ってΠ型とΣ型は関数型と積型を含む一般化です。ただし構文上の 定数族と定義的に同じか、同値を介して定数かは区別します。後者では明示的な輸送が必要な場合があります。

論理ではΠを全称量化、Σを証人を保持する存在として読み、非依存の場合との連続性を確認します。

Σn:Nat, Vector A n の第一射影で長さ、第二射影でその長さのベクトルを得ます。

三要素ベクトル v : Vector A 3 から ⟨3,v⟩ : Σn,Vector A n を作れます。入力pを場合分けして ⟨n,xs⟩ とすれば、結果型の中でもnとxsの対応を保ったまま利用できます。例えば xs の長さを再び添える関数は fun ⟨n,xs⟩ => ⟨n,xs⟩ です。第一射影だけを先に忘れると第二成分の型を記述できないため、依存消去は対を 一緒に開きます。

パーサが「長さとその長さの配列」を返すAPIでは、Σ型により整合性を返り値へ保存できます。

Leanの Exists はProp、Sigma はTypeに属することから消去先の違いを見ます。

∃x:A,P x は証明の存在を主張し、証明無関連性とPropからの消去制限の下で扱われます。Σx:A,B x は第一成分と 第二成分を計算データとして保持し、任意のTypeを返す関数で分解できます。存在証明から一般のプログラムとして証人を 抽出できるとは限りません。構成的証明が具体的な証人を作っていても、公開するインターフェースをPropにするかTypeに するかで利用可能性が変わります。

仕様の充足だけが必要なら命題、後続計算が証人を使うなら依存対というAPI設計基準にします。

等式証明を refl の場合へ帰着し、その場合の返り値を指定します。

対称性は p:x=y を消去し、目標 y=x を x=x へ帰着して refl x を返します。推移性は p:x=y を消去した後、q:y=z が q:x=z となるのでqを返せます。どちらも等式の唯一の導入子reflに対する 場合を与えたJの特殊化です。等式連鎖の法則も等式証明へ帰納すればreflの場合の計算へ還元されます。

輸送、合同性、置換原理をすべてJから導き、どれをライブラリの基本APIにするか比較します。

型族 P(k)=Vector A k に等式 p:n=m を使います。

v:Vector A n と p:n=m から transport P p v : Vector A m を得ます。pがreflなら輸送結果は定義的にvです。 一般のpではデータの要素を変更せず、型が参照する添字だけを同一視に沿って替えます。n+0=n の証明で Vector A (n+0) を Vector A n へ直す例では、等式の向きに応じてpまたは対称性pを選びます。

圏の対象等式に沿う射の型変更など、依存する構造を添字同一視に沿って移す操作へ一般化します。

命題外延性、関数外延性、商健全性、一価性がどの種類の同値を等式へ送るかを書きます。

命題外延性は P↔Q から P=Q、関数外延性は ∀x,f x=g x から f=g を与えます。商健全性は基礎関係 r a b を商内の等式へ送ります。一価性は型同値 A≃B を宇宙内の等式 A=B と対応させます。対象の層は 命題、関数、商の代表、型と異なり、互いを名前だけで代用できません。Leanでどれが定理・公理・商構成の規則かも 区別します。

外延的な数学を形式化するときは必要な等式原理を最小限にし、計算可能性への影響を記録します。

積形成規則 (s₁,s₂,s₃) が、どのソートの項へ依存する型をどのソートに作るかを表します。

PTSはソート、基礎公理 s₁:s₂、積形成三つ組で指定されます。規則 (s₁,s₂,s₃) があれば、 Γ⊢A:s₁ と Γ,x:A⊢B:s₂ から Γ⊢Πx:A.B:s₃ を作れます。したがって依存の可否はΠの見た目ではなく この三つ組により決まります。項から項、型から項、項から型、型から型という二軸を分類すると、ラムダ・キューブの 各頂点を復元できます。

新しい型理論を比較するときは表面構文ではなく、宇宙公理とΠ形成規則の差として整理します。

単純型付きラムダ計算から、三種類の依存を独立なスイッチとして加えます。

三軸は項に依存する型、型に依存する項である多相性、型に依存する型である型演算子です。スイッチなしが 単純型付きラムダ計算、各一軸を加えた体系、その組合せ四つで八頂点になります。全軸を許す頂点が構成計算であり、 依存型とインプレディカティブな命題を統合する基礎になります。頂点名を暗記するより、許されるΠ型の例を一つずつ 作れば位置を再構成できます。

宇宙階層や帰納型は元の三軸に含まれないため、現代の証明支援系をキューブだけで分類し尽くさないようにします。

判断を生成する規則と、その規則すべてについて外側から証明する性質を分けます。

変数・Π形成・抽象・適用・変換は体系内部の型付け規則です。弱化・代入・主部簡約は構文に関するメタ定理です。 型保存・強正規化・無矛盾性も規則から証明するメタ定理です。例えば変換規則があることと変換可能性が決定可能であることは別です。後者には 正規化や合流性が必要です。メタ定理を規則として無条件に追加すると、循環した「証明」になり得ます。

Leanのカーネル機能と、Lean自身について外部で証明・検証される健全性主張を同じ基準で区別します。

自然数nと証明 n<5 を部分型の構成子へ同時に渡します。

BelowFive := {n : Nat // n < 5} とすると、⟨3, by decide⟩ : BelowFive です。第一射影 .val は3、第二射影 .property は 3<5 の証明です。二つの値 x y : BelowFive の等しさには、基礎値 x.val=y.val を示せば 部分型外延性を使えます。証明成分を個別に比較する必要がないのは、命題の証明無関連性によります。

正規化済み構文、範囲内添字、単調関数など、値と不変条件を同じAPI境界で受け渡せます。

部分型上の演算では、第一成分の値と、結果が再び述語を満たす第二成分を別々に構成します。正の自然数同士の加算なら 値は通常の加算で作り、正値性は入力の証明から示します。空な部分型を示すときは候補値の探索ではなく、任意の候補に 要求される証明成分が矛盾することを示します。専用帰納型では不変条件を構成子の形で保つため、同じ性質でも除去原理と 定義的計算が変わります。

ブール値だけでなく、成功時に境界証明を含む Option を返します。

checkBelow (b n : Nat) : Option {k : Nat // k < b} を、if h:n<b then some ⟨n,h⟩ else none と定義します。 成功分岐の呼出し側はnと証明を受け取り、その後の添字操作で境界検査を繰り返しません。完全性は n<b → ∃x, checkBelow b n=some x、健全性は checkBelow b n=some x → x.val=n ∧ x.val<b です。 単なるBool検査では後者の証拠が返り値に保存されません。

パーサや入力検証でも、検査結果を精密な型へ昇格させるスマートコンストラクタを公開します。

部分型、篩型言語、依存対を「証明の保持」「自動推論」「計算データ」の軸で比較します。

Leanの部分型 {x:A // P x} は値とPropの証明を保持します。篩型体系は基礎型へ論理式を付し、部分型付けとSMTなどで 検査を自動化する設計が中心です。Σ型 Σx:A,B x は第二成分が任意のTypeに属し、計算データも保持できます。 歴史的には集合内包的な型の発想から、Freeman–Pfenningの篩型、Liquid Typesの決定可能な述語テンプレートへ展開しました。 同じ記法に見えても証明対象、消去規則、自動化の境界が異なります。

ライブラリ設計では、任意命題を扱う柔軟性と自動推論可能な論理断片のどちらを優先するか明記します。

Vector.nil の結果添字は0、cons は後者なので、空ベクトルにconsの場合はありません。

head : Vector A (n+1)→A を定義するとき、入力は cons a xs の形しか取りません。nil の結果型 Vector A 0 と要求型 Vector A (n+1) は構成子の非交差性により一致しないからです。これは実行時の長さ検査で 分岐を捨てるのではなく、型付けされた入力の構成可能性から分岐自体を除去しています。不可能性は添字等式 0=n+1 の矛盾としても読めます。

型付き構文の評価器では、式の型添字から加算式を関数として扱うような不正分岐を排除できます。

ベクトルのmapとappendについて、入力と出力の長さを型に残します。

map : (A→B)→Vector A n→Vector B n は長さnを保存します。nil分岐では0、cons分岐では帰納呼出しがnを保存し、 consが両辺を後者へ送ります。append : Vector A m→Vector A n→Vector A (m+n) では第一入力へ再帰します。 nil分岐の結果型は 0+n=n、cons分岐では帰納結果の長さ m+n を一つ増やして (m+1)+n と一致させます。

行列積を内側次元が一致する型に限定すれば、次元不一致を実装の分岐ではなく呼出し時に排除できます。

Vector A n と {xs : List A // xs.length=n} の構成子と帰納原理を比較します。

二つの表現はデータとして対応し、リストから長さ証明付き値を作り、ベクトルから要素列を忘却できます。部分型表現では リストの既存APIを再利用できますが、操作ごとに長さ証明を運びます。帰納族ではnilとconsの結果添字が定義に組み込まれ、 添字に精密な帰納原理が得られます。一方、基礎データを直接取り出すには変換が必要です。単なる同型性だけで、生成される 消去規則や定義等式まで同一とは限りません。

既存データ構造へ不変条件を後付けする場合と、不変条件が再帰構造を決める場合で表現を選びます。

各構成子について、再帰引数のすべてに帰納仮定を置いた場合を一つずつ作ります。

Expr τ に自然数、真偽値、加算、条件分岐があるなら、動機は P : ∀τ,Expr τ→Prop です。定数の場合を二つ、 加算では二つの部分式への帰納仮定から結果を、条件分岐では条件と両枝への三つの帰納仮定から結果を示します。 結論は ∀τ(e:Expr τ),P τ e です。添字τを動機に残すことで、各構成子の型制約を場合の中で利用できます。

相互・入れ子帰納型では単純な構成子一覧だけで足りない場合があり、生成された原理を必ず検査します。

式へ変数写像ρを適用する操作と、環境をρに沿って前合成する操作を対応させます。

主張は eval env (rename ρ e)=eval (env∘ρ) e です。eへの構造帰納で示します。変数の場合は定義から両辺が env (ρ x)。定数は不変です。加算や条件分岐ではrenameとevalを構成子ごとに展開し、部分式への帰納仮定で 書き換えます。添字付きExprならrenameが変数の型を保つ写像であることも型に現れます。

代入補題は環境に式を割り当てる名前変更の一般化として、同じ自然性の図式から導けます。

定義中の型Xが関数矢印の左を通る回数で極性を追います。

X↦A×X と X↦A+(B→X) ではXは正の位置なので帰納型を作れます。X↦X→A では矢印の始域にあり負です。 X↦(X→A)→A では二回反転して正ですが、厳密正値性検査はXを含む関数型全体が構成子引数の始域に現れるため 拒否するのが一般的です。厳密正値性は単なる符号計算より強く、生成される再帰子の健全性と単調な型作用素を保証する 構文的条件です。

高階抽象構文では負の出現が自然に現れるため、単調性証明や別の表現を使う必要があります。

W型 sup : (a:A)→(B a→W A B)→W A B でAを節点形、B aを子位置と読みます。

自然数では形を zero|succ、位置をzeroで空、succで一要素にします。二分木では葉と節を形にし、葉の位置を空、 節の位置をBoolにすれば左右二子を表せます。有限多分木では形を子数n、位置を Fin n とします。形aを選んだ後に 位置型B aが決まる依存性により、構成子ごとに異なる分岐数を一つのW型で表せます。

構文木やコンテナ型を形と位置へ分解すると、map・fold・導関手的操作を一様に設計できます。

形を none|some a、位置をそれぞれ空型と一要素型にします。

Wリストのnilは sup none と空位置からの唯一関数、cons a xsは sup (some a) と唯一位置をxsへ送る関数です。 W型からListへはW帰納でnoneをnil、some aをconsへ送ります。逆向きはリスト再帰でこの二構成を使います。 往復が恒等であることは、それぞれW帰納法とリスト帰納法により、構成子の場合の計算規則へ還元されます。

同型だけでなくfoldとの可換性を示すと、表現を替えても再帰プログラムの意味が保存されます。

W型を一層展開するF代数 in : F W→W と、任意の代数 α:F X→X を置きます。

foldは fold α : W→X であり、方程式 fold α ∘ in = α ∘ F(fold α) を満たします。左辺は一層をWへ組み立てて から再帰し、右辺は各子を再帰してからαで一層を処理します。W帰納法によりこの方程式を満たす写像は一意です。 従って (W,in) から任意のF代数への一意な代数射がfoldであり、これが始代数の普遍性です。

融合則は二つの代数射の合成と一意性から導き、再帰プログラム最適化の正当性へ接続できます。

f:A→B の逆gとホモトピー f(g b)=b から、ファイバー中心 ⟨g b,ε b⟩ を選びます。

b上のファイバーは Σa:A,f a=b です。中心を c_b=⟨g b,ε_b⟩ とします。任意の ⟨a,p⟩ へは、逆のもう一方の 法則 η_a:g(f a)=a とpに沿う輸送を組み合わせ、第一成分の道を作ります。Σ型の等式には、その道に沿って第二成分も 一致することが必要です。この整合性には逆データの随伴化、または等式帰納を使います。単なる左右逆の式から ファイバー可縮性へ進む際、道の高次整合性が隠れている点が重要です。

写像が同値である定義を可縮ファイバーで与えると、合成や基底変換に安定な形で扱えます。

型の等式から同値への標準写像 idtoequiv が何を満たすかを段階化します。

同一の型が同値であることはreflから常に示せます。同値な型を交換して命題の真偽を保存することも、個別の輸送で 実現できます。骨格を選んで同値類ごとに代表を取る主張は選択を含み、型そのものの等式は与えません。一価性はさらに idtoequiv : (A=B)→(A≃B) 自体が同値であると主張します。従って同値から道を作るだけでなく、その道空間の 高次構造まで同値空間と対応させます。

構造同一原理では、構造を保つ同型を構造の等式へ送るため、一価性と構造の同一性条件を組み合わせます。

円周は点 base:S¹ と道 loop:base=base で生成されます。

非依存再帰で f:S¹→X を作るには、点 x₀:X とループ p:x₀=x₀ を与えます。計算規則は f base=x₀ と、loopへの作用 ap f loop=p です。依存消去で族 P:S¹→Type の切断を作るには b:P base と、loopに沿う輸送がbをbへ戻す道が必要です。点の値だけでは生成するループの像を決められません。

高次帰納型では各点構成子に値、各道構成子に整合性を与えるという読み方を一般化します。

商射影qに対する健全性 r a b→q a=q b を使います。

整数を自然数対 (a,b) の差として表し、(a,b)∼(c,d) ↔ a+d=c+b とします。この関係が同値関係であることを示して 商を作ると、関係証明は商健全性により q(a,b)=q(c,d) へ送られます。ただし逆向き、商内で等しい代表が必ず 元の関係にあることは商構成の完全性に相当し、一般の関係では同値閉包を取るためそのままでは成り立ちません。

構文を書換え規則で商するとき、意図した等式理論が反射・対称・推移・合同閉包を含むことを確認します。

代表上の関数fが r a b→f a=f b を満たすことを先に証明します。

整数対の商から符号を無視した絶対値を定めるなら、代表 (a,b) へ自然数差の絶対値を割り当てます。関係 a+d=c+b から二つの差の絶対値が等しいことを示せば、商のliftで関数を得ます。代表の第一成分だけを返す関数は (1,0)∼(2,1) で値が異なり、降下しません。well-definednessは実装後の注意ではなく、商除去子の型が要求する 主要な証明義務です。

商上の二項演算では左右の代表を替えても結果が同値である合同性を二変数について示します。

部分型は許されない値を除き、商型は値同士の区別を除きます。

部分型 {x:A//P x} はAのうちPを満たす値だけを残し、包含写像でAへ戻せます。商型 A/∼ はAの全要素を射影しますが、 同値な要素の区別を忘れ、一般に代表を標準的には戻せません。前者の普遍的性質はPを満たす値からの因子化、後者は ∼を尊重する写像の因子化です。有限集合の「偶数だけ」と「合同類」は、それぞれ対象の削減と観察可能な区別の削減を 具体化します。

正規形の部分型と変換可能性による商を比較し、正規化定理が両表現を結ぶ条件を調べます。

モノイドの台、単位元、演算と、結合則・単位則を別々に列挙します。

データは型M、1:M、(·*·):M→M→M です。法則は結合則と左右単位則というPropのフィールドです。データだけなら マグマに単位元候補を添えたものにすぎません。Leanの構造体は両方を一つの辞書に格納し、演算の記法はデータフィールド、 書換え補題は法則フィールドまたはそこからの定理を参照します。法則が実行時データとして重要か、証明消去されるかも ソートから読み分けられます。

圏、順序、位相などでも「運ぶデータ」と「満たす公理」を分離して構造間の忘却写像を設計します。

型クラス引数を明示引数へ戻し、記法をフィールド射影へ展開します。

[Monoid M] を明示的な辞書 inst : Monoid M とすると、x*y は HMul.hMul x y を経てinstの乗法へ解決され、 1 も対応するOfNatやOne辞書のフィールドです。定理 mul_assoc x y z は暗黙のinstから法則を取り出します。 同じ型Mでも加法構造を乗法記法へラップした別辞書を渡せば意味が変わるため、探索は新しい数学を証明するのではなく 利用可能な構造値を合成して補う機構です。

デバッグ時は記法、型強制、既定インスタンスを順に展開し、どの辞書経路が選ばれたか追跡します。

同じ出力型を持つ候補が複数ある場合と、探索が再帰的に自分へ戻る場合を分けます。

一つの型へ数学的に異なる二つの順序を同じ LE インスタンスとして大域登録すると、優先順位に依存し意図が見えません。 新しいラッパー型で構造を区別するのが安全です。また C A を作るため C A 自身を要求するインスタンスは探索循環を 起こします。出力パラメータや優先順位は正当な標準経路を表す場合だけ使い、曖昧性を隠す手段にはしません。

圏論ライブラリの忘却・誘導インスタンスでは、ダイヤモンドが定義的に一致するかをAPI設計段階で確認します。

適用 f x ではfの型を未知の引数型から未知の結果型への矢印と等置します。

環境 f:α→β, x:α で f x を推論すると、部分項から型 α→β とαを得て、制約 α→β = γ→δ と α=γ を生成します。単一化の最汎解は γ↦α, δ↦β で、結果型はβです。導出木では 適用規則の中間型がα、実行器では新しいメタ変数γがその役割を担います。解いた置換を環境・項・結果型の全体へ 適用して初めて導出と一致します。

let多相を加える場合は一般化するメタ変数と環境に拘束されるメタ変数を分離します。

方程式集合と蓄積置換が同じ解集合を表すことを不変条件にします。

分解は同じ型構成子の引数へ進み、変数消去はoccurs checkを通った変数を型へ置換します。不変条件は、現状態の解へ 蓄積置換を合成したものが元の制約の解と一致することです。Nat=Bool は構成子衝突、α=α→Nat はoccurs check、 異なる項数の型構成子は形の衝突で失敗します。occurs checkを省くと有限型構文に無限型を暗黙に要求します。

高階単一化では最汎解や決定可能性が失われ得るため、対応する論理断片を明示します。

変数・注釈付き項・適用は型を合成し、ラムダや曖昧な構成は期待型に対して検査します。

双方向型付けでは Γ⊢t⇒A と Γ⊢t⇐A を分けます。変数と型注釈は型を合成し、適用は関数型を合成して引数を 始域へ検査します。注釈なしラムダは引数型を自力で決められないため、期待される A→B に対し本体をBへ検査します。 合成から検査へは得た型と期待型の変換可能性を確認します。注釈位置は情報が一方向へ流れる境界になります。

依存適用では前の引数が後続型へ代入されるため、引数順と明示注釈が推論可能性を左右します。