Replaying nondeterministic choices with fair coins

A nondeterministic machine with finitely many states and a binary alphabet has finitely many actions. Its choice table Turing.MultiTapeNTM.choiceTable is one fixed finite fair-coin table that replays a computation path from a list of coins. At a running configuration it scans the permitted actions in a fixed order (Turing.MultiTapeNTM.actions), one coin per candidate: the coin true takes the current candidate, the coin false moves on, and the last candidate is taken under either coin. A step of the nondeterministic machine choosing the candidate of (zero-based) index j therefore costs the coins false^j true, at most Nat.card of the action type. Every coin list thus selects permitted actions, except at a stuck configuration, which has none; there the table rejects: it halts without output.

The table emits nothing while it simulates. It records in its finite control whether the simulated output is empty, exactly [true] or something else (Turing.MultiTapeNTM.ChoiceTable.OutputTrack), and when the simulated machine halts it emits true exactly when the simulated output is [true]. So a running prefix of output [true] is never mistaken for acceptance. A halted table ignores the remaining coins, which allows padding.

Main definitions

• Turing.MultiTapeNTM.actions: the permitted actions, in a fixed order.
• Turing.MultiTapeNTM.choiceTable: the fair-coin table replaying choices. Its states Turing.MultiTapeNTM.ChoiceTable.ScanState record the simulated state, the candidate index and the track Turing.MultiTapeNTM.ChoiceTable.OutputTrack of the simulated output.

Main results

• Turing.MultiTapeNTM.accepts_of_runClosedCoins_choiceTable: a coin list on which the table emits [true] encodes an accepting computation path.
• Turing.MultiTapeNTM.exists_runClosedCoins_choiceTable: a computation path of t steps ending halted with output [true] is encoded by at most Nat.card (Action k Bool State) * t coins, followed by arbitrary padding.

noncomputable def Turing.MultiTapeNTM.actions {k : ℕ} {State : Type} [Finite State] (ntm : MultiTapeNTM k Bool State) (state : State) (symbol : Option Bool) (work : Fin k → Option Bool) : List (Action k Bool State)

The actions permitted by ntm at a state and read symbols, in a fixed order.

theorem Turing.MultiTapeNTM.mem_actions {k : ℕ} {State : Type} [Finite State] (ntm : MultiTapeNTM k Bool State) {state : State} {symbol : Option Bool} {work : Fin k → Option Bool} {action : Action k Bool State} : action ∈ ntm.actions state symbol work ↔ ntm.Tr state symbol work action

theorem Turing.MultiTapeNTM.length_actions_le {k : ℕ} {State : Type} [Finite State] (ntm : MultiTapeNTM k Bool State) (state : State) (symbol : Option Bool) (work : Fin k → Option Bool) : (ntm.actions state symbol work).length ≤ Nat.card (Action k Bool State)

There are at most as many permitted actions as actions.

inductive Turing.MultiTapeNTM.ChoiceTable.OutputTrack : Type

Whether an emitted word is empty, exactly [true], or something else.

• empty : OutputTrack

  Nothing has been emitted.

• accept : OutputTrack

  Exactly [true] has been emitted.

• other : OutputTrack

  Something else has been emitted.

@[instance_reducible]

instance Turing.MultiTapeNTM.ChoiceTable.instDecidableEqOutputTrack : DecidableEq OutputTrack

instance Turing.MultiTapeNTM.ChoiceTable.OutputTrack.instFinite : Finite OutputTrack

def Turing.MultiTapeNTM.ChoiceTable.OutputTrack.ofWord (word : List Bool) : OutputTrack

The track of a word.

def Turing.MultiTapeNTM.ChoiceTable.OutputTrack.emit : OutputTrack → Option Bool → OutputTrack

The track after emitting one more symbol, if any.

@[simp]

theorem Turing.MultiTapeNTM.ChoiceTable.OutputTrack.ofWord_nil : ofWord [] = empty

theorem Turing.MultiTapeNTM.ChoiceTable.OutputTrack.ofWord_append (word : List Bool) (symbol : Option Bool) : ofWord (word ++ symbol.toList) = (ofWord word).emit symbol

Emitting a symbol updates the track of the word.

theorem Turing.MultiTapeNTM.ChoiceTable.OutputTrack.ofWord_eq_accept_iff (word : List Bool) : ofWord word = accept ↔ word = [true]

A word is [true] exactly when its track is accept.

@[reducible, inline]

abbrev Turing.MultiTapeNTM.ChoiceTable.ScanState (k : ℕ) (State : Type) : Type

The states of the choice table: the simulated state, the index of the candidate action, and the track of the simulated output.

noncomputable def Turing.MultiTapeNTM.ChoiceTable.perform {k : ℕ} {State : Type} (track : OutputTrack) (action : Action k Bool State) : Action k Bool (ScanState k State)

Take a simulated action. Its output is recorded in the track instead of being emitted; when it halts, true is emitted exactly when the simulated output is [true].

def Turing.MultiTapeNTM.ChoiceTable.idle {k : ℕ} {S : Type} (next : Option S) : Action k Bool S

Leave the tapes unchanged and continue in next, or halt without output.

noncomputable def Turing.MultiTapeNTM.ChoiceTable.scan {k : ℕ} {State : Type} [Finite State] (ntm : MultiTapeNTM k Bool State) (s : ScanState k State) (symbol : Option Bool) (work : Fin k → Option Bool) (bit : Bool) : Action k Bool (ScanState k State)

One instruction of the choice table: take or skip the candidate j, or reject if there is no such candidate.

noncomputable def Turing.MultiTapeNTM.choiceTable {k : ℕ} {State : Type} [Finite State] (ntm : MultiTapeNTM k Bool State) : MultiTapePTM k Bool (ChoiceTable.ScanState k State)

The choice table. A fixed finite fair-coin table replaying the choices of ntm, one coin per candidate action.

theorem Turing.MultiTapeNTM.ChoiceTable.step_choiceTable {k : ℕ} {State : Type} [Finite State] {input : List Bool} (ntm : MultiTapeNTM k Bool State) {cfg : Cfg k Bool (ScanState k State) input} {s : ScanState k State} (h : cfg.state = some s) (bit : Bool) : MultiTapeTM.step cfg = (scan ntm s cfg.inputSymbol cfg.workTapeSymbols bit).apply cfg

A running instruction of the choice table applies scan.

def Turing.MultiTapeNTM.ChoiceTable.scanCfg {k : ℕ} {State : Type} {input : List Bool} (c : Cfg k Bool State input) (state : State) (j : Fin (Nat.card (Action k Bool State) + 1)) : Cfg k Bool (ScanState k State) input

The table simulating the running configuration c in state state, before candidate j.

def Turing.MultiTapeNTM.ChoiceTable.haltCfg {k : ℕ} {State : Type} {input : List Bool} (c : Cfg k Bool State input) : Cfg k Bool (ScanState k State) input

The halted table after simulating the halted configuration c.

noncomputable def Turing.MultiTapeNTM.ChoiceTable.simCfg {k : ℕ} {State : Type} {input : List Bool} (c : Cfg k Bool State input) : Cfg k Bool (ScanState k State) input

The table simulating a configuration, before its first candidate.

theorem Turing.MultiTapeNTM.ChoiceTable.initCfg_choiceTable {k : ℕ} {State : Type} [Finite State] (ntm : MultiTapeNTM k Bool State) (input : List Bool) : ntm.choiceTable.toNTM.initCfg input = simCfg (ntm.initCfg input)

The table starts by simulating the initial configuration.

theorem Turing.MultiTapeNTM.ChoiceTable.apply_perform {k : ℕ} {State : Type} {input : List Bool} (c : Cfg k Bool State input) (state : State) (j : Fin (Nat.card (Action k Bool State) + 1)) (action : Action k Bool State) : (perform (OutputTrack.ofWord c.output) action).apply (scanCfg c state j) = simCfg (action.apply c)

Taking a candidate simulates its step.

theorem Turing.MultiTapeNTM.ChoiceTable.apply_idle {k : ℕ} {input : List Bool} {S : Type} (next : Option S) (cfg : Cfg k Bool S input) : (idle next).apply cfg = { state := next, inputPos := cfg.inputPos, workTapes := cfg.workTapes, workTapePos := cfg.workTapePos, output := cfg.output }

An idle instruction changes only the control state.

theorem Turing.MultiTapeNTM.ChoiceTable.scan_of_getElem?_eq_none {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State} {state : State} {symbol : Option Bool} {work : Fin k → Option Bool} {j : Fin (Nat.card (Action k Bool State) + 1)} {track : OutputTrack} (hj : (ntm.actions state symbol work)[↑j]? = none) (bit : Bool) : scan ntm (state, j, track) symbol work bit = idle none

theorem Turing.MultiTapeNTM.ChoiceTable.scan_of_take {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State} {state : State} {symbol : Option Bool} {work : Fin k → Option Bool} {j : Fin (Nat.card (Action k Bool State) + 1)} {track : OutputTrack} {action : Action k Bool State} (hj : (ntm.actions state symbol work)[↑j]? = some action) {bit : Bool} (hbit : bit = true ∨ ↑j + 1 = (ntm.actions state symbol work).length) : scan ntm (state, j, track) symbol work bit = perform track action

theorem Turing.MultiTapeNTM.ChoiceTable.scan_of_skip {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State} {state : State} {symbol : Option Bool} {work : Fin k → Option Bool} {j : Fin (Nat.card (Action k Bool State) + 1)} {track : OutputTrack} {action : Action k Bool State} (hj : (ntm.actions state symbol work)[↑j]? = some action) (hlast : ↑j + 1 ≠ (ntm.actions state symbol work).length) : scan ntm (state, j, track) symbol work false = idle (some (state, ⟨↑j + 1, ⋯⟩, track))

theorem Turing.MultiTapeNTM.ChoiceTable.step_scanCfg_skip {k : ℕ} {State : Type} [Finite State] {input : List Bool} {ntm : MultiTapeNTM k Bool State} {c : Cfg k Bool State input} {state : State} {j : Fin (Nat.card (Action k Bool State) + 1)} {action : Action k Bool State} (hj : (ntm.actions state c.inputSymbol c.workTapeSymbols)[↑j]? = some action) (hlast : ↑j + 1 ≠ (ntm.actions state c.inputSymbol c.workTapeSymbols).length) : MultiTapeTM.step (scanCfg c state j) = scanCfg c state ⟨↑j + 1, ⋯⟩

Skipping a candidate that is not the last moves to the next candidate.

theorem Turing.MultiTapeNTM.ChoiceTable.step_scanCfg_take {k : ℕ} {State : Type} [Finite State] {input : List Bool} {ntm : MultiTapeNTM k Bool State} {c : Cfg k Bool State input} {state : State} {j : Fin (Nat.card (Action k Bool State) + 1)} {action : Action k Bool State} (hj : (ntm.actions state c.inputSymbol c.workTapeSymbols)[↑j]? = some action) {bit : Bool} (hbit : bit = true ∨ ↑j + 1 = (ntm.actions state c.inputSymbol c.workTapeSymbols).length) : MultiTapeTM.step (scanCfg c state j) = simCfg (action.apply c)

Taking a candidate, under the coin true or as the last candidate, simulates its step.

theorem Turing.MultiTapeNTM.ChoiceTable.step_scanCfg_reject {k : ℕ} {State : Type} [Finite State] {input : List Bool} {ntm : MultiTapeNTM k Bool State} {c : Cfg k Bool State input} {state : State} {j : Fin (Nat.card (Action k Bool State) + 1)} (hj : (ntm.actions state c.inputSymbol c.workTapeSymbols)[↑j]? = none) (bit : Bool) : MultiTapeTM.step (scanCfg c state j) = { state := none, inputPos := c.inputPos, workTapes := c.workTapes, workTapePos := c.workTapePos, output := [] }

Without a candidate j, the table rejects: it halts without output.

Soundness

def Turing.MultiTapeNTM.ChoiceTable.Replayable {k : ℕ} {State : Type} (ntm : MultiTapeNTM k Bool State) (input : List Bool) (b : Cfg k Bool (ScanState k State) input) : Prop

The configurations reachable by replaying coins: simulating a reachable running configuration, rejected, or accepted after an accepting computation path.

theorem Turing.MultiTapeNTM.ChoiceTable.Replayable.step {k : ℕ} {State : Type} [Finite State] {input : List Bool} {ntm : MultiTapeNTM k Bool State} {b : Cfg k Bool (ScanState k State) input} (h : Replayable ntm input b) (bit : Bool) : Replayable ntm input (MultiTapeTM.step b)

Every coin preserves replayability.

Completeness

theorem Turing.MultiTapeNTM.ChoiceTable.exists_coins_step {k : ℕ} {State : Type} [Finite State] {input : List Bool} {ntm : MultiTapeNTM k Bool State} {c c' : Cfg k Bool State input} {state : State} (hstate : c.state = some state) (h : ntm.Step c c') : ∃ (coins : List Bool), coins.length ≤ Nat.card (Action k Bool State) ∧ ntm.choiceTable.stepCoins coins (simCfg c) = simCfg c'

One step of a running configuration is replayed by at most Nat.card coins.

theorem Turing.MultiTapeNTM.ChoiceTable.exists_coins_runPath {k : ℕ} {State : Type} [Finite State] {input : List Bool} {ntm : MultiTapeNTM k Bool State} (p : ntm.RunPath input) : ∃ (coins : List Bool), coins.length ≤ Nat.card (Action k Bool State) * p.length ∧ ntm.choiceTable.stepCoins coins (simCfg (RelSeries.head p)) = simCfg (RelSeries.last p)

A run path is replayed from the simulation of its head by at most Nat.card coins per step. Halted steps need no coins.

theorem Turing.MultiTapeNTM.ChoiceTable.stepCoins_haltCfg {k : ℕ} {State : Type} [Finite State] {input : List Bool} {ntm : MultiTapeNTM k Bool State} (c : Cfg k Bool State input) (coins : List Bool) : ntm.choiceTable.stepCoins coins (haltCfg c) = haltCfg c

A halted table ignores further coins.

theorem Turing.MultiTapeNTM.accepts_of_runClosedCoins_choiceTable {k : ℕ} {State : Type} [Finite State] {input : List Bool} {ntm : MultiTapeNTM k Bool State} {coins : List Bool} (h : ntm.choiceTable.runClosedCoins coins input = [true]) : ntm.Accepts input

Soundness. A coin list on which the choice table emits [true] encodes an accepting computation path.

theorem Turing.MultiTapeNTM.exists_runClosedCoins_choiceTable {k : ℕ} {State : Type} [Finite State] {input : List Bool} {ntm : MultiTapeNTM k Bool State} (p : ntm.ComputationPath input) (hhalt : p.last.Halted) (hout : p.last.output = [true]) : ∃ (coins : List Bool), coins.length ≤ Nat.card (Action k Bool State) * p.time ∧ ∀ (padding : List Bool), ntm.choiceTable.runClosedCoins (coins ++ padding) input = [true]

Completeness. A computation path of t steps ending halted with output [true] is encoded by at most Nat.card (Action k Bool State) * t coins, after which any padding is ignored.