Repeating a probabilistic oracle machine until a tape goes blank

repeatUntilBlank i body runs body repeatedly. After each round it reads the cell under the head of work tape i, without moving a head, and halts if that cell is blank. Every round of a Turing.MultiTapePTM.RunsWords specification ends with all heads on the first cells of their words, so the loop stops exactly when the word on tape i is empty. The body always runs at least once. Rounds may halt at random times; the remaining rounds start from the halted configuration, with its tapes, oracle channels and external oracle state.

Main definitions

• Turing.MultiTapePTM.repeatUntilBlank: the looping machine.
• Turing.MultiTapePTM.RepeatUntilBlank.fromCheck: the same transition table started at its test.

Main results

• Turing.MultiTapePTM.RunsWords.repeatUntilBlank_round: one round followed by the remaining loop.
• Turing.MultiTapePTM.RunsWords.repeatUntilBlank: rounds rounds governed by an invariant run OracleComp.iterate rounds step within rounds * (t + 1) steps, preserving the joint law of the tape words and the external oracle state.

References

Adapts cslib's Plumbing/RepeatUntilBlank, by Christian Reitwiessner, to probabilistic oracle machines and the joint stateful semantics of Turing.MultiTapePTM.RunsWords.

theorem Turing.MultiTapePTM.runOracleConfigFrom_add {k : ℕ} {Operation : Type} {x : List Bool} [DecidableEq Operation] {S : Type} (machine : MultiTapePTM k Bool S Operation) (first second : ℕ) (cfg : MultiTapeMachine.Config k Bool S Operation x) : machine.runOracleConfigFrom (first + second) cfg = machine.runOracleConfigFrom first cfg >>= machine.runOracleConfigFrom second

Clocked runs compose by sequencing their programs.

def Turing.MultiTapePTM.RepeatUntilBlank.runAction {k : ℕ} {State Operation : Type} : MultiTapeMachine.Action k Bool State Operation → MultiTapeMachine.Action k Bool (MultiTapeTM.RepeatUntilBlankState State) Operation

Embed an action of the repeated machine, sending its halt to the blank test.

def Turing.MultiTapePTM.RepeatUntilBlank.idle {k : ℕ} {S : Type} (q : Option S) : Action k Bool S

The instruction that writes nothing, moves no head and enters q.

def Turing.MultiTapePTM.RepeatUntilBlank.checkAction {k : ℕ} {State Operation : Type} (i : Fin k) (initial : State) (work : Fin k → Option Bool) : MultiTapeMachine.Action k Bool (MultiTapeTM.RepeatUntilBlankState State) Operation

The blank test: halt if the cell under the head of work tape i is blank, and otherwise restart at initial, moving no head and writing nothing.

def Turing.MultiTapePTM.repeatUntilBlank {k : ℕ} {State Operation : Type} (i : Fin k) (body : MultiTapePTM k Bool State Operation) : MultiTapePTM k Bool (MultiTapeTM.RepeatUntilBlankState State) Operation

body, with its halting transitions sent to a test of the cell under the head of work tape i: a blank cell halts the loop, and any other cell restarts body.

def Turing.MultiTapePTM.RepeatUntilBlank.fromCheck {k : ℕ} {State Operation : Type} (i : Fin k) (body : MultiTapePTM k Bool State Operation) : MultiTapePTM k Bool (MultiTapeTM.RepeatUntilBlankState State) Operation

The loop's transition table, started at its blank test.

def Turing.MultiTapePTM.RepeatUntilBlank.runConfig {k : ℕ} {State Operation : Type} {x : List Bool} (cfg : MultiTapeMachine.Config k Bool State Operation x) : MultiTapeMachine.Config k Bool (MultiTapeTM.RepeatUntilBlankState State) Operation x

A configuration of the repeated machine as one of the loop: a live state q becomes run q and the halted state becomes the blank test.

theorem Turing.MultiTapePTM.RepeatUntilBlank.runOracleConfigFrom_fromCheck {k : ℕ} {State Operation : Type} {x : List Bool} [DecidableEq Operation] (i : Fin k) (body : MultiTapePTM k Bool State Operation) (fuel : ℕ) (cfg : MultiTapeMachine.Config k Bool (MultiTapeTM.RepeatUntilBlankState State) Operation x) : (fromCheck i body).runOracleConfigFrom fuel cfg = (repeatUntilBlank i body).runOracleConfigFrom fuel cfg

Starting at the test changes only the initial state, not the clocked program.

theorem Turing.MultiTapePTM.RepeatUntilBlank.runOracleConfigFrom_one_runConfig {k : ℕ} {State Operation : Type} {x : List Bool} [DecidableEq Operation] (i : Fin k) (body : MultiTapePTM k Bool State Operation) (cfg : MultiTapeMachine.Config k Bool State Operation x) (h : cfg.tapes.state ≠ none) : (repeatUntilBlank i body).runOracleConfigFrom 1 (runConfig cfg) = runConfig <$> body.runOracleConfigFrom 1 cfg

While the repeated machine is live, one loop instruction mirrors its complete program.

theorem Turing.MultiTapePTM.RepeatUntilBlank.run_interpret_runOracleConfigFrom_add {k : ℕ} {State Operation OracleState : Type} {x : List Bool} [DecidableEq Operation] (i : Fin k) (body : MultiTapePTM k Bool State Operation) (oracle : Operation × List Bool → StateT OracleState PMF (List Bool)) (cfg : MultiTapeMachine.Config k Bool State Operation x) (fuel rest : ℕ) (s : OracleState) (hrest : ∀ result ∈ ((Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) (body.runOracleConfigFrom fuel cfg)).run s).support, ∀ final ∈ ((Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) ((repeatUntilBlank i body).runOracleConfigFrom rest (runConfig result.1))).run result.2).support, final.1.tapes.state = none) : (Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) ((repeatUntilBlank i body).runOracleConfigFrom (fuel + rest) (runConfig cfg))).run s = ((Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) (body.runOracleConfigFrom fuel cfg)).run s).bind fun (result : MultiTapeMachine.Config k Bool State Operation x × OracleState) => (Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) ((repeatUntilBlank i body).runOracleConfigFrom rest (runConfig result.1))).run result.2

The loop runs a clocked phase of body and then continues from its configuration, even when body halts at a random time: an early halt reaches the blank test early, and the extra time is absorbed because the remaining loop halts within its own clock.

theorem Turing.MultiTapePTM.RepeatUntilBlank.apply_idle_wordsCfg {k : ℕ} {x : List Bool} {S : Type} (q q' : Option S) (ws : Fin k → List Bool) (out : List Bool) : (idle q).apply (wordsCfg x q' ws out) = wordsCfg x q ws out

An instruction that writes nothing and moves no head changes only the control state of a word configuration.

theorem Turing.MultiTapePTM.RepeatUntilBlank.step_idle_channels {k : ℕ} {Operation : Type} {x : List Bool} {S : Type} (cfg : MultiTapeMachine.Config k Bool S Operation x) (q : Option S) : (cfg.step (idle q) (fun (x : Operation) => none) fun (x : Operation) => 0).channels = cfg.channels

Such an instruction also leaves every oracle channel unchanged.

theorem Turing.MultiTapePTM.RunsWords.fromCheck_nil {k : ℕ} {State Operation : Type} {x : List Bool} [DecidableEq Operation] (i : Fin k) (body : MultiTapePTM k Bool State Operation) {ws : Fin k → List Bool} {out₀ : List Bool} (hi : ws i = []) : (RepeatUntilBlank.fromCheck i body).RunsWords x ws out₀ 1 (pure ()) (fun (x : Unit) => ws) fun (x : Unit) => []

At the blank test on an empty word, the loop halts after one instruction.

theorem Turing.MultiTapePTM.RunsWords.fromCheck_ne_nil {k : ℕ} {State Operation : Type} {x : List Bool} [DecidableEq Operation] (i : Fin k) {body : MultiTapePTM k Bool State Operation} {ws : Fin k → List Bool} {out₀ : List Bool} {t : ℕ} {α : Type} {program : Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) α} {ws' : α → Fin k → List Bool} {emit : α → List Bool} (hi : ws i ≠ []) (h : (MultiTapePTM.repeatUntilBlank i body).RunsWords x ws out₀ t program ws' emit) : (RepeatUntilBlank.fromCheck i body).RunsWords x ws out₀ (t + 1) program ws' emit

At the blank test on a non-empty word, the loop restarts its body after one instruction.

theorem Turing.MultiTapePTM.RunsWords.repeatUntilBlank_round {k : ℕ} {State Operation : Type} {x : List Bool} [DecidableEq Operation] (i : Fin k) {body : MultiTapePTM k Bool State Operation} {ws₀ : Fin k → List Bool} {out₀ : List Bool} {t₁ t₂ : ℕ} {α β : Type} {prog₁ : Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) α} {prog₂ : α → Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) β} {ws₁ : α → Fin k → List Bool} {emit₁ : α → List Bool} {ws₂ : α → β → Fin k → List Bool} {emit₂ : α → β → List Bool} (hinj : Function.Injective fun (a : α) => (ws₁ a, emit₁ a)) (h₁ : body.RunsWords x ws₀ out₀ t₁ prog₁ ws₁ emit₁) (h₂ : ∀ (a : α) (OracleState : Type) (oracle : Operation × List Bool → StateT OracleState PMF (List Bool)) (s s' : OracleState), (a, s') ∈ ((Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) prog₁).run s).support → (RepeatUntilBlank.fromCheck i body).RunsWords x (ws₁ a) (out₀ ++ emit₁ a) t₂ (prog₂ a) (ws₂ a) (emit₂ a)) : (MultiTapePTM.repeatUntilBlank i body).RunsWords x ws₀ out₀ (t₁ + t₂) (do let a ← prog₁ (fun (b : β) => (a, b)) <$> prog₂ a) (fun (p : α × β) => ws₂ p.1 p.2) fun (p : α × β) => emit₁ p.1 ++ emit₂ p.1 p.2

One round of body, followed by the loop started at its blank test. The round's final tape words and emitted output must determine its program value.

theorem Turing.MultiTapePTM.RunsWords.repeatUntilBlank {k : ℕ} {State Operation : Type} {x : List Bool} [DecidableEq Operation] (i : Fin k) {body : MultiTapePTM k Bool State Operation} {σ : Type} {ws : σ → Fin k → List Bool} (hws : Function.Injective ws) {step last : σ → Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) σ} {out₀ : List Bool} {t rounds : ℕ} {s₀ : σ} (invariant : ℕ → σ → Prop) (hbase : invariant 0 s₀) (hstep : ∀ n < rounds, ∀ (s : σ), invariant n s → body.RunsWords x (ws s) out₀ t (step s) ws fun (x : σ) => []) (hlast : ∀ (s : σ), invariant rounds s → body.RunsWords x (ws s) out₀ t (last s) ws fun (x : σ) => []) (hpreserve : ∀ n < rounds, ∀ (s : σ), invariant n s → ∀ (OracleState : Type) (oracle : Operation × List Bool → StateT OracleState PMF (List Bool)) (st st' : OracleState) (s' : σ), (s', st') ∈ ((Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) (step s)).run st).support → invariant (n + 1) s' ∧ ws s' i ≠ []) (hstop : ∀ (s : σ), invariant rounds s → ∀ (OracleState : Type) (oracle : Operation × List Bool → StateT OracleState PMF (List Bool)) (st st' : OracleState) (s' : σ), (s', st') ∈ ((Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) (last s)).run st).support → ws s' i = []) : (MultiTapePTM.repeatUntilBlank i body).RunsWords x (ws s₀) out₀ ((rounds + 1) * (t + 1)) (Cslib.OracleComp.iterate rounds step s₀ >>= last) ws fun (x : σ) => []

A loop of rounds + 1 rounds. Round n < rounds runs step s from the words ws s of a state s satisfying invariant n s, and leaves a non-empty word on tape i; the last round runs last s and leaves tape i empty. The loop then runs OracleComp.iterate rounds step followed by last within (rounds + 1) * (t + 1) steps, preserving the joint law of the tape words and the external oracle state, and emits nothing.