Documentation

VCVio.Interaction.Basic.Strategy

Strategies (Spec.Strategy) #

A Strategy m spec Output plays through spec, choosing moves and interleaving effects in m, producing a transcript-dependent result Output tr. Definitions are by structural recursion on the spec (Hancock–Setzer), avoiding positivity issues for generic m.

run executes a strategy; mapOutput is functorial in the output family. Dependent sequential composition Strategy.comp requires Spec.append from VCVio.Interaction.Basic.Append.

source
def Interaction.Spec.Strategy (m : Type u → Type u) (spec : Spec) :
(spec.Transcript → Type u) → Type u

One-player strategy with monadic effects: at each node, choose a move x and continue in m.

Instances For
    source
    @[reducible, inline]
    abbrev Interaction.Spec.Strategy' (m : Type u → Type u) (spec : Spec) (α : Type u) :
    Type u

    Non-dependent output type α at every transcript.

    Instances For
      source
      def Interaction.Spec.Strategy.run {m : Type u → Type u} [Monad m] (spec : Spec) {Output : spec.Transcript → Type u} :
      Strategy m spec Output → m ((tr : spec.Transcript) × Output tr)

      Run the strategy, returning the full transcript and the dependent output.

      Instances For
        source
        def Interaction.Spec.Strategy.mapOutput {m : Type u → Type u} [Functor m] {spec : Spec} {A B : spec.Transcript → Type u} :
        ((tr : spec.Transcript) → A tr → B tr) → Strategy m spec A → Strategy m spec B

        Map the dependent output family along a natural transformation over transcripts.

        Instances For
          source
          @[simp]
          theorem Interaction.Spec.Strategy.mapOutput_id {m : Type u → Type u} [Functor m] [LawfulFunctor m] {spec : Spec} {A : spec.Transcript → Type u} (σ : Strategy m spec A) :
          mapOutput (fun (x : spec.Transcript) (x_1 : A x) => x_1) σ = σ

          Pointwise identity on outputs is the identity on strategies (needs a lawful functor).

          source
          theorem Interaction.Spec.Strategy.mapOutput_comp {m : Type u → Type u} [Functor m] [LawfulFunctor m] {spec : Spec} {A B C : spec.Transcript → Type u} (g : (tr : spec.Transcript) → B tr → C tr) (f : (tr : spec.Transcript) → A tr → B tr) (σ : Strategy m spec A) :
          mapOutput (fun (tr : spec.Transcript) (x : A tr) => g tr (f tr x)) σ = mapOutput g (mapOutput f σ)

          mapOutput respects composition of output maps (needs a lawful functor).