Iterating a probabilistic oracle machine while its result is non-empty

tm.iterateWhile mark applies the tidy probabilistic oracle machine tm to its input, then to the result, and so on, until tm produces the empty word, and then outputs the last word before the empty one. The machine keeps the current word on one work tape and the next word on another. A round copies the next word to the current tape and computes the new next word from it with tm. Rounds are repeated by Turing.MultiTapePTM.repeatUntilBlank until the next word is empty. The tape layout helpers are module-private, as in the deterministic construction.

Each round makes exactly the oracle calls of tm on the current word, with the external oracle state left by the previous round. The final round's program returns the empty word, and the loop then halts; no further round is executed.

Main definitions

• Turing.MultiTapePTM.iterateWhileRound: one round of the iteration.
• Turing.MultiTapePTM.iterateWhile: the iterating machine.

Main results

• Turing.MultiTapePTM.ComputesTidily.iterateWhile: if tm tidily computes step w from every word w reached in the first r rounds and the empty word in round r, then tm.iterateWhile mark tidily computes OracleComp.iterate r step, preserving the joint law of the result and the external oracle state.

References

Adapts Combinators/IterateWhile (vendored crei:crei/tidy-universal @7f7c0696), by Christian Reitwiessner, and cslib's Plumbing/RepeatUntilBlank to probabilistic oracle machines.

The tapes

The deterministic phases

@[reducible, inline]

abbrev Turing.MultiTapePTM.IterateWhile.PrepareState : Type

The states of Turing.MultiTapePTM.IterateWhile.prepareRound.

@[reducible, inline]

abbrev Turing.MultiTapePTM.IterateWhile.FinishState : Type

The states of Turing.MultiTapePTM.IterateWhile.finish.

@[reducible, inline]

abbrev Turing.MultiTapePTM.IterateWhile.RoundState (State : Type) : Type

The states of Turing.MultiTapePTM.iterateWhileRound.

@[reducible, inline]

abbrev Turing.MultiTapePTM.IterateWhile.MachineState (State : Type) : Type

The states of Turing.MultiTapePTM.iterateWhile.

The machine

noncomputable def Turing.MultiTapePTM.iterateWhileRound {k : ℕ} {State Operation : Type} (tm : MultiTapePTM k Bool State Operation) (mark : Bool) : MultiTapePTM (k + 1 + 2) Bool (IterateWhile.RoundState State) Operation

One round: move the next word to the current tape, then apply tm from the current tape to the next tape, using mark to flag the left end of words.

noncomputable def Turing.MultiTapePTM.iterateWhile {k : ℕ} {State Operation : Type} (tm : MultiTapePTM k Bool State Operation) (mark : Bool) : MultiTapePTM (k + 1 + 2) Bool (IterateWhile.MachineState State) Operation

tm, applied repeatedly while its result is non-empty, using mark to flag the left end of words: load the input to the next tape, repeat rounds until the next tape is empty, then output the current word and clear its tape.

theorem Turing.MultiTapePTM.ComputesTidily.iterateWhile {k : ℕ} {State Operation : Type} [DecidableEq Operation] {tm : MultiTapePTM k Bool State Operation} (mark : Bool) {r t L : ℕ} {w₀ : List Bool} {step : List Bool → Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) (List Bool)} (invariant : ℕ → List Bool → Prop) (hbase : invariant 0 w₀) (hround : ∀ n < r, ∀ (w : List Bool), invariant n w → tm.ComputesTidily w t (step w)) (hpreserve : ∀ n < r, ∀ (w : List Bool), invariant n w → ∀ (OracleState : Type) (oracle : Operation × List Bool → StateT OracleState PMF (List Bool)) (s s' : OracleState) (w' : List Bool), (w', s') ∈ ((Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) (step w)).run s).support → invariant (n + 1) w' ∧ w' ≠ []) (hlast : ∀ (w : List Bool), invariant r w → tm.ComputesTidily w t (pure [])) (hlength : ∀ n ≤ r, ∀ (w : List Bool), invariant n w → w.length ≤ L) : (tm.iterateWhile mark).ComputesTidily w₀ ((r + 1) * (t + 10 * L + 23) + 8 * L + 17) (Cslib.OracleComp.iterate r step w₀)

If tm tidily computes step w within t steps from every word w reached after n < r rounds, and the empty word from every word reached after r rounds, all these words having length at most L, then tm.iterateWhile mark tidily computes OracleComp.iterate r step. Each round makes exactly the oracle calls of tm on its word, with the external oracle state left by the previous round, and no round follows the one producing the empty word.