Documentation

Complexity.Computability.Complexity.Reduction.TuringAutoreducible

Polynomial-time Turing autoreducibility #

A set A is polynomial-time Turing autoreducible if it can be decided in polynomial time by an oracle machine that never queries its own input (Ambos-Spies 1984; Buhrman, Fortnow, van Melkebeek and Torenvliet 2000).

Main definitions #

Main results #

References #

source
def Cslib.Complexity.PolyTimeTuringAutoreducible {α : Type} (encA : α ↪ List Bool) (A : Set α) :
Prop

A is polynomial-time Turing autoreducible: some deterministic polynomial-time oracle program decides A relative to the oracle for A without ever querying its own input.

Instances For
    source
    theorem Cslib.Complexity.PolyTimeTuringAutoreducible.polyTimeTuringReducible {α : Type} {encA : α ↪ List Bool} {A : Set α} (h : PolyTimeTuringAutoreducible encA A) :
    PolyTimeTuringReducible encA encA A A

    A polynomial-time Turing autoreduction is in particular a polynomial-time Turing reduction of A to A.

    source
    theorem Cslib.Complexity.polyTimeTuringAutoreducible_bits_iff {B : Set (List Bool)} :
    PolyTimeTuringAutoreducible Turing.MultiTapeTM.encBits B ↔ ∃ (program : List Bool → WordQueryComp Unit Bool), (Probability.IsOraclePPTOn Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool fun (a : List Bool) => OracleComp.interpret ProbOracleComp.query (program a)) ∧ (∀ (a : List Bool), ∀ q ∈ OracleComp.queriesWith (languageOracle B) (program a), q.2 ≠ a) ∧ ∀ (a : List Bool), a ∈ B ↔ OracleComp.interpret (languageOracle B) (program a) = true

    On bitstring languages with the default encoding encBits, the no-self-query condition simply requires q.2 ≠ a.

    source
    theorem Cslib.Complexity.polyTimeTuringAutoreducible_of_polyTimeReducible_fixedPointFree {α : Type} {encA : α ↪ List Bool} {A : Set α} {f : α → α} (hf : Turing.MultiTapeTM.ComputableInPolyTime f encA encA) (hne : ∀ (a : α), f a ≠ a) (hA : ∀ (a : α), a ∈ A ↔ f a ∈ A) :
    PolyTimeTuringAutoreducible encA A

    Every fixed-point-free polynomial-time many-one reduction of A to A induces a polynomial-time Turing autoreduction.

    source
    theorem Cslib.Complexity.polyTimeTuringAutoreducible_of_mem_P {α : Type} {encA : α ↪ List Bool} {A : Set α} (hA : A ∈ P encA) :
    PolyTimeTuringAutoreducible encA A

    Every problem in P is polynomial-time Turing autoreducible. The decider makes zero oracle queries, so the no-self-query condition is vacuously satisfied.

    source
    theorem Cslib.Complexity.PolyTimeManyOneAutoreducible.polyTimeTuringAutoreducible {α : Type} {encA : α ↪ List Bool} {A : Set α} (h : PolyTimeManyOneAutoreducible encA A) :
    PolyTimeTuringAutoreducible encA A

    Every polynomial-time many-one autoreduction is a polynomial-time Turing autoreduction.

    source
    theorem Cslib.Complexity.LogSpaceManyOneAutoreducible.polyTimeTuringAutoreducible {α : Type} {encA : α ↪ List Bool} {A : Set α} (h : LogSpaceManyOneAutoreducible encA A) :
    PolyTimeTuringAutoreducible encA A

    Every logspace many-one autoreduction is a polynomial-time Turing autoreduction.

    Truth-table to Turing autoreducibility #

    source
    theorem Cslib.Complexity.PolyTimeTruthTableAutoreducible.polyTimeTuringAutoreducible {α : Type} {encA : α ↪ List Bool} {A : Set α} (h : PolyTimeTruthTableAutoreducible encA A) :
    PolyTimeTuringAutoreducible encA A

    Every polynomial-time truth-table autoreduction is a polynomial-time Turing autoreduction. The query list (List.range (r a)).map (fun i => encA (q (a, i))) is evaluated sequentially against languageOracle (encA '' A), and every queried word has the form encA (q (a, i)) with i < r a, which is distinct from encA a by injectivity of encA.

    source
    theorem Cslib.Complexity.PolyTimeKTruthTableAutoreducible.polyTimeTuringAutoreducible {α : Type} {encA : α ↪ List Bool} {A : Set α} {k : ℕ} (h : PolyTimeKTruthTableAutoreducible k encA A) :
    PolyTimeTuringAutoreducible encA A

    Every polynomial-time k-truth-table autoreduction is a polynomial-time Turing autoreduction.

    source
    theorem Cslib.Complexity.PolyTimeBTTAutoreducible.polyTimeTuringAutoreducible {α : Type} {encA : α ↪ List Bool} {A : Set α} (h : PolyTimeBTTAutoreducible encA A) :
    PolyTimeTuringAutoreducible encA A

    Every polynomial-time bounded truth-table autoreduction is a polynomial-time Turing autoreduction.

    source
    theorem Cslib.Complexity.PolyTimeDTTAutoreducible.polyTimeTuringAutoreducible {α : Type} {encA : α ↪ List Bool} {A : Set α} (h : PolyTimeDTTAutoreducible encA A) :
    PolyTimeTuringAutoreducible encA A

    Every polynomial-time disjunctive truth-table autoreduction is a polynomial-time Turing autoreduction.

    source
    theorem Cslib.Complexity.PolyTimeCTTAutoreducible.polyTimeTuringAutoreducible {α : Type} {encA : α ↪ List Bool} {A : Set α} (h : PolyTimeCTTAutoreducible encA A) :
    PolyTimeTuringAutoreducible encA A

    Every polynomial-time conjunctive truth-table autoreduction is a polynomial-time Turing autoreduction.

    source
    theorem Cslib.Complexity.PolyTimeTruthTableMitotic.polyTimeTuringAutoreducible {α : Type} {encA : α ↪ List Bool} {A : Set α} (h : PolyTimeTruthTableMitotic encA A) :
    PolyTimeTuringAutoreducible encA A

    Every polynomial-time truth-table mitotic set is polynomial-time Turing autoreducible.

    source
    theorem Cslib.Complexity.PolyTimeBTTMitotic.polyTimeTuringAutoreducible {α : Type} {encA : α ↪ List Bool} {A : Set α} (h : PolyTimeBTTMitotic encA A) :
    PolyTimeTuringAutoreducible encA A

    Every polynomial-time bounded truth-table mitotic set is polynomial-time Turing autoreducible.

    source
    theorem Cslib.Complexity.PolyTimeKTruthTableMitotic.polyTimeTuringAutoreducible {α : Type} {encA : α ↪ List Bool} {A : Set α} {k : ℕ} (h : PolyTimeKTruthTableMitotic k encA A) :
    PolyTimeTuringAutoreducible encA A

    Every polynomial-time k-truth-table mitotic set is polynomial-time Turing autoreducible.

    source
    theorem Cslib.Complexity.PolyTimeDTTMitotic.polyTimeTuringAutoreducible {α : Type} {encA : α ↪ List Bool} {A : Set α} (h : PolyTimeDTTMitotic encA A) :
    PolyTimeTuringAutoreducible encA A

    Every polynomial-time disjunctive truth-table mitotic set is polynomial-time Turing autoreducible.

    source
    theorem Cslib.Complexity.PolyTimeManyOneMitotic.polyTimeTuringAutoreducible {α : Type} {encA : α ↪ List Bool} {A : Set α} (h : PolyTimeManyOneMitotic encA A) :
    PolyTimeTuringAutoreducible encA A

    Every polynomial-time many-one mitotic set is polynomial-time Turing autoreducible.