Skip to content

Latest commit

 

History

History
244 lines (217 loc) · 6.82 KB

26_to_25.md

File metadata and controls

244 lines (217 loc) · 6.82 KB

How I reduce 26 states to 25 states

Key idea is to eliminate unreachable branch.

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 the 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: 4.0 is redundant: 4.0 could be replaced with 7.0