Documentation

Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Replay.Deterministic

Coin-fixed runs, relabelling and finiteness of fair-coin oracle machines #

Fixing all coins of a fair-coin oracle machine to a constant bit gives a deterministic word-query program (Turing.MultiTapePTM.runConfigFrom with pure bit) whose result against every deterministic oracle is supported by the fair-coin run (Turing.MultiTapePTM.mem_support_runConfigFrom_pure).

Relabelling the control states along an equivalence preserves the run program (Turing.MultiTapePTM.runFrom_relabel), and tables with finitely many symbols, states and channels form a finite type (Turing.MultiTapeMachine.Action.instFinite, Turing.MultiTapePTM.finite).

Main definitions #

Main results #

References #

source
instance Turing.MultiTapeMachine.Action.instFinite {k : ℕ} {Symbol State Oracle : Type} [Finite Symbol] [Finite State] [Finite Oracle] :
Finite (Action k Symbol State Oracle)

Finitely many symbols, states and channels give finitely many instructions.

source
def Turing.MultiTapePTM.relabel {k : ℕ} {Symbol State State' Oracle : Type} (e : State ≃ State') (machine : MultiTapePTM k Symbol State Oracle) :
MultiTapePTM k Symbol State' Oracle

Rename the control states of a fair-coin table along an equivalence.

Instances For
    source
    @[simp]
    theorem Turing.MultiTapePTM.initialConfig_relabel {k : ℕ} {Symbol State State' Oracle : Type} (e : State ≃ State') (machine : MultiTapePTM k Symbol State Oracle) (input : List Symbol) :
    MultiTapeMachine.initialConfig (relabel e machine) input = MultiTapeMachine.Config.mapState (⇑e) (MultiTapeMachine.initialConfig machine input)
    source
    theorem Turing.MultiTapePTM.runConfigFrom_relabel {k : ℕ} {Symbol State State' Oracle : Type} {input : List Symbol} [DecidableEq Oracle] {Query : Type} {spec : Cslib.OracleSpec Query} (e : State ≃ State') (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) :
    (relabel e machine).runConfigFrom coin query fuel (MultiTapeMachine.Config.mapState (⇑e) cfg) = MultiTapeMachine.Config.mapState ⇑e <$> machine.runConfigFrom coin query fuel cfg

    Relabelling commutes with the run program, for every coin and request program.

    source
    theorem Turing.MultiTapePTM.runFrom_relabel {k : ℕ} {Symbol State State' Oracle : Type} {input : List Symbol} [DecidableEq Oracle] {Query : Type} {spec : Cslib.OracleSpec Query} (e : State ≃ State') (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) :
    (relabel e machine).runFrom coin query fuel (MultiTapeMachine.Config.mapState (⇑e) cfg) = machine.runFrom coin query fuel cfg

    Relabelling preserves the output program of every run.

    source
    instance Turing.MultiTapePTM.finite {k : ℕ} {Symbol State Oracle : Type} [Finite Symbol] [Finite State] [Finite Oracle] :
    Finite (MultiTapePTM k Symbol State Oracle)

    Finitely many symbols, states and channels give finitely many fair-coin tables.

    source
    theorem Turing.MultiTapePTM.mem_support_runConfigFrom_pure {k : ℕ} {Symbol State Oracle : Type} {input : List Symbol} [DecidableEq Oracle] {σ : Type} (machine : MultiTapePTM k Symbol State Oracle) (bit : Bool) (answer : Oracle × List Symbol → List Symbol) (s : σ) (fuel : ℕ) (cfg : MultiTapeMachine.Config k Symbol State Oracle input) :
    (Cslib.OracleComp.interpret answer (machine.runConfigFrom (pure bit) (fun (oracle : Oracle) (word : List Symbol) => Cslib.OracleComp.query (oracle, word)) fuel cfg), s) ∈ ((Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) fun (q : Oracle × List Symbol) (s : σ) => PMF.pure (answer q, s)) (machine.runConfigFrom (Cslib.ProbOracleComp.sample (Cslib.ProbComp.uniform Bool)) (fun (oracle : Oracle) (word : List Symbol) => Cslib.ProbOracleComp.query (oracle, word)) fuel cfg)).run s).support

    A coin-fixed run is supported. Against a deterministic oracle, the result of the run with every coin fixed to bit is a supported result of the fair-coin run, with the unchanged state.