Composition and execution semantics

Design synthesis, 7 October 2026. This chapter incorporates the supplied Astra report. Its models and acceptance tests describe intended architecture; they do not certify current implementation. The report inventoried 140 public routes and compared substantive sections of 51 documents. Repository source and current qualification receipts determine what ships.

Architecture thesis and invariants · Nodes, ports and hyperedge vocabulary · Composition and execution semantics · Compiler, source publication and consistency · Shadow, evidence and region releases · Authoring and industry precedents · Cross-runtime systems and worked scenarios · Impact, design obligations and qualification

7. Composition, rewriting and graph theory

A role-labelled incidence model makes n-ary relationships first class without turning every relation into a fake service. Let an incidence identify a hyperedge, node-owned port, role and optional position. A binary exclusive binding, a many-party session and a fanout relation share storage, but their role and cardinality laws remain different.

Open regions admit a useful category-theoretic model: boundaries are objects and implementations with exposed boundaries are morphisms. Sequential composition glues a shared interface; independent composition places regions side by side. Decorated cospans provide a formal construction under stated assumptions. Associativity and identity laws can become property tests for extraction, substitution and deployment partitioning. Reaktor still needs to choose an exact typed model and prove that its representation satisfies those laws. [Fong — Decorated Cospans (2015)] [Fong & Spivak — Seven Sketches in Compositionality]

Do not import copying or discarding laws for unique native resources merely because a diagram contains junctions. Ports with linear or affine ownership need restrictions. Likewise, DPO-style rewriting supplies structural matching/gluing conditions; it does not prove that replacing a payment or actor implementation preserves business behavior. [Patch Graph Rewriting: comparison with DPO rewriting] [WebAssembly Component Model — WIT] [Apache Arrow — C data interface]

Source-to-graph projections resemble lenses. Within a supported syntax subset, extracting after an accepted edit should recover the intended view, and writing an unchanged view should preserve the source modulo declared equivalence. Arbitrary foreign code cannot be promised a lossless round trip. Source ownership and staged publication are more important than claiming universal bidirectionality. [Foster et al. — Combinators for Bidirectional Tree Transformations] [Source ownership]

These theories should mostly produce compact specifications and acceptance tests. They are not a reason to implement a general category-theory engine inside the hot runtime.

8. Programming and execution semantics

Blueprint should denote a system, not just generate isolated Kotlin or JavaScript functions. The compiler output is a program bundle: graph revision, per-runtime region artifacts, service/FFI descriptors, schemas, placement and capability requirements, durable-work definitions, source maps, deployment intent and verification obligations. Build and realization are distinct phases.

The distributed abstract machine is semantic: named runtime islands with local execution, messages and sessions, resource owners, durable authorities and activation generations. It is not one physical interpreter spanning the network. A local pure call can lower to a direct function; a remote command lowers to a qualified service/work boundary. Failed or unavailable network execution is part of the language semantics, not an invisible implementation detail.

Keep three domain perspectives: topology/composition describes what exists and connects; behavior specifies state, control, values and effects; realization describes how approved definitions become running components. They share identity and schemas, but not one universal wire law. Each module dialect contributes legality and lowering rules. Code owns efficient algorithms; graph-owned regions make system composition inspectable and editable.

A source-owned region uses supported source edits. A structured-owned region has deterministic, versioned graph source and generates adapters or code. Layout, comments and editor coordinates stay separate from executable meaning. Cosmetic dragging must not change the semantic digest or invalidate Shadow. Transferring source ownership is an explicit migration, never a silent bidirectional overwrite. Reaktor Visual Language / Blueprints

General computation belongs inside behavior profiles with branches, calls, recursion/growable memory and explicit effects. Statecharts and workflow DAGs are useful restricted profiles, not the ceiling of the language. No generic static analysis can establish every behavioral property of arbitrary source; unsupported semantic knowledge is marked opaque while the boundary remains typed.

Ptolemy II is one of the closest architectural precedents: port-connected hierarchical actors whose directors specify models of computation. This strongly supports Reaktor’s use of qualified profiles rather than treating every connection as an ordinary function call and every cycle as an error. [Ptolemy II: hierarchy, ports and models of computation] [Lee & Parks — Dataflow Process Networks (1995)]

Use strongly connected components for recursive analysis or grouped activation, but let the semantic profile distinguish call recursion, delayed stream feedback, fixed-point queries and invalid ownership cycles. A condensed dependency graph being acyclic does not establish termination or a useful runtime schedule.

Session types and state machines make protocol phases checkable. A restricted workflow-net profile can visualize enabled work, outstanding branches and completion. Neither theory automatically handles every timeout, process crash, cancellation or unbounded program; their assumptions must survive projection and execution. [Honda, Yoshida & Carbone — Multiparty Asynchronous Session Types] [A Mechanised Theory of Multiparty Asynchronous Session Types (ECOOP 2025)] [van der Aalst et al. — Soundness of workflow nets]

Queueing theory connects the graph to operational behavior. Little’s law relates stable mean occupancy, arrival rate and response time. The M/M/1 model additionally assumes Poisson arrivals and exponential single-server service; its divergence near capacity explains why credits, admission and retry budgets matter. It is not a production latency model or a p99 predictor. [MIT OpenCourseWare — Queueing theory and Little’s law]

Placement is a constrained partitioning problem, not simply minimizing drawn network edges. Privacy, state ownership, memory domain, affinity and runtime availability are hard constraints. Optimize measured traffic or latency over feasible choices, using bounded methods or heuristics and exposing the chosen objective.

Composition is gluing a boundary, not drawing an arrow

The practical benefit is a reusable law for extraction, replacement and deployment partitioning.

Law / model / proof obligation: X → F ← Y, Y → G ← Z ⇒ X → (F +ᵧ G) ← Z

Reaktor design decision

Use open regions whose exported contracts stay fixed while their internals change. Composition should be associative up to the declared identity/isomorphism convention; identity regions should do nothing semantically.

What this does not establish

This is a proposed semantic model, not a proved theorem about current Reaktor. Do not infer arbitrary copying/deleting of linear resources from an unrestricted hypergraph/Frobenius construction.

Falsifiable acceptance test. Compose three pure regions with either parenthesization and compare observables and boundary ownership. Reject an attempt to duplicate a unique camera handle.

Theory, precedent and Reaktor context: Fong — Decorated Cospans (2015) Fong & Spivak — Seven Sketches in Compositionality The Living Graph

A safe rewrite explains what must remain

Treat a rewrite as a transaction proposal with a preserved interface and explicit preconditions.

Law / model / proof obligation: L ← K → R; require a legal match and gluing conditions, then discharge semantic obligations.

Reaktor design decision

DPO-style reasoning makes deletion and replacement conditions precise. Reaktor can use a simpler typed patch representation while testing equivalent preservation rules for the supported fragment.

What this does not establish

General graph matching can be expensive. Use stable identities and bounded matches for normal edits. Structural legality does not prove behavior equivalence or authorize an effect.

Falsifiable acceptance test. Toggle the external reference. A destructive rewrite is rejected while that unremapped reference remains.

Theory, precedent and Reaktor context: Patch Graph Rewriting: comparison with DPO rewriting Formal methods and evidence Stable foundations

Statecharts as an execution profile

Hierarchical states, parallel regions, guards and actors make protocol and interaction behavior explicit.

Vector diagram · click a marked item to inspect

Reaktor design decision

Define a qualified statechart dialect with explicit actor lifetime, event ordering, transition and effect semantics. Expose snapshots/microsteps through existing graph inspection.

Boundary / caveat

A statechart is not automatically durable or distributed. Pure guards do not undo commands already accepted by another authority.

Qualification test. Leave the Joining state while a request has committed remotely. Stop the child scope, but retrieve/reconcile the external result rather than claiming the effect vanished.

Official context and precedents: State machines and statecharts XState actor semantics Stately inspection API

Allow cycles where their semantics are defined

Do not impose DAG restrictions globally merely because they simplify one workflow executor.

Law / model / proof obligation: Condense(G) is a DAG; each SCC is a maximal mutually reachable set.

Reaktor design decision

Use SCCs for recursive dependency analysis, mutually dependent activation groups and fixed-point queries. Enforce acyclicity only on relations such as exclusive ownership containment that require it.

What this does not establish

A cycle can denote recursion, feedback with delay, a fixed point or deadlock. These are not interchangeable. Every accepted cycle needs the corresponding semantics and budget.

Falsifiable acceptance test. Accept a stream feedback loop with explicit delay/state; reject a cyclic ownership chain under the containment profile.

Theory, precedent and Reaktor context: The Living Graph Ptolemy II: hierarchy, ports and models of computation Compositionality of dataflow models

A well-typed message can still be an illegal action

Unary calls, streams, jobs and sessions need different interaction contracts.

Law / model / proof obligation: State × Event → State × Outcome; local projections must preserve the chosen global protocol.

Reaktor design decision

Use protocol automata to check request admission, cancellation, durable completion and recovery. Project a global choreography only where the chosen multiparty type theory supports projection and composition.

What this does not establish

Session-type progress results have assumptions. Crashes, timeouts, cancellation and transport reordering must be modeled or honestly excluded.

Falsifiable acceptance test. Advance the call phases. A lost acknowledgement must trigger receipt reconciliation, not a second commit.

Theory, precedent and Reaktor context: Graph protocol Service contracts Honda, Yoshida & Carbone — Multiparty Asynchronous Session Types A Mechanised Theory of Multiparty Asynchronous Session Types (ECOOP 2025) Durable work

Visualize what a workflow is waiting for

A finite Petri-net profile can make deadlock and completion obligations concrete.

Law / model / proof obligation: A transition fires only when enabled; m′ = m + C·u is necessary bookkeeping, not a reachability proof.

Reaktor design decision

Represent supported bounded workflow control as places, transitions and tokens. Test proper completion, missing branches and outstanding work instead of inferring completion from a drawn DAG.

What this does not establish

General extensions can make soundness difficult or undecidable. Bounded model checks apply to a pinned finite abstraction, not arbitrary Turing-complete behavior.

Falsifiable acceptance test. Step through split and join. The final token appears only after consuming both branch tokens.

Theory, precedent and Reaktor context: van der Aalst et al. — Soundness of workflow nets Durable work Data workflows

Backpressure is a first-class network contract

Capacity, buffering, retry and arrival behavior belong in the binding plan and evidence.

Law / model / proof obligation: Little: L = λW in a stable system. M/M/1: W = 1/(μ−λ), under the stated assumptions.

Reaktor design decision

Expose credits, queue depth, drop/coalesce policy, service capacity and deadline budget. Avoid retry policies that amplify overload and unchecked stream buffering that converts latency into memory exhaustion.

What this does not establish

This toy assumes Poisson arrivals, exponential service, one server and steady state. Real workloads need measurements and different models; no percentile or throughput claim follows.

Falsifiable acceptance test. Drive the toy arrival rate to capacity. The mean diverges rather than displaying a misleading finite prediction.

Theory, precedent and Reaktor context: MIT OpenCourseWare — Queueing theory and Little’s law FFI / Switchboard Live session topology Bus versus live Mesh

Make resource misuse unrepresentable where possible

The same lifetime contract must survive native, managed and asynchronous boundaries.

Law / model / proof obligation: Borrow lifetime ⊆ owner lifetime; one owned token cannot be duplicated without an explicit sharing operation.

Reaktor design decision

Use generated wrappers, static checks and runtime generation/lease validation. The graph catalogs the contract; the hot runtime enforces its qualified representation without serializing every resource.

What this does not establish

Static ownership laws cannot prevent every defect in opaque native code. A zero-copy path remains unsafe if a callback outlives the buffer, even when its bytes are correctly encoded.

Falsifiable acceptance test. Suspend an async consumer past the original borrowed call. Require a legal transfer/retain or reject the binding at generation/admission.

Theory, precedent and Reaktor context: FFI / Switchboard Component lifecycle WebAssembly Component Model — WIT Apache Arrow — C data interface

Do not transact an architecture edit for every state update

Surface and game-native workloads expose why one store or scheduler would be the wrong unification.

Law / model / proof obligation: Definition revision ≠ activation epoch ≠ durable event sequence ≠ reactive/frame state.

Reaktor design decision

Keep source maps and operation IDs across planes. A performance tracer joins an observed invocation to its activation and definition; it does not make every animation sample a semantic graph record.

What this does not establish

Reactive state can be persisted when the application requires it, but that is a separate state authority. Different streams have different retention and privacy policies.

Falsifiable acceptance test. Update a theme value or game transform without rebuilding topology. Hot-replace a stateful region only under its explicit migration and lifetime protocol.

Theory, precedent and Reaktor context: Surface contracts and interaction Dynamic UI and verification Surface performance and assets Operational graph evidence Component lifecycle