Implementing Oracle Queries in Other Monads

This file defines a type QueryImpl spec m to represent implementations of queries to spec in terms of the monad m. It also provides the bridge between explicit QueryImpls and the lightweight HasQuery capability from VCVio.OracleComp.HasQuery.Basic.

@[reducible]

def QueryImpl {ι : Type u_1} (spec : OracleSpec ι) (m : Type u → Type v) : Type (max v u_1)

A monadic handler for the polynomial interface induced by spec.

Concretely, this maps every oracle input x to a computation returning an answer of type spec.Range x. It extends first to OracleQuery spec by applying the continuation, then to OracleComp spec by preserving pure and bind; see QueryImpl.mapQuery and simulateQ.

theorem QueryImpl.eq_handler {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} : QueryImpl spec m = PFunctor.Handler m spec.toPFunctor

QueryImpl is definitionally PolyFun's generic monadic handler for the polynomial interface induced by an oracle specification.

@[instance_reducible]

instance QueryImpl.instInhabitedOfRangeOfPure {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} [(t : ι) → Inhabited (spec.Range t)] [Pure m] : Inhabited (QueryImpl spec m)

theorem QueryImpl.ext {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} {so so' : QueryImpl spec m} (h : ∀ (x : spec.Domain), so x = so' x) : so = so'

Two query implementations are the same if they are the same on all query inputs.

theorem QueryImpl.ext_iff {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} {so so' : QueryImpl spec m} : so = so' ↔ ∀ (x : spec.Domain), so x = so' x

def QueryImpl.restrictLeft {m : Type u → Type v} {ι₁ ι₂ : Type} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (impl : QueryImpl (spec₁ + spec₂) m) : QueryImpl spec₁ m

Restrict an implementation of a sum specification to its left component.

def QueryImpl.restrictRight {m : Type u → Type v} {ι₁ ι₂ : Type} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (impl : QueryImpl (spec₁ + spec₂) m) : QueryImpl spec₂ m

Restrict an implementation of a sum specification to its right component.

theorem QueryImpl.restrictLeft_apply {m : Type u → Type v} {ι₁ ι₂ : Type} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (impl : QueryImpl (spec₁ + spec₂) m) (t : spec₁.Domain) : impl.restrictLeft t = impl (Sum.inl t)

Applying a left restriction is the original implementation on a left input.

theorem QueryImpl.restrictRight_apply {m : Type u → Type v} {ι₁ ι₂ : Type} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (impl : QueryImpl (spec₁ + spec₂) m) (t : spec₂.Domain) : impl.restrictRight t = impl (Sum.inr t)

Applying a right restriction is the original implementation on a right input.

@[reducible, inline]

abbrev QueryImpl.toHasQuery {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} (impl : QueryImpl spec m) : HasQuery spec m

View a concrete query implementation as query capability in the same monad. This is useful when instantiating a generic HasQuery construction directly inside an analysis monad such as StateT σ ProbComp or WriterT ω (OracleComp spec).

@[simp]

theorem QueryImpl.toHasQuery_query {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} (impl : QueryImpl spec m) (t : spec.Domain) : query t = impl t

def QueryImpl.mapQuery {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} {α : Type u} [Functor m] (impl : QueryImpl spec m) (q : OracleQuery spec α) : m α

Embed an oracle query into a new functor by applying the implementation to the input value before applying the continuation of the element.

@[simp]

theorem QueryImpl.mapQuery_query {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} [Functor m] [LawfulFunctor m] (impl : QueryImpl spec m) (t : spec.Domain) : impl.mapQuery (OracleSpec.query t) = impl t

@[simp]

theorem QueryImpl.mapQuery_mk {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} {α : Type u} [Functor m] (impl : QueryImpl spec m) (t : spec.Domain) (f : spec.Range t → α) : impl.mapQuery (OracleQuery.mk t f) = f <$> impl t

Reduce mapQuery on an explicit constructor-form query. Companion to mapQuery_query for queries that arise from SubSpec-lift normalization (which produces OracleQuery.mk/anonymous-constructor forms rather than OracleSpec.query).

@[reducible, inline]

abbrev QueryImpl.liftTarget {ι : Type u_2} {spec : OracleSpec ι} {m : Type u → Type v} (n : Type u → Type u_1) [MonadLiftT m n] (impl : QueryImpl spec m) : QueryImpl spec n

Compatibility alias for the generic polynomial-handler target lift.

theorem QueryImpl.liftTarget_apply {ι : Type u_2} {spec : OracleSpec ι} {m : Type u → Type v} (n : Type u → Type u_1) [MonadLiftT m n] (impl : QueryImpl spec m) (t : spec.Domain) : liftTarget n impl t = liftM (impl t)

theorem QueryImpl.liftTarget_self {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} (impl : QueryImpl spec m) : liftTarget m impl = impl

Lifting an implementation to the original monad has no effect.

@[simp]

theorem QueryImpl.mapQuery_liftTarget {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} {α : Type u} (n : Type u → Type w) [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [MonadLiftT m n] [LawfulMonadLiftT m n] (impl : QueryImpl spec m) (q : OracleQuery spec α) : (liftTarget n impl).mapQuery q = liftM (impl.mapQuery q)

def QueryImpl.id {ι : Type u_1} (spec : OracleSpec ι) : QueryImpl spec (OracleQuery spec)

Identity implementation for queries, sending q : OracleQuery spec α to itself.

@[simp]

theorem QueryImpl.id_apply {ι : Type u_1} {spec : OracleSpec ι} (t : spec.Domain) : QueryImpl.id spec t = OracleSpec.query t

@[simp]

theorem QueryImpl.mapQuery_id {ι : Type u_2} {α : Type u_1} {spec : OracleSpec ι} (q : OracleQuery spec α) : (QueryImpl.id spec).mapQuery q = q

def QueryImpl.id' {ι : Type u_1} (spec : OracleSpec ι) : QueryImpl spec (OracleComp spec)

Version of QueryImpl.id that automatically lifts into OracleComp spec rather than just implementing queries in the lower level OracleQuery spec monad

@[simp]

theorem QueryImpl.id'_apply {ι : Type u_1} {spec : OracleSpec ι} (t : spec.Domain) : QueryImpl.id' spec t = liftM (OracleSpec.query t)

@[simp]

theorem QueryImpl.mapQuery_id' {ι : Type u_2} {α : Type u_1} {spec : OracleSpec ι} (q : OracleQuery spec α) : (QueryImpl.id' spec).mapQuery q = liftM q

def QueryImpl.ofLift {ι : Type u_1} (spec : OracleSpec ι) (m : Type u → Type v) [MonadLiftT (OracleQuery spec) m] : QueryImpl spec m

Given that queries in spec lift to the monad m we get an implementation via lifting.

@[simp]

theorem QueryImpl.ofLift_apply {ι : Type u_1} (spec : OracleSpec ι) (m : Type u → Type v) [MonadLiftT (OracleQuery spec) m] (t : spec.Domain) : ofLift spec m t = liftM (OracleSpec.query t)

@[simp]

theorem QueryImpl.mapQuery_ofLift {ι : Type u_1} {α : Type u} (spec : OracleSpec ι) (m : Type u → Type v) [Functor m] [MonadLiftT (OracleQuery spec) m] (q : OracleQuery spec α) : (ofLift spec m).mapQuery q = q.cont <$> liftM (OracleSpec.query q.input)

@[simp]

theorem QueryImpl.ofLift_eq_id {ι : Type u_1} {spec : OracleSpec ι} : ofLift spec (OracleQuery spec) = QueryImpl.id spec

@[simp]

theorem QueryImpl.ofLift_eq_id' {ι : Type u_1} {spec : OracleSpec ι} : ofLift spec (OracleComp spec) = QueryImpl.id' spec

def QueryImpl.ofFn {ι : Type u_1} {spec : OracleSpec ι} (f : (t : spec.Domain) → spec.Range t) : QueryImpl spec Id

View a function from oracle inputs to outputs as an implementation in the Id monad. Can be used to run a computation to get a specific value.

@[simp]

theorem QueryImpl.ofFn_apply {ι : Type u_1} {spec : OracleSpec ι} (f : (t : spec.Domain) → spec.Range t) (t : spec.Domain) : ofFn f t = f t

@[simp]

theorem QueryImpl.mapQuery_ofFn {ι : Type u_2} {spec : OracleSpec ι} {α : Type u_1} (f : (t : spec.Domain) → spec.Range t) (q : OracleQuery spec α) : (ofFn f).mapQuery q = q.cont (f q.input)

def QueryImpl.ofFn? {ι : Type u_1} {spec : OracleSpec ι} (f : (t : spec.Domain) → Option (spec.Range t)) : QueryImpl spec Option

Version of ofFn that allows queries to fail to return a value.

@[simp]

theorem QueryImpl.ofFn?_apply {ι : Type u_1} {spec : OracleSpec ι} (f : (t : spec.Domain) → Option (spec.Range t)) (t : spec.Domain) : ofFn? f t = f t

@[simp]

theorem QueryImpl.mapQuery_ofFn? {ι : Type u_2} {spec : OracleSpec ι} {α : Type u_1} (f : (t : spec.Domain) → Option (spec.Range t)) (q : OracleQuery spec α) : (ofFn? f).mapQuery q = Option.map q.cont (f q.input)

@[reducible]

def QueryImpl.ofPolynomial {R : Type u_1} [Semiring R] (p : Polynomial R) : QueryImpl (OracleSpec.ofFn fun (x : R) => R) Id

Implement a single oracle as evaluation of a Polynomial.

@[reducible]

noncomputable def QueryImpl.ofMvPolynomial {R : Type u_1} {σ : Type u_2} [CommSemiring R] (p : MvPolynomial σ R) : QueryImpl (OracleSpec.ofFn fun (x : σ → R) => R) Id

Implement a single oracle as the evaluation of an `MvPolynomial.

@[reducible]

def QueryImpl.ofVector {α : Type u_1} {n : ℕ} (v : Vector α n) : QueryImpl (OracleSpec.ofFn fun (x : Fin n) => α) Id

Implement a single oracle as indexing into a Vector.

@[reducible]

def QueryImpl.ofListVector {α : Type u_1} {n : ℕ} (v : List.Vector α n) : QueryImpl (OracleSpec.ofFn fun (x : Fin n) => α) Id

Oracle context for ability to query elements of a vector v.

def HasQuery.toQueryImpl {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} [HasQuery spec m] : QueryImpl spec m

Repackage HasQuery as a QueryImpl, for APIs that still consume explicit oracle implementations.

@[simp]

theorem HasQuery.toQueryImpl_apply {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} [HasQuery spec m] (t : spec.Domain) : toQueryImpl t = query t

theorem HasQuery.toQueryImpl_eq_id' {ι : Type u_1} {spec : OracleSpec ι} : toQueryImpl = QueryImpl.id' spec

On OracleComp spec, HasQuery.toQueryImpl is the identity handler QueryImpl.id'.

Not @[simp]: in definitions where toQueryImpl.liftTarget appears inside a simplifying unfold, the rewrite toQueryImpl → id' = liftTarget _ (id _) nests liftTargets and triggers unbounded depth. Use via explicit rw instead.