正本：FormalLab/TypeTheory/WTypes.lean

第37章：W型・整礎木・多項式的帰納型#

自然数、リスト、有限分岐木は異なる構成子を持ちますが、各節点で「どの形を選ぶか」と「その形にはどの位置の子があるか」を指定する点は共通しています。この二段階を型 A と型族 B : A → Type で表すと、多くの帰納型を一つの整礎木として記述できます。

本章ではW型 W A B を定義します。節点のラベル a:A と、各位置 b:B a にある部分木から値を作り、 foldで全木を消費します。自然数とリストを具体的に符号化した後、一層の形 Σ(a:A). B(a) → X とW型のroll/unrollを比較します。これにより厳密正値性、始代数、多項式関手へ進む共通語彙を準備します。

一つの節点を形と位置に分ける#

A の要素は節点の形、B a の要素は形 a が持つ子の位置です。各位置へ再びW木を割り当てると一節点ができます。

\frac{a:A\qquad c:B(a)\to W(A,B)} {\mathsf{sup}(a,c):W(A,B)}.

B a が空型なら葉、単位型なら子を一つ、Fin n なら子を n 個持ちます。子をリストで格納するのではなく、位置から部分木への関数として与える点がW型の一般性です。

Leankernel-checked counterpartL29–41

namespace FormalLab.TypeTheory.WTypes

universe u v w

inductive W (A : Type u) (B : A → Type v) : Type (max u v) where
  | sup : (shape : A) → (B shape → W A B) → W A B

def root {A : Type u} {B : A → Type v} : W A B → A
  | .sup shape _ => shape

def children {A : Type u} {B : A → Type v} (tree : W A B) : B (root tree) → W A B :=
  match tree with
  | .sup _ branches => branches

children tree の始域は root tree に依存します。根を先に観察すると、その形に許された位置だけを指定して子を取り出せます。葉の根では位置型が空なので、存在しない子番号を渡すことはできません。

foldは全ての部分木の結果から節点の結果を作る#

結果型 C と、一層の結果をまとめる演算 algebra : (a:A) → (B a → C) → C を与えます。各子を再帰的にfoldし、その結果関数をalgebraへ渡します。

Leankernel-checked counterpartL53–62

def fold {A : Type u} {B : A → Type v} {C : Type w}
    (algebra : (shape : A) → (B shape → C) → C) : W A B → C
  | .sup shape branches =>
      algebra shape (fun position => fold algebra (branches position))

theorem fold_sup {A : Type u} {B : A → Type v} {C : Type w}
    (algebra : (shape : A) → (B shape → C) → C)
    (shape : A) (branches : B shape → W A B) :
    fold algebra (.sup shape branches) =
      algebra shape (fun position => fold algebra (branches position)) := rfl

fold_sup はfoldの計算規則です。帰納原理では結果型 C を木に依存するmotiveへ一般化し、各部分木そのものと帰納仮定をalgebraの場合へ渡します。通常の再帰と依存除去の差は、前章と同じくmotiveの依存度にあります。

自然数は零形と後者形を持つW木である#

形を真偽値とし、false を零、true を後者と読みます。零形の位置は空、後者形の位置は単位型です。

Leankernel-checked counterpartL74–96

def NatPositions : Bool → Type
  | false => Empty
  | true => Unit

abbrev WNat := W Bool NatPositions

def wzero : WNat :=
  .sup false (fun impossible => nomatch impossible)

def wsucc (number : WNat) : WNat :=
  .sup true (fun _ => number)

def toNat : WNat → Nat :=
  fold fun
    | false, _ => 0
    | true, result => result () + 1

theorem toNat_wzero : toNat wzero = 0 := rfl

theorem toNat_wsucc (number : WNat) : toNat (wsucc number) = toNat number + 1 :=
  rfl

theorem toNat_two : toNat (wsucc (wsucc wzero)) = 2 := rfl

wsucc の子関数は単位型の唯一の位置へ前の数を置きます。toNat は零形で 0、後者形で唯一の子の結果に一を加えます。Peano自然数の二構成子が、形と位置の選択へ分解されました。

リストは空形と要素付き形を持つW木である#

要素型 α に対し、形 none を空リスト、some a を先頭要素 a のあるリストとします。後者の子は残りのリスト一つです。

Leankernel-checked counterpartL108–128

def ListPositions {α : Type u} : Option α → Type
  | none => Empty
  | some _ => Unit

abbrev WList (α : Type u) := W (Option α) ListPositions

def wnil {α : Type u} : WList α :=
  .sup none (fun impossible => nomatch impossible)

def wcons {α : Type u} (head : α) (tail : WList α) : WList α :=
  .sup (some head) (fun _ => tail)

def length {α : Type u} : WList α → Nat :=
  fold fun
    | none, _ => 0
    | some _, result => result () + 1

theorem length_wcons {α : Type u} (head : α) (tail : WList α) :
    length (wcons head tail) = length tail + 1 := rfl

theorem length_bool_example : length (wcons true (wcons false wnil)) = 2 := rfl

W符号化は通常の List α と同じAPIを自動的には持ちません。両者の間に相互変換と逆法則を証明して初めて同じ帰納構造を表すといえます。符号化可能性と、Leanの組込みリストが定義的にW型であることを区別します。

一層の多項式とroll/unroll#

型族 X を一層の再帰位置へ代入した形を Layer A B X = Σa:A. B a → X と定めます。W型の構成子は Layer A B (W A B) → W A B、観察は逆向きの関数です。

P_{A,B}(X)=\sum_{a:A}X^{B(a)}, \qquad W(A,B)\cong P_{A,B}(W(A,B)).

Leankernel-checked counterpartL146–163

def Layer (A : Type u) (B : A → Type v) (X : Type w) :=
  Sigma fun shape : A => B shape → X

def roll {A : Type u} {B : A → Type v} : Layer A B (W A B) → W A B
  | ⟨shape, branches⟩ => .sup shape branches

def unroll {A : Type u} {B : A → Type v} : W A B → Layer A B (W A B)
  | .sup shape branches => ⟨shape, branches⟩

theorem roll_unroll {A : Type u} {B : A → Type v} (tree : W A B) :
    roll (unroll tree) = tree := by
  cases tree
  rfl

theorem unroll_roll {A : Type u} {B : A → Type v} (layer : Layer A B (W A B)) :
    unroll (roll layer) = layer := by
  cases layer
  rfl

二つの逆法則はW木が一層の形と部分木へ完全に分解できることを示します。ここから W A B ≅ Σa. B a → W A B という不動点方程式が得られます。ただし、関手、代数、始性はまだ定義していません。後の章で Layer A B を多項式関手として示し、foldの一意性を始代数の普遍性として証明します。

要点#

W型は節点の形 a:A と、その形の位置 B a から部分木への関数で生成される。
空・単位・有限位置型により、葉、一子、有限分岐を同じ構成子で表せる。
foldは全ての子の再帰結果を一層のalgebraへ渡す。
自然数とリストは適切な形・位置族を選んだW型として符号化できる。
roll と unroll は多項式の一層とW型の不動点方程式を示すが、始性は別に証明する。

研究史と文献案内#

W型はMartin-Löf型理論における一般的な整礎木と帰納定義を表す構成です [ML84]。帰納族との関係と一般化は [DYB94] を参照してください。本章の W はLeanで教育用に再定義したもので、Leanの全帰納型が内部でこの宣言へ変換されるという実装主張ではありません。多項式関手、始代数、W型の普遍性は後の圏論および橋章で、それぞれの定義を導入してから扱います。

問題#

形と位置から三種類の木を設計する#

二分木、有限分岐木、各節点が自然数個の子を持つ木について、形型 A と位置族 B を定義してください。葉と内部節点の位置型を具体化し、それぞれの W A B の値を二層以上構成します。存在しない子を要求する式が型付けできない理由を位置型から説明します。三つの符号化について、節点ラベル、分岐数、部分木を格納する関数の始域を同じ表で比較すれば完了です。

Wリストと通常のリストを往復する#

List α → WList α と WList α → List α を定義し、両合成が恒等であることを各側の帰納法で証明してください。 W側の証明で関数として格納された唯一の子をどう扱うかを示します。長さが相互変換で保存されることも導き、符号化と定義的同一性の差を説明します。各逆法則が rfl だけでは終わらない分岐を特定し、そこで使う帰納仮定と関数外延性の有無を記録すれば完了です。

foldを始代数の主張へ翻訳する準備をする#

Layer A B X、roll、任意の algebra : Layer A B C → C を通常の多項式記法へ戻してください。 fold algebra が満たす可換方程式を fold_sup から導きます。さらに同じ方程式を満たす別関数がfoldと等しいという一意性に必要な関数外延性とW帰納法を特定し、後の始代数定理の形を書けば完了です。