Whole-tree strategies over interaction syntax

This file turns local syntax into whole-tree strategy families. It sits after SyntaxOver and ShapeOver: syntax describes one node, shape adds local continuation reindexing, and StrategyOver recursively interprets that syntax over an entire FreeM tree.

def Interaction.StrategyOver {P : PFunctor.{uA, uB}} {Q : PFunctor.{uA₂, uB₂}} {α : Type t} {Agent : Type a} {Γ : P.A → Type vΓ} {l : P.Lens Q} (syn : SyntaxOver l Agent Γ) (agent : Agent) (spec : P.FreeM α) : PFunctor.FreeM.Displayed.Decoration Γ spec → (PFunctor.FreeM.PathAlong l spec → Type w) → Type w

Whole-tree local strategy induced by lens-indexed local syntax.

At leaves it returns the output family. At a control node it presents the local node object supplied by syn, whose continuation family is recursively the strategy for the abstract branch selected by the lens.

structure Interaction.StrategyOver.Hom {P : PFunctor.{uA, uB}} {Q : PFunctor.{uA₂, uB₂}} {Γ : P.A → Type vΓ} {Agent₁ : Type a} {Agent₂ : Type u} {l : P.Lens Q} (syn₁ : SyntaxOver l Agent₁ Γ) (agent₁ : Agent₁) (syn₂ : SyntaxOver l Agent₂ Γ) (agent₂ : Agent₂) : Type (max (max (max uA uB₂) vΓ) (w + 1))

A local homomorphism between two lens-executed StrategyOver fibers.

The source and target may use different local syntax objects and different agents, while sharing the same control lens and node-context decoration. At each node, mapNode translates the source node object into the target node object after recursive continuations have already been translated.

• mapNode {pos : P.A} {γ : Γ pos} {A B : Q.B (l.toFunA pos) → Type w} : ((d : Q.B (l.toFunA pos)) → A d → B d) → syn₁.Node agent₁ pos γ A → syn₂.Node agent₂ pos γ B

def Interaction.StrategyOver.map {P : PFunctor.{uA, uB}} {Q : PFunctor.{uA₂, uB₂}} {α : Type t} {Γ : P.A → Type vΓ} {Agent₁ : Type a} {Agent₂ : Type u} {l : P.Lens Q} {syn₁ : SyntaxOver l Agent₁ Γ} {agent₁ : Agent₁} {syn₂ : SyntaxOver l Agent₂ Γ} {agent₂ : Agent₂} (η : Hom syn₁ agent₁ syn₂ agent₂) {spec : P.FreeM α} {ctxs : PFunctor.FreeM.Displayed.Decoration Γ spec} {A B : PFunctor.FreeM.PathAlong l spec → Type w} : ((path : PFunctor.FreeM.PathAlong l spec) → A path → B path) → StrategyOver syn₁ agent₁ spec ctxs A → StrategyOver syn₂ agent₂ spec ctxs B

Map a lens-executed whole-tree strategy along a local homomorphism, while also mapping its leaf output family.

The recursion follows runtime directions through PathAlong l spec; the lens maps each runtime direction back to the corresponding control branch.

structure Interaction.StrategyOver.ContextHom {P : PFunctor.{uA, uB}} {Q : PFunctor.{uA₂, uB₂}} {Γ : P.A → Type vΓ} {Agent₁ : Type a} {Agent₂ : Type u} {l : P.Lens Q} {Δ : P.A → Type vΔ} (syn₁ : SyntaxOver l Agent₁ Γ) (agent₁ : Agent₁) (syn₂ : SyntaxOver l Agent₂ Δ) (agent₂ : Agent₂) (φ : (pos : P.A) → Γ pos → Δ pos) : Type (max (max (max uA uB₂) vΓ) (w + 1))

A local homomorphism between two StrategyOver fibers while changing the node-local context through φ.

This is the context-changing analogue of StrategyOver.Hom: the source node at context value γ is translated to a target node at context value φ γ.

• mapNode {pos : P.A} {γ : Γ pos} {A B : Q.B (l.toFunA pos) → Type w} : ((d : Q.B (l.toFunA pos)) → A d → B d) → syn₁.Node agent₁ pos γ A → syn₂.Node agent₂ pos (φ pos γ) B

def Interaction.StrategyOver.mapContext {P : PFunctor.{uA, uB}} {Q : PFunctor.{uA₂, uB₂}} {α : Type t} {Γ : P.A → Type vΓ} {Agent₁ : Type a} {Agent₂ : Type u} {l : P.Lens Q} {Δ : P.A → Type vΔ} {syn₁ : SyntaxOver l Agent₁ Γ} {agent₁ : Agent₁} {syn₂ : SyntaxOver l Agent₂ Δ} {agent₂ : Agent₂} {φ : (pos : P.A) → Γ pos → Δ pos} (η : ContextHom syn₁ agent₁ syn₂ agent₂ φ) {spec : P.FreeM α} {ctxs : PFunctor.FreeM.Displayed.Decoration Γ spec} {Out : PFunctor.FreeM.PathAlong l spec → Type w} : StrategyOver syn₁ agent₁ spec ctxs Out → StrategyOver syn₂ agent₂ spec (PFunctor.FreeM.Displayed.Decoration.map φ spec ctxs) Out

Map a whole-tree strategy across a local context-changing homomorphism.

The context decoration is mapped structurally by the same context map φ.

structure Interaction.StrategyOver.ShapeContextHom {P : PFunctor.{uA, uB}} {Q : PFunctor.{uA₂, uB₂}} {Γ : P.A → Type vΓ} {Agent₁ : Type a} {Agent₂ : Type u} {l : P.Lens Q} {Δ : P.A → Type vΔ} (shape₁ : ShapeOver l Agent₁ Γ) (agent₁ : Agent₁) (shape₂ : ShapeOver l Agent₂ Δ) (agent₂ : Agent₂) (φ : (pos : P.A) → Γ pos → Δ pos) extends Interaction.StrategyOver.ContextHom shape₁.toSyntaxOver agent₁ shape₂.toSyntaxOver agent₂ φ : Type (max (max (max uA uB₂) vΓ) (w + 1))

A context-changing homomorphism between functorial shapes, natural in recursive continuation maps.

The naturality field is the reason mapContext commutes with ShapeOver.mapOutput: translating a node after mapping its continuations is the same as mapping continuations after translating the node.

• mapNode {pos : P.A} {γ : Γ pos} {A B : Q.B (l.toFunA pos) → Type w} : ((d : Q.B (l.toFunA pos)) → A d → B d) → shape₁.Node agent₁ pos γ A → shape₂.Node agent₂ pos (φ pos γ) B
• mapNode_map {pos : P.A} {γ : Γ pos} {A B C D : Q.B (l.toFunA pos) → Type w} (f₁ : (d : Q.B (l.toFunA pos)) → A d → B d) (f₂ : (d : Q.B (l.toFunA pos)) → A d → C d) (g₁ : (d : Q.B (l.toFunA pos)) → B d → D d) (g₂ : (d : Q.B (l.toFunA pos)) → C d → D d) (comm : ∀ (d : Q.B (l.toFunA pos)) (x : A d), g₁ d (f₁ d x) = g₂ d (f₂ d x)) (node : shape₁.Node agent₁ pos γ A) : self.mapNode g₁ (shape₁.map f₁ node) = shape₂.map g₂ (self.mapNode f₂ node)

theorem Interaction.StrategyOver.forAgent {P : PFunctor.{uA, uB}} {Q : PFunctor.{uA₂, uB₂}} {α : Type t} {Agent : Type a} {Γ : P.A → Type vΓ} {l : P.Lens Q} (syn : SyntaxOver l Agent Γ) (agent : Agent) {spec : P.FreeM α} (ctxs : PFunctor.FreeM.Displayed.Decoration Γ spec) {Out : PFunctor.FreeM.PathAlong l spec → Type w} : StrategyOver (syn.forAgent agent) PUnit.unit spec ctxs Out = StrategyOver syn agent spec ctxs Out

The whole-tree strategy induced by SyntaxOver.forAgent syn agent is the agent fiber of the original participant-indexed whole-tree strategy.

theorem Interaction.StrategyOver.comap {P : PFunctor.{uA, uB}} {Q : PFunctor.{uA₂, uB₂}} {α : Type t} {Agent : Type a} {Γ : P.A → Type vΓ} {l : P.Lens Q} {Δ : P.A → Type vΔ} (syn : SyntaxOver l Agent Δ) (f : (pos : P.A) → Γ pos → Δ pos) {agent : Agent} {spec : P.FreeM α} (ctxs : PFunctor.FreeM.Displayed.Decoration Γ spec) {Out : PFunctor.FreeM.PathAlong l spec → Type w} : StrategyOver (SyntaxOver.comap f syn) agent spec ctxs Out = StrategyOver syn agent spec (PFunctor.FreeM.Displayed.Decoration.map f spec ctxs) Out

Whole-tree families for SyntaxOver.comap f syn are exactly families for syn evaluated on the mapped decoration.

def Interaction.ShapeOver.toStrategyHom {P : PFunctor.{uA, uB}} {Q : PFunctor.{uA₂, uB₂}} {l : P.Lens Q} {Agent : Type a} {Γ : P.A → Type vΓ} (shape : ShapeOver l Agent Γ) (agent : Agent) : StrategyOver.Hom shape.toSyntaxOver agent shape.toSyntaxOver agent

View a functorial shape as a local strategy homomorphism on one agent fiber.

def Interaction.ShapeOver.mapOutput {P : PFunctor.{uA, uB}} {Q : PFunctor.{uA₂, uB₂}} {α : Type t} {l : P.Lens Q} {Agent : Type a} {Γ : P.A → Type vΓ} (shape : ShapeOver l Agent Γ) {agent : Agent} {spec : P.FreeM α} (ctxs : PFunctor.FreeM.Displayed.Decoration Γ spec) {A B : PFunctor.FreeM.PathAlong l spec → Type w} : ((path : PFunctor.FreeM.PathAlong l spec) → A path → B path) → StrategyOver shape.toSyntaxOver agent spec ctxs A → StrategyOver shape.toSyntaxOver agent spec ctxs B

Map leaf outputs through a whole lens-executed strategy.

This is the recursive global form of the local ShapeOver.map field. The runtime path index is PathAlong l spec, so it applies equally to plain specs and to control specs such as Oracle.Spec executed through a lens.

theorem Interaction.StrategyOver.mapContext_mapOutput {P : PFunctor.{uA, uB}} {Q : PFunctor.{uA₂, uB₂}} {α : Type t} {l : P.Lens Q} {Γ : P.A → Type vΓ} {Agent₁ : Type a} {Agent₂ : Type u} {Δ : P.A → Type vΔ} {shape₁ : ShapeOver l Agent₁ Γ} {agent₁ : Agent₁} {shape₂ : ShapeOver l Agent₂ Δ} {agent₂ : Agent₂} {φ : (pos : P.A) → Γ pos → Δ pos} (η : ShapeContextHom shape₁ agent₁ shape₂ agent₂ φ) {spec : P.FreeM α} {ctxs : PFunctor.FreeM.Displayed.Decoration Γ spec} {A B : PFunctor.FreeM.PathAlong l spec → Type w} (f : (path : PFunctor.FreeM.PathAlong l spec) → A path → B path) (strat : StrategyOver shape₁.toSyntaxOver agent₁ spec ctxs A) : mapContext η.toContextHom (shape₁.mapOutput ctxs f strat) = shape₂.mapOutput (PFunctor.FreeM.Displayed.Decoration.map φ spec ctxs) f (mapContext η.toContextHom strat)

Context-changing strategy maps commute with functorial output maps.

theorem Interaction.ShapeOver.family_comap {P : PFunctor.{uA, uB}} {Q : PFunctor.{uA₂, uB₂}} {α : Type t} {l : P.Lens Q} {Agent : Type a} {Γ : P.A → Type vΓ} {Δ : P.A → Type vΔ} (shape : ShapeOver l Agent Δ) (f : (pos : P.A) → Γ pos → Δ pos) {agent : Agent} {spec : P.FreeM α} (ctxs : PFunctor.FreeM.Displayed.Decoration Γ spec) {Out : PFunctor.FreeM.PathAlong l spec → Type w} : StrategyOver (comap f shape).toSyntaxOver agent spec ctxs Out = StrategyOver shape.toSyntaxOver agent spec (PFunctor.FreeM.Displayed.Decoration.map f spec ctxs) Out

Whole-tree families for ShapeOver.comap f shape are exactly families for shape evaluated on the mapped decoration.