Polynomial Time Computations #
Polynomial complexity for computations with oracles.
More background theory on TM2ComputableInPolyTime would be needed
to make this kind of approach usable in practice.
More adaptation would also be needed to handle dependent types
inductive
OracleComp.PolyTimeOC
{ι : Type}
{spec : OracleSpec ι}
{α β : Type}
:
(α → OracleComp spec β) → Prop
Predicate for capturing polynomial complexity of an OracleComp.
Functions by extending the turing-machine definition from mathlib.
- polyTime_query {ι : Type} {spec : OracleSpec ι} {α : Type} (i : ι) (f : α → spec.domain i) (hf : (ea : Computability.FinEncoding α) × (eb : Computability.FinEncoding (spec.domain i)) × Turing.TM2ComputableInPolyTime ea eb f) : PolyTimeOC fun (x : α) => liftM (OracleSpec.query i (f x))
- polyTime_return {ι : Type} {spec : OracleSpec ι} {α β : Type} (f : α → β) (hf : (ea : Computability.FinEncoding α) × (eb : Computability.FinEncoding β) × Turing.TM2ComputableInPolyTime ea eb f) : PolyTimeOC fun (x : α) => pure (f x)
- polyTime_bind {ι : Type} {spec : OracleSpec ι} {α β γ : Type} (oa : α → OracleComp spec β) (ob : α → β → OracleComp spec γ) (hoa : PolyTimeOC oa) (hob : PolyTimeOC (Function.uncurry ob)) : PolyTimeOC fun (x : α) => do let y ← oa x ob x y