第5部 再帰・不動点・無限

問題1測度を設計して再帰呼出しを検査する

Problem

問題

リストから一要素ずつ除く関数、自然数を二で割り続ける関数、二つの自然数を交互に減らす関数について状態型と自然数値の測度を定めてください。各再帰呼出しの前後の測度を計算し、厳密不等式をLeanで証明します。等しいままの分岐があれば、測度または状態遷移を修正できれば完了です。三例の測度が捨てる状態情報と、停止の証明にはその情報が不要な理由も比較してください。

ヒント

入力を自然数へ送る測度を選び、すべての再帰呼出しで狭義に減る不等式を示します。

解答

リストを半分ずつ処理する関数なら測度を長さとします。空または一要素で停止し、それ以外では分割した各リストの長さが元の長さより小さいことを証明します。辞書式再帰では (m,n) に辞書式順序を入れ、第一成分が減るか、第一成分を保って第二成分が減ることを各呼出しで示します。測度の非増加では自己呼出しを排除できないので、狭義性が必要です。

構文変換では節点数、書換え系では多重集合順序など、計算が実際に消費する資源を測度に選びます。

Lean検査済みL244–253

theorem halfDecreases {n : Nat} (positive : 0 < n) : n / 2 < n := by
  omega

theorem alternatingMeasureDecreasesLeft {left right : Nat} (positive : 0 < left) :
    (left - 1) + right < left + right := by
  omega

theorem alternatingMeasureDecreasesRight {left right : Nat} (positive : 0 < right) :
    left + (right - 1) < left + right := by
  omega

問題2接近可能性から帰納原理を展開する

Problem

問題

Acc.rec または WellFounded.induction の型を調べ、strongInductionOnNat の各引数へ対応づけてください。通常の後者帰納法から強い帰納法を導く証明とも比較します。帰納仮定の量化範囲と、実際に利用する小さい数を導出木で示し、循環した仮定がないことを説明すれば完了です。

ヒント

Acc r x の唯一の構成子が、すべての先行者の接近可能性を保持することを使います。

解答

Acc.intro : (∀y, r y x→Acc r y)→Acc r x です。Acc r x からP xを示すには、その導出へ帰納し、 h : ∀y,r y x→Acc r y と各yへの帰納仮定 P y を得ます。整礎性 ∀x,Acc r x があれば、局所ステップ ∀x,(∀y,r y x→P y)→P x を任意のxへ適用して ∀x,P x を得ます。再帰関数でも同じ導出木を辿るため、無限下降列を作れません。

相互再帰は状態を直和へまとめ、その全体に整礎関係を定義すると一つの原理で扱えます。

Lean検査済みL259–261

#check Acc.rec
#check WellFounded.induction
#check FormalLab.Recursion.WellFounded.strongInductionOnNat

出力

Acc.rec.{u_1, u} {α : Sort u} {r : α → α → Prop} {motive : (a : α) → Acc r a → Sort u_1}
  (intro : (x : α) → (h : ∀ (y : α), r y x → Acc r y) → ((y : α) → (a : r y x) → motive y ⋯) → motive x ⋯) {a✝ : α}
  (t : Acc r a✝) : motive a✝ t

出力

WellFounded.induction.{u} {α : Sort u} {r : α → α → Prop} (hwf : WellFounded r) {C : α → Prop} (a : α)
  (h : ∀ (x : α), (∀ (y : α), r y x → C y) → C x) : C a

出力

FormalLab.Recursion.WellFounded.strongInductionOnNat (property : Nat → Prop)
  (step : ∀ (n : Nat), (∀ (m : Nat), m < n → property m) → property n) (n : Nat) : property n

問題3互除法の停止性と正しさを分離する

Problem

問題

gcd 48 18 の呼出し列と第二引数の列を書き、各段の剰余不等式を確認してください。次に「返り値が両数を割る」と「任意の公約数が返り値を割る」を別補題として定式化します。停止証明のどの行からもこれらが直接は得られないことを指摘し、Euclidの補題を追加した帰納証明の構造を示せば完了です。

ヒント

停止には剰余の減少、正しさには公約数集合の保存を使います。

解答

gcd a 0=a、gcd a b=gcd b (a%b) とします。b>0 なら a%b<b なので第二引数を測度にすれば停止します。正しさは d∣a ∧ d∣b ↔ d∣b ∧ d∣a%b を用い、再帰前後で公約数が一致することから示します。停止証明だけでは返り値が最大公約数だとは分からず、公約数保存だけでも再帰が値を返すとは分かりません。二つは異なる不変条件です。

アルゴリズム検証では変種関数を停止へ、ループ不変量を部分正当性へ割り当てます。

Lean検査済みL267–271

open FormalLab.Recursion.WellFounded

#eval gcd 48 18

example : gcd 48 18 = 6 := by native_decide

出力

第27章

束・完備格子・単調作用素

問題1二項演算から普遍性を復元する

Problem

問題

BinaryJoin と BinaryMeet について、上界・下界条件と最小性・最大性を四本の推論規則に分けてください。積集合や和集合の具体的要素を使う証明と、順序記法だけの証明を並べます。常に左引数を返す偽のjoinがどの規則を破るかを比較不能な述語二つで示せば完了です。最後に、外延的に同じ上限候補が反対称性によって等しくなる一意性証明を加えてください。

ヒント

x⊓y が下界である二条件と、任意の下界がそれ以下である条件を書きます。

解答

交わりmは m≤x、m≤y を満たし、任意のzについて z≤x∧z≤y→z≤m を満たします。この三条件からmは一意です。結びjは順序を反転して x≤j、y≤j、x≤z∧y≤z→j≤z です。吸収則などの代数法則はこの普遍性から、両辺が同じ下界または上界を分類することにより導けます。演算記号だけでなく比較対象全体への最良性が本体です。

積・余積や極限・余極限でも、候補の構成と任意対象からの一意な比較を同じ順で確認します。

問題2空族を含む任意上限・下限を計算する

Problem

問題

三つの自然数述語から成る族を選び、Supremum と Infimum の所属条件を量化記号へ戻してください。一要素族、空族、全述語から成る族について上限と下限を計算します。空虚な全称と存在不能をLean証明の各分岐へ対応づけ、最上元と最大元を混同していないことを説明すれば完了です。族の要素数ではなく量化範囲が普遍性を決めることも、各場合の定義展開から確認してください。

ヒント

空族の上界・下界条件は空虚に真になることから最小・最大要素を求めます。

解答

完備格子では任意の部分集合Sに sSup S と sInf S があります。冪集合格子では上限は和集合、下限は共通部分です。空族の和集合は空集合で、すべての集合の下にある最小元です。空族の共通部分は全体集合で、すべての集合の上にある最大元です。従って任意上限の存在は底、任意下限の存在は頂を含み、「非空族だけ」の完備性とは異なります。

零項の積と余積が終対象と始対象になることを、空族の極限・余極限として読み替えます。

問題3作用素の単調性を正例と反例で判定する

Problem

問題

二項関係 step に対し F(X)={start}∪{y∣∃x∈X.step(x,y)} を定義し、単調性を証明してください。補集合、集合差、定数作用素についても判定し、失敗するものには包含 X⊆Y と出力要素の反例を与えます。前不動点と後不動点を一つずつ計算し、単調性とは異なる量化であることを示せば完了です。

ヒント

X⊆Y→F X⊆F Y を要素ごとに示し、否定位置へXが現れる作用素を反例候補にします。

解答

固定集合Aに対する F(X)=A∪X は、X⊆YならA∪X⊆A∪Yなので単調です。逆像作用素も所属を関数適用へ展開すれば単調です。一方 G(X)=A\X は反単調です。例えばAが一要素集合で ∅⊆A ですが、G(∅)=A は G(A)=∅ に包含されません。述語変数が含意の前件や否定の下に現れると向きが反転します。

帰納的定義の規則形式を設計するとき、定義対象が正の位置だけに現れることを単調性として検査します。

Lean検査済みL277–288

open FormalLab.Recursion.Lattices

def reachableStep (start : Nat) (step : Nat → Nat → Prop)
    (set : PredSet Nat) : PredSet Nat :=
  fun y => y = start ∨ ∃ x, set x ∧ step x y

theorem reachableStepMonotone (start : Nat) (step : Nat → Nat → Prop) :
    Monotone (reachableStep start step) := by
  intro left right included y generated
  rcases generated with atStart | ⟨x, member, moves⟩
  · exact Or.inl atStart
  · exact Or.inr ⟨x, included member, moves⟩

第28章

最小・最大不動点とKnaster–Tarski定理

問題1最小不動点証明の二度の単調性を追う

Problem

問題

operatorLeastBelowLeast と leastBelowOperatorLeast を通常の集合記法へ翻訳してください。各証明で比較する二集合、単調性へ渡す包含、前不動点性を使う位置を表にします。単調性を削除したとき最初に型付けできなくなる推論を特定し、単なる記号の反転でないことを説明すれば完了です。

ヒント

前固定点全体の下限 μF に対し、まず F(μF)≤μF、次に逆向きを示します。

解答

μF=inf {X | F X≤X} とします。各前固定点Xへ μF≤X なので単調性から F(μF)≤F X≤X です。従って F(μF) は全前固定点の下界であり F(μF)≤μF。この結果へ単調性をもう一度使うと F(F(μF))≤F(μF) なので F(μF) 自身が前固定点です。下限の定義から μF≤F(μF)。よって等号です。

証明支援系では前固定点の下限、閉性、最小性を別補題にし、向きの取り違えを型で検出します。

補足

最初の単調性は F(μF) が全前固定点の下界であることを作り、二度目の単調性は F(μF) 自身が前固定点であるという資格を作ります。同じ仮定を二度使っていても、得ている事実の種類は異なります。最大不動点では順序を反転し、後固定点の上限から始めます。その際も「上界」と「後固定点」という二つの資格を区別します。

問題2帰納的生成を別の規則へ移す

Problem

問題

偶数を零と二加算で生成する作用素、二進木を葉と節点で生成する作用素を述語集合上に定義してください。単調性を証明し、最小不動点に属する代表値を帰納法で示します。任意の前不動点を受け取る形へ証明を一般化し、生成規則ごとの帰納仮定がどこに現れるかを示せば完了です。偶数作用素の最小不動点に奇数が入らない逆向きも証明し、生成の十分性と必要性を分けてください。

ヒント

偶数を0と「2を足す」規則で生成し、その規則作用素の最小不動点として表します。

解答

F(X)={0}∪{n+2 | n∈X} と置きます。Fは単調で、最小不動点μFは0を含み、要素へ2を足して閉じています。帰納法は、集合Pが0を含み2加算で閉じる、すなわち F(P)⊆P なら μF⊆P という最小性です。これにより μFの全要素が2で割り切れることを示せます。逆に各 2k がμFに属することはkへの自然数帰納法で示します。

到達可能状態や構文の導出可能性も、初期事実と閉包規則が作る最小不動点として扱えます。

問題3最大不動点を直接に特徴づける

Problem

問題

最大側の四定理について、最小側から反転した語と包含方向を列挙してください。その上で一つの後不動点を具体的に選び、greatestFixedPoint の和へ入る証人を構成します。νF⊆F(νF) と逆包含で単調性が別々にどう使われるかを証明項から説明できれば完了です。最小側の証明を機械的に反転しただけでは型が合わない箇所を一つ示し、その原因を量化から説明してください。

ヒント

後固定点の上限 νF=sup {X | X≤F X} を用い、等式の両方向を追います。

解答

各後固定点Xについて X≤νF なので単調性から X≤F X≤F(νF)。従ってF(νF)は全後固定点の上界で νF≤F(νF) です。単調性から F(νF)≤F(F(νF)) となり、F(νF)も後固定点です。上限の定義により F(νF)≤νF、従って不動点です。任意の不動点は後固定点なのでνF以下で、最大性も確認できます。

安全性や無限振る舞いをνFで定義するとき、余帰納法は X≤F X→X≤νF という最大性として使います。

第29章

最大不動点・余帰納的述語・双模倣

問題1常時安全性を有限観察へ展開する

Problem

問題

Always_now と Always_next を組み合わせ、Always good next x から最初の五状態が全て good を満たすことを証明してください。自然数時刻 n へ一般化し、どこで時刻について帰納し、どこで最大不動点を一段展開するかを分離します。有限観察だけから逆に Always を得られる条件も述べれば完了です。

ヒント

安全状態集合Sに対し F(X)={s∈S | すべての一歩後続がXに属す} と置きます。

解答

常時安全な状態はνFです。s∈νF なら不動点等式からsは安全で、すべての後続が再びνFに属します。これをn回繰り返すと任意の有限実行接頭辞の全状態がSに属します。逆に、すべての有限接頭辞が安全な状態の集合Xは、一歩後続から始めた有限接頭辞も安全なので X⊆F(X)。余帰納法から X⊆νF です。

モデル検査では有限深さ近似を下降列で計算し、有限状態なら安定した段階が最大不動点になります。

Lean検査済みL294–306

open FormalLab.Recursion.CoinductivePredicates

def iterate (next : A → A) : Nat → A → A
  | 0, state => state
  | time + 1, state => iterate next time (next state)

theorem Always_at {A : Type} {good : A → Prop} {next : A → A} {state : A}
    (always : Always good next state) : ∀ time, good (iterate next time state) := by
  intro time
  induction time generalizing state with
  | zero => exact Always_now always
  | succ time inductionHypothesis =>
      exact inductionHypothesis (Always_next always)

問題2余帰納不変量を小さく選ぶ

Problem

問題

三状態の周期遷移と、一状態だけを除く安全述語を定義してください。anyBool のような全体集合では後不動点にならない例を作り、安全に閉じた最大の候補を選び直します。各状態の現在条件と次状態条件を表にし、coinduction へ渡す一段証明を構成すれば完了です。選んだ候補から状態を一つ除いた場合にも後不動点かを調べ、不変量が最大である必要の有無を述べてください。

ヒント

証明したい状態だけでなく、その後続として実際に現れる状態を閉じる最小限の集合を候補にします。

解答

二状態が交互に遷移する系 a→b→a の常時安全性なら、候補Rを {a} にするとaの後続bを含まず R⊆F R が失敗します。R={a,b} なら両状態が安全で後続もR内なので後固定点です。全状態集合を選んでもよい場合がありますが、危険状態を含めれば安全条件で失敗します。到達閉包を基礎に小さい候補を選ぶと、必要な義務が減り反例も見えます。

双模倣関係でも対象の一対だけで閉じなければ、その遷移先の対を加えて関係を閉じます。

Lean検査済みL312–332

open FormalLab.Recursion.CoinductivePredicates

inductive Phase where | zero | one | two deriving DecidableEq

def next : Phase → Phase
  | .zero => .one
  | .one => .two
  | .two => .zero

def safe : Phase → Prop
  | .zero | .one => True
  | .two => False

def invariant : Phase → Prop
  | .zero | .one => True
  | .two => False

example : ¬Always safe next .zero := by
  intro always
  have afterTwo := Always_next (Always_next always)
  exact Always_now afterTwo

問題3双模倣と単なる観察一致を分ける

Problem

問題

最初の観察だけは等しいが次状態で異なる二系を作り、観察一致関係が後不動点でないことを示してください。次に周期の位相をずらした二系の双模倣関係を構成します。関係の各対について観察と次状態を検査し、最大不動点への包含から無限の観察列が一致する理由を説明すれば完了です。関係へ不要な対を加えたとき一段条件が壊れる例も示し、関係の大きさと証明の容易さを比較してください。

ヒント

現在の出力は同じでも、次状態の出力が異なる二状態を作ります。

解答

状態pとqがともに0を出力し、pは永遠に0を出す状態へ、qは次に1を出す状態へ遷移するとします。現在の観察だけなら pとqは一致します。しかし双模倣には出力一致に加え、各遷移を相手が模倣し、後続対も同じ関係に属することが必要です。後続の出力が0と1なので、この対を含む双模倣はありません。決定的ストリーム系では双模倣から全有限接頭辞の一致が従い、その逆も成り立ちます。

非決定系では一つの実行列の一致では足りず、分岐する各遷移への往復条件を検査します。

第30章

領域理論・連続写像・再帰方程式

問題1反復列の上限が固定される証明を分解する

Problem

問題

kleene_is_fixed の二つの包含を通常の順序記法で書き、零段と後者段を分けてください。連続性を使う行、像鎖と元の鎖を一段ずらす行、反対称性を使う行を特定します。連続性を単調性だけへ弱めた場合に不足する等式を明示し、証明の穴を仮定で隠していないことを確認すれば完了です。さらに元の鎖と像鎖の最初の四項を書き、添字の一段ずれが各Lean項のどこに現れるかを対応づけてください。

ヒント

x₀=⊥、x_{n+1}=F x_n とし、連続性がω鎖の上限を保存する式を使います。

解答

単調性から x₀≤x₁≤… です。x=sup_n x_n と置くと、ω連続性により F x=F(sup_n x_n)=sup_n F(x_n)=sup_n x_{n+1}=x です。最後の等号は先頭の⊥を除いても上限が変わらないためです。さらに任意の不動点yについて、⊥≤yから帰納的に x_n≤y。従ってx≤yであり、xは最小不動点です。

再帰プログラムの有限展開をx_nと見れば、意味はすべての有限近似の上限として構成できます。

問題2平坦順序のω鎖を分類する

Problem

問題

Option Bool 上の増大列を複数作り、none だけの列、途中で some true に確定する列、異なる確定値へ移ろうとする非例を比較してください。最後の列がどの隣接段階で FlatLe を破るかを示します。任意の正しい鎖が未定義のままか一つの値へ安定する理由を述べ、上限候補を構成すれば完了です。

ヒント

底⊥以外の異なる二値は比較不能であることを使います。

解答

平坦領域 A⊥ では ⊥≤a だけを追加し、異なるa,bは比較不能です。上昇ω鎖は、すべて⊥であるか、ある段階まで ⊥で、その後は同じ値aに固定されるしかありません。aの後に異なるbへ移れば a≤b が必要となり矛盾します。前者の上限は⊥、後者の上限はaです。この順序は「未定義から一つの確定値へ」という情報増加を表します。

部分関数空間では各入力点で同じ分類を行い、点ごとの情報増加として近似順序を読みます。

Lean検査済みL338–344

open FormalLab.Recursion.DomainTheory

example : FlatLe (none : Option Bool) (some true) := by
  trivial

example : ¬FlatLe (some true) (some false) := by
  simp [FlatLe]

問題3燃料近似を意味論的近似へ接続する

Problem

問題

factorialApproximation fuel n が燃料について FlatLe で増大することを、fuel と n のどちらへ帰納すべきか検討して証明してください。十分な燃料で通常の階乗値を返す補題も別に定式化します。停止入力、燃料不足、永久発散を Option の結果だけでどこまで区別できるかを説明すれば完了です。