Documentation

VCVio.OracleComp.SimSemantics.SimulateQ

Simulation Semantics for Oracles in a Computation #

source
def simulateQ {ι : Type u_1} {spec : OracleSpec ι} {r : Type u → Type u_2} [Monad r] (impl : QueryImpl spec r) {α : Type u} (mx : OracleComp spec α) :
r α

Given an implementation of spec in the monad r, convert an OracleComp spec α to a implementation in r α by substituting impl t for query t throughout.

Equations
    Instances For
      source
      @[simp]
      theorem simulateQ_pure {α : Type u} {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] (impl : QueryImpl spec r) (x : α) :
      simulateQ impl (pure x) = pure x
      source
      @[simp]
      theorem simulateQ_bind {α β : Type u} {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] (impl : QueryImpl spec r) [LawfulMonad r] (mx : OracleComp spec α) (my : α → OracleComp spec β) :
      simulateQ impl (mx >>= my) = do let x ← simulateQ impl mx simulateQ impl (my x)
      source
      @[reducible]
      def simulateQ' {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] [LawfulMonad r] (impl : QueryImpl spec r) :
      OracleComp spec →ᵐ r

      Version of simulateQ that bundles into a monad hom.

      Equations
        Instances For
          source
          @[simp]
          theorem simulateQ_query {α : Type u} {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] (impl : QueryImpl spec r) [LawfulMonad r] (q : OracleQuery spec α) :
          simulateQ impl (liftM q) = q.cont <$> impl q.input
          source
          @[simp]
          theorem simulateQ_query_bind {α β : Type u} {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] (impl : QueryImpl spec r) [LawfulMonad r] (q : OracleQuery spec α) (ou : α → OracleComp spec β) :
          simulateQ impl (liftM q >>= ou) = do let u ← liftM (impl q.input) simulateQ impl (ou (q.cont u))
          source
          @[simp]
          theorem simulateQ_map {α β : Type u} {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] (impl : QueryImpl spec r) [LawfulMonad r] (mx : OracleComp spec α) (f : α → β) :
          simulateQ impl (f <$> mx) = f <$> simulateQ impl mx
          source
          @[simp]
          theorem simulateQ_seq {α β : Type u} {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] (impl : QueryImpl spec r) [LawfulMonad r] (og : OracleComp spec (α → β)) (mx : OracleComp spec α) :
          simulateQ impl (og <*> mx) = simulateQ impl og <*> simulateQ impl mx
          source
          @[simp]
          theorem simulateQ_seqLeft {α β : Type u} {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] (impl : QueryImpl spec r) [LawfulMonad r] (mx : OracleComp spec α) (my : OracleComp spec β) :
          simulateQ impl (mx <* my) = simulateQ impl mx <* simulateQ impl my
          source
          @[simp]
          theorem simulateQ_seqRight {α β : Type u} {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] (impl : QueryImpl spec r) [LawfulMonad r] (mx : OracleComp spec α) (my : OracleComp spec β) :
          simulateQ impl (mx *> my) = simulateQ impl mx *> simulateQ impl my
          source
          @[simp]
          theorem simulateQ_ite {α : Type u} {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] (impl : QueryImpl spec r) (p : Prop) [Decidable p] (mx mx' : OracleComp spec α) :
          simulateQ impl (if p then mx else mx') = if p then simulateQ impl mx else simulateQ impl mx'
          source
          theorem simulateQ_def {α : Type u} {ι : Type u_1} {spec : OracleSpec ι} {n : Type u → Type v} [Monad n] [LawfulMonad n] (impl : QueryImpl spec n) (mx : OracleComp spec α) :
          simulateQ impl mx = (fun {α : Type u} (x : spec.toPFunctor.FreeM α) => (PFunctor.FreeM.mapMHom impl).toFun α x) mx
          source
          @[simp]
          theorem simulateQ_id' {α : Type u} {ι : Type u_1} {spec : OracleSpec ι} (mx : OracleComp spec α) :
          simulateQ (QueryImpl.id' spec) mx = mx

          QueryImpl.id' is an identity for simulateQ with implementaiton in OracleComp spec.

          source
          theorem simulateQ_ofLift_eq_self {ι : Type u_1} {spec : OracleSpec ι} {α : Type u} (mx : OracleComp spec α) :
          simulateQ (QueryImpl.ofLift spec (OracleComp spec)) mx = mx

          Lifting queries to their original implementation has no effect on a computation.