Geb.Prototypes.Computability.TreeScanner.Machine

Imports

/-
Copyright (c) 2026 Terence Rokop. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Terence Rokop
-/
module

public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic
public import Geb.Mathlib.Data.Tree.Ranked.Binary

A linear-time tree scanner

A deterministic multi-tape Turing machine deciding RankedAlphabet.Binary.binRanked.validBool. The pending count is the work head's position, with distinct markers at cells 0 and 1 so that one read separates a count of 0, of 1, and of 2 or more — the three-way distinction a node bit's guard and the final test between them require. The machine is a one-counter recognizer for a prefix-code term language.

Main definitions

boolEmb — the input alphabet's embedding into the machine alphabet.

stSeek, stPlant, stLive, stDead — the four states.

treeScanner — the machine.

seekCfg, plantCfg, sweepCfg — the closed-form configurations.

Main statements

validBool_eq_ok_and_depth — the decision function as the pair of conditions the machine computes.

seekCfg_state, seekCfg_inputPos_val, seekCfg_workTapePos, seekCfg_workTapes, plantCfg_state, plantCfg_inputPos_val, plantCfg_workTapePos, plantCfg_workTapes, sweepCfg_state, sweepCfg_inputPos_val, sweepCfg_workTapePos, sweepCfg_workTapes — the field projections of the three configurations.

sweepCfg_state_live, sweepCfg_state_dead — the sweep configuration's state at a live and at a failed scan.

sweepCfg_workTapeSymbols_eq — the sweep configuration's work-symbol function, in the unapplied form tr consumes.

seekCfg_zero — seekCfg at index 0 is treeScanner.initCfg.

Implementation notes

Cfg is indexed by the input, so no proof here inducts on the input; each configuration is a closed form in a step or drop index.

Tags

Turing machine, tree, preorder encoding, linear time

              @[expose] public sectionnamespace Geb.TreeScanneropen Turing MultiTapeTM RankedAlphabet.Binary

The input alphabet's embedding into the machine alphabet: false to 0 and true to 1.

def boolEmb : Bool ↪ Fin 2 where
  toFun b := if b then 1 else 0
  inj' a b := bya:Boolb:Bool⊢ (fun b ↦ if b = true then 1 else 0) a = (fun b ↦ if b = true then 1 else 0) b → a = b cases afalseb:Bool⊢ (fun b ↦ if b = true then 1 else 0) false = (fun b ↦ if b = true then 1 else 0) b → false = btrueb:Bool⊢ (fun b ↦ if b = true then 1 else 0) true = (fun b ↦ if b = true then 1 else 0) b → true = b <;>falseb:Bool⊢ (fun b ↦ if b = true then 1 else 0) false = (fun b ↦ if b = true then 1 else 0) b → false = btrueb:Bool⊢ (fun b ↦ if b = true then 1 else 0) true = (fun b ↦ if b = true then 1 else 0) b → true = b cases btrue.false⊢ (fun b ↦ if b = true then 1 else 0) true = (fun b ↦ if b = true then 1 else 0) false → true = falsetrue.true⊢ (fun b ↦ if b = true then 1 else 0) true = (fun b ↦ if b = true then 1 else 0) true → true = true <;>false.false⊢ (fun b ↦ if b = true then 1 else 0) false = (fun b ↦ if b = true then 1 else 0) false → false = falsefalse.true⊢ (fun b ↦ if b = true then 1 else 0) false = (fun b ↦ if b = true then 1 else 0) true → false = truetrue.false⊢ (fun b ↦ if b = true then 1 else 0) true = (fun b ↦ if b = true then 1 else 0) false → true = falsetrue.true⊢ (fun b ↦ if b = true then 1 else 0) true = (fun b ↦ if b = true then 1 else 0) true → true = true simpAll goals completed! 🐙

The state that walks the input head to the right end.

def stSeek : Fin 4 := ⟨0, by⊢ 0 < 4 omegaAll goals completed! 🐙⟩

The state that writes the second marker.

def stPlant : Fin 4 := ⟨1, by⊢ 1 < 4 omegaAll goals completed! 🐙⟩

The state that sweeps a live scan right to left.

def stLive : Fin 4 := ⟨2, by⊢ 2 < 4 omegaAll goals completed! 🐙⟩

The state that sweeps a failed scan right to left.

def stDead : Fin 4 := ⟨3, by⊢ 3 < 4 omegaAll goals completed! 🐙⟩

The machine. One work tape; the count is the work head's position, with a marker at cell 0 and a different marker at cell 1.

def treeScanner : MultiTapeTM 1 (Fin 2) (Fin 4) where
  q₀ := stSeek
  tr q inSym work :=
    if q = stSeek then
      match inSym with
      | none => { inputMove := -1, workActions := fun _ ↦ (some (some 0), 1),
                  outS := none, q' := some stPlant }
      | some _ => { inputMove := 1, workActions := fun _ ↦ (none, 0),
                    outS := none, q' := some stSeek }
    else if q = stPlant then
      { inputMove := 0, workActions := fun _ ↦ (some (some 1), -1),
        outS := none, q' := some stLive }
    else if q = stLive then
      match inSym with
      | some 0 => { inputMove := -1, workActions := fun _ ↦ (none, 1),
                    outS := none, q' := some stLive }
      | some _ =>
        match work 0 with
        | none => { inputMove := -1, workActions := fun _ ↦ (none, -1),
                    outS := none, q' := some stLive }
        | some _ => { inputMove := -1, workActions := fun _ ↦ (none, 0),
                      outS := none, q' := some stDead }
      | none =>
        match work 0 with
        | some 1 => { inputMove := 0, workActions := fun _ ↦ (none, 0),
                      outS := some 1, q' := none }
        | _ => { inputMove := 0, workActions := fun _ ↦ (none, 0),
                 outS := some 0, q' := none }
    else
      match inSym with
      | some _ => { inputMove := -1, workActions := fun _ ↦ (none, 0),
                    outS := none, q' := some stDead }
      | none => { inputMove := 0, workActions := fun _ ↦ (none, 0),
                  outS := some 0, q' := none }

The configuration after t seek steps: the input head at t + 1, the work tape blank and its head at cell 0. At t = 0 this is initCfg.

def seekCfg (w : List Bool) (t : ℕ) (ht : t ≤ w.length) :
    Cfg 1 (Fin 2) (Fin 4) (w.map boolEmb) where
  state := some stSeek
  inputPos := ⟨t + 1, byw:List Boolt:ℕht:t ≤ w.length⊢ t + 1 < (List.map (⇑boolEmb) w).length + 2 simp only [List.length_map]w:List Boolt:ℕht:t ≤ w.length⊢ t + 1 < w.length + 2; omegaAll goals completed! 🐙⟩
  workTapes _ _ := none
  workTapePos _ := 0

The configuration after the seek's exit step: the first marker written, the work head at cell 1, the input head at position w.length.

def plantCfg (w : List Bool) : Cfg 1 (Fin 2) (Fin 4) (w.map boolEmb) where
  state := some stPlant
  inputPos := ⟨w.length, byw:List Bool⊢ w.length < (List.map (⇑boolEmb) w).length + 2 simp only [List.length_map]w:List Bool⊢ w.length < w.length + 2; omegaAll goals completed! 🐙⟩
  workTapes _ z := if z = 0 then some 0 else none
  workTapePos _ := 1

The configuration at the sweep boundary where w.drop k has been consumed: the count is that suffix's pending depth and the state is live exactly when the suffix's scan has not failed.

def sweepCfg (w : List Bool) (k : ℕ) (hk : k ≤ w.length) :
    Cfg 1 (Fin 2) (Fin 4) (w.map boolEmb) where
  state := if ok (w.drop k) then some stLive else some stDead
  inputPos := ⟨k, byw:List Boolk:ℕhk:k ≤ w.length⊢ k < (List.map (⇑boolEmb) w).length + 2 simp only [List.length_map]w:List Boolk:ℕhk:k ≤ w.length⊢ k < w.length + 2; omegaAll goals completed! 🐙⟩
  workTapes _ z := if z = 0 then some 0 else if z = 1 then some 1 else none
  workTapePos _ := (depth (w.drop k) : ℤ)

section CfgProjectionsvariable (w : List Bool) (t k : ℕ) (ht : t ≤ w.length) (hk : k ≤ w.length)

seekCfg is in the seeking state.

@[simp] theorem seekCfg_state : (seekCfg w t ht).state = some stSeek := rfl

seekCfg's input head is at t + 1.

@[simp] theorem seekCfg_inputPos_val : (seekCfg w t ht).inputPos.val = t + 1 := rfl

seekCfg's work head is at cell 0.

@[simp] theorem seekCfg_workTapePos (i : Fin 1) : (seekCfg w t ht).workTapePos i = 0 := rfl

seekCfg's work tape is blank everywhere. Not @[simp]: a step lemma cites this rather than letting simp unfold seekCfg in place.

theorem seekCfg_workTapes (i : Fin 1) (z : ℤ) : (seekCfg w t ht).workTapes i z = none := rfl

plantCfg is in the planting state.

@[simp] theorem plantCfg_state : (plantCfg w).state = some stPlant := rfl

plantCfg's input head is at w.length.

@[simp] theorem plantCfg_inputPos_val : (plantCfg w).inputPos.val = w.length := rfl

plantCfg's work head is at cell 1.

@[simp] theorem plantCfg_workTapePos (i : Fin 1) : (plantCfg w).workTapePos i = 1 := rfl

plantCfg's work tape holds the first marker at cell 0 and is blank elsewhere. Not @[simp]: a step lemma cites this rather than letting simp unfold plantCfg in place.

theorem plantCfg_workTapes (i : Fin 1) (z : ℤ) :
    (plantCfg w).workTapes i z = if z = 0 then some 0 else none := rfl

sweepCfg's state is live exactly where the consumed suffix's scan has not failed.

theorem sweepCfg_state :
    (sweepCfg w k hk).state = if ok (w.drop k) then some stLive else some stDead := rfl

Where the consumed suffix's scan has not failed, sweepCfg is in the live state.

theorem sweepCfg_state_live (hok : ok (w.drop k) = true) :
    (sweepCfg w k hk).state = some stLive := byw:List Boolk:ℕhk:k ≤ w.lengthhok:ok (List.drop k w) = true⊢ (sweepCfg w k hk).state = some stLive
  rw [sweepCfg_state,w:List Boolk:ℕhk:k ≤ w.lengthhok:ok (List.drop k w) = true⊢ (if ok (List.drop k w) = true then some stLive else some stDead) = some stLive ite_eq_left hokw:List Boolk:ℕhk:k ≤ w.lengthhok:ok (List.drop k w) = true⊢ some stLive = some stLive]All goals completed! 🐙

Where the consumed suffix's scan has failed, sweepCfg is in the dead state.

theorem sweepCfg_state_dead (hok : ok (w.drop k) = false) :
    (sweepCfg w k hk).state = some stDead := byw:List Boolk:ℕhk:k ≤ w.lengthhok:ok (List.drop k w) = false⊢ (sweepCfg w k hk).state = some stDead
  rw [sweepCfg_state,w:List Boolk:ℕhk:k ≤ w.lengthhok:ok (List.drop k w) = false⊢ (if ok (List.drop k w) = true then some stLive else some stDead) = some stDead hokw:List Boolk:ℕhk:k ≤ w.lengthhok:ok (List.drop k w) = false⊢ (if false = true then some stLive else some stDead) = some stDead]w:List Boolk:ℕhk:k ≤ w.lengthhok:ok (List.drop k w) = false⊢ (if false = true then some stLive else some stDead) = some stDead
  rflAll goals completed! 🐙

sweepCfg's input head is at k.

@[simp] theorem sweepCfg_inputPos_val : (sweepCfg w k hk).inputPos.val = k := rfl

sweepCfg's work head is at the consumed suffix's pending depth.

@[simp] theorem sweepCfg_workTapePos (i : Fin 1) :
    (sweepCfg w k hk).workTapePos i = (depth (w.drop k) : ℤ) := rfl

sweepCfg's work tape holds the first marker at cell 0, the second at cell 1, and is blank elsewhere. Not @[simp]: a step lemma cites this rather than letting simp unfold sweepCfg in place.

theorem sweepCfg_workTapes (i : Fin 1) (z : ℤ) :
    (sweepCfg w k hk).workTapes i z = if z = 0 then some 0 else if z = 1 then some 1 else none :=
  rfl

end CfgProjections

The work-symbol function at a sweep configuration, in the unapplied form tr consumes: tr takes the work-symbol function, not its value at 0. It separates a pending depth of 0, of 1, and of at least 2.

theorem sweepCfg_workTapeSymbols_eq (w : List Bool) (k : ℕ) (hk : k ≤ w.length) :
    (sweepCfg w k hk).workTapeSymbols =
      fun _ ↦ if depth (w.drop k) = 0 then some 0
        else if depth (w.drop k) = 1 then some 1 else none := byw:List Boolk:ℕhk:k ≤ w.length⊢ (sweepCfg w k hk).workTapeSymbols = fun x ↦
  if depth (List.drop k w) = 0 then some 0 else if depth (List.drop k w) = 1 then some 1 else none
  funext iw:List Boolk:ℕhk:k ≤ w.lengthi:Fin 1⊢ (sweepCfg w k hk).workTapeSymbols i =
  if depth (List.drop k w) = 0 then some 0 else if depth (List.drop k w) = 1 then some 1 else none
  unfold Cfg.workTapeSymbols sweepCfgw:List Boolk:ℕhk:k ≤ w.lengthi:Fin 1⊢ { state := if ok (List.drop k w) = true then some stLive else some stDead, inputPos := ⟨k, ⋯⟩,
        workTapes := fun x z ↦ if z = 0 then some 0 else if z = 1 then some 1 else none,
        workTapePos := fun x ↦ ↑(depth (List.drop k w)) }.workTapes
    i
    ({ state := if ok (List.drop k w) = true then some stLive else some stDead, inputPos := ⟨k, ⋯⟩,
          workTapes := fun x z ↦ if z = 0 then some 0 else if z = 1 then some 1 else none,
          workTapePos := fun x ↦ ↑(depth (List.drop k w)) }.workTapePos
      i) =
  if depth (List.drop k w) = 0 then some 0 else if depth (List.drop k w) = 1 then some 1 else none
  dsimp onlyw:List Boolk:ℕhk:k ≤ w.lengthi:Fin 1⊢ (if ↑(depth (List.drop k w)) = 0 then some 0 else if ↑(depth (List.drop k w)) = 1 then some 1 else none) =
  if depth (List.drop k w) = 0 then some 0 else if depth (List.drop k w) = 1 then some 1 else none
  split_ifsposw:List Boolk:ℕhk:k ≤ w.lengthi:Fin 1h✝¹:↑(depth (List.drop k w)) = 0h✝:depth (List.drop k w) = 0⊢ some 0 = some 0posw:List Boolk:ℕhk:k ≤ w.lengthi:Fin 1h✝²:↑(depth (List.drop k w)) = 0h✝¹:¬depth (List.drop k w) = 0h✝:depth (List.drop k w) = 1⊢ some 0 = some 1negw:List Boolk:ℕhk:k ≤ w.lengthi:Fin 1h✝²:↑(depth (List.drop k w)) = 0h✝¹:¬depth (List.drop k w) = 0h✝:¬depth (List.drop k w) = 1⊢ Falseposw:List Boolk:ℕhk:k ≤ w.lengthi:Fin 1h✝²:¬↑(depth (List.drop k w)) = 0h✝¹:↑(depth (List.drop k w)) = 1h✝:depth (List.drop k w) = 0⊢ some 1 = some 0posw:List Boolk:ℕhk:k ≤ w.lengthi:Fin 1h✝³:¬↑(depth (List.drop k w)) = 0h✝²:↑(depth (List.drop k w)) = 1h✝¹:¬depth (List.drop k w) = 0h✝:depth (List.drop k w) = 1⊢ some 1 = some 1negw:List Boolk:ℕhk:k ≤ w.lengthi:Fin 1h✝³:¬↑(depth (List.drop k w)) = 0h✝²:↑(depth (List.drop k w)) = 1h✝¹:¬depth (List.drop k w) = 0h✝:¬depth (List.drop k w) = 1⊢ Falseposw:List Boolk:ℕhk:k ≤ w.lengthi:Fin 1h✝²:¬↑(depth (List.drop k w)) = 0h✝¹:¬↑(depth (List.drop k w)) = 1h✝:depth (List.drop k w) = 0⊢ Falseposw:List Boolk:ℕhk:k ≤ w.lengthi:Fin 1h✝³:¬↑(depth (List.drop k w)) = 0h✝²:¬↑(depth (List.drop k w)) = 1h✝¹:¬depth (List.drop k w) = 0h✝:depth (List.drop k w) = 1⊢ Falsenegw:List Boolk:ℕhk:k ≤ w.lengthi:Fin 1h✝³:¬↑(depth (List.drop k w)) = 0h✝²:¬↑(depth (List.drop k w)) = 1h✝¹:¬depth (List.drop k w) = 0h✝:¬depth (List.drop k w) = 1⊢ none = none <;>posw:List Boolk:ℕhk:k ≤ w.lengthi:Fin 1h✝¹:↑(depth (List.drop k w)) = 0h✝:depth (List.drop k w) = 0⊢ some 0 = some 0posw:List Boolk:ℕhk:k ≤ w.lengthi:Fin 1h✝²:↑(depth (List.drop k w)) = 0h✝¹:¬depth (List.drop k w) = 0h✝:depth (List.drop k w) = 1⊢ some 0 = some 1negw:List Boolk:ℕhk:k ≤ w.lengthi:Fin 1h✝²:↑(depth (List.drop k w)) = 0h✝¹:¬depth (List.drop k w) = 0h✝:¬depth (List.drop k w) = 1⊢ Falseposw:List Boolk:ℕhk:k ≤ w.lengthi:Fin 1h✝²:¬↑(depth (List.drop k w)) = 0h✝¹:↑(depth (List.drop k w)) = 1h✝:depth (List.drop k w) = 0⊢ some 1 = some 0posw:List Boolk:ℕhk:k ≤ w.lengthi:Fin 1h✝³:¬↑(depth (List.drop k w)) = 0h✝²:↑(depth (List.drop k w)) = 1h✝¹:¬depth (List.drop k w) = 0h✝:depth (List.drop k w) = 1⊢ some 1 = some 1negw:List Boolk:ℕhk:k ≤ w.lengthi:Fin 1h✝³:¬↑(depth (List.drop k w)) = 0h✝²:↑(depth (List.drop k w)) = 1h✝¹:¬depth (List.drop k w) = 0h✝:¬depth (List.drop k w) = 1⊢ Falseposw:List Boolk:ℕhk:k ≤ w.lengthi:Fin 1h✝²:¬↑(depth (List.drop k w)) = 0h✝¹:¬↑(depth (List.drop k w)) = 1h✝:depth (List.drop k w) = 0⊢ Falseposw:List Boolk:ℕhk:k ≤ w.lengthi:Fin 1h✝³:¬↑(depth (List.drop k w)) = 0h✝²:¬↑(depth (List.drop k w)) = 1h✝¹:¬depth (List.drop k w) = 0h✝:depth (List.drop k w) = 1⊢ Falsenegw:List Boolk:ℕhk:k ≤ w.lengthi:Fin 1h✝³:¬↑(depth (List.drop k w)) = 0h✝²:¬↑(depth (List.drop k w)) = 1h✝¹:¬depth (List.drop k w) = 0h✝:¬depth (List.drop k w) = 1⊢ none = none first | rflAll goals completed! 🐙 | omegaAll goals completed! 🐙

seekCfg at index 0 is treeScanner's initial configuration.

theorem seekCfg_zero (w : List Bool) :
    seekCfg w 0 (Nat.zero_le _) = treeScanner.initCfg (w.map boolEmb) := rfl

At width one no incomplete block survives, so the decision function is the pair of conditions the machine computes: whether the scan stayed live, and whether the pending count is 1.

theorem validBool_eq_ok_and_depth (w : List Bool) :
    binRanked.validBool w = (ok w && depth w == 1) := byw:List Bool⊢ binRanked.validBool w = (ok w && depth w == 1)
  unfold RankedAlphabet.validBool ok depthw:List Bool⊢ ((binRanked.scanFinal w).live && (binRanked.scanFinal w).buf.isEmpty && (binRanked.scanFinal w).depth == 1) =
  ((binRanked.scanFinal w).live && (binRanked.scanFinal w).depth == 1)
  rw [buf_scanFinal_eq_nil,w:List Bool⊢ ((binRanked.scanFinal w).live && [].isEmpty && (binRanked.scanFinal w).depth == 1) =
  ((binRanked.scanFinal w).live && (binRanked.scanFinal w).depth == 1) List.isEmpty_nil,w:List Bool⊢ ((binRanked.scanFinal w).live && true && (binRanked.scanFinal w).depth == 1) =
  ((binRanked.scanFinal w).live && (binRanked.scanFinal w).depth == 1) Bool.and_truew:List Bool⊢ ((binRanked.scanFinal w).live && (binRanked.scanFinal w).depth == 1) =
  ((binRanked.scanFinal w).live && (binRanked.scanFinal w).depth == 1)]All goals completed! 🐙

end Geb.TreeScanner