第56章：自己関手の余代数と余代数準同型#

代数の構造射 F(A)→A は一層分の部品を値へ組み立てました。矢印を反転した射 S→F(S) は、状態を 一段観察して、その観察結果と次の状態へ分解します。これが自己関手の余代数です。

有限データを構成する代数に対し、余代数は遷移系、潜在的に無限なストリーム、部分計算などを記述します。 本章ではOption自己関手で停止し得る状態遷移を構成し、余代数準同型が観察を保つ可換正方形を定義します。 次章では全ての余代数から一意な準同型を受ける終余代数とanamorphismへ進みます。

一段観察は状態を形と次状態へ分ける#

圏 C の自己関手 F:C→C に対し、F-余代数は対象 S と構造射

$$c:S\to F(S).$$

から成ります。c は状態を破壊的に消費する操作ではなく、圏の射として一段の観察を与えます。

namespace FormalLab.CategoryFoundations.EndofunctorCoalgebras

open _root_.CategoryTheory
open _root_.CategoryTheory.Endofunctor
open FormalLab.CategoryFoundations.EndofunctorAlgebras

universe v u

variable {C : Type u} [Category.{v} C]
variable {F : C ⥤ C}
variable (S : Coalgebra F)

example : C := S.V
example : S.V ⟶ F.obj S.V := S.str

余代数には余モナドの余単位・余乗法との整合条件はありません。自己関手余代数 Coalgebra F と、余モナドの Eilenberg–Moore余代数を区別します。

Option余代数は停止し得る一段遷移である#

F(X)=Option X なら、構造射 S→Option S は各状態で停止するか、次状態を一つ返します。自然数を残り回数と するcountdownを定義します。

def countdownStep : Nat → Option Nat
  | 0 => none
  | n + 1 => some n

def countdownCoalgebra : Coalgebra optionEndofunctor where
  V := Nat
  str := ↾countdownStep

theorem countdown_stops_at_zero : countdownStep 0 = none := rfl
theorem countdown_four_steps_to_three : countdownStep 4 = some 3 := rfl

def runCountdown : Nat → List Nat
  | 0 => [0]
  | n + 1 => (n + 1) :: runCountdown n

#eval runCountdown 4

theorem runCountdown_length (n : Nat) : (runCountdown n).length = n + 1 := by
  induction n with
  | zero => rfl
  | succ n inductionHypothesis =>
      simp [runCountdown, inductionHypothesis, Nat.add_assoc]

[4, 3, 2, 1, 0]

runCountdown は外部から有限回観察した結果を集める補助関数です。余代数自身は全実行列をデータとして 持たず、一段観察だけを指定します。有限停止性や生産性は構造射の型だけからは従わず、別に証明します。

余代数準同型は観察を保つ#

余代数 (S,c), (T,d) の間の準同型は射 f:S→T で

$$c;F(f)=f;d.$$

を満たします。

左経路は元の状態を観察して次状態を写し、右経路は状態を写してから観察します。

variable {S T : Coalgebra F}
variable (f : S ⟶ T)

example : S.V ⟶ T.V := f.f
example : S.str ≫ F.map f.f = f.f ≫ T.str := f.h

def countdownIdentity : countdownCoalgebra ⟶ countdownCoalgebra where
  f := 𝟙 _

example : countdownIdentity.f = 𝟙 Nat := rfl

準同型は内部状態の表現を変えても一段観察を一致させます。忠実な状態符号化だけでなく、複数状態を同じ振舞いへ まとめる写像もあり得ます。終余代数への一意な準同型は各状態をその完全な観察振舞いへ送ります。

余代数の圏#

恒等射と合成は観察保存条件を保つため、F-余代数は圏をなします。忘却関手は台状態対象と台射だけを残します。

example : Category (Coalgebra F) := inferInstance
example : Coalgebra F ⥤ C := Coalgebra.forget F

代数との双対性#

C 上の F-余代数は、適切に反対圏へ移した自己関手上の代数として読めます。構造射、準同型の正方形、 始性・終性が全て反転します。ただし同じ圏の中で F(A)→A を単に逆向きに書けるわけではありません。 反対圏上の関手と射の型を同時に変える必要があります。

双模倣への入口#

二状態が同じ一段観察を持ち、対応する次状態も再び関係するとき、その関係を双模倣と呼びます。終余代数が 存在すると、二状態が同じ終余代数上の振舞いへ写ることと双模倣可能性が適切な条件下で対応します。本章では 準同型による観察保存までを扱い、関係持ち上げと双模倣原理は終余代数および橋章で明示します。

要点#

• 自己関手 F の余代数は対象 S と一段観察 S→F(S) から成る。
• Option余代数は停止または次状態を返す部分的な遷移系を表せる。
• 余代数の型だけでは停止性、生産性、無限実行の存在は保証されない。
• 余代数準同型は c;F(f)=f;d により一段観察を保つ。
• 自己関手余代数、余モナド代数、終余代数、双模倣は段階の異なる概念である。

研究史と文献案内#

余代数による状態遷移系の統一は、代数の双対化から発展し、計算機科学では振舞意味論と双模倣の基盤になりました。 Rutten [RUT00] は集合上の多様なシステムを普遍余代数として統一する代表的研究です。始代数との対称性と存在条件は [AMM25]、mathlibの Endofunctor.Coalgebra と Coalgebra.Hom は [MATHLIB] を参照してください。

問題#

停止し得る遷移の準同型を作る#

自然数countdownを、正の自然数だけを二段ずつ減らす別表現へ符号化してください。候補写像がOption余代数準同型に なるか、零、奇数、偶数で可換正方形を検査します。成立しない候補では、状態写像と一段観察のどちらが情報を 失いすぎたかを最小の反例から特定し、単なる関数と観察保存写像を区別できれば完了です。

余代数準同型の合成を証明する#

三余代数と準同型 f:S→T, g:T→U を置き、c;F(f;g)=(f;g);e を関手の合成保存則と二つの可換正方形から 導いてください。恒等射の場合も検査し、余代数圏の結合律自体は台圏から、構造保存の閉性は自然な等式計算から 得られることを分離して説明してください。代数準同型の証明と全ての射向きが逆になる一方、台射の合成順は 変わらないことまで比較できれば完了です。

代数の定義を反対圏で双対化する#

C 上の自己関手 F から反対圏上の対応する関手を仮定し、F-余代数の構造射と準同型条件が代数の条件へ どう移るかを全ての始域・終域つきで書いてください。射一つだけを反転しても型が合わないことを確認し、 始代数が終余代数へ移るまでの定義列を復元してください。さらにLambekの補題の二つの逆法則を双対化し、 構造射の同型性が同じ証明図式から得られることを示せれば完了です。