Documentation

VCVio.OracleComp.SimSemantics.QueryImpl.Compose

Composition of oracle implementations #

The free-monad fold composes implementations by its universal naturality law. Composition preserves the target monad's effects and needs no probabilistic interpretation.

source
def QueryImpl.compose {m : Type u → Type v} [Monad m] {ι : Type u_1} {ι' : Type u_2} {spec : OracleSpec ι} {spec' : OracleSpec ι'} (so' : QueryImpl spec' m) (so : QueryImpl spec (OracleComp spec')) :
QueryImpl spec m

Given an implementation of spec in terms of a new set of oracles spec', and an implementation of spec' in terms of arbitrary m, implement spec in terms of m.

Instances For
    source
    def QueryImpl.«term_∘ₛ_» :
    Lean.TrailingParserDescr
    Instances For
      source
      @[simp]
      theorem QueryImpl.apply_compose {m : Type u → Type v} [Monad m] {ι : Type u_1} {ι' : Type u_2} {spec : OracleSpec ι} {spec' : OracleSpec ι'} (so' : QueryImpl spec' m) (so : QueryImpl spec (OracleComp spec')) (t : spec.Domain) :
      (so' ∘ₛ so) t = simulateQ so' (so t)
      source
      @[simp]
      theorem QueryImpl.simulateQ_compose {m : Type u → Type v} [Monad m] {ι : Type u_1} {ι' : Type u_2} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {α : Type u} [LawfulMonad m] (so' : QueryImpl spec' m) (so : QueryImpl spec (OracleComp spec')) (oa : OracleComp spec α) :
      simulateQ (so' ∘ₛ so) oa = simulateQ so' (simulateQ so oa)
      source
      @[simp]
      theorem QueryImpl.compose_id' {m : Type u → Type v} [Monad m] {ι : Type u_1} {spec : OracleSpec ι} [LawfulMonad m] (so : QueryImpl spec m) :
      so ∘ₛ QueryImpl.id' spec = so