Documentation

VCVio.OracleComp.Coinductive.Bridge

Bridge between OracleComp and ITree #

OracleComp spec α is the inductive free monad on spec.toPFunctor; ITree spec.toPFunctor α is the coinductive (M-type) free monad on the same polynomial functor. Every finite, terminating OracleComp program has a canonical embedding into the (potentially-infinite) ITree world.

This module provides that embedding, OracleComp.toITree, together with a small handful of structural simp lemmas (toITree_pure, toITree_queryBind, toITree_bind).

The reverse map "ITree-to-OracleComp" exists only on terminating ITrees and requires productivity / well-foundedness arguments that are not yet in scope; hence we provide only the forward direction here.

Universe restriction #

To keep the polynomial functor uniform-universe, we specialise to OracleSpec.{u, u} ι. The general OracleSpec.{u, v} case would force Poly F α to live in Type (max u v + 1), which is at odds with our single-universe ITree definition.

source
def OracleComp.toITree {ι : Type u} {spec : OracleSpec ι} {α : Type u} (oa : OracleComp spec α) :
ITree spec.toPFunctor α

Embed an OracleComp spec α into the corresponding ITree. Each pure x becomes ITree.pure x; each queryBind t k becomes ITree.query t (toITree ∘ k). The recursion is structural on OracleComp (which is an inductive free monad), so productivity is automatic.

Instances For
    source
    @[simp]
    theorem OracleComp.toITree_pure {ι : Type u} {spec : OracleSpec ι} {α : Type u} (x : α) :
    (pure x).toITree = ITree.pure x
    source
    @[simp]
    theorem OracleComp.toITree_queryBind {ι : Type u} {spec : OracleSpec ι} {α : Type u} (t : spec.Domain) (k : spec.Range t → OracleComp spec α) :
    (queryBind t k).toITree = ITree.query t fun (u : spec.toPFunctor.B t) => (k u).toITree