Documentation

Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.ExtendTapes

Reserving work tapes for probabilistic machines #

The common tape compiler applies to Boolean-indexed choices by naturality of mapping a coin program. It preserves the program itself, allowing stateful coin and query interpreters.

Main definitions #

Main results #

References #

The common proof in MultiTape.Machine.ExtendTapes adapts the cslib crypto branch's MultiTape/Oracle/ExtendTapes.lean at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

source
@[reducible, inline]
abbrev Turing.MultiTapePTM.extendTapes {k k' : ℕ} {Symbol State Oracle : Type} (machine : MultiTapePTM k Symbol State Oracle) (e : Fin k ↪ Fin k') :
MultiTapePTM k' Symbol State Oracle

The common tape compiler specialized to Boolean-indexed transitions.

Instances For
    source
    theorem Turing.MultiTapePTM.runConfigFrom_embed {k k' : ℕ} {Symbol State Oracle Query : Type} {spec : Cslib.OracleSpec Query} {input : List Symbol} [DecidableEq Oracle] (machine : MultiTapePTM k Symbol State Oracle) (e : Fin k ↪ Fin k') (coin : Cslib.OracleComp spec Bool) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (cfg : MultiTapeMachine.Config k Symbol State Oracle input) (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) (fuel : ℕ) :
    (machine.extendTapes e).runConfigFrom coin query fuel (cfg.embed e extraTapes extraPos) = (fun (final : MultiTapeMachine.Config k Symbol State Oracle input) => final.embed e extraTapes extraPos) <$> machine.runConfigFrom coin query fuel cfg

    Reindexing preserves the entire program and all contents on additional tapes.

    source
    theorem Turing.MultiTapePTM.runClosed_extendTapes {k k' : ℕ} {Symbol State : Type} (machine : MultiTapePTM k Symbol State) (e : Fin k ↪ Fin k') (fuel : ℕ) (input : List Symbol) :
    (machine.extendTapes e).runClosed fuel input = machine.runClosed fuel input

    Reserving blank scratch tapes preserves the closed program, before interpretation.