25 states is enough

no 16 merge 16 to 4 17 => 16 18 => 17 ... 24 => 23 25 => 24
lengyijun · Nov 17, 2024 · 77155ae · 77155ae
1 parent b084c1a
commit 77155ae
Show file tree

Hide file tree

Showing 15 changed files with 471 additions and 151 deletions.
diff --git a/26_to_25.md b/26_to_25.md
@@ -0,0 +1,242 @@
+# How I reduce 26 states to 25 states
+
+Notice 16.1 is unreachable.
+
+So we need to find state X where X.0 is unreachable so that we can merge X and 16.
+
+## Outline
+1. search unvisited triples
+2. review suspicious triples, try merge branches
+3. state 4 is found
+
+
+## Details
+1. `lake exe sim26 > /tmp/log/26` to collect 100M logs.
+
+2. I use this script to list all possible triples X-Y-Z where (X.0 -> Y OR X.1 -> Y) AND (Y.0 -> Z OR Y.1 -> Z)
+
+```
+import GoldbachTm.Tm26.TuringMachine26
+import GoldbachTm.Basic
+import Init.Data.List.Basic
+
+open Tm26
+
+unsafe def bar : (zs: List (Fin 26 × Fin 26 × Fin 26 × Stmt)) -> IO Unit
+| [] => pure ()
+| ⟨a, b, c, _⟩ :: zs =>
+      if b < 10 then
+        if c < 10 then
+          do
+            IO.println s!"'rg --multiline -l \"{a}.*\\n {b}.*\\n {c}\"'"
+            bar zs
+        else
+          do
+            IO.println s!"'rg --multiline -l \"{a}.*\\n {b}.*\\n{c}\"'"
+            bar zs
+      else
+        if c < 10 then
+          do
+            IO.println s!"'rg --multiline -l \"{a}.*\\n{b}.*\\n {c}\"'"
+            bar zs
+        else
+          do
+            IO.println s!"'rg --multiline -l \"{a}.*\\n{b}.*\\n{c}\"'"
+            bar zs
+
+
+unsafe def main : List String → IO Unit
+| _ =>  let x : List (Fin 26) := [
+  ⟨0, by omega⟩,
+  ⟨1, by omega⟩,
+  ⟨2, by omega⟩,
+  ⟨3, by omega⟩,
+  ⟨4, by omega⟩,
+  ⟨5, by omega⟩,
+  ⟨6, by omega⟩,
+  ⟨7, by omega⟩,
+  ⟨8, by omega⟩,
+  ⟨9, by omega⟩,
+  ⟨10, by omega⟩,
+  ⟨11, by omega⟩,
+  ⟨12, by omega⟩,
+  ⟨13, by omega⟩,
+  ⟨14, by omega⟩,
+  ⟨15, by omega⟩,
+  ⟨16, by omega⟩,
+  ⟨17, by omega⟩,
+  ⟨18, by omega⟩,
+  ⟨19, by omega⟩,
+  ⟨20, by omega⟩,
+  ⟨21, by omega⟩,
+  ⟨22, by omega⟩,
+  ⟨23, by omega⟩,
+  ⟨24, by omega⟩,
+  ⟨25, by omega⟩,
+]
+        let y := x.map (fun q => [
+          (machine q Γ.zero).map (fun ⟨a, b⟩ => (q, a)),
+          (machine q Γ.one).map  (fun ⟨a, b⟩ => (q, a))
+        ])
+        let z := y.flatten.reduceOption
+        let z := z.map (fun ⟨q1, q2⟩ => [
+          (machine q2 Γ.zero).map (fun c => (q1, q2, c)),
+          (machine q2 Γ.one).map (fun c => (q1, q2, c)),
+        ])
+        let z := z.flatten.reduceOption
+        bar z
+```
+
+Copy the output to following `/tmp/b.sh`
+
+```
+#!/bin/bash
+
+# /tmp/b.sh
+
+# List of commands
+commands=(
+
+'rg --multiline -l "0.*\n23.*\n24"'
+'rg --multiline -l "0.*\n23.*\n23"'
+'rg --multiline -l "0.*\n 1.*\n17"'
+'rg --multiline -l "0.*\n 1.*\n 2"'
+'rg --multiline -l "1.*\n17.*\n18"'
+'rg --multiline -l "1.*\n17.*\n17"'
+'rg --multiline -l "1.*\n 2.*\n21"'
+'rg --multiline -l "1.*\n 2.*\n 3"'
+'rg --multiline -l "2.*\n21.*\n24"'
+'rg --multiline -l "2.*\n21.*\n21"'
+'rg --multiline -l "2.*\n 3.*\n21"'
+'rg --multiline -l "2.*\n 3.*\n 4"'
+'rg --multiline -l "3.*\n21.*\n24"'
+'rg --multiline -l "3.*\n21.*\n21"'
+'rg --multiline -l "3.*\n 4.*\n 9"'
+'rg --multiline -l "3.*\n 4.*\n 5"'
+'rg --multiline -l "4.*\n 9.*\n10"'
+'rg --multiline -l "4.*\n 9.*\n22"'
+'rg --multiline -l "4.*\n 5.*\n 4"'
+'rg --multiline -l "4.*\n 5.*\n 5"'
+'rg --multiline -l "5.*\n 4.*\n 9"'
+'rg --multiline -l "5.*\n 4.*\n 5"'
+'rg --multiline -l "5.*\n 5.*\n 4"'
+'rg --multiline -l "5.*\n 5.*\n 5"'
+'rg --multiline -l "6.*\n 8.*\n 9"'
+'rg --multiline -l "6.*\n 8.*\n 8"'
+'rg --multiline -l "6.*\n 7.*\n 9"'
+'rg --multiline -l "6.*\n 7.*\n 7"'
+'rg --multiline -l "7.*\n 9.*\n10"'
+'rg --multiline -l "7.*\n 9.*\n22"'
+'rg --multiline -l "7.*\n 7.*\n 9"'
+'rg --multiline -l "7.*\n 7.*\n 7"'
+'rg --multiline -l "8.*\n 9.*\n10"'
+'rg --multiline -l "8.*\n 9.*\n22"'
+'rg --multiline -l "8.*\n 8.*\n 9"'
+'rg --multiline -l "8.*\n 8.*\n 8"'
+'rg --multiline -l "9.*\n10.*\n10"'
+'rg --multiline -l "9.*\n10.*\n11"'
+'rg --multiline -l "9.*\n22.*\n18"'
+'rg --multiline -l "9.*\n22.*\n22"'
+'rg --multiline -l "10.*\n10.*\n10"'
+'rg --multiline -l "10.*\n10.*\n11"'
+'rg --multiline -l "10.*\n11.*\n12"'
+'rg --multiline -l "10.*\n11.*\n11"'
+'rg --multiline -l "11.*\n12.*\n14"'
+'rg --multiline -l "11.*\n12.*\n13"'
+'rg --multiline -l "11.*\n11.*\n12"'
+'rg --multiline -l "11.*\n11.*\n11"'
+'rg --multiline -l "12.*\n14.*\n15"'
+'rg --multiline -l "12.*\n14.*\n14"'
+'rg --multiline -l "12.*\n13.*\n 6"'
+'rg --multiline -l "12.*\n13.*\n13"'
+'rg --multiline -l "13.*\n 6.*\n 8"'
+'rg --multiline -l "13.*\n 6.*\n 7"'
+'rg --multiline -l "13.*\n13.*\n 6"'
+'rg --multiline -l "13.*\n13.*\n13"'
+'rg --multiline -l "14.*\n15.*\n16"'
+'rg --multiline -l "14.*\n15.*\n19"'
+'rg --multiline -l "14.*\n14.*\n15"'
+'rg --multiline -l "14.*\n14.*\n14"'
+'rg --multiline -l "15.*\n16.*\n17"'
+'rg --multiline -l "15.*\n19.*\n20"'
+'rg --multiline -l "15.*\n19.*\n19"'
+'rg --multiline -l "16.*\n17.*\n18"'
+'rg --multiline -l "16.*\n17.*\n17"'
+'rg --multiline -l "17.*\n18.*\n 9"'
+'rg --multiline -l "17.*\n18.*\n25"'
+'rg --multiline -l "17.*\n17.*\n18"'
+'rg --multiline -l "17.*\n17.*\n17"'
+'rg --multiline -l "18.*\n 9.*\n10"'
+'rg --multiline -l "18.*\n 9.*\n22"'
+'rg --multiline -l "18.*\n25.*\n24"'
+'rg --multiline -l "19.*\n20.*\n 2"'
+'rg --multiline -l "19.*\n20.*\n20"'
+'rg --multiline -l "19.*\n19.*\n20"'
+'rg --multiline -l "19.*\n19.*\n19"'
+'rg --multiline -l "20.*\n 2.*\n21"'
+'rg --multiline -l "20.*\n 2.*\n 3"'
+'rg --multiline -l "20.*\n20.*\n 2"'
+'rg --multiline -l "20.*\n20.*\n20"'
+'rg --multiline -l "21.*\n24.*\n 0"'
+'rg --multiline -l "21.*\n24.*\n24"'
+'rg --multiline -l "21.*\n21.*\n24"'
+'rg --multiline -l "21.*\n21.*\n21"'
+'rg --multiline -l "22.*\n18.*\n 9"'
+'rg --multiline -l "22.*\n18.*\n25"'
+'rg --multiline -l "22.*\n22.*\n18"'
+'rg --multiline -l "22.*\n22.*\n22"'
+'rg --multiline -l "23.*\n24.*\n 0"'
+'rg --multiline -l "23.*\n24.*\n24"'
+'rg --multiline -l "23.*\n23.*\n24"'
+'rg --multiline -l "23.*\n23.*\n23"'
+'rg --multiline -l "24.*\n 0.*\n23"'
+'rg --multiline -l "24.*\n 0.*\n 1"'
+'rg --multiline -l "24.*\n24.*\n 0"'
+'rg --multiline -l "24.*\n24.*\n24"'
+'rg --multiline -l "25.*\n24.*\n 0"'
+'rg --multiline -l "25.*\n24.*\n24"'
+
+)
+
+# Execute commands
+for cmd in "${commands[@]}"; do
+    output=$(eval "$cmd")
+    if [ -z "$output" ]; then
+        echo "$cmd"
+    fi
+done
+```
+
+```
+# filter out unvisited triples
+cd /tmp/log/26
+bash /tmp/b.sh
+```
+
+We got thost unvisited triples, grouped by middle state : 
+
+```
+rg --multiline -l "5.*\n 4.*\n 5"
+rg --multiline -l "3.*\n 4.*\n 9"
+
+rg --multiline -l "23.*\n24.*\n 0"
+rg --multiline -l "25.*\n24.*\n24"
+
+rg --multiline -l "4.*\n 9.*\n22"
+rg --multiline -l "7.*\n 9.*\n22"
+rg --multiline -l "18.*\n 9.*\n10"
+
+rg --multiline -l "20.*\n 2.*\n21"
+rg --multiline -l "4.*\n 5.*\n 4"
+rg --multiline -l "6.*\n 8.*\n 9"
+rg --multiline -l "12.*\n13.*\n 6"
+rg --multiline -l "12.*\n14.*\n15"
+rg --multiline -l "16.*\n17.*\n18"
+rg --multiline -l "22.*\n18.*\n 9"
+rg --multiline -l "19.*\n20.*\n 2"
+rg --multiline -l "3.*\n21.*\n24"
+rg --multiline -l "9.*\n22.*\n18"
+```
+
+We notice that state 4 maybe the optimizer.
+
diff --git a/27_to_26.md b/27_to_26.md
@@ -0,0 +1,5 @@
+# How I reduce 27 states to 26 states
+
+Use `sort TuringMachine27.lean | uniq -D` to inspect duplicate lines
+Check them one by one.
+You will found 24 and 22 are duplicates
diff --git a/GoldbachTm.lean b/GoldbachTm.lean
@@ -4,13 +4,13 @@ import GoldbachTm.Basic
 import GoldbachTm.Format
 import GoldbachTm.ListBlank
 
-import GoldbachTm.Tm26.TuringMachine26
-import GoldbachTm.Tm26.Search0
-import GoldbachTm.Tm26.Transition
-import GoldbachTm.Tm26.Miscellaneous
-import GoldbachTm.Tm26.Prime
-import GoldbachTm.Tm26.PBP
-import GoldbachTm.Tm26.Content
+import GoldbachTm.Tm25.TuringMachine25
+import GoldbachTm.Tm25.Search0
+import GoldbachTm.Tm25.Transition
+import GoldbachTm.Tm25.Miscellaneous
+import GoldbachTm.Tm25.Prime
+import GoldbachTm.Tm25.PBP
+import GoldbachTm.Tm25.Content
 
 import GoldbachTm.Tm31.TuringMachine31
 import GoldbachTm.Tm31.Search0

diff --git a/GoldbachTm/Basic.lean b/GoldbachTm/Basic.lean
@@ -129,7 +129,7 @@ induction n with
 
 /-
 P i => nth_cfg i ≠ none
-Q i n => nth_cfg i = some ⟨⟨25, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (2*n+4) Γ.one), Turing.ListBlank.mk []⟩⟩
+Q i n => nth_cfg i = some ⟨⟨24, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (2*n+4) Γ.one), Turing.ListBlank.mk []⟩⟩
 -/
 theorem propagating_induction (P : ℕ → Prop) (Q : ℕ → ℕ → Prop)
                (base : ℕ) (hbase : Q base 0)

diff --git a/GoldbachTm/Tm26/Content.lean → GoldbachTm/Tm25/Content.lean b/GoldbachTm/Tm26/Content.lean → GoldbachTm/Tm25/Content.lean
@@ -1,20 +1,20 @@
-import GoldbachTm.Tm26.TuringMachine26
-import GoldbachTm.Tm26.Search0
-import GoldbachTm.Tm26.PBP
+import GoldbachTm.Tm25.TuringMachine25
+import GoldbachTm.Tm25.Search0
+import GoldbachTm.Tm25.PBP
 import Mathlib.Data.Nat.Prime.Defs
 
-namespace Tm26
+namespace Tm25
 
-theorem lemma_22 (n : ℕ) (i : ℕ)
+theorem lemma_21 (n : ℕ) (i : ℕ)
 (even_n : Even (n+2))
 (g :
-nth_cfg i = some ⟨⟨22, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (n+4) Γ.one), Turing.ListBlank.mk []⟩⟩ )
+nth_cfg i = some ⟨⟨21, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (n+4) Γ.one), Turing.ListBlank.mk []⟩⟩ )
 ( hpp : Goldbach (n+4)) :
-∃ j>i, nth_cfg j = some ⟨⟨22, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (n+4+2) Γ.one), Turing.ListBlank.mk []⟩⟩
+∃ j>i, nth_cfg j = some ⟨⟨21, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (n+4+2) Γ.one), Turing.ListBlank.mk []⟩⟩
 := by
 forward g
 repeat rw [← List.replicate_succ] at g
-apply (leap_18 _ _ 0) at g
+apply (leap_17 _ _ 0) at g
 any_goals omega
 any_goals assumption
 refine (?_ ∘ g) ?_
@@ -40,7 +40,7 @@ refine (?_ ∘ g) ?_
 
 lemma never_halt_step (n : ℕ) :
 (∀ i < n, Goldbach (2*i+4)) ->
-∃ j, nth_cfg j = some ⟨⟨22, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (2*n+4) Γ.one), Turing.ListBlank.mk []⟩⟩
+∃ j, nth_cfg j = some ⟨⟨21, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (2*n+4) Γ.one), Turing.ListBlank.mk []⟩⟩
  := by
 induction n with
 | zero =>
@@ -54,7 +54,7 @@ refine (?_ ∘ induction_step) ?_
 . intros g
   obtain ⟨j, g⟩ := g
   specialize h n (by omega)
-  apply lemma_22 at g
+  apply lemma_21 at g
   . specialize g h
     obtain ⟨k, g⟩ := g
     use k
@@ -73,7 +73,7 @@ apply never_halt_step at IH
 obtain ⟨j, g⟩ := IH
 forward g
 repeat rw [← List.replicate_succ] at g
-apply (leap_18_halt _ _ 0) at g
+apply (leap_17_halt _ _ 0) at g
 any_goals omega
 by_contra! h
 refine (?_ ∘ g) ?_
@@ -88,10 +88,10 @@ refine (?_ ∘ g) ?_
 
 theorem halt_lemma_rev' (h : ∀ n, Goldbach (2*n+4)) :
 ∀ i, nth_cfg i ≠ none := by
-apply propagating_induction (fun i => nth_cfg i ≠ none) (fun i n => nth_cfg i = some ⟨⟨22, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (2*n+4) Γ.one), Turing.ListBlank.mk []⟩⟩) 45
+apply propagating_induction (fun i => nth_cfg i ≠ none) (fun i n => nth_cfg i = some ⟨⟨21, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (2*n+4) Γ.one), Turing.ListBlank.mk []⟩⟩) 45
 . simp [cfg45]; tauto
 . intros i n g
-  apply (lemma_22 (2*n)) at g
+  apply (lemma_21 (2*n)) at g
   . specialize g (h _)
     obtain ⟨j, g⟩ := g
     use j
@@ -120,7 +120,7 @@ by rw [← Mathlib.Tactic.PushNeg.not_not_eq (Goldbach (2*i+4))]
 )
 forward hj
 repeat rw [← List.replicate_succ] at hj
-apply (leap_18_halt _ _ 0) at hj
+apply (leap_17_halt _ _ 0) at hj
 any_goals omega
 apply hj
 intros x y _
@@ -135,4 +135,4 @@ by_contra! g
 apply halt_lemma_rev' at g
 tauto
 
-end Tm26
+end Tm25
diff --git a/GoldbachTm/Tm26/Miscellaneous.lean → GoldbachTm/Tm25/Miscellaneous.lean b/GoldbachTm/Tm26/Miscellaneous.lean → GoldbachTm/Tm25/Miscellaneous.lean
@@ -1,9 +1,9 @@
 -- some lemmas tm31 doesn't contain
 
-import GoldbachTm.Tm26.TuringMachine26
-import GoldbachTm.Tm26.Transition
+import GoldbachTm.Tm25.TuringMachine25
+import GoldbachTm.Tm25.Transition
 
-namespace Tm26
+namespace Tm25
 
 theorem lemma7 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
 nth_cfg i = some ⟨⟨7, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ →
@@ -39,7 +39,7 @@ induction k with (intros i l r h; simp_all)
 
 theorem lemma5 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
 nth_cfg i = some ⟨⟨5, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ →
-nth_cfg (i + k + 2) = some ⟨⟨4, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (Γ.zero :: l), Turing.ListBlank.mk (List.replicate k Γ.zero ++ r)⟩⟩ := by
+nth_cfg (i + k + 2) = some ⟨⟨7, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (Γ.zero :: l), Turing.ListBlank.mk (List.replicate k Γ.zero ++ r)⟩⟩ := by
 induction k with (intros i l r h; simp_all)
 | zero => iterate 2 forward h
           rw [← h]
@@ -111,4 +111,4 @@ cases r1 with simp_all
              simp [h]
              omega
 
-end Tm26
+end Tm25