正本：FormalLab/Bridges/PolynomialFunctorsAndWTypes.lean

第67章：W型・多項式関手・自由代数——形と位置から帰納構造を作る#

自然数の一層は 1+X でした。リストなら 1+A×X、二分木なら 1+X² です。これらの式は、構成子を選ぶことと、その構成子が要求する再帰的な引数を埋めることに分解できます。形の型を A、形 a の位置の型を B(a) とすれば、一層全体は

P(X)=\sum_{a:A}X^{B(a)} =\sum_{a:A}(B(a)\to X).

です。この形の自己関手を多項式関手と呼びます。本章では第37章で定義したW型をこの関手の始代数として構成します。次に変数を葉として加えた木を作り、それが指定した生成元上の自由代数になることを証明します。

不動点、始代数、自由代数は順に要求が強くなるという単純な序列ではありません。始代数は生成元を持たない普遍対象であり、自由代数は指定した型から代数へ入る写像を普遍化します。自由代数は、変数を定数項として加えた別の自己関手の始代数として表せます。この二つの見方を同じLean定義で照合します。

多項式は形の和と位置の積からできる#

P(X)=Σa.B(a)→X の要素は、形 a と、各位置へ X の要素を置く関数の対です。通常の一変数多項式 Σₙ Aₙ×Xⁿ では次数 n が位置数を表します。依存する位置型 B(a) を使う表現は、形ごとに異なる分岐を一つの式へまとめます。

Leankernel-checked counterpartL30–57

namespace FormalLab.Bridges.PolynomialFunctorsAndWTypes

open _root_.CategoryTheory
open _root_.CategoryTheory.Endofunctor
open _root_.CategoryTheory.Limits
open FormalLab.TypeTheory.WTypes

universe u

def polynomialFunctor (A : Type u) (B : A → Type u) : Type u ⥤ Type u where
  obj X := Layer A B X
  map f := ↾fun layer => ⟨layer.1, fun position => f (layer.2 position)⟩
  map_id X := by
    ext layer
    cases layer
    rfl
  map_comp f g := by
    ext layer
    cases layer
    rfl

example (A : Type u) (B : A → Type u) (X : Type u) :
    (polynomialFunctor A B).obj X = Layer A B X := rfl

example (A : Type u) (B : A → Type u) {X Y : Type u} (f : X → Y)
    (shape : A) (branches : B shape → X) :
    (polynomialFunctor A B).map (↾f) ⟨shape, branches⟩ =
      ⟨shape, fun position => f (branches position)⟩ := rfl

関手の射作用は形を変えず、各位置の値だけを f で写します。map_id と map_comp は、位置ごとの恒等写像と関数合成の法則です。式が対象について多項式らしく見えるだけでは関手になりません。射への作用と二つの関手法則までが必要です。

W型の構成子は多項式代数の構造射である#

W型 W A B の構成子 sup は、一層の形 P(W A B) を一つの木へ畳みます。従って構造射

\mathsf{sup}:P(W_{a:A}B(a))\longrightarrow W_{a:A}B(a)

を持つ P-代数になります。

Leankernel-checked counterpartL75–94

def wAlgebra (A : Type u) (B : A → Type u) : Algebra (polynomialFunctor A B) where
  a := W A B
  str := ↾roll

def wFold {A : Type u} {B : A → Type u}
    (C : Algebra (polynomialFunctor A B)) : W A B → C.a :=
  fold fun shape results => C.str ⟨shape, results⟩

theorem wFold_sup {A : Type u} {B : A → Type u}
    (C : Algebra (polynomialFunctor A B)) (shape : A) (branches : B shape → W A B) :
    wFold C (.sup shape branches) =
      C.str ⟨shape, fun position => wFold C (branches position)⟩ := rfl

def wFoldHom {A : Type u} {B : A → Type u}
    (C : Algebra (polynomialFunctor A B)) : wAlgebra A B ⟶ C where
  f := ↾wFold C
  h := by
    ext layer
    cases layer
    rfl

準同型条件はfoldの計算規則を可換正方形として書いたものです。各子を先にfoldしてから C の構造射で一層を解釈する経路と、先にW木を一節点へ畳んでから全体をfoldする経路が一致します。

W帰納法がfoldの一意性を与える#

始性にはfoldの存在だけでなく一意性が必要です。任意の代数準同型 f は構造射を保存するので、根における値は子における値から決まります。全ての子で f とfoldが一致すると仮定し、W帰納法で木全体の一致を示します。

Leankernel-checked counterpartL106–127

theorem wFold_unique {A : Type u} {B : A → Type u}
    (C : Algebra (polynomialFunctor A B)) (f : wAlgebra A B ⟶ C) :
    f = wFoldHom C := by
  apply Algebra.ext
  ext tree
  induction tree with
  | sup shape branches ih =>
      have h := types_congr_hom f.h ⟨shape, branches⟩
      change C.str ⟨shape, fun position => f.f (branches position)⟩ =
        f.f (.sup shape branches) at h
      change f.f (.sup shape branches) =
        C.str ⟨shape, fun position => wFold C (branches position)⟩
      rw [← h]
      congr 2
      funext position
      exact ih position

def wIsInitial (A : Type u) (B : A → Type u) : IsInitial (wAlgebra A B) :=
  IsInitial.ofUniqueHom (fun C => wFoldHom C) (fun C f => wFold_unique C f)

example (A : Type u) (B : A → Type u) : IsIso (wAlgebra A B).str :=
  Algebra.Initial.str_isIso (wIsInitial A B)

これで第37章では保留した主張が完成しました。roll と unroll の逆法則はW型が P の不動点であることを示します。wIsInitial はさらに、任意の P-代数への準同型が存在して一意であることを示します。証明の追加部分はW帰納法による一意性です。

生成元を加えると自由代数になる#

型 X の各要素を変数として持つ木を考えます。変数は子を持たない葉ですが、署名 A,B の定数構成子とは区別します。

Leankernel-checked counterpartL140–170

inductive FreeTree (A : Type u) (B : A → Type u) (X : Type u) : Type u where
  | var : X → FreeTree A B X
  | sup : (shape : A) → (B shape → FreeTree A B X) → FreeTree A B X

def freeAlgebra (A : Type u) (B : A → Type u) (X : Type u) :
    Algebra (polynomialFunctor A B) where
  a := FreeTree A B X
  str := ↾fun layer => .sup layer.1 layer.2

def generator {A : Type u} {B : A → Type u} {X : Type u} :
    X → (freeAlgebra A B X).a :=
  FreeTree.var

def freeFold {A : Type u} {B : A → Type u} {X : Type u}
    (C : Algebra (polynomialFunctor A B)) (η : X → C.a) : FreeTree A B X → C.a
  | .var x => η x
  | .sup shape branches =>
      C.str ⟨shape, fun position => freeFold C η (branches position)⟩

def freeFoldHom {A : Type u} {B : A → Type u} {X : Type u}
    (C : Algebra (polynomialFunctor A B)) (η : X → C.a) :
    freeAlgebra A B X ⟶ C where
  f := ↾freeFold C η
  h := by
    ext layer
    cases layer
    rfl

theorem freeFoldHom_generator {A : Type u} {B : A → Type u} {X : Type u}
    (C : Algebra (polynomialFunctor A B)) (η : X → C.a) (x : X) :
    (freeFoldHom C η).f (generator x) = η x := rfl

写像 η:X→C は生成元を代数 C でどう解釈するかを指定します。freeFoldHom C η は構成子を保つ代数準同型へ一意に延長されます。ここでの一意性は、変数の場合には延長条件を、節点の場合には準同型条件と帰納仮定を使います。

Leankernel-checked counterpartL178–203

theorem freeFoldHom_unique {A : Type u} {B : A → Type u} {X : Type u}
    (C : Algebra (polynomialFunctor A B)) (η : X → C.a)
    (f : freeAlgebra A B X ⟶ C)
    (hExt : ∀ x, f.f (generator x) = η x) :
    f = freeFoldHom C η := by
  apply Algebra.ext
  ext tree
  induction tree with
  | var x => exact hExt x
  | sup shape branches ih =>
      have h := types_congr_hom f.h ⟨shape, branches⟩
      change C.str ⟨shape, fun position => f.f (branches position)⟩ =
        f.f (.sup shape branches) at h
      change f.f (.sup shape branches) =
        C.str ⟨shape, fun position => freeFold C η (branches position)⟩
      rw [← h]
      congr 2
      funext position
      exact ih position

theorem freeUniversalProperty {A : Type u} {B : A → Type u} (X : Type u)
    (C : Algebra (polynomialFunctor A B)) (η : X → C.a) :
    ∃! f : freeAlgebra A B X ⟶ C, ∀ x, f.f (generator x) = η x := by
  refine ⟨freeFoldHom C η, freeFoldHom_generator C η, ?_⟩
  intro f hExt
  exact freeFoldHom_unique C η f hExt

これは「FreeTree A B X は X 上の自由 P-代数である」という主張です。自由とは要素を好きに選べるという意味ではなく、生成元の写像 η が代数準同型へただ一通り延長されるという普遍性を指します。

自由代数は変数を加えた関手の始代数でもある#

変数を零項構成子として一層へ組み込むと、自己関手

Q_X(Y)=X+P(Y).

を得ます。FreeTree A B X の二構成子は、ちょうど Q_X の構造射を与えます。

Leankernel-checked counterpartL220–282

def polynomialWithVariables (A : Type u) (B : A → Type u) (X : Type u) :
    Type u ⥤ Type u where
  obj Y := X ⊕ Layer A B Y
  map f := ↾fun
    | .inl x => .inl x
    | .inr layer => .inr ⟨layer.1, fun position => f (layer.2 position)⟩
  map_id Y := by
    ext value
    cases value with
    | inl x => rfl
    | inr layer => cases layer; rfl
  map_comp f g := by
    ext value
    cases value with
    | inl x => rfl
    | inr layer => cases layer; rfl

def freeTreeAsAlgebra (A : Type u) (B : A → Type u) (X : Type u) :
    Algebra (polynomialWithVariables A B X) where
  a := FreeTree A B X
  str := ↾fun
    | .inl x => .var x
    | .inr layer => .sup layer.1 layer.2

def freeTreeInitialFold {A : Type u} {B : A → Type u} {X : Type u}
    (C : Algebra (polynomialWithVariables A B X)) : FreeTree A B X → C.a
  | .var x => C.str (.inl x)
  | .sup shape branches =>
      C.str (.inr ⟨shape, fun position => freeTreeInitialFold C (branches position)⟩)

def freeTreeInitialHom {A : Type u} {B : A → Type u} {X : Type u}
    (C : Algebra (polynomialWithVariables A B X)) : freeTreeAsAlgebra A B X ⟶ C where
  f := ↾freeTreeInitialFold C
  h := by
    ext value
    cases value with
    | inl x => rfl
    | inr layer => cases layer; rfl

theorem freeTreeInitialHom_unique {A : Type u} {B : A → Type u} {X : Type u}
    (C : Algebra (polynomialWithVariables A B X))
    (f : freeTreeAsAlgebra A B X ⟶ C) : f = freeTreeInitialHom C := by
  apply Algebra.ext
  ext tree
  induction tree with
  | var x =>
      have h := types_congr_hom f.h (Sum.inl x)
      exact h.symm
  | sup shape branches ih =>
      have h := types_congr_hom f.h (Sum.inr ⟨shape, branches⟩)
      change C.str (.inr ⟨shape, fun position => f.f (branches position)⟩) =
        f.f (.sup shape branches) at h
      change f.f (.sup shape branches) =
        C.str (.inr ⟨shape, fun position => freeTreeInitialFold C (branches position)⟩)
      rw [← h]
      congr 3
      funext position
      exact ih position

def freeTreeIsInitial (A : Type u) (B : A → Type u) (X : Type u) :
    IsInitial (freeTreeAsAlgebra A B X) :=
  IsInitial.ofUniqueHom (fun C => freeTreeInitialHom C)
    (fun C f => freeTreeInitialHom_unique C f)

二つの普遍性は同じ再帰計算を別の圏で述べます。freeUniversalProperty は P-代数と生成元写像の組への一意な準同型を述べます。freeTreeIsInitial は生成元を Q_X の定数構成子へ移し、通常の始対象の言葉で述べます。この翻訳を介さず「始代数だから自由代数」とだけ言うと、何の上で自由なのかが消えてしまいます。

要点#

多項式関手 P(X)=Σa.B(a)→X は形を保存し、各位置の値を射で写す。
W型の構成子は P(W)→W という代数構造であり、W帰納法がfoldの一意性を与える。
不動点同型に一意な代数準同型を加えたものがW型の始代数性である。
変数を葉として持つ FreeTree A B X は、生成元写像を一意に延長する X 上の自由 P-代数である。
同じ自由代数は、変数を定数項として加えた自己関手 Q_X(Y)=X+P(Y) の始代数としても表せる。
「自由」は生成元の型と忘却先を指定した普遍性であり、始代数という語だけではその基底を表せない。

研究史と文献案内#

Martin-Löf型理論におけるW型は [ML84]、帰納族への一般化は [DYB94] を参照してください。始代数意味論をプログラム意味論と結ぶ研究は [GTWW77] に遡ります。Gambino–Hyland [GH04] はW型と依存多項式関手を局所デカルト閉圏で研究し、広い関手類の始代数との関係を示しました。本章は Type 上の非依存な一変数多項式関手に範囲を限定しており、[GH04] の依存多項式関手全体を形式化したものではありません。 Leanコードは教育用の W とmathlibの Endofunctor.Algebra を接続します。mathlib固有の現行APIは [MATHLIB] に従い、組込み帰納型の内部表現に関する主張は行いません。

問題#

自然数とリストの多項式を回収する#

第37章の NatPositions と ListPositions を polynomialFunctor へ代入してください。自然数では Σb:Bool.NatPositions(b)→X が 1+X、リストでは Σo:Option A.ListPositions(o)→X が 1+A×X と同値であることを、両方向の関数と逆法則で示します。同値が対象ごとにあるだけでなく、射の作用と可換して自然同型になるために必要な式も書き、単なる要素数の一致との差を説明できれば完了です。

W型の始性証明を可換図式から再構成する#

任意の P-代数 C に対する wFoldHom C の準同型条件を、形と位置関数を明示した等式へ展開してください。次に別の準同型 f をW帰納法で比較します。帰納仮定が一つの値ではなく ∀b:B(a) という族になる理由を構成子の型から説明し、関数外延性を適用する正確な位置をLean証明と数式の双方で特定できれば完了です。

自由代数の二つの普遍性を往復する#

freeUniversalProperty から freeTreeIsInitial を導くため、Q_X-代数から P-代数と生成元写像を取り出してください。逆に P-代数 C と η:X→C から Q_X-代数を作ります。二つの変換が準同型条件を保存し、一意性の主張を対応させることを示します。どの圏の始対象を述べているかを各段階で明記できれば完了です。

多項式ではない厳密正値関手との境界を調べる#

本章の表示 Σa.B(a)→X が和・積・冪をどのように表すかを整理し、商や関数空間の共変な組合せを含む厳密正値関手が同じ表示を持つか検討してください。表示可能性、関手性、始代数の存在を別々の主張として扱い、一つが失敗しても他の二つが直ちに否定されない例を挙げます。Leanの正値性検査と圏論的な多項式関手の定義を同一視できない理由を、受理条件と普遍性の差から説明できれば完了です。