Functorial local syntax over interaction trees

This file introduces the functorial refinement of the local syntax core.

Spec.SyntaxOver in Basic/Syntax is the most general local syntax object: it describes which node object an agent has at one protocol node, with no assumption that recursive continuations can be reindexed generically.

Spec.ShapeOver is the functorial refinement of that base notion: it equips a SyntaxOver with a continuation map. This is exactly the extra structure needed to define generic output transport such as ShapeOver.mapOutput.

Many important interaction objects are syntax without being shapes in this sense: if recursive continuations are hidden under an opaque outer constructor, then a generic continuation map may not exist. This is why SyntaxOver is the semantic base layer, while ShapeOver is the stronger interface used when continuations are exposed functorially enough.

Naming note: ShapeOver keeps the suffix form because it is the primary functorial refinement of syntax, with plain Shape recovered as the trivial-context specialization. This differs from Decoration.Over, which is literally dependent data over a fixed base decoration value.

structure Interaction.Spec.ShapeOver (Agent : Type a) (Γ : Node.Context) extends Interaction.Spec.SyntaxOver Agent Γ : Type (max (max (max a (u + 1)) u_1) (w + 1))

ShapeOver Agent Γ is a functorial local-syntax object over realized node contexts Γ.

It answers the following question:

Suppose we are standing at one protocol node whose move space is X. The node carries realized node-local context γ : Γ X. If the protocol continues with family Cont : X → Type w, what is the type of the local object that agent a stores at this node?

Unlike bare SyntaxOver, a ShapeOver also provides a generic continuation map. So a shape is syntax that is functorial in its recursive continuations.

This is the right abstraction when node objects support a generic reindexing of their continuation payload, for example when those continuations remain exposed or are stored under constructors with a functorial action.

• Node (agent : Agent) (X : Type u) (γ : Γ X) : (X → Type w) → Type w
• map {agent : Agent} {X : Type u} {γ : Γ X} {A B : X → Type w} : ((x : X) → A x → B x) → self.Node agent X γ A → self.Node agent X γ B

  map expresses that a node object is functorial in its continuation family.

  If we know how to transform each continuation value A x into a continuation value B x, then we can transform a local node object with continuation family A into one with continuation family B.

  Importantly, map does not change:

  • the agent,
  • the move space,
  • the node-local context,
  • or the move x that will eventually be chosen.

  It only reinterprets what happens after each possible move. This is the local ingredient needed to define the generic whole-tree ShapeOver.mapOutput below.

@[reducible, inline]

abbrev Interaction.Spec.Shape (Agent : Type a) : Type (max (max (max a (u_1 + 1)) u_2) (u_3 + 1))

Shape Agent is the specialization of ShapeOver with no node-local context.

This is the right facade when the protocol tree carries no node metadata at all. Equivalently, it is ShapeOver Agent Spec.Node.Context.empty.

@[implicit_reducible]

instance Interaction.Spec.instCoeShapeOverSyntaxOver {Agent : Type a} {Γ : Node.Context} : Coe (ShapeOver Agent Γ) (SyntaxOver Agent Γ)

def Interaction.Spec.ShapeOver.comap {Agent : Type a} {Γ : Node.Context} {Δ : Node.Context} (shape : ShapeOver Agent Δ) (f : Node.ContextHom Γ Δ) : ShapeOver Agent Γ

Reindex a local syntax object contravariantly along a node-context morphism.

If f : Γ → Δ, then any shape over Δ can be viewed as a shape over Γ by first viewing its underlying syntax through SyntaxOver.comap f.

@[reducible, inline]

abbrev Interaction.Spec.ShapeOver.comapSchema {Agent : Type a} {Γ : Node.Context} {Δ : Node.Context} {S : Node.Schema Γ} {T : Node.Schema Δ} (shape : ShapeOver Agent Δ) (f : S.SchemaMap T) : ShapeOver Agent Γ

Reindex a local syntax object contravariantly along a schema morphism, using the underlying realized context morphism.

@[simp]

theorem Interaction.Spec.ShapeOver.comap_id {Agent : Type a} {Γ : Node.Context} (shape : ShapeOver Agent Γ) : shape.comap (Node.ContextHom.id Γ) = shape

theorem Interaction.Spec.ShapeOver.comap_comp {Agent : Type a} {Γ : Node.Context} {Δ : Node.Context} {Λ : Node.Context} (shape : ShapeOver Agent Λ) (g : Node.ContextHom Δ Λ) (f : Node.ContextHom Γ Δ) : (shape.comap g).comap f = shape.comap (g.comp f)

@[reducible, inline]

abbrev Interaction.Spec.ShapeOver.Family {Agent : Type a} {Γ : Node.Context} (shape : ShapeOver Agent Γ) (agent : Agent) (spec : Spec) : Decoration Γ spec → (spec.Transcript → Type w) → Type w

Whole-tree families for a shape are inherited from the underlying SyntaxOver.

def Interaction.Spec.ShapeOver.mapOutput {Agent : Type a} {Γ : Node.Context} (shape : ShapeOver Agent Γ) {agent : Agent} {spec : Spec} (ctxs : Decoration Γ spec) {A B : spec.Transcript → Type w} : ((tr : spec.Transcript) → A tr → B tr) → shape.Family agent spec ctxs A → shape.Family agent spec ctxs B

ShapeOver.mapOutput lifts a pointwise transformation of leaf outputs to a transformation of whole-tree participant objects.

This is the recursive global form of the local ShapeOver.map field. It leaves the underlying interactive structure unchanged and only rewrites the terminal output family.

theorem Interaction.Spec.ShapeOver.family_comap {Agent : Type a} {Γ : Node.Context} {Δ : Node.Context} (shape : ShapeOver Agent Δ) (f : Node.ContextHom Γ Δ) {agent : Agent} {spec : Spec} (ctxs : Decoration Γ spec) {Out : spec.Transcript → Type w} : (shape.comap f).Family agent spec ctxs Out = shape.Family agent spec (Decoration.map f spec ctxs) Out

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

theorem Interaction.Spec.ShapeOver.family_comapSchema {Agent : Type a} {Γ Δ : Node.Context} {S : Node.Schema Γ} {T : Node.Schema Δ} (shape : ShapeOver Agent Δ) (f : S.SchemaMap T) {agent : Agent} {spec : Spec} (ctxs : Decoration Γ spec) {Out : spec.Transcript → Type w} : (shape.comapSchema f).Family agent spec ctxs Out = shape.Family agent spec (Decoration.Schema.map f spec ctxs) Out