Fixed-coin steps of sequential probabilistic machines #
Main results #
Turing.MultiTapePTM.step_withCoin_seq_left: a running first phase follows its own step.Turing.MultiTapePTM.step_withCoin_seq_right: the second phase follows its own step.Turing.MultiTapePTM.replay_append,Turing.MultiTapePTM.replay_seq_cases: concatenate coin replays and identify the active phase of a sequential machine.Turing.MultiTapePTM.output_length_le_replay,Turing.MultiTapePTM.replay_halted: output length is monotone along a replay, and halted configurations remain fixed.Turing.MultiTapePTM.completed_replay_mem_support,Turing.MultiTapePTM.replay_output_length_le: connect completed replays to run support and transfer support-wise output bounds to arbitrary replay prefixes.
theorem Turing.MultiTapePTM.step_withCoin_seq_left {k : ℕ} {Symbol : Type} {input : List Symbol} {S₀ S₁ : Type} (first : MultiTapePTM k Symbol S₀) (second : MultiTapePTM k Symbol S₁) (bit : Bool) (c : MultiTapeMachine.Config k Symbol S₀ Empty input) (hc : c.tapes.state ≠ none) :
((first.seq second).withCoin bit).step (MultiTapeMachine.Sequential.left second c) = MultiTapeMachine.Sequential.left second ((first.withCoin bit).step c)
With a fixed coin, a running first phase of a sequential machine steps as the first machine.
theorem Turing.MultiTapePTM.step_withCoin_seq_right {k : ℕ} {Symbol : Type} {input : List Symbol} {S₀ S₁ : Type} (first : MultiTapePTM k Symbol S₀) (second : MultiTapePTM k Symbol S₁) (bit : Bool) (c : MultiTapeMachine.Config k Symbol S₁ Empty input) :
((first.seq second).withCoin bit).step (MultiTapeMachine.Sequential.right c) = MultiTapeMachine.Sequential.right ((second.withCoin bit).step c)
With a fixed coin, the second phase of a sequential machine steps as the second machine.
theorem Turing.MultiTapePTM.replay_append {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapePTM k Symbol State) (before after : List Bool) (cfg : MultiTapeMachine.Config k Symbol State Empty input) :
machine.runClosedConfigFromCoins (before ++ after) cfg = machine.runClosedConfigFromCoins after (machine.runClosedConfigFromCoins before cfg)
Running a sequential concatenation of coin sequences is equivalent to running them consecutively.
theorem Turing.MultiTapePTM.replay_seq_cases {k : ℕ} {Symbol : Type} {input : List Symbol} {State₀ State₁ : Type} (first : MultiTapePTM k Symbol State₀) (second : MultiTapePTM k Symbol State₁) (initial : MultiTapeMachine.Config k Symbol State₀ Empty input) (coins : List Bool) :
(∃ (before : List Bool),
(first.seq second).runClosedConfigFromCoins coins (MultiTapeMachine.Sequential.left second initial) = MultiTapeMachine.Sequential.left second (first.runClosedConfigFromCoins before initial)) ∨ ∃ (before : List Bool) (after : List Bool),
(first.runClosedConfigFromCoins before initial).tapes.state = none ∧ (first.seq second).runClosedConfigFromCoins coins (MultiTapeMachine.Sequential.left second initial) = MultiTapeMachine.Sequential.right
(second.runClosedConfigFromCoins after
(MultiTapeMachine.Sequential.start second (first.runClosedConfigFromCoins before initial)))
Replaying a sequence of coins on a sequentially composed machine either stays in the first phase or transitions to the second.
theorem Turing.MultiTapePTM.output_length_le_replay {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapePTM k Symbol State) (coins : List Bool) (cfg : MultiTapeMachine.Config k Symbol State Empty input) :
The output tape length is monotonically non-decreasing during a run.
theorem Turing.MultiTapePTM.replay_halted {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapePTM k Symbol State) (coins : List Bool) (cfg : MultiTapeMachine.Config k Symbol State Empty input) (h : cfg.tapes.state = none) :
A halted configuration does not change when further coins are replayed.
theorem Turing.MultiTapePTM.completed_replay_mem_support {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapePTM k Symbol State) (initial : MultiTapeMachine.Config k Symbol State Empty input) (time : ℕ) (hhalt : ∀ final ∈ (machine.runClosedConfigFrom time initial).eval.support, final.tapes.state = none) (coins : List Bool) (hcoins : (machine.runClosedConfigFromCoins coins initial).tapes.state = none) :
machine.runClosedConfigFromCoins coins initial ∈ (machine.runClosedConfigFrom time initial).eval.support
A replay that halts belongs to the support of the closed run evaluation.
theorem Turing.MultiTapePTM.replay_output_length_le {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapePTM k Symbol State) (time bound : ℕ) (hhalt :
∀ final ∈ (machine.runClosedConfigFrom time (MultiTapeMachine.initialConfig machine input)).eval.support,
final.tapes.state = none) (hbound : ∀ word ∈ (machine.runClosed time input).eval.support, word.length ≤ bound) (coins : List Bool) :
(machine.runClosedConfigFromCoins coins (MultiTapeMachine.initialConfig machine input)).tapes.output.length ≤ bound
Bounds the output length of any replay given a bound on the support of the closed run.