Documentation

VCVio.OracleComp.SimSemantics.QueryImpl.Basic

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.

source
@[reducible]
def QueryImpl {ι : Type u_1} (spec : OracleSpec ι) (m : Type u → Type v) :
Type (max v u_1)

Specifies a way to implement queries to oracles in spec using the monad m. This is defined in terms of a mapping of input elements to oracle outputs, which extends to a mapping on OracleQuery spec by copying over the continuation, and then further to OracleComp spec by preserving the pure and bind operations. See QueryImpl.mapQuery and simulateQ for these two operations.

Instances For
    source
    @[implicit_reducible]
    instance QueryImpl.instInhabitedOfInhabitedOfPure {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} [spec.Inhabited] [Pure m] :
    Inhabited (QueryImpl spec m)
    source
    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.

    source
    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
    source
    @[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).

    Instances For
      source
      @[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
      source
      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.

      Instances For
        source
        @[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
        source
        @[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).

        source
        def 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

        Gadget for auto-adding a lift to the end of a query implementation.

        Instances For
          source
          @[simp]
          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)
          source
          @[simp]
          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.

          source
          @[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)
          source
          def QueryImpl.id {ι : Type u_1} (spec : OracleSpec ι) :
          QueryImpl spec (OracleQuery spec)

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

          Instances For
            source
            @[simp]
            theorem QueryImpl.id_apply {ι : Type u_1} {spec : OracleSpec ι} (t : spec.Domain) :
            QueryImpl.id spec t = OracleSpec.query t
            source
            @[simp]
            theorem QueryImpl.mapQuery_id {ι : Type u_2} {α : Type u_1} {spec : OracleSpec ι} (q : OracleQuery spec α) :
            (QueryImpl.id spec).mapQuery q = q
            source
            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

            Instances For
              source
              @[simp]
              theorem QueryImpl.id'_apply {ι : Type u_1} {spec : OracleSpec ι} (t : spec.Domain) :
              QueryImpl.id' spec t = liftM (OracleSpec.query t)
              source
              @[simp]
              theorem QueryImpl.mapQuery_id' {ι : Type u_2} {α : Type u_1} {spec : OracleSpec ι} (q : OracleQuery spec α) :
              (QueryImpl.id' spec).mapQuery q = liftM q
              source
              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.

              Instances For
                source
                @[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)
                source
                @[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)
                source
                @[simp]
                theorem QueryImpl.ofLift_eq_id {ι : Type u_1} {spec : OracleSpec ι} :
                ofLift spec (OracleQuery spec) = QueryImpl.id spec
                source
                @[simp]
                theorem QueryImpl.ofLift_eq_id' {ι : Type u_1} {spec : OracleSpec ι} :
                ofLift spec (OracleComp spec) = QueryImpl.id' spec
                source
                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.

                Instances For
                  source
                  @[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
                  source
                  @[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)
                  source
                  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.

                  Instances For
                    source
                    @[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
                    source
                    @[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)
                    source
                    @[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.

                    Instances For
                      source
                      @[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.

                      Instances For
                        source
                        @[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.

                        Instances For
                          source
                          @[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.

                          Instances For
                            source
                            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.

                            Instances For
                              source
                              @[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
                              source
                              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 unifFwdImpl-style definitions where toQueryImpl.liftTarget appears inside a simp [unifFwdImpl] call, the rewrite toQueryImpl → id' = liftTarget _ (id _) nests liftTargets and triggers unbounded depth. Use via explicit rw instead.