第8部 型・計算・圏を結ぶ

問題1再帰子から始代数性を再構成する

Problem

問題

任意の 1+X-代数 A に対し、自然数再帰子から fold_A を定義してください。基底・後者の計算規則から fold_A が代数準同型であることを示します。次に任意の準同型 f が同じ二方程式を満たすことを構造射の可換条件から取り出し、自然数帰納法で f=fold_A を証明してください。存在と一意性がどの原理を使ったかを別々に記録できれば完了です。

ヒント

任意のF代数αへのfoldを再帰子で作り、η則から一意性を示します。

解答

帰納型μFの構成子 in:FμF→μF と再帰子が、各αに fold α:μF→A および in≫fold α=F(fold α)≫α を与えるとします。さらに同じ方程式を満たすhについて帰納的η則 h=fold α があれば、 foldは唯一の代数準同型です。従って (μF,in) は始F代数。計算規則だけでは存在を与えるに留まり、始性には関数一意性を与えるη原理または帰納法が必要です。

言語仕様の再帰子を圏論的普遍性へ格上げするとき、存在・計算・一意性を別々に確認します。

Lean検査済みL247–260

def foldNat {A : Type} (zero : A) (successor : A → A) : Nat → A
  | 0 => zero
  | n + 1 => successor (foldNat zero successor n)

theorem foldNatUnique {A : Type} (zero : A) (successor : A → A)
    (candidate : Nat → A)
    (atZero : candidate 0 = zero)
    (atSuccessor : ∀ n, candidate (n + 1) = successor (candidate n)) :
    candidate = foldNat zero successor := by
  funext n
  induction n with
  | zero => exact atZero
  | succ n inductionHypothesis =>
      rw [atSuccessor, foldNat, inductionHypothesis]

補足

自然数では、零を z:A、後者を s:A→A へ送る関数を再帰で構成できます。同じ二方程式を満たす任意の候補との一致は自然数帰納法で示します。二方程式は代数準同型であること、帰納法による関数等式はその準同型の一意性に対応します。一般の圏では要素ごとの帰納法や関数外延性をそのまま使えないため、始代数性を別途仮定または証明する必要があります。

問題2全空間による依存帰納を計算する

Problem

問題

P(n) を「長さが n のリスト」の型とし、空リストと先頭への要素追加を帰納段階に選んでください。 totalAlgebra と totalFold を計算し、第一成分が入力した自然数、第二成分がその長さのリストになることを確認します。cast がどの等式に沿ってどのファイバー間を移送するかを型まで書き、非依存foldから依存する値が得られる仕組みを説明してください。

ヒント

族 P:μF→Type の全空間 Σx,P x にF代数構造を入れ、始性から射を得ます。

解答

帰納ステップはFで組み立てた部分データと各部分のP証明から、構成後のP証明を返します。これにより F(Σx,Px)→Σx,Px を定義でき、第一射影は元の代数構造と可換します。始性から h:μF→Σx,Px を得ます。第一射影との合成はμFから自身への代数射なので恒等。従ってhの第二成分は各xに P x を与え、依存帰納原理になります。

fibration内の始代数を使うと、全空間の技巧を依存型の圏論的意味論へ一般化できます。

問題3不動点・代数・始代数を反例で分ける

Problem

問題

恒等関手 Id では全対象が不動点同型 X≅Id(X) を持ちます。構造射を自己写像として選んだ Id-代数を調べ、全てが始代数ではないことを示してください。次に構造射が同型という条件を加えても一意な準同型が得られない例を探します。どの反例が存在、一意性、依存帰納のどれを失うかを分類できれば完了です。

ヒント

恒等関手で、同型 FA≅A、構造射 FA→A、始性の強さを比較します。

解答

F=Idなら任意のAが不動点です。また任意の自己写像α:A→AがF代数を与えます。しかし始代数はId代数圏の始対象に限られます。 Type では空型上の恒等代数が始ですが、Nat上の恒等代数はBool上の恒等代数へ複数の準同型を持ち一意性に失敗します。従って不動点は対象同型、代数は向き付き構造、始代数は全代数への一意な構造保存射まで含みます。

再帰型方程式を解いたことと、帰納原理を得たことを同一視せず、普遍性を別途証明します。

問題4一般圏で不足する構造を特定する

Problem

問題

任意の圏 C に始 F-代数があると仮定し、Type で使った Σn,P(n)、第一射影、等式輸送に対応する構造を列挙してください。述語をスライス圏またはファイブレーションの対象として表し、始代数から依存帰納を得るには F の持ち上げが必要になる理由を説明します。「始代数がある」だけでは書けない式を正確に一つ示せれば完了です。

ヒント

始代数から非依存foldは得られても、依存族や全空間を圏内で扱うための構造を列挙します。

解答

一般圏の始F代数は任意のF代数へのfoldを与えますが、命題族 P:x↦Type やΣ全空間を自動では持ちません。依存帰納にはスライス・ファイブレーション、再添字付け、Fの持ち上げ、全空間を表すΣ型などが必要です。さらに始代数が持ち上げた圏でも保存される条件が要ります。Setで自明な要素論的証明を、任意圏へそのまま移すことはできません。

圏論的一般化では「図式だけで述べられる部分」と「内部論理に依存する部分」を境界として明記します。

第67章

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

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

Problem

問題

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

ヒント

自然数は 1+X、A要素リストは 1+A×X の始代数として一層を分解します。

解答

自然数の一層は零を表す1と、後者の再帰位置Xの和なので F X=1+X。構造射はinlをzero、inrをsuccへ送ります。リストはnilの1と、先頭A・尾Xの組なので G X=1+A×X。構造射はnil/consです。いずれも Σs:S,(P s→X) と書け、形は構成子、位置は各構成子の再帰引数を表します。

構成子宣言から形と再帰位置を抽出し、一層関手とmapを系統的に設計できます。

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

Problem

問題

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

ヒント

任意の多項式代数αに対し、W再帰で各子の再帰結果をαへ渡します。

解答

W要素 sup s k に対し fold α(sup s k)=α⟨s,fun p⇒fold α(k p)⟩ と定義します。この計算式は構造射との可換正方形です。別の代数射hも同じ式を満たすので、W帰納法で各子についてh=fold αを仮定し、関数外延性で位置関数の像が一致、αの合同性で根も一致します。従ってh=fold αで始性が得られます。

多分岐構文のfoldを実装するとき、位置関数全体への帰納仮定を漏らさないようにします。

問題3自由代数の二つの普遍性を往復する

Problem

問題

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

ヒント

自由F代数L(X)は、写像 X→U(A,α) を代数準同型へ一意に延長します。

解答

自由代数関手Lが忘却Uの左随伴なら、hom同型 Alg_F(LX,A)≅C(X,UA) が普遍性です。単位 η_X:X→U(LX) を恒等代数射の像として取り、任意fの逆像を自由延長f♯とします。逆にηと一意延長があればhom全単射を定義でき、自然性は延長の一意性から従います。Xが始対象ならLXはF代数圏の始対象になります。

項代数は変数集合X上の自由代数、閉項の帰納型はXが空の場合として同じ構成に入ります。

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

Problem

問題

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

ヒント

定数・和・積・依存和積で表せるコンテナと、冪集合や商を含む関手を比較します。

解答

多項式関手は形と位置 Σs,X^{P(s)} で表され、各再帰出現を独立な位置として列挙します。有限冪集合関手や対称平方は置換による同一視を含むため、通常のコンテナだけでは重複や順序の商を表せません。それでも厳密正値で始代数を持つ場合があります。従って「多項式」は厳密正値関手の扱いやすい部分族であり、すべてではありません。

解析関手、容器の商、商帰納型へ進むときは、位置の対称性を追加データとして扱います。

第68章

余帰納法・双模倣・最大不動点・終余代数——関係と振舞いを接続する

問題1双模倣からストリーム等式までの二種類の帰納を分ける

Problem

問題

stream_eq_of_bisimilar を、最大不動点の一段展開、位置についての自然数帰納法、関数外延性の三段階に分解して書き直してください。余帰納仮定が正当化するのはどの関係所属で、自然数帰納法が進めるのはどの有限観察かを各ゴールの型で示します。一段条件を確認しない循環証明が作れない理由もLeanの型から説明できれば完了です。

ヒント

関係が一歩後に保存される証明と、任意の有限観察深度で一致する証明を別々にします。

解答

まず関係Rの各対について先頭が等しく、尾の対が再びRに属すことを示します。これはRが関係作用素の後固定点である証明で、余帰納法から最大双模倣に含まれます。次にRで関係するストリームの先頭n要素が一致することをnへの自然数帰納法で示せます。最後に全nでのprefix一致からストリーム等式を外延性で得ます。状態関係の余帰納と観察深度の帰納は異なる原理です。

余帰納証明を有限近似へ落とすとき、どこで観察外延性が必要か明記します。

問題2異なる内部状態表現の機械を比較する

Problem

問題

偶数列を、状態 Nat から 2n を出す機械と、偶数だけからなる部分型を状態にして値を直接出す機械の二通りで構成してください。二状態型の間に関係を定義し、観察一致と次状態保存を示します。両機械を一つの直和状態機械へまとめるか異種関係版の作用素を使い、対応する初期状態が同じ終ストリームへ写ることまで証明してください。

ヒント

自然数カウンタと、既出要素を保持するリスト状態が同じ数列を出す関係を作ります。

解答

機械Mは状態nでnを出しn+1へ、機械Nは状態リストxsでlength xsを出し unit::xs へ進むとします。関係 R(n,xs)↔n=length xs を選びます。関係する状態の出力は等しく、後続では n+1=length(unit::xs) なのでRが保存されます。従ってRは二機械間の双模倣で、初期状態0と[]の振舞ストリームは等しいです。

実装最適化前後の内部状態が異なっても、双模倣で外部観察の一致を証明できます。

問題3終余代数への核関係が後不動点になる理由を一般化する

Problem

問題

behaviorallyEqual_postfixed の証明で、位置 0 と n+1 の等式がそれぞれ何を使っているかを可換正方形へ戻してください。一般の関手 F について同じ証明を書くために必要な関係持ち上げを定義し、終余代数の等式関係を持ち上げた関係へ送る条件を列挙します。ストリーム積関手では条件が成分ごとの等式へ簡約されることを示せれば完了です。

ヒント

振舞射 beh:S→νF の核 x∼y↔beh x=beh y にFの関係持ち上げを使います。

解答

behは余代数準同型なので c≫Fbeh=beh≫out。beh x=beh yならoutを適用して Fbeh(c x)=Fbeh(c y) を得ます。 Fが関係持ち上げと弱い引戻しを適切に保つなら、この等式からc xとc yの対応成分が再び核関係にあると読めます。従って核は双模倣作用素の後固定点です。任意の双模倣は終性により同じ振舞へ送られるので核に含まれます。

非多項式関手では関係持ち上げの性質を検査し、双模倣と行動同値の一致条件を明記します。

問題4最大不動点・不動点同型・終性の反例を整理する

Problem

問題

恒等関手や定数関手を使い、構造射が同型であっても終余代数でない余代数を探してください。次に、状態対上の双模倣最大不動点が存在することから終余代数の存在が直ちに従わない理由を、作用素の定義域と普遍量化の違いから説明します。三概念について必要な圏・順序・射・関係を表にし、誤った含意ごとに最小の反例を対応させれば完了です。

ヒント

順序上の最大後固定点、対象同型 X≅FX、余代数圏の終対象を別の列にします。

解答

最大不動点は完備格子上の単調作用素に対する順序概念です。不動点同型は圏内の対象XとFXの同型で、他の余代数を量化しません。終余代数はすべてのF余代数から一意な準同型を受けます。F=Idなら全対象が不動点同型を持ちますが、終余代数は元の圏の終対象だけです。最大不動点との対応には部分対象格子や関係作用素など、両世界を結ぶ追加構造が必要です。

「最大の解」という表現を使う際は、最大性を測る順序と終性を測る射の圏を特定します。

第69章

無限の三つの意味——基数・尽きない観察・無限図式

問題1状態数と振舞い数の四つの組合せを作る

Problem

問題

有限状態・有限振舞い、有限状態・尽きない振舞い、無限状態・一振舞い、無限状態・複数振舞いの機械をそれぞれ構成してください。状態型の基数、終余代数への像、任意長prefixの存在を別々に証明します。一つの証明を別の欄へ流用できない箇所を特定し、状態同型と振舞等価の差を最小の二機械で説明できれば完了です。

ヒント

状態集合の有限・無限と、異なる生成ストリームの有限・無限を独立に組み合わせます。

解答

有限状態・有限振舞いは一状態定数出力機械。有限状態・無限振舞いは、入力や初期位相を許さない決定的有限機械では不可能ですが、有限アルファベット上の非決定的生成器なら無限個のストリームを生成できます。無限状態・有限振舞いは全自然数状態が同じ0列を出す機械。無限状態・無限振舞いは状態nがnの定数列を出す機械です。機械モデルと「振舞い」の数え方を固定する必要があります。

最小化は状態数ではなく振舞写像の核による商を扱い、到達可能性も別軸として加えます。

問題2有限prefixの糸とストリームの同値を完成する

Problem

問題

streamToThread と threadToStream の残る合成が恒等になることを証明してください。整合条件を一段だけ使う補題を作り、長いprefixを位置の差だけ繰り返し制限する帰納法へ一般化します。Subtype外延性、関数外延性、Fin の値と境界証明の扱いを分離し、どの等式が計算で、どの等式が整合性から従うかを記録できれば完了です。

ヒント

整合する族 p_n∈A^n から、k番目要素を p_{k+1}(k) と定義します。

解答

ストリームsは各nへ先頭n要素 take n s を与え、切捨て写像に対して整合します。逆に整合族pから s(k)=p_{k+1}(k) と定義します。整合性によりm>kならp_mのk成分も同じなので定義は安定です。sから作った族を戻せば各座標でs、pから作ったsのtake nは整合性によりp_nです。関数外延性で二方向が恒等になります。

無限対象を有限近似の整合族として構成する逆極限の典型として利用します。

問題3一般の錐として可算逆極限を再構成する

Problem

問題

自然数を反対向きの射で結ぶ圏を定義し、InverseSequence をその圏から Type への関手へ移してください。 SequenceCone をmathlibの Cone、CompatibleThread を極限錐へ対応させ、threadLift_fac と threadLift_unique が IsLimit.fac と IsLimit.uniq のどの引数になるかを全ての射型つきで示してください。

ヒント

図式 …→X₂→X₁→X₀ への錐を、遷移と整合する成分族として展開します。

解答

逆極限Lの要素は族 (x_n) で p_n(x_{n+1})=x_n を満たすものです。射影π_nはn成分を取り、錐条件を満たします。任意の錐 f_n:Y→X_n からの媒介射は y↦(f_n(y))_n。錐条件が整合性を保証し、各射影との合成がf_nになります。全射影が一致すれば族の各成分が一致するため媒介射は一意です。

完備化、p進整数、無限ジェットを有限段階の整合族として同じ極限形式で構成できます。

問題4ストリーム全体の基数と一つの観察列を分ける

Problem

問題

boolStreamsNotEnumeratedByNat の量化順序を書き下し、任意の列挙候補から対角ストリームを作る段階を追跡してください。一方、固定したストリームの位置が自然数で列挙される写像を示します。「位置の集合が可算だからストリームの集合も可算」という誤推論で交換された量化を特定し、有限アルファベットの場合へ一般化できれば完了です。