Generic local execution laws over interaction trees

This file introduces the execution-side counterpart to Spec.SyntaxOver.

Spec.InteractionOver is a local operational law for agent-indexed node objects. It says how a whole profile of local objects, one for each agent, is combined at a single protocol node in order to choose the next move and continue the interaction. The node-local information seen by those objects is packaged as a realized Spec.Node.Context.

The role-based prover/verifier runners used elsewhere in the library are specializations of this more general notion, obtained by choosing suitable node contexts and syntax objects.

Just as SyntaxOver reindexes contravariantly along node-context morphisms, InteractionOver.comap transports a local execution law along the same kind of context change.

Naming note: InteractionOver keeps the suffix form for the same reason as ShapeOver: it is the primary generalized execution notion, while Interaction is its trivial-data specialization rather than a base value that InteractionOver depends on.

structure Interaction.Spec.InteractionOver (Agent : Type a) (Γ : Node.Context) (syn : SyntaxOver Agent Γ) (m : Type w → Type w) : Type (max (max (max a (u + 1)) u_1) (w + 1))

InteractionOver Agent Γ syn m is the most general local execution law for agent-indexed participant objects.

It answers the following question:

Suppose we are standing at one protocol node with move space X. Every agent a has a local node object of type syn.Node a X γ (Cont a). How do we execute this node, choose the next move x : X, and continue with the continuation values of all agents at that x?

So:

• SyntaxOver describes the local syntax available to each agent;
• InteractionOver describes the local operational semantics for one protocol step built from that syntax.

This is the level at which the execution discipline lives: who chooses the move, how it is sampled or observed, how the local node objects synchronize, and how effects in m are used.

• interact {X : Type u} {γ : Γ X} {Cont : Agent → X → Type w} {Result : Type w} : ((agent : Agent) → syn.Node agent X γ (Cont agent)) → ((x : X) → ((agent : Agent) → Cont agent x) → m Result) → m Result

  interact executes one protocol node.

  Inputs:

  • a move space X;
  • realized node-local context γ : Γ X;
  • for each agent a, a local node object syn.Node a X γ (Cont a);
  • a continuation k explaining how to proceed once a move x : X has been chosen and each agent supplies its continuation value at that x.

  Output:

  • one monadic step of type m Result.

  In other words, interact is the one-step execution rule for the whole agent profile at this node.

@[reducible, inline]

abbrev Interaction.Spec.Interaction (Agent : Type a) (syn : Syntax Agent) (m : Type w → Type w) : Type (max (max (max a (u_1 + 1)) u_2) (w + 1))

Interaction Agent syn m is the specialization of InteractionOver with no node-local context.

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

def Interaction.Spec.InteractionOver.comap {Agent : Type a} {Γ : Node.Context} {Δ : Node.Context} {syn : SyntaxOver Agent Δ} {m : Type w → Type w} (I : InteractionOver Agent Δ syn m) (f : Node.ContextHom Γ Δ) : InteractionOver Agent Γ (syn.comap f) m

Reindex a local execution law contravariantly along a node-context morphism.

If f : Γ → Δ, then an execution law for Δ-contexts can be reused on Γ-contexts by first viewing the local syntax through SyntaxOver.comap f. At each node, the translated context value f X γ is what the original execution law sees.

@[reducible, inline]

abbrev Interaction.Spec.InteractionOver.comapSchema {Agent : Type a} {Γ : Node.Context} {Δ : Node.Context} {S : Node.Schema Γ} {T : Node.Schema Δ} {syn : SyntaxOver Agent Δ} {m : Type w → Type w} (I : InteractionOver Agent Δ syn m) (f : S.SchemaMap T) : InteractionOver Agent Γ (syn.comapSchema f) m

Reindex a local execution law contravariantly along a schema morphism, using the underlying realized context morphism.

@[simp]

theorem Interaction.Spec.InteractionOver.comap_id {Agent : Type a} {Γ : Node.Context} {syn : SyntaxOver Agent Γ} {m : Type w → Type w} (I : InteractionOver Agent Γ syn m) : I.comap (Node.ContextHom.id Γ) = I

theorem Interaction.Spec.InteractionOver.comap_comp {Agent : Type a} {Γ : Node.Context} {Δ : Node.Context} {Λ : Node.Context} {syn : SyntaxOver Agent Λ} {m : Type w → Type w} (I : InteractionOver Agent Λ syn m) (g : Node.ContextHom Δ Λ) (f : Node.ContextHom Γ Δ) : (I.comap g).comap f = I.comap (g.comp f)

def Interaction.Spec.InteractionOver.run {Agent : Type u} {Γ : Node.Context} {syn : SyntaxOver Agent Γ} {m : Type u → Type u} (I : InteractionOver Agent Γ syn m) [Monad m] {spec : Spec} (ctxs : Decoration Γ spec) {Out : Agent → spec.Transcript → Type u} (profile : (agent : Agent) → syn.Family agent spec ctxs (Out agent)) : m ((tr : spec.Transcript) × ((agent : Agent) → Out agent tr))

Execute a whole protocol tree using the local one-step law interact.

Inputs:

• spec is the underlying interaction tree;
• ctxs : Decoration Γ spec supplies the realized node context at each node;
• Out : Agent → Transcript spec → Type u is the final output family for each agent;
• profile supplies, for every agent, that agent's whole-tree participant object induced by syn.

Output:

• a monadic computation producing
  • a concrete transcript tr, and
  • for each agent a, the final output Out a tr obtained by following that transcript.

So run is the whole-tree execution induced by the local execution law InteractionOver.interact. It is the generic profile-level analogue of the specialized two-party runners elsewhere in the library.

This first executable version is intentionally specialized to the common single-universe setting used throughout the current interaction layer. The underlying SyntaxOver and InteractionOver abstractions remain more general.