正本：FormalLab/TypeTheory/SubtypesAndRefinements.lean

第34章：部分型と篩型#

自然数全体ではなく正の自然数だけを受け取る関数を考えます。呼び出すたびに 0 < n を仮定として渡す代わりに、値 n と条件の証明を一つの型へまとめれば、検査済みという事実を関数の入口で再利用できます。この「値の集合を述語で絞る」発想には、基礎理論と型検査方式の異なる複数の篩型（refinement type）があります。

本章ではLeanの Subtype を値成分と証明成分から構成し、検査前の値から安全に移る境界を Option で表します。その後、一般の篩型、述語集合、Σ型、添字付き帰納族との違いを比較します。この比較により、Leanの部分型を篩型研究全体と同一視しない基準を得ます。

値とその値が満たす条件を一つの型にする#

型 $A$ と述語 $P:A\to\mathsf{Prop}$ から、条件を満たす値だけを集める型を

\{x:A\mid P(x)\}

と書きます。この記号が集合の内包表記か篩型かは文献の基礎理論に依存します。型理論的には項を作るために a : A と p : P(a) の両方が必要です。

Leanの {x : A // P x} は Subtype P の記法です。項は val : A と property : P val を持ち、第二成分は Prop の証明です。

「篩う」とは、元の値を実行時に自動検査して除外することとは限りません。Leanの部分型を直接構成するときは、値だけでなく条件の証明も渡します。いったん構成できれば、利用側は条件を再検査せず property として使えます。証明責任が消えるのではなく、値を作る境界へ移動します。

Leankernel-checked counterpartL37–37

namespace FormalLab.TypeTheory.SubtypesAndRefinements

値と条件の証明を同時に構成する#

部分型の形成・導入・除去を分けて読みます。

形成：α : Type と p : α → Prop から {x : α // p x} を作る。
導入：value : α と proof : p value から ⟨value, proof⟩ を作る。
除去：n.val で元の値、n.property でその値に対応する証明を得る。

第二成分の型に第一成分が現れるため、誤った値と正しい証明を別々に組み合わせることはできません。

形成・導入・二つの射影は、通常の記法では次の判断として表せます。

\frac{A:\mathsf{Type} \qquad P:A\to\mathsf{Prop}} {\{x:A\mid P(x)\}:\mathsf{Type}} \qquad \frac{a:A \qquad p:P(a)} {\langle a,p\rangle:\{x:A\mid P(x)\}}

\pi_1\langle a,p\rangle \equiv a \qquad \pi_2\langle a,p\rangle : P(\pi_1\langle a,p\rangle).

記号 $\equiv$ は、ここでは射影を計算すると定義展開だけで同じ項へ簡約されることを表します。Leanでは $\pi_1$ が .val、 $\pi_2$ が .property、対 $\langle a,p\rangle$ が ⟨a, p⟩ に対応します。

正であるという証明を伴う自然数です。

Leankernel-checked counterpartL72–73

def PositiveNat :=
  {n : Nat // 0 < n}

値 1 と 0 < 1 の証明を組にします。

Leankernel-checked counterpartL76–77

def one : PositiveNat :=
  ⟨1, Nat.zero_lt_succ 0⟩

値を増やすと同時に、正値性も保存します。

Leankernel-checked counterpartL80–81

def succ (n : PositiveNat) : PositiveNat :=
  ⟨n.val + 1, Nat.zero_lt_succ n.val⟩

通常の自然数を検査し、証明できた場合だけ正の自然数へ精密化します。

Leankernel-checked counterpartL84–85

def toPositive? (n : Nat) : Option PositiveNat :=
  if h : 0 < n then some ⟨n, h⟩ else none

入力 n の正値性検査について、成功値または0である証明を保持します。

Leankernel-checked counterpartL88–90

inductive PositiveClassification (n : Nat) where
  | positive (value : PositiveNat) (sameValue : value.val = n)
  | zero (proof : n = 0)

検査失敗時にも、入力が0だったという証明を残します。

Leankernel-checked counterpartL93–100

def classifyPositive (n : Nat) : PositiveClassification n :=
  if h : 0 < n then
    .positive ⟨n, h⟩ rfl
  else
    .zero (Nat.eq_zero_of_not_pos h)

#eval (toPositive? 3).map Subtype.val
#eval (toPositive? 0).map Subtype.val

出力

some 3

出力

none

toPositive? は外部から未検証の値を受け取る境界の一例です。if h : 0 < n は条件を判定するだけでなく、真の分岐へ証明 h を導入します。任意の Prop が自動的に判定可能なわけではないので、この変換は一般の部分型について常に書けるわけではありません。

Option の none は失敗理由を保持しません。classifyPositive は成功側に証明付きの値と元の入力との等式を、失敗側に n = 0 の証明を返します。自然数では「正でない」と「0」が一致するために書ける分類です。一般の型と述語では、否定側に返せるのは通常 $\neg P(a)$ であり、さらに具体的な理由が得られるとは限りません。

入力型に事前条件を持たせる#

正値性は入力の .property から再利用できます。

Leankernel-checked counterpartL115–116

theorem positiveProperty (n : PositiveNat) : 0 < n.val :=
  n.property

正の入力だけを受け取るため、関数内部に失敗分岐がありません。

Leankernel-checked counterpartL119–122

def predecessor (n : PositiveNat) : Nat :=
  n.val - 1

example : predecessor one = 0 := rfl

上界未満という条件を引数化した部分型です。

Leankernel-checked counterpartL125–129

def Below (bound : Nat) :=
  {n : Nat // n < bound}

def zeroBelowSucc (bound : Nat) : Below (bound + 1) :=
  ⟨0, Nat.zero_lt_succ bound⟩

証明成分ではなく値成分が部分型の同一性を決める#

値成分が等しい二つの部分型の項は等しい。

Leankernel-checked counterpartL134–135

theorem ext {m n : PositiveNat} (sameValue : m.val = n.val) : m = n :=
  Subtype.ext sameValue

Subtype.ext が証明成分の等しさを要求しないのは、Prop の証明無関係性によります。ただし、条件 p が不要だという意味ではありません。値を構成し利用可能な操作を制限する役割は型検査時に果たし、同じ値に付いた証明の作り方だけを同一性から無視します。

Leankernel-checked counterpartL143–145

#eval one.val
#eval (succ one).val
#check (bound : Nat) → Below (bound + 1)

出力

(bound : Nat) → Below (bound + 1) : Type

`Subtype`の等式と証明無関係性#

Leanの {x : α // p x} は Subtype p の記法で、値フィールド val と Prop に属する証明フィールド property を持ちます。Subtype.ext が値成分の等式だけを要求するのは、一般の篩型という語の定義からではなく、Leanの Prop における証明無関係性から従います。自動的な制約解消やSMTによる型検査も Subtype 自体の機能ではありません。

部分型と一般の篩型#

一般の篩型システムには、決定可能な述語だけを許す設計、SMTで条件を自動証明する設計、実行時検査を挿入する設計などがあります。Leanの Subtype は任意の Prop の証明項を利用者が構成する依存型です。自動化の有無や実行方式まで含めて同一だとはしません。

条件を型へ移すと利用側は安全になりますが、構成側は証明を要求されます。これは情報を消す最適化ではなく、証明責任を境界へ移動する設計です。

部分型は既存の型から値を選ぶので、後の添字付き帰納族のようにデータの構成方法そのものを再設計するわけではありません。また述語集合 α → Prop は所属条件だけですが、部分型は実際の値とその所属証明を項として持ちます。

述語・部分型・存在命題・依存対を分ける#

同じ記号を似た目的で使えても、次の四つは所属するsortと除去規則が異なります。

表現	Leanでの代表形	属するsort	項が保持するもの
述語	`P : α → Prop`	関数型	値ごとの命題を返す規則
部分型	`{x : α // P x}`	`Sort (max 1 u)`	実行時の値 `x` と、消去される証明
存在命題	`∃ x : α, P x`	`Prop`	命題が真である証拠。一般のデータへ証人を取り出せない
依存対	`Σ x : α, B x`	`Type`	第一成分と、それに依存する計算上のデータ

述語 $P$ は「どの値を選ぶか」を記述しますが、それ自体は選ばれた値ではありません。部分型は射影 $\pi_1:\{x:A\mid P(x)\}\to A$ を持つため、項から元の値を計算に使えます。存在命題は命題全体が Prop に属し、 Leanの制限付き除去により、一般のデータ型へ証人を取り出すプログラムは定義できません。

依存対 $\Sigma x:A.\,B(x)$ では第二成分 $B(x)$ も計算上のデータです。部分型では第二成分が Prop の証明なので、 Leanのコンパイラはそれを消去し、実行時には基底型の値と同じ表現を使います。このゼロオーバーヘッド性と Subtype.ext の等式原理はLean固有の Prop とコンパイル規則に由来し、篩型一般の定義からは従いません。

仕様として強くしても値は増えない#

二つの述語 $P,Q:A\to\mathsf{Prop}$ が全ての $x$ について $Q(x)\to P(x)$ を満たすとします。このとき、より強い条件 $Q$ の部分型から $P$ の部分型へ、値を変えずに写せます。

より強い条件の部分型を、値を保ったまま弱い条件の部分型へ写します。

Leankernel-checked counterpartL195–202

def weakenSubtype {α : Type} {p q : α → Prop}
    (implies : ∀ x, q x → p x) : Subtype q → Subtype p
  | ⟨x, hx⟩ => ⟨x, implies x hx⟩

theorem weakenSubtype_preserves_value {α : Type} {p q : α → Prop}
    (implies : ∀ x, q x → p x) (x : Subtype q) :
    (weakenSubtype implies x).val = x.val :=
  rfl

数学的には、含意 $\forall x.\,Q(x)\to P(x)$ が部分型間の忘却写像を誘導します。Leanの weakenSubtype では値成分をそのまま保ち、証明成分だけを含意で変換します。逆向きには一般に写せません。弱い条件 $P(x)$ から強い条件 $Q(x)$ は導けないからです。篩型の「精密さ」は値へ新しい計算を施す順序ではなく、要求する述語の強さによる順序として現れます。

要点#

部分型 {x : α // p x} の項は値 x と、その値についての証明 p x を持つ。
条件を入力型へ移すと、利用側は証明済みの事前条件を再利用できる。
未検証値から部分型を作るには証明が必要で、判定可能なら Option を返す検査境界も書ける。
証明無関係性により、同じ値を持つ部分型の項は証明の作り方によらず等しい。
述語集合・部分型・添字付き帰納族は、似た不変条件を異なる位置に持たせる。

研究史と文献案内#

Freeman–Pfenningの1991年の篩型 [FP91] は、MLのdatatypeを精密化する体系です。 Leanの Subtype と同じ型形成・推論方式ではありません。その後の篩型研究には決定手続き、制約生成、SMT連携など複数の設計があります。型精密化を言語体系の中で比較するには [PFPL16]、Leanの Subtype と証明無関係性の現行仕様は [LEAN-REF] を参照します。

問題#

値と性質を一つの項として構成する#

one : PositiveNat の値成分と証明成分を指し、PositiveNat を Nat へ射影したとき何が失われるかを説明せよ。二つの正の自然数の和を再び PositiveNat として返す関数を定義し、値の計算と閉性の証明を分けて記述する。

対照として {n : Nat // n < 0} の項を構成しようとし、失敗が自然数の値の不足ではなく証明成分の不可能性に由来することを構成子の型から示す。

検査から精密な型へ移す#

toPositive? の成功・失敗の各分岐で得られる仮定を展開し、実行時の比較結果が後続の証明でどう使われるかを追え。入力が正なら証明付きの値を返し、そうでなければ失敗の理由を返す改良版を設計し、結果型が保持する情報を比較する。

述語を判定することと、述語の証明を型の成分として保存することを区別せよ。全ての述語が計算可能な判定手続きを持つわけではない点も、構成と検証を混同せずに説明すること。

三つの精密化表現と研究史を比較する#

偶数を、述語集合、Leanの部分型、偶数専用の帰納型で表現し、構成・除去・計算・証明の再利用を比較せよ。同じ外延を表していても、どの情報を構文へ組み込むかで帰納原理と定義的計算が変わる。

さらに [FP91] の篩型とLeanの Subtype を、基礎言語、型検査、証明項の保持の三点で比較する。「篩型」は広い研究領域の標準訳として用いつつ、特定の体系とLeanの一構成子を同一視しない記述にすること。