正本：FormalLab/Foundation/Universes.lean

第5章：宇宙階層と宇宙多相#

自然数が型を持つように、型自身も形式体系の式であるなら分類が必要です。しかし Type : Type として一つの領域へ閉じ込めると、十分に強い依存型理論では逆理を構成できます。型について型の内部で語る能力を保ちながら、この循環をどう制御するかが宇宙の問題です。

本章では $\mathsf{Type}_0:\mathsf{Type}_1:\mathsf{Type}_2:\cdots$ という階層と、一つの定義を任意の階層で再利用する宇宙多相を導入します。後の命題、依存型、圏のサイズ条件に現れる宇宙変数を、単なるLeanの記号ではなく理論上の仮定として読めるようにします。

型自身に型を与えるときの階層#

型理論では型自身も項として分類されます。しかし全てを一つの自己所属 Type : Type にすると、依存関数型を備えた十分に強い体系ではGirardの逆理に至り、論理として不整合になります。問題は「自己参照は何となく危険」という印象ではなく、型を分類する型を同じ階層へ無制限に戻す規則が強すぎることです。宇宙階層を持つ体系では代わりに

\mathsf{Type}_u:\mathsf{Type}_{u+1}

という階層を使います。Type は Type 0 の略です。universe u は特定の数値へ固定しないレベル変数 u を宣言し、Type u はそのレベルにある型の宇宙を表します。

宇宙を一段ずつ分類する#

Type 0 : Type 1 は、左辺の宇宙に属する全ての型が右辺の項だという意味ではありません。正確には式 Type 0 自身の型が Type 1 です。通常の型 Nat : Type 0 と並べると、一段ずつ上がる構造が見えます。

0:\mathsf{Nat},\qquad \mathsf{Nat}:\mathsf{Type}_0,\qquad \mathsf{Type}_0:\mathsf{Type}_1,\qquad \mathsf{Type}_1:\mathsf{Type}_2.

Leanにおける`Sort`と`Type`#

Leanでは Type u は Sort (u + 1) の記法です。次章で導入する Prop は Sort 0 で、通常の型宇宙とは異なる証明用の規則を持ちます。Sort はこれらを統一して表記する最上位の構文であり、「全sortを含む一つの最大sort」ではありません。

Leanのレベル記法を数式へ移すと

\mathsf{Prop}=\mathsf{Sort}(0), \qquad \mathsf{Type}_u=\mathsf{Sort}(u+1)

です。添字 $u$ は宇宙の項ではなく、宣言をインスタンス化するときに解かれるメタレベルのレベル式です。

なぜ一般の定義に宇宙変数が要るのか#

「関数・適用・合成」の identity {α : Type} は α : Type 0 に限られます。多くの値には十分ですが、 Type 自身を入力型に選ぶことはできません。ライブラリの恒等関数や合成を型の大きさに関係なく再利用するには、特定のレベルでなく変数 u を使う必要があります。

ここでいう宇宙多相は、同じ宣言を各宇宙レベルへインスタンス化できるという意味です。値や型を引数に取る通常のパラメトリック多相とは、一般化している対象が違います。

Leankernel-checked counterpartL68–68

universe u v w

一つの定義を全宇宙で使う#

任意の宇宙レベルの型で働く恒等関数です。

Leankernel-checked counterpartL74–75

def polymorphicIdentity {α : Type u} (x : α) : α :=
  x

入力二型が異なる宇宙レベルにあっても使える定数関数です。

Leankernel-checked counterpartL78–79

def polymorphicConstant {α : Type u} {β : Type v} (x : α) (_ : β) : α :=
  x

三つの宇宙レベルを独立に一般化した関数合成です。

Leankernel-checked counterpartL82–89

def polymorphicCompose {α : Type u} {β : Type v} {γ : Type w}
    (g : β → γ) (f : α → β) : α → γ :=
  fun x => g (f x)

#check Type
#check Type 1
#check @polymorphicIdentity
#check @polymorphicCompose

出力

Type : Type 1

出力

Type 1 : Type 2

出力

@polymorphicIdentity : {α : Type u_1} → α → α

出力

@polymorphicCompose : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (β → γ) → (α → β) → α → γ

polymorphicIdentity では α := Type とでき、そのとき α は Type 1 に属します。先に定義した非宇宙多相な identity は α : Type 0 に固定されているため、この使い方を持ちません。

Leankernel-checked counterpartL96–96

#check polymorphicIdentity (α := Type) Nat

出力

polymorphicIdentity Nat : Type

出力宇宙は入力から計算される#

二つの型を組にする Prod は、入力が異なる宇宙にあっても使えます。結果の宇宙は通常、両入力レベルの最大値で決まります。宇宙レベルは実行時の整数データではなく、型検査時に解かれる式です。

\alpha:\mathsf{Type}_u,\ \beta:\mathsf{Type}_v \quad\Longrightarrow\quad \alpha\times\beta:\mathsf{Type}_{\max(u,v)}.

Leankernel-checked counterpartL112–113

#check Prod
#check @Prod

出力

Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)

出力

Prod : Type u_1 → Type u_2 → Type (max u_1 u_2)

依存関数型のレベル式 `imax`#

Leanの最も一般の規則では、 $A:\mathsf{Sort}(u)$ と各 $x:A$ に対する $B(x):\mathsf{Sort}(v)$ から

(\Pi x:A.\,B(x)):\mathsf{Sort}(\operatorname{imax}(u,v))

を得ます。imax u v は値域のレベル $v$ が0なら0、そうでなければ max u v です。

\operatorname{imax}(u,v)= \begin{cases} 0 & (v=0),\\ \max(u,v) & (v\ne0). \end{cases}

値域が Prop = Sort 0 なら、どの宇宙の対象を量化しても依存関数型全体は Prop に留まります。これがLeanの Prop の非可述性です。値域が Type v = Sort (v+1) ならレベルは0でないため、通常の最大値規則へ戻ります。直積の max と命題量化の imax は別々の暗記項目ではなく、この一般則の二場合です。

異なる宇宙にある二型の直積は、レベルの最大値に属します。

Leankernel-checked counterpartL141–142

def universeProduct (α : Type u) (β : Type v) : Type (max u v) :=
  α × β

任意の宇宙の型を量化しても、値域が命題なら全体は Prop です。

Leankernel-checked counterpartL145–146

def allInUniverse (α : Type u) (p : α → Prop) : Prop :=
  ∀ x, p x

universeProduct の出力注釈は max の場合を、allInUniverse の出力注釈は imax u 0 = 0 の場合を kernelに検査させます。どちらも宇宙レベルを実行時に計算する関数ではなく、型の整合性を表す宣言です。

{α : Type u} は型についての暗黙引数、u はその型が属する宇宙についての暗黙の一般性です。前章までの Type 版は誤りではなく、u = 0 に限定した特殊例でした。

u、v、w を独立に置くのは、三型が同じ大きさだと仮定する理由がないからです。必要ならLeanがレベル制約を解き、宣言を具体的な宇宙へインスタンス化します。

非累積性と明示的な持ち上げ#

Lean 4の型宇宙は非累積です。α : Type u だからといって、同じ式 α が自動的に Type (u + 1) の項として扱われるわけではありません。異なる階層へデータを移す必要がある場合は ULift のような明示的な型構成を使います。これは値を失わず宇宙だけを上げる操作で、自己所属を許す操作ではありません。

Leankernel-checked counterpartL166–167

#check ULift
#check ULift.up

出力

ULift.{r, s} (α : Type s) : Type (max s r)

出力

ULift.up.{r, s} {α : Type s} (down : α) : ULift α

宇宙階層だけからは従わないこと#

宇宙多相は、一つの定義を各宇宙レベルで再利用する仕組みです。「全ての型を要素として持ち、自分自身も要素である一つの型」を作る仕組みではありません。命題の宇宙 Prop にはさらに証明に固有の規則があり、「命題・証明・含意」で導入します。「純粋型システム、ラムダ・キューブ、構成計算」では、Leanの階層を古典的なラムダ・キューブの二sort表示と比較します。

宇宙階層はRussellの分岐型理論そのものでも、集合論の階数階層そのものでもありません。逆理を避けるという問題意識を共有しても、形成規則と同一性の基準が異なります。

要点#

型も項なので型を必要としますが、Type : Type とはせず Type u : Type (u + 1) と階層化します。宇宙変数は一つの定義を各階層で再利用する一般性を表し、宇宙多相は通常の型引数の多相性とは別です。Lean 4の型宇宙は非累積で、階層移動は明示します。

研究史と文献案内#

Russellの分岐型理論 [RUS08] は、論理的悪循環を制御するための階層です。Martin-Löf型理論の宇宙 [ML84] やLeanの非累積な宇宙階層とは同一ではありません。PTSにおけるsort公理と積形成規則は [BAR91]、Leanの Sort、max、imax、宇宙多相の現行仕様は [LEAN-REF] を参照します。

問題#

コロンの連鎖を三つの判断へ戻す#

0 : Nat : Type : Type 1 という略記を三つの独立した判断へ分解し、各判断で左辺が項なのか型なのかを述べてください。 #check Type、#check Type 1、#check Type 2 の出力を予想して確かめ、一般の Type u : Type (u + 1) へ引き上げます。

次に、仮に Type : Type を許した場合と、実際の宇宙変数 u を使った場合を対比します。宇宙多相が階層を消すのではなく、定義ごとに階層番号を一般化することを、一つの具体的な型付け例で示してください。

宇宙変数が一つでは足りない定義を診断する#

polymorphicCompose の始域、中間型、終域をそれぞれ Type u、Type v、Type w に属させます。そのうえで、三変数が独立である使用例を作ります。次に三変数を一つに固定した版を書き、その版では表現できない合成を示します。

非宇宙多相な identity、polymorphicIdentity、ULift について、「定義を再利用する宇宙」「値が実際に属する宇宙」「型を明示的に持ち上げるか」を比較表にします。三者を単なる「汎用化」の強弱として並べない説明が必要です。

`max` と `imax` を仕様から読み、具体例へ適用する#

α : Type u、β : Type v に対する Prod α β : Type (max u v) を、u < v、u = v、v < u の三場合に分けて計算します。各場合で出力宇宙が両成分を収容できる最小の階層になることを説明してください。

[LEAN-REF] の宇宙節で max と imax の定義上の役割を確認し、非依存直積と依存関数型の宇宙計算を比較します。解答には仕様の該当節を明記し、引用した規則がどのLean型に現れるかを少なくとも一例示します。