正本：FormalLab/TypeTheory/PureTypeSystems.lean

第33章：純粋型システム・ラムダ・キューブ・構成計算#

単純型、依存型、パラメトリック多相、型演算子は、互いに無関係な機能なのでしょうか。それとも「何が何に依存できるか」という少数の規則から統一的に分類できるのでしょうか。

この章は名称の暗記から始めません。まず単純型付きラムダ計算の判断 $\Gamma \vdash t : A$ に、型自身を分類する判断 $\Gamma \vdash A : s$ を加えます。次に、Π型の束縛変数と本体がどの階層に属するかを三つの軸として読みます。八体系の名前は、その組合せに後から付く座標名です。最後に全三軸を持つCoCを位置づけ、帰納型・宇宙・商などを備える Lean 4やCICと同一視できない理由を明確にします。

sort公理とΠ形成規則から型理論を指定する#

PTSは三つ組 $(\mathcal S,\mathcal A,\mathcal R)$ で指定されます。 $\mathcal S$ はsortの集合、 $\mathcal A \subseteq \mathcal S^2$ はsort公理、 $\mathcal R \subseteq \mathcal S^3$ はΠ形成規則です。項・型・kindは別々の文法カテゴリではなく、判断 $\Gamma \vdash M : A$ の中で担う役割によって区別されます。下のLeanコードはこの考え方の構文とラムダ・キューブの座標をモデル化するもので、完全なPTS型検査器ではありません。

Leankernel-checked counterpartL25–25

namespace FormalLab.TypeTheory.PureTypeSystems

項・型・kindを一つの構文で表す#

純粋型システム（pure type system; PTS）では、項と型に別々の文法を用意しません。変数・適用・ラムダ抽象・依存積・sortを、同じ式の文法で表します。ある式が項・型・ kindのどれとして働くかは、構文の形だけでなく型判断によって決まります。

次の Expression はその共通構文の骨格です。lam domain body は λ (x : domain). body、pi domain codomain は Π (x : domain), codomain を表します。 de Bruijn添字 0 は最も近い束縛子を参照します。

ラムダ・キューブを記述する二つのsort。

Leankernel-checked counterpartL40–42

inductive PTSSort where
  | star
  | box

sort集合を型 SortType で表したPTS仕様。公理関係とΠ形成関係だけを保持する。

Leankernel-checked counterpartL45–47

structure PTSSpec (SortType : Type) where
  sortAxiom : SortType → SortType → Prop
  productRule : SortType → SortType → SortType → Prop

PTSの共通構文の骨格。型もkindも同じ構文の式として表す。

Leankernel-checked counterpartL50–55

inductive Expression where
  | sort : PTSSort → Expression
  | var : Nat → Expression
  | app : Expression → Expression → Expression
  | lam : Expression → Expression → Expression
  | pi : Expression → Expression → Expression

注釈付き恒等関数 λ (x : A). x の構文。

Leankernel-checked counterpartL58–59

def annotatedIdentity (A : Expression) : Expression :=
  .lam A (.var 0)

*（star）は項を分類する型のsort、□（box）は型を分類するkindのsortとして読みます。ラムダ・キューブの標準的なPTS表示では公理 $* : \Box$ を置き、 $\Box$ 自身の型はこの二sort 体系の内部では与えません。ここでの * と □ はLeanの Type と Sort の別名ではありません。Leanの可算な宇宙階層を、二sortへ潰して理解してはいけません。

三つ組のうち集合 $\mathcal S$ はLeanの型引数 SortType に、公理関係 $\mathcal A$ は PTSSpec.sortAxiom に、形成関係 $\mathcal R$ は PTSSpec.productRule に対応します。この構造体は規則の許可範囲だけを記録します。項の導出、文脈の整形式性、簡約関係はまだ含みません。

Π形成規則を座標にする#

PTSの積形成規則はsortの三つ組 $(s_1,s_2,s_3)$ で指定されます。 $(s_1,s_2,s_3)\in\mathcal R$ であるとき、次の形成規則を使えます。

\frac{\Gamma \vdash A:s_1 \qquad \Gamma,x:A \vdash B:s_2} {\Gamma \vdash \Pi x:A.\,B:s_3} \;\textsc{(product)}

ラムダ・キューブでは、単純関数に必要な (*, *, *) を全頂点が持ち、残る三規則を加えるか否かで座標を作ります。

ラムダ・キューブで区別する四種類のΠ形成規則。

Leankernel-checked counterpartL88–88

inductive ProductRule where

(*, *, *)：項から項への通常の関数。

Leankernel-checked counterpartL90–90

| termToTerm

(□, *, *)：型を束縛して項を作る多相。

Leankernel-checked counterpartL92–92

| typeToTerm

(*, □, □)：項を束縛して型構成子を作る依存型。

Leankernel-checked counterpartL94–94

| termToType

(□, □, □)：型を束縛して型構成子を作る型演算子。

Leankernel-checked counterpartL96–96

| typeToType

規則名をPTSのsort三つ組へ戻す。

Leankernel-checked counterpartL99–103

def productRuleSorts : ProductRule → PTSSort × PTSSort × PTSSort
  | .termToTerm => (.star, .star, .star)
  | .typeToTerm => (.box, .star, .star)
  | .termToType => (.star, .box, .box)
  | .typeToType => (.box, .box, .box)

(*, □, □) が「型が項に依存する」軸なのは、型族そのものが λ (x : A). B という型レベルの関数だからです。その型 Π (x : A), * はkindに属します。一方、個々の依存積 Π (x : A), B x の形成だけを見て三軸を推測すると向きを取り違えます。

三つの独立な追加機能#

CubeFeatures の三つの真偽値は次を表します。

dependentTypes：型が項に依存できる。
polymorphism：項が型に依存できる。
typeOperators：型が型に依存できる。

項が項に依存する通常の関数は全頂点に共通なので、座標には含めません。

ラムダ・キューブの頂点を決める三つの独立な機能。

Leankernel-checked counterpartL122–125

structure CubeFeatures where
  dependentTypes : Bool
  polymorphism : Bool
  typeOperators : Bool

ある頂点で積形成規則が許されるか。通常の関数規則は常に許す。

Leankernel-checked counterpartL128–132

def CubeFeatures.allows (features : CubeFeatures) : ProductRule → Bool
  | .termToTerm => true
  | .typeToTerm => features.polymorphism
  | .termToType => features.dependentTypes
  | .typeToType => features.typeOperators

三軸の指定から二sortのPTS仕様を作る。

Leankernel-checked counterpartL135–138

def lambdaCubeSpec (features : CubeFeatures) : PTSSpec PTSSort where
  sortAxiom s₁ s₂ := s₁ = .star ∧ s₂ = .box
  productRule s₁ s₂ s₃ :=
    ∃ rule, productRuleSorts rule = (s₁, s₂, s₃) ∧ features.allows rule = true

形成だけでは項を型付けできない#

$\mathcal A$ の要素 $(s_1,s_2)$ は、空の文脈でsortを導入します。

\frac{(s_1,s_2)\in\mathcal A}{\varnothing\vdash s_1:s_2} \;\textsc{(axiom)}

変数を文脈へ加えるには、その型自身がsortを持つことを先に確かめます。文脈 $\Gamma$ が整形式で、 $\Gamma\vdash A:s$ なら、 $\Gamma,x:A\vdash x:A$ を導けます。弱化は、既存の判断を新しい未使用変数の下へ持ち上げます。形成済みのΠ型に対するラムダ抽象と適用は次の形です。

\frac{\Gamma,x:A\vdash b:B \qquad \Gamma\vdash \Pi x:A.\,B:s} {\Gamma\vdash \lambda x:A.\,b:\Pi x:A.\,B} \;\textsc{(abstraction)}

\frac{\Gamma\vdash f:\Pi x:A.\,B \qquad \Gamma\vdash a:A} {\Gamma\vdash f\,a:B[x:=a]} \;\textsc{(application)}

右下の $B[x:=a]$ は、 $B$ に現れる自由な $x$ を $a$ で捕獲を避けて置換した式です。値域 $B$ が $x$ を含まなければ通常の関数型 $A\to B$ に戻ります。さらに型がβ変換で一致するときの変換規則が、計算と型付けを結びます。したがって PTSSpec の二関係は体系の可変部分を指定しますが、型付け関係そのものではありません。

三軸を代表項から見分ける#

三つの追加規則は、すべて「型を引数に取る」という一語では区別できません。外側の束縛子と本体のsortを調べます。

$(\Box,*,*)$ は、型 $A:*$ を束縛して項を作ります。多相恒等関数の型は $\Pi A:*.\,\Pi x:A.\,A$ です。
$(*,\Box,\Box)$ は、項 $x:A$ を束縛して型族を作ります。例えば $\lambda n:\mathsf{Nat}.\,\mathsf{Vec}\;A\;n$ は $\Pi n:\mathsf{Nat}.*$ というkindを持ちます。
$(\Box,\Box,\Box)$ は、型 $A:*$ を束縛して型演算子を作ります。例えば $\lambda A:*.\,A\to A$ のkindは $\Pi A:*.*$ です。

多相恒等関数と型演算子は、どちらも型変数 $A$ を束縛します。前者の本体は項でありsort $*$ に分類され、後者の本体は型でありkindの側に分類されます。この値域のsortが、項の多相と高階の型演算を分けます。

八頂点#

三つの独立な真偽値には $2^3=8$ 通りあります。文献では次の名称が標準的です。 $\lambda\underline{\omega}$ と $\lambda\omega$ は下線の有無が意味を持つため、プレーンテキストでは機能の列も必ず併記します。

体系	型←項	項←型	型←型	通称・役割
`λ→`	×	×	×	単純型付きラムダ計算
`λP`	○	×	×	依存型
`λ2`	×	○	×	System F、二階多相
$\lambda\underline{\omega}$	×	×	○	型演算子だけを加えた体系
`λP2`	○	○	×	依存型＋多相
`λPω`	○	×	○	依存型＋型演算子
$\lambda\omega$	×	○	○	System Fω
`λC`	○	○	○	構成計算（CoC）

矢印 型←項 は「左のものが右のものに依存する」と読みます。関数の入出力方向ではありません。

λ→：三機能を追加しない基点。

Leankernel-checked counterpartL206–206

def lambdaArrow : CubeFeatures := ⟨false, false, false⟩

λP：型が項に依存する。

Leankernel-checked counterpartL209–209

def lambdaP : CubeFeatures := ⟨true, false, false⟩

λ2（System F）：項が型に依存する。

Leankernel-checked counterpartL212–212

def lambda2 : CubeFeatures := ⟨false, true, false⟩

λ\underline{ω}：型が型に依存する。

Leankernel-checked counterpartL215–215

def lambdaOmegaUnderlined : CubeFeatures := ⟨false, false, true⟩

λP2：依存型と多相を組み合わせる。

Leankernel-checked counterpartL218–218

def lambdaP2 : CubeFeatures := ⟨true, true, false⟩

λPω：依存型と型演算子を組み合わせる。

Leankernel-checked counterpartL221–221

def lambdaPOmega : CubeFeatures := ⟨true, false, true⟩

λω（System Fω）：多相と型演算子を組み合わせる。

Leankernel-checked counterpartL224–224

def lambdaOmega : CubeFeatures := ⟨false, true, true⟩

λC（CoC）：三機能を全て組み合わせる。

Leankernel-checked counterpartL227–249

def lambdaC : CubeFeatures := ⟨true, true, true⟩

theorem lambdaArrow_has_only_term_functions :
    lambdaArrow.allows .termToTerm = true ∧
    lambdaArrow.allows .typeToTerm = false ∧
    lambdaArrow.allows .termToType = false ∧
    lambdaArrow.allows .typeToType = false :=
  ⟨rfl, rfl, rfl, rfl⟩

theorem lambdaC_has_all_product_rules (rule : ProductRule) :
    lambdaC.allows rule = true := by
  cases rule <;> rfl

theorem lambdaCube_has_star_box_axiom (features : CubeFeatures) :
    (lambdaCubeSpec features).sortAxiom .star .box :=
  ⟨rfl, rfl⟩

theorem lambdaC_spec_contains_every_cube_product (rule : ProductRule) :
    (lambdaCubeSpec lambdaC).productRule
      (productRuleSorts rule).1
      (productRuleSorts rule).2.1
      (productRuleSorts rule).2.2 := by
  exact ⟨rule, rfl, lambdaC_has_all_product_rules rule⟩

構成計算（CoC）#

CoCはキューブの対角頂点 λC です。単純型付きラムダ計算を基点にすると、次を同時に許します。

依存型：型族が項を引数に取る。
パラメトリック多相：項が型を引数に取る。
高階の型演算子：型構成子が型を引数に取る。

ただし規則一覧だけでは型理論は完成しません。PTSの型判断には、sort公理と変数規則が必要です。さらに弱化、Π形成、ラムダ抽象、適用、β変換による変換規則を備えます。文脈の整形式性と代入補題も必要です。型保存、合流性、強正規化などは、体系について証明するメタ定理です。「表現力が高い」ことから無矛盾性や停止性は自動では出ません。

命題＝型対応の下では、型は命題、項は証明、β簡約は証明の正規化として読めます。 CoCが「構成」と「計算」を同じ言語で扱う要点はここにあります。

キューブの分類表をLeanで検査する範囲#

ProductRule と CubePoint はラムダ・キューブの三軸と八頂点を有限データとして検査するための Lean上の表現です。これはPTSの構文・文脈・型判断・β変換・メタ理論を全て実装したものではありません。rfl で閉じる各定理は表の定義展開を検査しており、CoCの正規化や無矛盾性を証明しているわけではありません。

CoC、CIC、Lean 4を同一視しない#

古典的なラムダ・キューブのCoCは二sort * : □ と四種類のΠ形成規則を持つ小さな核です。 Lean 4はこれに似た依存ラムダ計算を核としますが、実際には可算な非累積宇宙、非可述的かつ証明無関係な Prop、帰納族、商などを備えます。したがってLeanを単に「キューブの λC」と呼ぶだけでは、kernelの重要な規則を落とします。CoCは設計の座標軸、 Leanはその発展形の一つとして理解します [LEAN-DTT]。

また、帰納構成計算（Calculus of Inductive Constructions; CIC）は、CoCへ帰納的定義を組み込む系統の名称です。LeanとRocq（旧Coq）はCIC系の発想を共有しますが、宇宙の累積性、証明無関係性、商、再帰のkernel上の扱いなどに差があります [LEAN-FAQ]。

要点#

PTSは項・型・kindを同じ構文で書き、sort公理とΠ形成規則で役割を判定する。
ラムダ・キューブの三軸は、項による型への依存、型による項への依存、型による型への依存である。
八頂点は三機能の有無による分類で、発明順や強弱だけを表す年代図ではない。
CoCは三軸をすべて持つが、帰納型などを備えるCICやLean 4そのものではない。
形成規則、型判断、計算規則、メタ定理がそれぞれ何を定めるかを混同しない。

研究史と文献案内#

CoquandとHuetは1988年の論文でCoCの基本理論を提示しました [CH88]。Barendregtは1991年、型付きラムダ計算群を一般化型システムとして統一し、CoCを八体系の標準的な立方体として細分しました [BAR91]。ラムダ・キューブはCoCの発明順をそのまま描く年代図ではなく、許される依存規則による包含関係の分類です。

CoC原論文 [CH88] とBarendregtのPTSによる再編 [BAR91] は役割が異なります。CoC・System F・正規化をproof theoryから読むには [GLT89] を参照してください。LeanとCIC系の差は [LEAN-DTT; LEAN-FAQ; LEAN-REF] が扱います。

問題#

PTSの規則から依存の許可範囲を読む#

純粋型システムのsort、公理、Π形成規則をそれぞれ定義せよ。形成規則に現れる三つのsortについて、定義域、値域、形成されるΠ型の分類を順に説明する。同じ構文範疇に項・型・kindを置けても、型判断における役割まで同じになるわけではないことを具体的な判断で示す。

[CH88] のCoCと [BAR91] のPTSによる整理を対照し、原体系の記法と後世の一般化を混同しない表を作れ。表には原典が与える規則、一般化でパラメータ化された部分、本章のLean上のモデルを含める。

ラムダ・キューブを暗記せず復元する#

ラムダ・キューブの三軸を「何が何に依存するか」という文で表し、各軸を追加したときに初めて書ける代表的な型を一つずつ挙げよ。その記述から λP2、λPω、λω の機能を表を見ずに復元し、八頂点を包含関係に従って配置する。

ポリモーフィック恒等関数と、型構成子を引数に取る高階演算を別々の軸へ分類せよ。両者を単に「ジェネリック」と呼ぶと失われる区別を、束縛変数のsortから説明すること。

体系の規則とメタ定理を切り分ける#

型形成規則を列挙することと、その体系について保存、合流性、強正規化を証明することを区別せよ。各メタ定理が何を量化し、どの簡約関係に依存するかを書き、ある規則集合から自動的に全てが従うわけではない理由を述べる。

CoC、CIC、Lean 4の差を比較する。少なくとも帰納型、宇宙、計算・再帰の扱いを比較項目に含める。LeanがCoCの系譜にあるという歴史的説明を、LeanのkernelがCoCそのものであるという同一視へ強めてはならない。