Skip to content

The RelationalMachineArena is the full interaction type of a RelationalMachine — the pair (Σ, I) of step types that enter and the global sections Γ(H*) that exit, specifying who can connect to the machine and what they will receive.

Relational Machine Arena

What this is

The RelationalMachineArena is the full interaction type of a RelationalMachine: what the machine accepts as input and what it returns as output, stated as a typed contract.

The arena name comes from compositional game theory (Ghani, Hedges et al.): an arena (X, S) specifies what a game receives from its context (X) and what it returns (S). Applied to the RelationalMachine: the input type is the RelationalMachinePort (the step set Σ with independence relation I) and the output type is the settled global sections emitted by the Observation Layer.

Knowing the arena of two RelationalMachines is sufficient to determine whether they can be connected: the output type of one must be receivable as an input type by the other.

Mathematical grounding

The input side of the arena is the RelationalMachinePort: steps s ∈ Σ, with commutation relation I. Each step s ∈ Σ indexes a sequential comonad G_s on R (directed-comonad). The CoKleisli category coKl(G_s) formalizes interaction: a morphism G_s X → Y is a process that consumes one step of type s and produces Y. The RelationalMachineArena is the type-level summary of all such morphisms: what step types enter (the port) and what settled sections exit (the observation layer output).

The output side is Γ(H*_{t’}) ∖ Γ(H*_t): the global sections newly settled after step t → t’ = s★t. This is the machine’s output per step: the sections that became stable as a result of processing the step.

In the FARS

In a FlatfileAgentialResourceSystem locale:

  • Input type: the four FlatfileAgentialResourceSystemMessage types {FixNeeded, GapFound, Discovery, Coordination}
  • Output type: messages deposited in other locales’ INBOX.md files and newly settled entity files

Two locales can be connected when the output type of one locale is a subset of the input type of the other locale’s RelationalMachinePort.

A RelationalMachineArena MUST name both the input type (RelationalMachinePort) and the output type (settled sections). It MUST be sufficient to determine connection compatibility between two RelationalMachines.

Open questions

Relations

Ast
Date created
Date modified
Input port
Relational universe
Output
Relational universe
Output sections
Relational history fiber fixed layer