Generic local syntax over interaction trees

This file introduces the most general local syntax layer in the Interaction framework.

SyntaxOver is the base local-syntax object: it says what kind of node object an agent has at one protocol node, as a function of

• the agent,
• the move space at that node,
• the realized node-local context available there, and
• the continuation family after each possible move.

Crucially, SyntaxOver does not require any functorial action on continuations. This matters because many important interaction nodes hide their recursive continuations under outer constructors such as monads, oracle queries, state transitions, or other effect wrappers. Such nodes are valid local syntax, but they need not support a generic continuation map.

ShapeOver in Basic/Shape is the functorial refinement of this base notion: it adds continuation reindexing when the local syntax really does support it.

Role-based APIs are specializations of this pattern:

• Spec.Node.Context is the semantic family of node-local data;
• Spec.Node.Schema is the telescope-style front-end for building such contexts;
• Spec.Node.ContextHom and SyntaxOver.comap express contravariant reindexing of local syntax along context morphisms;
• fun _ => Role is one example of a simple node context;
• StrategyOver is the whole-tree local strategy induced by one-node syntax.

Naming note: SyntaxOver is the base local-syntax notion. ShapeOver uses the same suffix to signal that it is the functorial refinement of syntax, with continuation reindexing available as part of the interface.

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

SyntaxOver l Agent Γ is local syntax over an arbitrary control polynomial executed through a runtime lens l.

At control position pos : P.A, node metadata has type Γ pos, while the local continuation family is indexed by runtime directions Q.B (l.toFunA pos). The lens maps each runtime direction back to the abstract control branch used for recursion.

• Node (agent : Agent) (pos : P.A) (γ : Γ pos) : (Q.B (l.toFunA pos) → Type w) → Type w

def Interaction.SyntaxOver.comap {P : PFunctor.{uA, uB}} {Q : PFunctor.{uA₂, uB₂}} {l : P.Lens Q} {Agent : Type a} {Γ : P.A → Type vΓ} {Δ : P.A → Type vΔ} (f : (pos : P.A) → Γ pos → Δ pos) (syn : SyntaxOver l Agent Δ) : SyntaxOver l Agent Γ

Reindex a local syntax object contravariantly along a node metadata map.

If f : Γ → Δ, then any syntax over Δ can be viewed as syntax over Γ by translating the local metadata value before passing it to the original syntax.

@[simp]

theorem Interaction.SyntaxOver.comap_id {P : PFunctor.{uA, uB}} {Q : PFunctor.{uA₂, uB₂}} {l : P.Lens Q} {Agent : Type a} {Γ : P.A → Type vΓ} (syn : SyntaxOver l Agent Γ) : comap (fun (x : P.A) (γ : Γ x) => γ) syn = syn

theorem Interaction.SyntaxOver.comap_comp {P : PFunctor.{uA, uB}} {Q : PFunctor.{uA₂, uB₂}} {l : P.Lens Q} {Agent : Type a} {Γ : P.A → Type vΓ} {Δ : P.A → Type vΔ} {Λ : P.A → Type vΛ} (syn : SyntaxOver l Agent Λ) (g : (pos : P.A) → Δ pos → Λ pos) (f : (pos : P.A) → Γ pos → Δ pos) : comap f (comap g syn) = comap (fun (pos : P.A) => g pos ∘ f pos) syn

def Interaction.SyntaxOver.forAgent {P : PFunctor.{uA, uB}} {Q : PFunctor.{uA₂, uB₂}} {l : P.Lens Q} {Agent : Type a} {Γ : P.A → Type vΓ} (syn : SyntaxOver l Agent Γ) (agent : Agent) : SyntaxOver l PUnit.{u_2 + 1} Γ

Restrict a participant-indexed syntax to one fixed agent.

The resulting singleton-agent syntax has the same node objects as syn at agent; the dummy PUnit agent argument is ignored.

@[reducible, inline]

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

Syntax Agent is the specialization of generic SyntaxOver to plain Spec trees with no node-local context.

This is the right facade when the protocol tree carries no node metadata at all.