Fair-coin machines as nondeterministic machines

A closed fair-coin table offers one action for each coin at every running configuration. Keeping the set of these actions gives a table with Set-valued choices (Turing.MultiTapePTM.branches), and hence, through Turing.MultiTapeMachine.toNTM, the nondeterministic machine Turing.MultiTapePTM.toNTM, which may take either action. A step of this machine is a step of the table under some coin, and a halted configuration steps only to itself on both sides. Hence the run paths of length n are exactly the replays of coin lists of length n, and the configurations supported by a closed fair-coin run with clock n are exactly the last configurations of these run paths.

In particular, a fair-coin machine that halts on every supported branch within its clock runs within the same time as a nondeterministic machine. Its supported outputs at that clock are exactly the outputs of its halted computation paths; halted self-loops allow their lengths to differ without changing their endpoints.

Main definitions

• Turing.MultiTapePTM.branches: the table permitting the action of either coin.
• Turing.MultiTapePTM.toNTM: the nondeterministic machine of a closed fair-coin table.

Main results

• Turing.MultiTapePTM.step_toNTM_iff: a step is a deterministic step under some coin.
• Turing.MultiTapePTM.exists_step_toNTM: no configuration is stuck.
• Turing.MultiTapePTM.exists_runPath_toNTM_iff: run paths are the replays of coin lists.
• Turing.MultiTapePTM.mem_support_runClosedConfigFrom_iff: supported configurations are the last configurations of run paths of clock length.
• Turing.MultiTapePTM.runsInTime_toNTM: halting on every supported branch is a time bound.
• Turing.MultiTapePTM.exists_computationPath_toNTM_iff: computation paths of clock length end in exactly the supported configurations.

def Turing.MultiTapePTM.branches {k : ℕ} {Symbol State : Type} (machine : MultiTapePTM k Symbol State) : MultiTapeMachine k Symbol State Empty Set

The table of a closed fair-coin machine with Set-valued choices: the actions of both coins.

def Turing.MultiTapePTM.toNTM {k : ℕ} {Symbol State : Type} (machine : MultiTapePTM k Symbol State) : MultiTapeNTM k Symbol State

The nondeterministic machine of a closed fair-coin table: at a running configuration, it may take the action selected by either coin.

theorem Turing.MultiTapePTM.initCfg_toNTM {k : ℕ} {Symbol State : Type} (machine : MultiTapePTM k Symbol State) (input : List Symbol) : machine.toNTM.initCfg input = (MultiTapeMachine.initialConfig machine input).tapes

The nondeterministic machine starts where the fair-coin table does.

theorem Turing.MultiTapePTM.tr_toNTM_iff {k : ℕ} {Symbol State : Type} (machine : MultiTapePTM k Symbol State) {state : State} {symbol : Option Symbol} {work : Fin k → Option Symbol} {action : Action k Symbol State} : machine.toNTM.Tr state symbol work action ↔ ∃ (bit : Bool), (machine.withCoin bit).toTM.Tr state symbol work action

A transition of the nondeterministic machine is the transition of the table under some coin.

theorem Turing.MultiTapePTM.step_toNTM_iff {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapePTM k Symbol State) {c c' : Cfg k Symbol State input} : machine.toNTM.Step c c' ↔ ∃ (bit : Bool), MultiTapeTM.step c = c'

A step of the nondeterministic machine is a deterministic step under some coin.

theorem Turing.MultiTapePTM.exists_step_toNTM {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapePTM k Symbol State) (c : Cfg k Symbol State input) : ∃ (c' : Cfg k Symbol State input), machine.toNTM.Step c c'

The nondeterministic machine of a fair-coin table is never stuck: every configuration has a successor.

noncomputable def Turing.MultiTapePTM.stepCoins {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapePTM k Symbol State) (coins : List Bool) (c : Cfg k Symbol State input) : Cfg k Symbol State input

One deterministic step under each coin of a list, on upstream configurations.

@[simp]

theorem Turing.MultiTapePTM.stepCoins_nil {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapePTM k Symbol State) (c : Cfg k Symbol State input) : machine.stepCoins [] c = c

theorem Turing.MultiTapePTM.stepCoins_cons {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapePTM k Symbol State) (bit : Bool) (coins : List Bool) (c : Cfg k Symbol State input) : machine.stepCoins (bit :: coins) c = machine.stepCoins coins (MultiTapeTM.step c)

theorem Turing.MultiTapePTM.stepCoins_append {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapePTM k Symbol State) (coins more : List Bool) (c : Cfg k Symbol State input) : machine.stepCoins (coins ++ more) c = machine.stepCoins more (machine.stepCoins coins c)

Replaying concatenated coins pauses and resumes.

theorem Turing.MultiTapePTM.tapes_runClosedConfigFromCoins {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapePTM k Symbol State) (coins : List Bool) (cfg : MultiTapeMachine.Config k Symbol State Empty input) : (machine.runClosedConfigFromCoins coins cfg).tapes = machine.stepCoins coins cfg.tapes

Replaying coins acts on the tapes by upstream deterministic steps.

theorem Turing.MultiTapePTM.exists_runPath_toNTM_iff {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapePTM k Symbol State) {c c' : Cfg k Symbol State input} {n : ℕ} : (∃ (p : machine.toNTM.RunPath input), RelSeries.head p = c ∧ p.length = n ∧ RelSeries.last p = c') ↔ ∃ (coins : List Bool), coins.length = n ∧ machine.stepCoins coins c = c'

Run paths are coin replays. The nondeterministic machine has a run path of length n from c to c' exactly when some coin list of length n replays c to c'. Halted configurations ignore their coins and step only to themselves.

theorem Turing.MultiTapePTM.mem_support_runClosedConfigFrom_iff {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapePTM k Symbol State) {fuel : ℕ} {cfg final : MultiTapeMachine.Config k Symbol State Empty input} : final ∈ (machine.runClosedConfigFrom fuel cfg).eval.support ↔ ∃ (p : machine.toNTM.RunPath input), RelSeries.head p = cfg.tapes ∧ p.length = fuel ∧ RelSeries.last p = final.tapes

Supported configurations are endpoints of run paths. A configuration is supported by the closed fair-coin run with clock fuel exactly when the nondeterministic machine has a run path of length fuel to it.

theorem Turing.MultiTapePTM.runsInTime_toNTM {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapePTM k Symbol State) {t : ℕ} (h : ∀ final ∈ (machine.runClosedConfigFrom t (MultiTapeMachine.initialConfig machine input)).eval.support, final.tapes.state = none) : machine.toNTM.RunsInTime input t

Halting on every branch is a time bound. If every configuration supported by the closed fair-coin run with clock t is halted, then every computation path of the nondeterministic machine with at least t steps ends halted.

theorem Turing.MultiTapePTM.exists_computationPath_toNTM_iff {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapePTM k Symbol State) {t : ℕ} {P : Cfg k Symbol State input → Prop} : (∃ (p : machine.toNTM.ComputationPath input), p.time = t ∧ P p.last) ↔ ∃ final ∈ (machine.runClosedConfigFrom t (MultiTapeMachine.initialConfig machine input)).eval.support, P final.tapes

The last configurations of computation paths of length t are the configurations supported by the closed fair-coin run with clock t.