以下の内容はhttps://lpha-z.hatenablog.com/entry/2025/08/17/231500より取得しました。

Lean 4 で巨大数の大きさの証明のつづき

先週の記事（Lean 4 で巨大数の大きさを証明してみる - よーる）で、ふぃっしゅ数バージョン1のSS変換を1回行った段階で得られる数が、4変数アッカーマン関数を使って表現できる数A(1,0,1,1)より大きいことを示しました。 今回の記事では、SS変換を2回行うことで得られる数が、A(1,0,1,2)より大きいことを示します。

SS変換1回

ふぃっしゅ数バージョン1のSS変換を1回行った段階で得られる数を n_1と書くことにします。 前回の記事では、 n_1がA(1,0,1,1)より大きいことを示したのですが、上限は示していませんでした。 そこで手ごろな上限を示そうと思ったのですが、実はA(4,1,1)に完全に等しいことがわかりました。

Repeat S_transform 4 (3, fun x => x + 1) = (Ackermann3 4 0 $ Ackermann3 3 0 $ Ackermann3 2 0 $ Ackermann3 1 0 3)ですが、最後の3をAckermann3 0 1 1と読み替えれば、A(4,1,1)を（値呼びの順番で）評価した時の展開に一致するからです。

theorem F1_first_iteration_upper : (SS_transform ((3, fun x => x + 1), S_transform)).fst.fst = Ackermann3 4 1 1 := by
  rw [SS_transform]
  rw [F1_first_iteration_eq_lemma]
  apply Eq.symm
  repeat rw [Ackermann3]

この結果は、S変換が3変数アッカーマン関数の最左引数を増やす効果があることを示してしまえば、あとは純粋に定義からの等式変形のみにより得られます。 つまり、「アッカーマン関数は最左引数が大きい方が“当然”“強い”」のような、証明が面倒な性質は使っていません。 したがってこの結果はすでに、（形式的かはともかく）“数学的”とみなせる厳密さで示されていることかもしれません。 しかしこの結果を私は見たことがなかったため、3変数アッカーマン関数できれいに表せるという事実には驚きました。 巨大数の文脈では主に増大度が議論され、厳密な大きさの評価が必要となることは少ないため、このような結果が仮に得られていたとしてもあまり参照されなかったのかもしれません。

余談：展開の順番について

アッカーマン関数の大小評価をする際、展開の順序を気を付けないと迷い込んでしまいます。 ところで、この展開の順序は、巨大数の文脈であまり意識されず問題になっている話に関係があるなと思いましたので、メモを書いておきます。

展開（評価）の順序は、以下の二つのものが有名です。

  • 正規順序（最外最左簡約*1）
    • なるべく外側、その中でも左側から展開していく
    • 例えば、A(1,0,0,A(c,b,a))とあれば、A(c,b,a)を計算するのではなく、「A(1,0,0」の部分で確定する展開を採用してA(0,A(c,b,a),0,A(c,b,a))にする
    • 無限ループに陥る可能性が最も低い展開順序である
      • この展開順序で無限ループする場合、他のいかなる展開順序でも無限ループする、という意味で「可能性が最低」
    • 計算コストの意味で最適とは限らない
      • 使わない計算を避けられる利点がある一方、コピーが発生すると計算が複数回に複製される欠点がある。メモリ確保（Haskellのサンクとか）で避けられるけれど、これ自体が非効率の元*2
    • Lean 4はこの戦略を取りがち（？）
      • 式が無意味に膨らんでわかりづらくなる欠点がある。関数型言語としてこの展開順序を選ぶことは理解できるけれど……
  • 正格評価（値呼び）
    • 関数の引数の値を確定させるまで、関数を展開しない
    • 例えば、A(1,0,0,x)とあれば、A(0,x,0,x)にするのではなく、まずxの値を計算する
    • 普通のプログラミング言語はほとんどこの順番で評価する

アッカーマン関数は、どんな展開順序をとっても停止しますし、返ってくる値は同じです。 しかしながら、一般の項書き換えシステムでは以下の四パターンがあり得えて、ルールの適用順序によっては停止しなかったり異なる値が返ってきたりすることがあり得ます。 項書き換えシステムで巨大数を定義する際には注意が必要です。

  1. いかなる展開順序を選んでも、常に計算が停止し、同じ結果が得られる。
    • 停止性と合流性がある場合。例えば単純型付きラムダ計算など
    • 普通の*3、場合分けが排他で網羅できている再帰関数として書き表すと、再帰の単調進行性を示した時点でこの枠組みに入るので、いつでもそうだと勘違いしがち
    • 合流性は要するに、コピーして別の位置にいっても、同じ引数なら常に同じ結果が得られるということに基づく。つまり、計算してからコピーしても、コピーしてから計算しても、どちらでも同じになるから、全体としても展開順序によらない
  2. いかなる展開順序を選んでも、計算が停止した時には同じ結果が得られる。しかし、計算が停止しない展開順序も存在する。
    • 停止性がない場合。型なしラムダ計算が該当する
    • 例えば、Ω=(λx. x x)(λx. x x)とfst=λx.λy. xに対して、fst 0 Ωがいい例となる
      • 正規順序で計算すれば、0が返ってきて停止する
      • 正格評価だと、Ωを無限に展開し続けて停止しない
      • きまぐれでいろんな展開順序を取る場合、停止する場合は常に0が返ってくる
    • なお、停止する展開順序が一つない場合も、空虚な真ということで「いかなる展開順序を選んでも、計算が停止した時には同じ結果が得られる」を満たすのでこの四つのパターンのうちではこのパターンに該当する
  3. いかなる展開順序を選んでも常に計算が停止するが、異なる結果が得られることがある。
    • 合流性がない場合。典型的には、適用可能な展開ルールが複数あり、かつ展開により部分項がコピーされると周りの環境に影響を与えて違う計算が行われるような場合が該当する
    • 例えば、aRb=(a+1)*bと定義した時、1R2R3は、左から展開すれば4R3=15になり、右から展開すれば1R9=18になる。結合順序を規定しなかったり、マッチした部分はどこでも書き換えていいみたいなルールを作るとこういうことになりがちなので注意
  4. 展開順序によっては停止しないし、停止する場合でも異なる結果が得られることがある。
    • 停止性も合流性もない場合

SS変換2回

先ほど説明したように、ふぃっしゅ数バージョン1のSS変換を1回行った段階で得られる数を n_1と書くことにしています。 これに加えて、その段階で得られている関数を f_1、変換を T_1と書くことにします。

f_1は、Ackermann3 4 0です。 Ackermann3は引数を三つ取る関数のはずなのに二つしか取っていない部分が気になるかもしれません。 これはカリー化された関数定義に対して部分適用することに得られる一引数関数になっています。 要するに f_1(x) = A(4,0,x)であるということです。 fun x => Ackermann3 4 0 xとも書けますが、この種の表記が以降でたくさん出てくるので、なるべく短く書ける記法を使っていくことにします。

証明のスケッチ

ふぃっしゅ数バージョン1のSS変換を2回行った段階で得られる数を n_2と書くことにします。 二回目のSS変換の中では、 T_1を p_1 = f_1(n_1)回繰り返すことになります。 T_1はS変換4回なので、S変換を 4p_1回行うことになります。 SS変換1回目ではS変換を4回行っていたことを思い出すと、S変換を合計 4p_1+4回行うことで得られる数が n_2であるということになります。 したがって、 n_2 = A(4p_1+4,1,1)となります。 ちなみに、 p_1 = A(4,0,A(4,1,1)) = A(4,1,2)です。

3変数アッカーマン関数の最左引数に値が入るのは、4変数アッカーマン関数の最左引数を減らしたときです。 それと A(1,0,1,1) \lt n_1 = A(4,1,1) \lt A(4,1,2) = p_1を念頭に置くと、 A(1,0,1,2) = A(1,0,0,A(1,0,1,1)) \lt A(1,0,0,p_1) = A(p_1,0,p_1) \lt A(4p_1+4,1,1)=n_2のように証明すればよさそうです。

S変換の繰り返しが3変数アッカーマン関数の最左引数を増やす

S変換を1回適用することが3変数アッカーマン関数の最左引数を1増やすことは以前に示しました。 以下に再掲します（微妙に補題の命名を変えました。また、部分適用を使った形にしています）。

lemma B_func_Ackermann3_eq_lemma1 : B_func (Ackermann3 q 0) x y = Ackermann3 q x y := by
  induction x generalizing y with
  | zero => rw [B_func.eq_1]
  | succ x ihx =>
      induction y with
      | zero => rw [B_func.eq_2, Ackermann3]; exact ihx
      | succ y ihy => rw [B_func.eq_3, Ackermann3]; simpa [ihy] using ihx

lemma B_func_Ackermann3_eq_lemma2 : B_func (Ackermann3 q 0) x x = Ackermann3 (q+1) 0 x := by
  rw [B_func_Ackermann3_eq_lemma1, Ackermann3]

lemma S_transform_Ackermann3_eq_lemma1 :
  S_transform (m, Ackermann3 q 0) = (Ackermann3 (q+1) 0 m, Ackermann3 (q+1) 0) := by
  simp [S_transform, B_func_Ackermann3_eq_lemma2]

theorem S_transform_Ackermann3_eq_lemma2 :
  S_transform (Ackermann3 q 1 1, Ackermann3 q 0) = (Ackermann3 (q+1) 1 1, Ackermann3 (q+1) 0) := by
  simp [S_transform_Ackermann3_eq_lemma1, Ackermann3]

引数が全て具体的な数の時にsimp [Ackermann3]とかやるとすべてを展開しようとして再帰深度制限にかかりますが、このような一般的な補題の証明の時はできるところまでで止まる（qがzeroかsuccかわからないため）ので、便利に使うことができます。

Repeat関数の定義変更

S変換をn回繰り返すことが3変数アッカーマン関数の最左引数をn増やすことは、帰納法の各ステップでこれを使えば示せそうです。 しかしながら、前回の記事でのRepeat関数の定義はいまいちで、帰納法との相性がかなり悪いことがわかりました。 そこで、以前使っていたRepeat関数の定義を次の定義で置き換えることにします。

def Repeat {T : Type} (f : T -> T) : Nat -> (T -> T)
| 0 => id
| Nat.succ m => fun p => f $ Repeat f m p

この定義は、m+1回の繰り返しの定義が、m回の繰り返しの後1回行う、という順番になっています。 「m回の繰り返し」は帰納法の仮定として得られることが多いので、自然な順番です。

以前使っていたRepeat関数の定義は、Repeat'と名付けることにします。

def Repeat' {T : Type} (f : T -> T) : Nat -> (T -> T)
| 0 => id
| Nat.succ m => fun p => Repeat' f m $ f p

Repeat'は末尾再帰になっていて、定義としては自然です（定義した時は特に深く考えていませんでした）。 しかし、m+1回の繰り返しが、1回行った後m回繰り返す、という定義になっています。 この「m回の繰り返し」は、何に適用するかが毎回変わるので帰納法と相性が悪いです。

ここで、この定義変更が問題ないことを示します。 具体的には、Repeat'関数とRepeat関数が同じことを行っていることを、帰納法により示します。 Repeat'関数は数学的帰納法と相性が悪いため、一筋縄ではいきません。 帰納法のステップ自体を帰納法で示す必要があるようです。

lemma Repeat'_shift_lemma n p : Repeat' f n (f p) = f (Repeat' f n p) := by
  induction n generalizing p with
  | zero => simp [Repeat']
  | succ n ihn => simp [Repeat', ihn]

theorem Repeat'_eq_Repeat {T : Type} {f : T -> T} {n : Nat} {p : T} : Repeat' f n p = Repeat f n p := by
  induction n with
  | zero => simp [Repeat', Repeat]
  | succ n ihn => simpa [Repeat', Repeat, ← ihn] using Repeat'_shift_lemma n p

これにより、Repeat関数は元の定義と同じことを行うことが示せました。 以下、この使いやすい方の定義で証明を行っていきます。

余談ですが、これをη変換したRepeat' = Repeatは、暗黙引数が推論できないとのエラーになりました。 暗黙引数を補った上で型を明示することで推論できるようになるようです。

証明

今定義した使いやすい方のRepeat関数であれば、定理の証明は帰納法で一発です。

lemma Repeat_S_transform_Ackermann3_lemma :
  Repeat S_transform n (Ackermann3 q 1 1 , Ackermann3 q 0)
    = (Ackermann3 (q+n) 1 1, Ackermann3 (q+n) 0) := by
  induction n with
  | zero => simp [Repeat]
  | succ n ihn => simpa [Repeat, ihn] using S_transform_Ackermann3_eq_lemma2

SS変換1回の時の等式を証明しなおす

先週の記事では、SS変換1回の場合の証明を、単純に4回展開することで行っていました。 上で証明した補題を使って、一気に証明しましょう。

def F1_1st_iteration := Repeat SS_transform 1 ((3, fun x => x + 1), S_transform)

theorem F1_1st_iteration_eq :
  F1_1st_iteration = ((Ackermann3 4 1 1, Ackermann3 4 0), Repeat S_transform 4) := by
  rw [F1_1st_iteration]
  rw [Repeat, Repeat]
  simp [SS_transform]
  rw [show (fun x => x + 1) = Ackermann3 0 0 by funext; simp [Ackermann3]]
  rw [show 3 = Ackermann3 0 1 1 by simp [Ackermann3]]
  exact Repeat_S_transform_Ackermann3_lemma

S変換の回数の加算と乗算

加算

S変換をm回行った後S変換をn回行うと、S変換をn+m回行ったことになることを示します。 内側であるmを固定したほうが証明が簡単になります。

lemma Repeat_S_transform_add_lemma :
  Repeat S_transform n (Repeat S_transform m p) = Repeat S_transform (n+m) p := by
  induction n with
  | zero => simp [Repeat]
  | succ n ihn => simp [show n+1+m = n+m+1 by bound, Repeat, ihn]

乗算

「S変換n回」をm回繰り返すと、S変換をn*m回行ったことになることを示します。 内側であるnを固定したほうが証明が簡単になります。

lemma Repeat_S_transform_mul_lemma :
  Repeat (Repeat S_transform n) m = Repeat S_transform (n*m) := by
  induction m with
  | zero => simp [Repeat]
  | succ m ihm =>
      simp [Repeat, ihm]
      funext
      rw [Repeat_S_transform_add_lemma]
      group

証明の準備

大小関係に関する定理を、より使いやすい形で再定義します。 暗黙引数を使うことで、使う時に長々書かなくてよいようにしました。 また、単調性に関する定理は、$を使って証明を書きやすいような順番で仮定を受け取るようにしました。

lemma Ackermann3_monotonic_3rd :
  (y > 0 ∨ z > 0) → x < w → Ackermann3 x y z < Ackermann3 w y z := by
  intro hc
  induction w with
  | zero => tauto
  | succ w ihw =>
      intro
      by_cases h : w = x
      · rw [h]
        exact Ackermann3_monotonic_3rd_ih x y z hc
      · have h : x < w := by omega
        calc
          Ackermann3 x y z < Ackermann3 w y z := ihw h
          _                < Ackermann3 (w+1) y z := Ackermann3_monotonic_3rd_ih w y z hc

theorem Ackermann3_inc : z < Ackermann3 x y z := (Ackermann3_monotonic1 x y z).left

theorem Ackermann3_monotonic_1st : z < w → Ackermann3 x y z < Ackermann3 x y w := by
  intro h; exact (Ackermann3_monotonic1 x y z).right.right w h

さらに、「最左引数を増やすと大きくなる」という性質を最右引数がアッカーマン関数の計算結果になっている時に示したい場合を片付ける補題を用意しました。 これにより、Ackermann3_monotonic_3rdだと、条件である(y > 0 ∨ z > 0)がomegaなどのタクティックでは示せない（別途補題が必要になって面倒）という問題を解決します。

theorem Ackermann3_positive : Ackermann3 x y z > 0 := by
  calc
    0 ≤ z := by simp
    _ < Ackermann3 x y z := Ackermann3_inc

theorem Ackermann3_Ackermann3_monotonic_3rd :
  x < w → (Ackermann3 x y $ Ackermann3 c b a) < (Ackermann3 w y $ Ackermann3 c b a)
    := Ackermann3_monotonic_3rd (by right; exact Ackermann3_positive)

練習：SS変換1回目の大小関係

よりシンプルに証明を書けるようになったはずなので、練習がてら証明してみます。

theorem F1_1st_lower_bound : Ackermann4 1 0 1 1 < F1_1st_iteration.fst.fst := by
  simp [F1_1st_iteration_eq]
  calc
    (Ackermann4 1 0 1 1)
      = (Ackermann3 3 0 3) := example2
    _ < (Ackermann3 4 0 3) := Ackermann3_monotonic_3rd (by omega) (by decide)
    _ < (Ackermann3 4 0 $ Ackermann3 3 0 3)
           := Ackermann3_monotonic_1st $ Ackermann3_inc
    _ < (Ackermann3 4 0 $ Ackermann3 3 0 $ Ackermann3 2 0 3)
           := Ackermann3_monotonic_1st $ Ackermann3_monotonic_1st $ Ackermann3_inc
    _ < (Ackermann3 4 0 $ Ackermann3 3 0 $ Ackermann3 2 0 $ Ackermann3 1 0 3)
           := Ackermann3_monotonic_1st $ Ackermann3_monotonic_1st $ Ackermann3_monotonic_1st $ Ackermann3_inc
    _ = (Ackermann3 4 0 $ Ackermann3 3 0 $ Ackermann3 2 0 $ Ackermann3 1 0 $ Ackermann3 0 1 1)
           := by rw [show 3 = Ackermann3 0 1 1 by simp [Ackermann3]]
    _ = (Ackermann3 4 1 1) := by apply Eq.symm; repeat rw [Ackermann3]

(Ackermann3 4 0 $ Ackermann3 3 0 $ Ackermann3 2 0 $ Ackermann3 1 0 $ Ackermann3 0 1 1) = (Ackermann3 4 1 1)をrepeat rw [Ackermann3]で証明できたのには驚きました。 右辺を右引数優先の（＝cdeclで自然な評価順）値呼びの順番で展開すれば一発で証明できますが、Lean 4の書き換えのパターンマッチは左側に現れるものから順番に行われる（なので正規順序に似た順序で展開しているように見える？）ため、その順番では展開してくれません。 apply Eq.symmで等式を逆順にすることで、rwがAckermann3 4 1 1の方に適用されるように誘導していたのですが、実は意図した効果を生んでおらず、結局Ackermann3 4 0 x = Ackermann3 3 x xの展開が先に行われているようでした。

どんどん式が膨らむ向きに展開していくようだったのでちゃんと見ていませんが、定義のうち前にあるものを優先的に適用しているのかもしれません。 この仮説が正しいとすると、最後に定義された | x, Nat.succ b, Nat.succ a => Ackermann3 x b $ Ackermann3 x (b+1) aを適用するのが後回しとなり、本格的なアッカーマン関数の再帰の沼に陥る前に証明が完了するのかもしれません。 そうだとすると、「A(x,b+1,a+1)=A(x,b,A(x,b+1,a))という等式を適用しない範囲での正規形」に落とし込むことによる自動証明が（引数が小さければ）可能ということなのかもしれません。 しかしながら、apply Eq.symmを消すと再帰深度制限に引っかかるのが謎です。 正規形に落とし込むことによる自動証明の成否は、等式の向きに左右されないはずだからです。 したがって、この仮説も完全には正しくないのでしょう。

実際には、19回展開する中で等式が以下のように書き換えられて証明が完了したようです。 でもよく見ると、Ackermann3 1 0 1とAckermann3 0 1 1の違いが残っているような……？ 途中までしか表示されていないのかもしれません。

証明の途中経過（クリックして展開。長いです）

case h
⊢ Ackermann3 4 1 1 =
  Ackermann3 3 (Ackermann3 3 0 (Ackermann3 2 0 (Ackermann3 1 0 (Ackermann3 0 1 1))))
    (Ackermann3 3 0 (Ackermann3 2 0 (Ackermann3 1 0 (Ackermann3 0 1 1))))
case h
⊢ Ackermann3 4 1 1 =
  Ackermann3 3
    (Ackermann3 2 (Ackermann3 2 0 (Ackermann3 1 0 (Ackermann3 0 1 1)))
      (Ackermann3 2 0 (Ackermann3 1 0 (Ackermann3 0 1 1))))
    (Ackermann3 2 (Ackermann3 2 0 (Ackermann3 1 0 (Ackermann3 0 1 1)))
      (Ackermann3 2 0 (Ackermann3 1 0 (Ackermann3 0 1 1))))
case h
⊢ Ackermann3 4 1 1 =
  Ackermann3 3
    (Ackermann3 2 (Ackermann3 1 (Ackermann3 1 0 (Ackermann3 0 1 1)) (Ackermann3 1 0 (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 1 0 (Ackermann3 0 1 1)) (Ackermann3 1 0 (Ackermann3 0 1 1))))
    (Ackermann3 2 (Ackermann3 1 (Ackermann3 1 0 (Ackermann3 0 1 1)) (Ackermann3 1 0 (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 1 0 (Ackermann3 0 1 1)) (Ackermann3 1 0 (Ackermann3 0 1 1))))
case h
⊢ Ackermann3 4 1 1 =
  Ackermann3 3
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))))
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))))
case h
⊢ Ackermann3 4 0 (Ackermann3 4 (0 + 1) 0) =
  Ackermann3 3
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))))
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))))
case h
⊢ Ackermann3 3 (Ackermann3 4 (0 + 1) 0) (Ackermann3 4 (0 + 1) 0) =
  Ackermann3 3
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))))
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))))
case h
⊢ Ackermann3 3 (Ackermann3 4 0 1) (Ackermann3 4 0 1) =
  Ackermann3 3
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))))
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))))
case h
⊢ Ackermann3 3 (Ackermann3 3 1 1) (Ackermann3 3 1 1) =
  Ackermann3 3
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))))
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))))
case h
⊢ Ackermann3 3 (Ackermann3 3 0 (Ackermann3 3 (0 + 1) 0)) (Ackermann3 3 0 (Ackermann3 3 (0 + 1) 0)) =
  Ackermann3 3
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))))
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))))
case h
⊢ Ackermann3 3 (Ackermann3 2 (Ackermann3 3 (0 + 1) 0) (Ackermann3 3 (0 + 1) 0))
    (Ackermann3 2 (Ackermann3 3 (0 + 1) 0) (Ackermann3 3 (0 + 1) 0)) =
  Ackermann3 3
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))))
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))))
case h
⊢ Ackermann3 3 (Ackermann3 2 (Ackermann3 3 0 1) (Ackermann3 3 0 1)) (Ackermann3 2 (Ackermann3 3 0 1) (Ackermann3 3 0 1)) =
  Ackermann3 3
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))))
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))))
case h
⊢ Ackermann3 3 (Ackermann3 2 (Ackermann3 2 1 1) (Ackermann3 2 1 1)) (Ackermann3 2 (Ackermann3 2 1 1) (Ackermann3 2 1 1)) =
  Ackermann3 3
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))))
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))))
case h
⊢ Ackermann3 3 (Ackermann3 2 (Ackermann3 2 0 (Ackermann3 2 (0 + 1) 0)) (Ackermann3 2 0 (Ackermann3 2 (0 + 1) 0)))
    (Ackermann3 2 (Ackermann3 2 0 (Ackermann3 2 (0 + 1) 0)) (Ackermann3 2 0 (Ackermann3 2 (0 + 1) 0))) =
  Ackermann3 3
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))))
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))))
case h
⊢ Ackermann3 3
    (Ackermann3 2 (Ackermann3 1 (Ackermann3 2 (0 + 1) 0) (Ackermann3 2 (0 + 1) 0))
      (Ackermann3 1 (Ackermann3 2 (0 + 1) 0) (Ackermann3 2 (0 + 1) 0)))
    (Ackermann3 2 (Ackermann3 1 (Ackermann3 2 (0 + 1) 0) (Ackermann3 2 (0 + 1) 0))
      (Ackermann3 1 (Ackermann3 2 (0 + 1) 0) (Ackermann3 2 (0 + 1) 0))) =
  Ackermann3 3
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))))
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))))
case h
⊢ Ackermann3 3
    (Ackermann3 2 (Ackermann3 1 (Ackermann3 2 0 1) (Ackermann3 2 0 1))
      (Ackermann3 1 (Ackermann3 2 0 1) (Ackermann3 2 0 1)))
    (Ackermann3 2 (Ackermann3 1 (Ackermann3 2 0 1) (Ackermann3 2 0 1))
      (Ackermann3 1 (Ackermann3 2 0 1) (Ackermann3 2 0 1))) =
  Ackermann3 3
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))))
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))))
case h
⊢ Ackermann3 3
    (Ackermann3 2 (Ackermann3 1 (Ackermann3 1 1 1) (Ackermann3 1 1 1))
      (Ackermann3 1 (Ackermann3 1 1 1) (Ackermann3 1 1 1)))
    (Ackermann3 2 (Ackermann3 1 (Ackermann3 1 1 1) (Ackermann3 1 1 1))
      (Ackermann3 1 (Ackermann3 1 1 1) (Ackermann3 1 1 1))) =
  Ackermann3 3
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))))
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))))
case h
⊢ Ackermann3 3
    (Ackermann3 2 (Ackermann3 1 (Ackermann3 1 0 (Ackermann3 1 (0 + 1) 0)) (Ackermann3 1 0 (Ackermann3 1 (0 + 1) 0)))
      (Ackermann3 1 (Ackermann3 1 0 (Ackermann3 1 (0 + 1) 0)) (Ackermann3 1 0 (Ackermann3 1 (0 + 1) 0))))
    (Ackermann3 2 (Ackermann3 1 (Ackermann3 1 0 (Ackermann3 1 (0 + 1) 0)) (Ackermann3 1 0 (Ackermann3 1 (0 + 1) 0)))
      (Ackermann3 1 (Ackermann3 1 0 (Ackermann3 1 (0 + 1) 0)) (Ackermann3 1 0 (Ackermann3 1 (0 + 1) 0)))) =
  Ackermann3 3
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))))
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))))
case h
⊢ Ackermann3 3
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 1 (0 + 1) 0) (Ackermann3 1 (0 + 1) 0))
        (Ackermann3 0 (Ackermann3 1 (0 + 1) 0) (Ackermann3 1 (0 + 1) 0)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 1 (0 + 1) 0) (Ackermann3 1 (0 + 1) 0))
        (Ackermann3 0 (Ackermann3 1 (0 + 1) 0) (Ackermann3 1 (0 + 1) 0))))
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 1 (0 + 1) 0) (Ackermann3 1 (0 + 1) 0))
        (Ackermann3 0 (Ackermann3 1 (0 + 1) 0) (Ackermann3 1 (0 + 1) 0)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 1 (0 + 1) 0) (Ackermann3 1 (0 + 1) 0))
        (Ackermann3 0 (Ackermann3 1 (0 + 1) 0) (Ackermann3 1 (0 + 1) 0)))) =
  Ackermann3 3
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))))
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))))
case h
⊢ Ackermann3 3
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 1 0 1) (Ackermann3 1 0 1))
        (Ackermann3 0 (Ackermann3 1 0 1) (Ackermann3 1 0 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 1 0 1) (Ackermann3 1 0 1))
        (Ackermann3 0 (Ackermann3 1 0 1) (Ackermann3 1 0 1))))
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 1 0 1) (Ackermann3 1 0 1))
        (Ackermann3 0 (Ackermann3 1 0 1) (Ackermann3 1 0 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 1 0 1) (Ackermann3 1 0 1))
        (Ackermann3 0 (Ackermann3 1 0 1) (Ackermann3 1 0 1)))) =
  Ackermann3 3
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))))
    (Ackermann3 2
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1)))
      (Ackermann3 1 (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))
        (Ackermann3 0 (Ackermann3 0 1 1) (Ackermann3 0 1 1))))

△展開ここまで

SS変換2回目の等式

SS変換を2回行った時点で、

  • 数：Ackermann3 (4*(Ackermann3 4 1 2)+4) 1 1
  • 関数：Ackermann3 (4*(Ackermann3 4 1 2)+4) 0
  • 変換：S変換を4*(Ackermann3 4 1 2)回

になっていることを示します。

def F1_2nd_iteration := Repeat SS_transform 2 ((3, fun x => x + 1), S_transform)

theorem F1_2nd_iteration_eq :
  F1_2nd_iteration
    = (
        (
          Ackermann3 (4*(Ackermann3 4 1 2)+4) 1 1,
          Ackermann3 (4*(Ackermann3 4 1 2)+4) 0
        ),
        Repeat S_transform (4*(Ackermann3 4 1 2))
      ) := by
  rw [F1_2nd_iteration, Repeat]
  simp [SS_transform]
  rw [← F1_1st_iteration, F1_1st_iteration_eq]
  simp [show Ackermann3 4 1 2 = (Ackermann3 4 0 $ Ackermann3 4 1 1) by rw [Ackermann3.eq_4]]
  set p := (Ackermann3 4 0 $ Ackermann3 4 1 1)
  constructor
  · rw [Repeat_S_transform_mul_lemma]
    rw [Repeat_S_transform_Ackermann3_lemma]
    group
  · rw [Repeat_S_transform_mul_lemma]

本題：SS変換2回目の大小関係

準備：4変数アッカーマン関数の最右引数単調増加性

使う部分であるx < y → A(1,0,0,x) < A(1,0,0,y)だけを証明します。 証明の方針としては、

  • x≠0ならば、A(x,0,x)<A(y,0,y)を証明する
  • x=0の時、1≤yを使ってA(1,0,0,0)<A(1,0,0,1)≤A(1,0,0,y)を証明する。
    • そのために、上記補題（<→<型）を弱めた補題（≤→≤型）を証明して利用する

といった形です。

<→<型の定理を≤→≤型の定理に弱める定理は標準ライブラリにあってもよさそうですが、見つかりませんでした。

lemma Ackermann4_monotonic_easy : x < y → Ackermann4 1 0 0 x < Ackermann4 1 0 0 y := by
  intro hxy

  have ht z : z ≠ 0 → z < y → Ackermann4 1 0 0 z < Ackermann4 1 0 0 y := by
    intro hz hzy
    simp [Ackermann4, Ackermann4zero_eq_Ackermann3]
    calc
      Ackermann3 z 0 z
        < Ackermann3 y 0 z := Ackermann3_monotonic_3rd (by omega) hzy
      _ < Ackermann3 y 0 y := Ackermann3_monotonic_1st hzy

  have ht' z : z ≠ 0 → z ≤ y → Ackermann4 1 0 0 z ≤ Ackermann4 1 0 0 y := by
    by_cases hzy : z = y
    · intro _ _; rw [hzy]
    · intro hz hzy; exact Nat.le_of_succ_le $ Nat.succ_le_of_lt $ ht z hz (by omega)

  by_cases hx : x = 0
  · rw [hx]; calc
      Ackermann4 1 0 0 0 < Ackermann4 1 0 0 1 := by simp [Ackermann4]
      _                  ≤ Ackermann4 1 0 0 y := ht' 1 (by decide) (by bound)
  · exact ht x hx hxy

便利補題

アッカーマン関数を展開する方向は結構簡単ですが、その逆は面倒なので、補題を用意すると便利です。 一般化した定理になっているおかげで、単にsimp [Ackermann3]で証明できるのもうれしいところです。 simpを用いた等式の証明は要するに「正規形」に達するまで展開し続けることによる証明だ、というのをわかっていると、こういうことを怯えずにできてよいですね。

lemma Ackermann3_unfold1 n :
  (Ackermann3 n 0 $ Ackermann3 n 1 1) = Ackermann3 n 1 2 := by simp [Ackermann3]
lemma Ackermann3_unfold2 n :
  (Ackermann3 (n+1) 0 $ Ackermann3 n 1 1) = Ackermann3 (n+1) 1 1 := by simp [Ackermann3]

この二つを組み合わせると、A(n,1,2)よりもA(n+1,1,1)の方が大きいことを簡単に示せて便利です。

本題：SS変換2回目の大小関係

記事の最初で紹介したような方針で示すことができます。

theorem F1_2nd_lower_bound : Ackermann4 1 0 1 2 < F1_2nd_iteration.fst.fst := by
  simp [F1_2nd_iteration_eq]
  set p := Ackermann3 4 1 2 with hp
  calc
    Ackermann4 1 0 1 2
      = (Ackermann4 1 0 0 $ Ackermann4 1 0 1 1)   := Ackermann4.eq_5 1 0 0 1
    _ = (Ackermann4 1 0 0 $ Ackermann3 3 0 3)     := by rw [example2]
    _ < (Ackermann4 1 0 0 $ Ackermann3 4 1 2)     := Ackermann4_monotonic_easy ?h₁
    _ = (Ackermann3 p 0 $ Ackermann3 4 1 2)
           := by rw [Ackermann4.eq_2, Ackermann4zero_eq_Ackermann3]
    _ < (Ackermann3 p 0 $ Ackermann3 (4*p+3) 1 1) := Ackermann3_monotonic_1st ?h₂
    _ < (Ackermann3 (4*p+4) 0 $ Ackermann3 (4*p+3) 1 1)
           := Ackermann3_Ackermann3_monotonic_3rd (by bound)
    _ = Ackermann3 (4*p+4) 1 1                    := Ackermann3_unfold2 (4*p+3)

  · show Ackermann3 3 0 3 < Ackermann3 4 1 2
    calc
      Ackermann3 3 0 3
        ≤ Ackermann3 3 1 2 := (Ackermann3_monotonic1 3 0 2).right.left
      _ < Ackermann3 4 1 2 := Ackermann3_monotonic_3rd (by decide) (by decide)

  · show Ackermann3 4 1 2 < Ackermann3 (4*p+3) 1 1
    have : p > 2 := Ackermann3_inc
    calc
      Ackermann3 4 1 2
        = (Ackermann3 4 0 $ Ackermann3 4 1 1) := by rw [Ackermann3.eq_4]
      _ < (Ackermann3 5 0 $ Ackermann3 4 1 1) := Ackermann3_Ackermann3_monotonic_3rd (by decide)
      _ = (Ackermann3 5 1 1)       := Ackermann3_unfold2 4
      _ < (Ackermann3 (4*p+3) 1 1) := Ackermann3_monotonic_3rd (by decide) (by bound)

ここで、?h₁や?h₂はプレースホルダーで、「ここの証明は後回しにする」ということができます。 これにより、calcタクティックを使った変形の見通しを良くすることができます。

さらに精密な評価

A(1,0,0, 4p_1+4) \lt n_2 \lt A(1,0,0,4p_1+5)まで精密に挟むことができます。

上界

上界の証明は簡単です。

theorem F1_2nd_fine_upper_bound :
  F1_2nd_iteration.fst.fst < (Ackermann4 1 0 0 $ 4 * Ackermann3 4 1 2 + 5) := by
  simp [F1_2nd_iteration_eq]
  set p := Ackermann3 4 1 2 with hp
  calc
    Ackermann3 (4*p+4) 1 1
      < Ackermann3 (4*p+4) (4*p+5) (4*p+5) := Ackermann3_monotonic2 (4*p+4) 1 1 (4*p+5) (4*p+5) (by omega)
    _ = Ackermann3 (4*p+5) 0 (4*p+5)       := by rw [Ackermann3]
    _ = Ackermann4 0 (4*p+5) 0 (4*p+5)     := Eq.symm Ackermann4zero_eq_Ackermann3
    _ = Ackermann4 1 0 0 (4*p+5)           := by rw [Ackermann4]

下界

下界の証明は、3変数アッカーマン関数に関する補題がもう少し必要そうです。

準備

lemma Ackermann3_2nd_monotonic_weak :
  b₁ ≤ b₂ → Ackermann3 c b₁ a ≤ Ackermann3 c b₂ a := by
  induction b₂ with
  | zero => intro; rw [show b₁ = 0 by omega]
  | succ n ihn =>
      by_cases h : b₁ = n+1
      · simp [h]
      · intro
        refine Nat.le_of_succ_le $ Nat.succ_le_of_lt ?_ -- a < b を示すことで、a ≤ b を証明
        calc
          Ackermann3 c b₁ a
            ≤ Ackermann3 c n a     := ihn (by omega)
          _ < Ackermann3 c n (a+1) := Ackermann3_monotonic_1st (by simp)
          _ ≤ Ackermann3 c (n+1) a := (Ackermann3_monotonic1 _ _ _).right.left

最右引数が同じ場合の単調性（≤→≤）については証明していなかったので、ここで証明しました。

lemma Ackermann3_2nd_monotonic :
  b₁ < b₂ → Ackermann3 c b₁ a < Ackermann3 c b₂ a := by
  induction b₂ with
  | zero => intro; contradiction
  | succ n ihn =>
      suffices Ackermann3 c n a < Ackermann3 c (n+1) a by
        by_cases h : b₁ = n
        · rw [h]; intro; exact this
        · intro; exact Nat.lt_trans (ihn (show b₁ < n by omega)) this
      calc
        Ackermann3 c n a
        _ < Ackermann3 c n (a+1) := Ackermann3_monotonic_1st (by simp)
        _ ≤ Ackermann3 c (n+1) a := (Ackermann3_monotonic1 _ _ _).right.left

<→<についても証明してみました。二回同じのが出てくるのでsufficesでまとめてみましたが、それほど見やすくなるわけではないですね……

lemma Ackermann3_3rd_is_stronger_than_1st c a m :
  Ackermann3 c 0 (a+(m+1)) < Ackermann3 (c+(m+1)) 0 (a+1) := by
  induction m generalizing c with
  | zero =>
      calc
        Ackermann3 (c+1) 0 (a+1)
        _ = Ackermann3 c (a+1) (a+1) := by simp [Ackermann3]
        _ > Ackermann3 c 0 (a+1) := Ackermann3_2nd_monotonic (by simp)
  | succ m ihm =>
      calc
        Ackermann3 (c+(m+1+1)) 0 (a+1)
        _ = Ackermann3 (c+1+(m+1)) 0 (a+1)   := by group
        _ > Ackermann3 (c+1) 0 (a+(m+1))     := ihm (c+1)
        _ = Ackermann3 c (a+(m+1)) (a+(m+1)) := by simp [Ackermann3]
        _ = Ackermann3 c (a+m+1) (a+m+1)     := by group
        _ ≥ Ackermann3 c (a+m) (a+m+1+1)     := (Ackermann3_monotonic1 _ _ _).right.left
        _ ≥ Ackermann3 c 0 (a+m+1+1)         := Ackermann3_2nd_monotonic_weak (by simp)
        _ = Ackermann3 c 0 (a+(m+1+1))       := by group

最右引数を減らして最左引数を増やすと大きくなるという補題です。 a>0とかm>0とかをつけるのが面倒だったので、a+1とかm+1とか書いています。 推論するのが大変な形になっているので、あらわに引数を取る形にしました。 推論に任せる形だと、ihmのc引数も推論引数になってあらわに渡せないので、証明中も混乱します。

下界の証明

theorem F1_2nd_fine_lower_bound :
  (Ackermann4 1 0 0 $ 4 * Ackermann3 4 1 2 + 4) < F1_2nd_iteration.fst.fst := by
  simp [F1_2nd_iteration_eq]
  set p := Ackermann3 4 1 2 with hp
  calc
    Ackermann4 1 0 0 (4*p+4)
      = Ackermann4 0 (4*p+4) 0 (4*p+4)                := by rw [Ackermann4]
    _ = Ackermann3 (4*p+4) 0 (4*p+4)                  := Ackermann4zero_eq_Ackermann3
    _ < Ackermann3 (4*p+4) 0 (Ackermann3 (4*p+4) 0 1) := Ackermann3_monotonic_1st ?h₁
    _ = Ackermann3 (4*p+4) 1 1                        := by simp [Ackermann3]

  · show (4*p+4) < Ackermann3 (4*p+4) 0 1
    calc
      (4*p+4) < Ackermann3 0 0 (4*p+4) := by simp [Ackermann3]
      _       < Ackermann3 (4*p+4) 0 1 := by simpa using Ackermann3_3rd_is_stronger_than_1st 0 0 (4*p+3)

よくみたら、Ackermann3_3rd_is_stronger_than_1stは、A(c+m,0,a)のA(c,0,a+m)の関係ではなく、A(c+m,0,a+1)のA(c,0,a+m)の関係になっていましたね……。 結果的には証明したい命題により適合していたのでOKですが、再利用性を考えると修正する必要があるかもしれません。

まとめ

ふぃっしゅ数バージョン1のSS変換を2回行った段階で得られる数 n_2が、4変数アッカーマン関数を使って表現できる数A(1,0,1,2)より大きいことを示しました。 また、より精密な評価として、 A(1,0,0, 4\times A(4,1,2)+4) \lt n_2 \lt A(1,0,0,4\times A(4,1,2)+5)を示しました。 なお、 n_2 = A(4\times A(4,1,2)+4,1,1)であることも示しました。

証明技法としては、Repeat関数のようなものは、末尾再帰にしないほうが数学的帰納法と相性が良いことがわかりました。

Lean 4的には、プレースホルダーを用いて証明の見通しを良くする方法を学びました。

*1:https://www.kb.ecei.tohoku.ac.jp/~sumii/class/keisanki-software-kougaku-2005/lambda.pdf

*2:Haskellで効率の良いプログラムが書けないと言っているわけではありません。Bangパターンとかを使えば解決できます。普通の言語で遅延評価データ構造を作るときの大変さを考えればわかると思いますが、効率の良いプログラムを書く時に、プログラマが評価順序をよく考える必要があるのは当然のことです。

*3:「普通の」というのがどの範囲を指すのかはよくわかりませんが、少なくとも自然数であれば成り立つはずです。二重リストアッカーマン関数などの、可変長配列を引数とするものもこの枠組みに入りそうなので、適切に場合分けを設計すれば大丈夫なのでしょう。一方で、保留にした関数呼び出しの形に対するマッチングを含む定義があると、合流性が失われる可能性があるので怪しそうです。弱冠頭標準形に対する場合分けのみで成り立っていれば大丈夫そうでしょうか？



以上の内容はhttps://lpha-z.hatenablog.com/entry/2025/08/17/231500より取得しました。
このページはhttp://font.textar.tv/のウェブフォントを使用してます
不具合報告/要望等はこちらへお願いします。
モバイルやる夫Viewer Ver0.14