Buffering probabilistic machine output

The common output compiler applies directly to Boolean-indexed choices, preserving the whole typed program, including stateful coin and query effects. The buffer starts blank.

Main definitions

• Turing.MultiTapePTM.outputToTape: redirect output to a fresh work tape.

Main results

• Turing.MultiTapePTM.runConfigFrom_outputToTape: preserve the source configuration program.

References

Specializes MultiTape.Machine.OutputToTape, adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8 and upstream's deterministic output redirection.

@[reducible, inline]

abbrev Turing.MultiTapePTM.outputToTape {k : ℕ} {Symbol State Oracle : Type} (machine : MultiTapePTM k Symbol State Oracle) : MultiTapePTM (k + 1) Symbol State Oracle

The common output compiler specialized to Boolean-indexed transitions.

theorem Turing.MultiTapePTM.runConfigFrom_outputToTape {k : ℕ} {Symbol State Oracle Query : Type} {spec : Cslib.OracleSpec Query} {input : List Symbol} [DecidableEq Oracle] (machine : MultiTapePTM k Symbol State Oracle) (coin : Cslib.OracleComp spec Bool) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (fuel : ℕ) (cfg : MultiTapeMachine.Config k Symbol State Oracle input) : machine.outputToTape.runConfigFrom coin query fuel (MultiTapeMachine.OutputToTape.config cfg) = MultiTapeMachine.OutputToTape.config <$> machine.runConfigFrom coin query fuel cfg

Buffer output while retaining the complete clocked program and every oracle channel.