/-! # 全問題の解答：帰納・余帰納・無限 ## 第66章：帰納型・帰納法・始代数——三つの生成原理を接続する ### 問題1：再帰子から始代数性を再構成する #### ヒント 任意のF代数αへのfoldを再帰子で作り、η則から一意性を示します。 #### 解答 帰納型μFの構成子 `in:FμF→μF` と再帰子が、各αに `fold α:μF→A` および `in≫fold α=F(fold α)≫α` を与えるとします。さらに同じ方程式を満たすhについて帰納的η則 `h=fold α` があれば、 foldは唯一の代数準同型です。従って `(μF,in)` は始F代数。計算規則だけでは存在を与えるに留まり、始性には 関数一意性を与えるη原理または帰納法が必要です。 言語仕様の再帰子を圏論的普遍性へ格上げするとき、存在・計算・一意性を別々に確認します。 #### 補足 自然数では、零を `z:A`、後者を `s:A→A` へ送る関数を再帰で構成できます。同じ二方程式を満たす任意の候補との 一致は自然数帰納法で示します。二方程式は代数準同型であること、帰納法による関数等式はその準同型の一意性に対応します。 一般の圏では要素ごとの帰納法や関数外延性をそのまま使えないため、始代数性を別途仮定または証明する必要があります。 ### 問題2：全空間による依存帰納を計算する #### ヒント 族 `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：不動点・代数・始代数を反例で分ける #### ヒント 恒等関手で、同型 `FA≅A`、構造射 `FA→A`、始性の強さを比較します。 #### 解答 F=Idなら任意のAが不動点です。また任意の自己写像α:A→AがF代数を与えます。しかし始代数はId代数圏の始対象に限られます。 `Type` では空型上の恒等代数が始ですが、Nat上の恒等代数はBool上の恒等代数へ複数の準同型を持ち一意性に失敗します。 従って不動点は対象同型、代数は向き付き構造、始代数は全代数への一意な構造保存射まで含みます。 再帰型方程式を解いたことと、帰納原理を得たことを同一視せず、普遍性を別途証明します。 ### 問題4：一般圏で不足する構造を特定する #### ヒント 始代数から非依存foldは得られても、依存族や全空間を圏内で扱うための構造を列挙します。 #### 解答 一般圏の始F代数は任意のF代数へのfoldを与えますが、命題族 `P:x↦Type` やΣ全空間を自動では持ちません。依存帰納には スライス・ファイブレーション、再添字付け、Fの持ち上げ、全空間を表すΣ型などが必要です。さらに始代数が持ち上げた 圏でも保存される条件が要ります。Setで自明な要素論的証明を、任意圏へそのまま移すことはできません。 圏論的一般化では「図式だけで述べられる部分」と「内部論理に依存する部分」を境界として明記します。 ## 第67章：W型・多項式関手・自由代数——形と位置から帰納構造を作る ### 問題1：自然数とリストの多項式を回収する #### ヒント 自然数は `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を系統的に設計できます。 ### 問題2：W型の始性証明を可換図式から再構成する #### ヒント 任意の多項式代数αに対し、W再帰で各子の再帰結果をαへ渡します。 #### 解答 W要素 `sup s k` に対し `fold α(sup s k)=α⟨s,fun p⇒fold α(k p)⟩` と定義します。この計算式は構造射との 可換正方形です。別の代数射hも同じ式を満たすので、W帰納法で各子についてh=fold αを仮定し、関数外延性で位置関数の 像が一致、αの合同性で根も一致します。従ってh=fold αで始性が得られます。 多分岐構文のfoldを実装するとき、位置関数全体への帰納仮定を漏らさないようにします。 ### 問題3：自由代数の二つの普遍性を往復する #### ヒント 自由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：多項式ではない厳密正値関手との境界を調べる #### ヒント 定数・和・積・依存和積で表せるコンテナと、冪集合や商を含む関手を比較します。 #### 解答 多項式関手は形と位置 `Σs,X^{P(s)}` で表され、各再帰出現を独立な位置として列挙します。有限冪集合関手や対称平方は 置換による同一視を含むため、通常のコンテナだけでは重複や順序の商を表せません。それでも厳密正値で始代数を持つ場合が あります。従って「多項式」は厳密正値関手の扱いやすい部分族であり、すべてではありません。 解析関手、容器の商、商帰納型へ進むときは、位置の対称性を追加データとして扱います。 ## 第68章：余帰納法・双模倣・最大不動点・終余代数——関係と振舞いを接続する ### 問題1：双模倣からストリーム等式までの二種類の帰納を分ける #### ヒント 関係が一歩後に保存される証明と、任意の有限観察深度で一致する証明を別々にします。 #### 解答 まず関係Rの各対について先頭が等しく、尾の対が再びRに属すことを示します。これはRが関係作用素の後固定点である証明で、 余帰納法から最大双模倣に含まれます。次にRで関係するストリームの先頭n要素が一致することをnへの自然数帰納法で示せます。 最後に全nでのprefix一致からストリーム等式を外延性で得ます。状態関係の余帰納と観察深度の帰納は異なる原理です。 余帰納証明を有限近似へ落とすとき、どこで観察外延性が必要か明記します。 ### 問題2：異なる内部状態表現の機械を比較する #### ヒント 自然数カウンタと、既出要素を保持するリスト状態が同じ数列を出す関係を作ります。 #### 解答 機械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：終余代数への核関係が後不動点になる理由を一般化する #### ヒント 振舞射 `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：最大不動点・不動点同型・終性の反例を整理する #### ヒント 順序上の最大後固定点、対象同型 `X≅FX`、余代数圏の終対象を別の列にします。 #### 解答 最大不動点は完備格子上の単調作用素に対する順序概念です。不動点同型は圏内の対象XとFXの同型で、他の余代数を量化しません。 終余代数はすべてのF余代数から一意な準同型を受けます。F=Idなら全対象が不動点同型を持ちますが、終余代数は元の圏の 終対象だけです。最大不動点との対応には部分対象格子や関係作用素など、両世界を結ぶ追加構造が必要です。 「最大の解」という表現を使う際は、最大性を測る順序と終性を測る射の圏を特定します。 ## 第69章：無限の三つの意味——基数・尽きない観察・無限図式 ### 問題1：状態数と振舞い数の四つの組合せを作る #### ヒント 状態集合の有限・無限と、異なる生成ストリームの有限・無限を独立に組み合わせます。 #### 解答 有限状態・有限振舞いは一状態定数出力機械。有限状態・無限振舞いは、入力や初期位相を許さない決定的有限機械では不可能ですが、 有限アルファベット上の非決定的生成器なら無限個のストリームを生成できます。無限状態・有限振舞いは全自然数状態が同じ0列を 出す機械。無限状態・無限振舞いは状態nがnの定数列を出す機械です。機械モデルと「振舞い」の数え方を固定する必要があります。 最小化は状態数ではなく振舞写像の核による商を扱い、到達可能性も別軸として加えます。 ### 問題2：有限prefixの糸とストリームの同値を完成する #### ヒント 整合する族 `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：一般の錐として可算逆極限を再構成する #### ヒント 図式 `…→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：ストリーム全体の基数と一つの観察列を分ける #### ヒント `A^N` という集合の濃度と、固定した `s:N→A` の観察過程を別の判断にします。 #### 解答 二要素Aならストリーム全体 `A^N` は実数と同じ非可算濃度を持ちます。一方、一つのストリームsは自然数nごとに値s(n)を 観察する一本の可算列です。「観察が無限に続く」ことは一対象の時間構造であり、「可能な振舞いが非可算個ある」ことは 対象集合の基数です。定数0列も尽きない観察を持ちますが、その単一振舞いの集合は一要素です。 確率過程や実数展開でも、標本路一つ、標本空間、時間添字の三種類の無限を混同しないようにします。 -/ namespace FormalLab.Appendix.Solutions.Chapter066Exercise001 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] end FormalLab.Appendix.Solutions.Chapter066Exercise001