Documentation

Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.OrElse

Running a second fair-coin machine when the first does not accept #

first.orElse second runs first on its own block of work tapes, with its output suppressed and summarized in the control state by Turing.MultiTapeNTM.outputClass. If first halts with output [true], the machine outputs true and halts. Otherwise it moves the input head back to the first input symbol and runs second on a separate, blank block of work tapes, with fresh coins. One more work tape holds a flag recording that first accepted; the two phases are joined by Turing.MultiTapePTM.seq. Both machines use the Boolean alphabet and no oracle channels.

If first and second halt on every branch within t₁ and t₂ steps on an input of length n, then first.orElse second halts on every branch within t₁ + (n + 2 + t₂) steps: rewinding the input head takes at most n + 2 steps. Its output distribution is that of the program "run first; if it outputs [true], output [true], and otherwise run second". Since both phases halt, this is exact, not a bound. Every work-tape head stays within the cells that first or second alone would use, so a space bound for both machines gives one for the combination.

The phases are analysed through two general rules for fair-coin machines without oracle channels: a map of configurations commuting with each coin's step maps the configuration distribution, and a step that ignores its coin is taken with certainty.

Main definitions #

Main results #

References #

Repeating a one-sided-error algorithm and accepting when some run accepts is the standard error reduction for one-sided error Arora and Barak, Section 7.4.1; see Cslib.Complexity.mem_RL_iff_error_le for its use in randomized logarithmic space.

source
theorem Turing.MultiTapePTM.runClosedConfigFromCoins_map {k k' : ℕ} {Symbol S S' : Type} {input : List Symbol} (M : MultiTapePTM k Symbol S) (N : MultiTapePTM k' Symbol S') (f : MultiTapeMachine.Config k Symbol S Empty input → MultiTapeMachine.Config k' Symbol S' Empty input) (h : ∀ (bit : Bool) (c : MultiTapeMachine.Config k Symbol S Empty input), (N.withCoin bit).step (f c) = f ((M.withCoin bit).step c)) (coins : List Bool) (c : MultiTapeMachine.Config k Symbol S Empty input) :
N.runClosedConfigFromCoins coins (f c) = f (M.runClosedConfigFromCoins coins c)

A map of configurations that commutes with each coin's step commutes with every replay.

source
theorem Turing.MultiTapePTM.eval_runClosedConfigFrom_map {k k' : ℕ} {Symbol S S' : Type} {input : List Symbol} (M : MultiTapePTM k Symbol S) (N : MultiTapePTM k' Symbol S') (f : MultiTapeMachine.Config k Symbol S Empty input → MultiTapeMachine.Config k' Symbol S' Empty input) (h : ∀ (bit : Bool) (c : MultiTapeMachine.Config k Symbol S Empty input), (N.withCoin bit).step (f c) = f ((M.withCoin bit).step c)) (fuel : ℕ) (c : MultiTapeMachine.Config k Symbol S Empty input) :
(N.runClosedConfigFrom fuel (f c)).eval = PMF.map f (M.runClosedConfigFrom fuel c).eval

One-step simulation. A map of configurations that commutes with each coin's step maps the closed configuration distribution.

source
theorem Turing.MultiTapePTM.eval_runClosedConfigFrom_succ_of_step {k' : ℕ} {Symbol S' : Type} {input : List Symbol} (N : MultiTapePTM k' Symbol S') {c c' : MultiTapeMachine.Config k' Symbol S' Empty input} (h : ∀ (bit : Bool), (N.withCoin bit).step c = c') (fuel : ℕ) :
(N.runClosedConfigFrom (fuel + 1) c).eval = (N.runClosedConfigFrom fuel c').eval

A step that does not depend on the coin is taken with certainty.

source
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.

source
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.

Tape layout #

Output classes #

The first phase #

The second phase #

source
noncomputable def Turing.MultiTapePTM.orElse {k₁ k₂ : ℕ} {S₁ S₂ : Type} (first : MultiTapePTM k₁ Bool S₁) (second : MultiTapePTM k₂ Bool S₂) :
MultiTapePTM (k₁ + k₂ + 1) Bool (S₁ × Option Bool ⊕ Bool ⊕ S₂)

Run a second machine if the first does not accept. The machine runs first on its own work tapes, with its output suppressed and summarized in the control state. If first halts with output [true], it outputs true and halts. Otherwise it moves the input head back to the first input symbol and runs second on fresh work tapes, with fresh coins. One additional work tape holds a flag recording the outcome of first.

Instances For

    Space #

    source
    theorem Turing.MultiTapePTM.runsInSpace_toNTM_orElse {k₁ k₂ : ℕ} {S₁ S₂ : Type} (first : MultiTapePTM k₁ Bool S₁) (second : MultiTapePTM k₂ Bool S₂) {input : List Bool} {s₁ s₂ : ℕ} (hs₁ : first.toNTM.RunsInSpace input s₁) (hs₂ : second.toNTM.RunsInSpace input s₂) :
    (first.orElse second).toNTM.RunsInSpace input ((k₁ + k₂ + 1) * (2 * max s₁ s₂ + 1))

    Space of first.orElse second. If every computation path of first and of second visits at most s₁ and s₂ work-tape cells, then every head of the combined machine stays in the window [-max s₁ s₂, max s₁ s₂], so each of its k₁ + k₂ + 1 work tapes uses at most 2 * max s₁ s₂ + 1 cells.

    source
    theorem Turing.MultiTapePTM.orElse_halted {k₁ k₂ : ℕ} {S₁ S₂ : Type} (first : MultiTapePTM k₁ Bool S₁) (second : MultiTapePTM k₂ Bool S₂) (input : List Bool) (t₁ t₂ : ℕ) (h₁ : ∀ final ∈ (first.runClosedConfigFrom t₁ (MultiTapeMachine.initialConfig first input)).eval.support, final.tapes.state = none) (h₂ : ∀ final ∈ (second.runClosedConfigFrom t₂ (MultiTapeMachine.initialConfig second input)).eval.support, final.tapes.state = none) (final : MultiTapeMachine.Config (k₁ + k₂ + 1) Bool (S₁ × Option Bool ⊕ Bool ⊕ S₂) Empty input) :
    final ∈ ((first.orElse second).runClosedConfigFrom (t₁ + (input.length + 2 + t₂)) (MultiTapeMachine.initialConfig (first.orElse second) input)).eval.support → final.tapes.state = none

    first.orElse second halts on every branch within t₁ + (n + 2 + t₂) steps when first halts within t₁ and second within t₂ steps, where n is the input length.

    source
    theorem Turing.MultiTapePTM.eval_runClosed_orElse {k₁ k₂ : ℕ} {S₁ S₂ : Type} (first : MultiTapePTM k₁ Bool S₁) (second : MultiTapePTM k₂ Bool S₂) (input : List Bool) (t₁ t₂ : ℕ) (h₁ : ∀ final ∈ (first.runClosedConfigFrom t₁ (MultiTapeMachine.initialConfig first input)).eval.support, final.tapes.state = none) (h₂ : ∀ final ∈ (second.runClosedConfigFrom t₂ (MultiTapeMachine.initialConfig second input)).eval.support, final.tapes.state = none) :
    ((first.orElse second).runClosed (t₁ + (input.length + 2 + t₂)) input).eval = do let word ← (first.runClosed t₁ input).eval if word = [true] then pure [true] else (second.runClosed t₂ input).eval

    The output distribution of first.orElse second: run first; if it outputs [true], output [true], and otherwise run second with fresh coins. Both machines must halt on every branch within their clocks.