Graph model, protocols and computation
Technical preprint, 16 September 2026 — web reading edition. This preserves the supplied paper’s content and its historical evidence boundary. Proposed interfaces, conditional propositions and constructed studies are not released APIs or deployment proof. Aligned equations, tables and listings retain their source layout. Source figure pages retain the original vector artwork. The accompanying finite model and coverage-map source package were not supplied; their reported results have not been independently reproduced here.
Current guides: reaktor-unified-system-graph · graph-kernel-analysis · reaktor-actor-model.
The engine and feature composition · Graph model, protocols and computation · Platforms, identity and polyglot execution · Data authority, contracts and federation · Build, compilation and resource budgets · LiveUpdate, coordinator and human-agent authoring · Assurance and adoption studies · Precedents, evaluation and implementation sequence · References, notation, exercises and source lineage
8. Mathematical foundations for architectural reasoning
A mathematical model is useful when it removes ambiguity that would otherwise become an implementation bug. The purpose of the following vocabulary is therefore operational. A function makes ownership single-valued. A relation represents potentially many dependencies. An invariant restricts every permitted state. A partial order distinguishes causality from an arbitrary display order. A refinement states what an implementation must preserve when its representation changes. Standard treatments of sets, relations, induction, and state machines supply the basic background [36].
8.1 Sets, identities, functions, and relations
A set specifies which entities exist in a model. Identity is membership in the set of entities, not the entity’s display name or memory address. Two services called billing may belong to different tenants. Two running replicas can implement one logical service. A release can change an implementation without changing the operation it implements. These distinctions should be reflected in the identifier types before any graph algorithm is introduced. A function 𝑓 : 𝑋 → 𝑌 gives exactly one result for every member of 𝑋. The ownership function 𝑜 : 𝑃 → 𝑁 therefore says that each port has exactly one node owner. It does not say that a node has only one port, because several inputs to a function may map to the same output. An injective function maps different inputs to different outputs. An interface exposure map can be injective when each exposed entry names a distinct port. A relation 𝑅 ⊆ 𝑋 × 𝑌 can associate one entity with several others or none. Placement eligibility, test coverage, and data derivation are naturally relational. A chosen placement might subsequently become a function from a particular runtime instance to its execution domain. Eligibility and the chosen plan must not be confused: the former describes allowed alternatives, the latter a decision. For a finite example, let 𝑁 = {𝑢, 𝑠} be a user-interface component and a service. Let 𝑃 = {𝑐, ℎ} be their caller and handler ports, with 𝑜(𝑐) = 𝑢 and 𝑜(ℎ) = 𝑠. A connection between 𝑐 and ℎ is an entity with its own identity. Its request schema, cancellation behavior, and chosen transport are not additional owners of either port. A database table can store all four records centrally and still preserve these functions exactly.
8.2 Types distinguish legal objects from merely encodable objects
A storage system can encode a port connected to a source file or an authorization policy used as a network address. That does not make either relationship legal. A type schema states the permitted entity kinds, fields, relationships, and endpoint roles. A typed instance must satisfy that schema. At the simplest level, a type predicate can establish that an edge has one caller and one handler. A richer contract can state that the caller sends values the handler accepts. These are different obligations. Exact type identity is an easy sufficient compatibility rule, but versioned schemas often require a directional compatibility relation. For request/reply, the handler must accept the caller’s possible requests, while the caller must understand the handler’s possible results. A broad error union accepted by both parties may simplify evolution; silently replacing a result schema does not. Behavioral types add ordering information. A session that permits Open, then several Item messages, then Close cannot safely receive Item before Open. Session-type research formalizes communication sequences and role compatibility [37]. Reaktor’s initial standard profiles should use small explicit state machines. General multiparty protocol checking is an extension with its own assumptions, not an automatic consequence of a typed payload.
8.3 Partial orders, causality, and information growth
A partial order ⪯ is reflexive, antisymmetric, and transitive. Unlike a total order, it need not compare every pair. Two unrelated events in different services may be concurrent. Imposing an arbitrary sort order for a timeline is useful for display but does not establish causality. The same mathematical notion describes growing information. A partial graph fragment can contain fewer established facts than a larger fragment. Under an information order, acquiring more facts moves upward. It must not retroactively turn an unobserved event into a proven absence. In particular, the absence of a service call in sampled traces means only that the sample did not include it. Monotonicity means preserving an order: 𝑥 ⪯ 𝑦 implies 𝑓 (𝑥) ⪯ 𝑓 (𝑦). If a query only accumulates possible dependencies as new facts arrive, it is monotone with respect to set inclusion. A query for “components with no outgoing calls” is not: a later observation can invalidate an earlier result. This distinction affects caching, incremental proofs, distributed computation, and the permissions granted from incomplete knowledge. CALM relates monotonicity to coordination-free consistency under a particular distributed-computation model; it is not permission to ignore application invariants [38, 39].
8.4 Fixed points and closure
A fixed point of 𝑓 is a value 𝑥 for which 𝑓 (𝑥) = 𝑥. Many architecture analyses repeatedly add consequences until nothing changes. To determine a live-update region, begin with changed entities, add unmediated lifetime dependencies and mandatory co-update partners, and repeat. To determine the impact of a schema change, repeatedly follow the relationships selected by that analysis. Let 𝑉 be a finite entity set, 𝑆 ⊆ 𝑉 the initial selection, and 𝐷 ⊆ 𝑉 × 𝑉 the dependency relation for a particular closure. Define
𝐹 (𝑋) = 𝑆 ∪ 𝑋 ∪ {𝑣 | ∃𝑢 ∈ 𝑋 : (𝑢, 𝑣) ∈ 𝐷}. (2)
Starting at 𝑋0 = 𝑆 and setting 𝑋𝑖+1 = 𝐹 (𝑋𝑖 ) produces a growing sequence.
Proposition 8.1 (Finite closure). The sequence reaches a fixed point after at most |𝑉 \ 𝑆| strict expansions. Its limit is the least set containing 𝑆 and closed under 𝐷.
Proof. Each strict expansion adds at least one previously absent member of the finite set 𝑉. At termination,
every dependency successor is already included. Any other closed set containing 𝑆 contains 𝑋0 and,
inductively, every 𝑋𝑖 ; it therefore contains the limit. □
The proposition says nothing about whether 𝐷 is the correct dependency relation. A closure over imports alone can omit captured callbacks or shared state. The domain analysis must establish which relationships are required.
8.5 State machines, invariants, and traces
A transition system consists of possible states and permitted transitions. An execution is a sequence of
states connected by those transitions. An invariant 𝐼 holds in every reachable state. Induction gives the
usual proof pattern:
𝐼 (𝑥 0 ), 𝐼 (𝑥) ∧ 𝑁𝑒𝑥𝑡 (𝑥, 𝑥 ′ ) ⇒ 𝐼 (𝑥 ′ ). (3)
The first condition establishes the invariant initially. The second establishes that every allowed step
preserves it. Checking only the successful path is insufficient when failure, cancellation, retry, or
concurrent mutation is also allowed.
A trace records observable actions, possibly hiding internal transitions. A caller may observe that
its request was accepted and later receive a result without seeing a serializer allocation or a routing-
table lookup. This distinction allows an optimized implementation to differ internally from a simple
specification. A trace-refinement claim restricts observable behavior; additional arguments are needed for progress when an implementation could perform internal actions forever [40, 41].
8.6 Compositional reasoning and its limits
The attraction of modules is that a large proof should not require reopening every implementation detail. An assume–guarantee contract states that a component provides guarantee 𝐺 when its environment satisfies assumption 𝐴. Composition must show that the surrounding components really establish 𝐴. For example, a consumer may guarantee bounded memory if the producer honors a credit protocol. The producer’s guarantee must refer to the same credit ownership and message-loss assumptions. If both sides merely assume the other eventually acts, neither has established progress. Cyclic assumptions need a justified temporal argument, not a diagram in which the arrows happen to form a cycle. Category-theoretic composition makes interfaces and combinations mathematically explicit. A category supplies objects, composable arrows, identities, and associativity. In an open-system interpretation, objects describe boundaries and arrows describe systems exposing those boundaries. A symmetric monoidal structure additionally represents placing systems side by side. These laws justify rearranging a composition expression without changing its meaning, provided the selected formal construction actually has those laws [42, 43]. Reaktor need not expose categorical terminology in application APIs. The practical consequence is that module nesting, flattening, and wiring must agree on a defined boundary semantics. An identity adapter must not introduce a hidden policy change. A compiler that fuses two modules must preserve the effects visible outside their combined boundary.
8.7 Mathematics as an engineering interface
The value of these concepts is visible in implementation decisions. Total ownership functions become non-null owner references plus validation. Incidence occurrences become explicit records. Fixed-point analyses become worklists. Partial orders become causal or revision tokens. Invariants become admission checks and proof obligations. Refinements become contracts between source IR, storage, generated code, and runtime adapters. The correspondence is not automatic. A Kotlin type declaration may describe a property that a deserializer can violate. A graph validator may omit a mutation path. A proof may reason about unbounded integers while runtime counters wrap. Each representation boundary therefore needs a stated mapping and either a proof, a check, or an acknowledged trust assumption. Formal structure improves engineering precisely because it exposes these obligations.
Original page layout, starting at page 20
9. The graph-theoretic model
9.1 Typed incidence structure
Definition 9.1 (Port multihypergraph). At a fixed revision, the structural model is
𝐻 = (𝑁, 𝑃, 𝐸, 𝐽, 𝑜, 𝑎, 𝑏, 𝑟, 𝜏, 𝐹), (4)
where 𝑁, 𝑃, 𝐸, and 𝐽 are disjoint finite sets of nodes, ports, edges, and incidence occurrences. The total
functions
𝑜 : 𝑃 → 𝑁, 𝑎 : 𝐽 → 𝐸, 𝑏:𝐽→𝑃 (5)
give port ownership and incidence attachment. The map 𝑟 : 𝐽 → Roles assigns incidence roles. The
family 𝜏 assigns node, endpoint, and edge types. The family 𝐹 contains schema-checked attributes.
For 𝑥 ∈ 𝐸, let 𝐽 𝑥 = { 𝑗 ∈ 𝐽 | 𝑎( 𝑗) = 𝑥}. A binary edge has |𝐽 𝑥 | = 2; a hyperedge may have any arity admitted by its type. Edge identity is independent of its endpoints, so parallel edges remain distinct. Incidence occurrences preserve repeated positions and separately configured memberships; replacing 𝐽 𝑥 with an unlabeled set of ports would lose this information. Ports are semantically owned by nodes:
∀𝑝 ∈ 𝑃, ∃!𝑛 ∈ 𝑁 : 𝑜( 𝑝) = 𝑛. (6)
Central storage of port records does not alter this ownership relation. A graph is the container and authority for a revision; a node remains the owner of its interface. Attributed hierarchical port graphs provide a precedent for nested port structure and rewriting [44]. Annotated hypergraphs provide a precedent for roles in multi-party relations [45]. The present construction adds software-specific typing and interpretation; theorems about either precedent require an explicit encoding before they apply.
9.2 Typing and structural validity
A type schema specifies admissible node kinds, endpoint signatures, protocol roles, edge profiles, and attribute domains. Every incidence must be compatible with both its endpoint type and its edge role. Distinct occurrences can refine a generic endpoint role into named participants, such as a coordinator, an input position, or a subscription membership. Let Valid𝑠 (𝐻) denote structural validity. It includes total ownership, referential integrity, type compatibility, role constraints, cardinality constraints, unique identities, and module-boundary rules. It does not imply arbitrary business correctness. A cyclic dependency is not globally forbidden: feedback, recursion, and stateful communication can be legitimate. Particular dialects may require acyclicity or an explicit delay on cycles.
9.3 Protocols determine direction and enablement
An edge is structural. Its interaction profile supplies an interpretation
𝜂(𝑥) = (Π 𝑥 , 𝜒𝑥 , 𝛿 𝑥 , 𝜅 𝑥 ), (7)
where Π 𝑥 is a protocol, 𝜒𝑥 coordination behavior, 𝛿 𝑥 delivery and buffering behavior, and 𝜅 𝑥 a set of requirements. The implementation may intern this descriptor; the notation does not require a separate runtime object per field. For lane ℓ of an edge protocol, derive source and destination incidence sets 𝑇𝑥,ℓ , 𝐻 𝑥,ℓ ⊆ 𝐽 𝑥 . A request/reply edge has caller-to-handler request traffic and handler-to-caller outcomes. Cancellation and demand can have additional directions. Dependency orientation is a separate projection. A hyperedge does not imply that every participant must be ready simultaneously. A broadcast, an anycast operation, and an AND-join can share an incidence shape while having different enablement rules. Directed-hypergraph algorithms therefore require the relevant path and enablement semantics [46]. An ordinary breadth-first traversal of an incidence projection establishes structural adjacency, not protocol progress or the feasibility of a join.
9.4 Incidence encoding and representation correctness
Proposition 9.2 (Lossless incidence encoding). A finite port multihypergraph has a lossless typed-graph encoding with 𝑂 (|𝑁 | + |𝑃| + |𝐸 | + |𝐽 |) structural records, plus the storage for encoded identities, types, and attribute payloads, provided incidence occurrences, ownership, and roles are retained.
Proof. Create typed vertices for the elements of 𝑁, 𝑃, 𝐸, and 𝐽. Encode 𝑜 as one labeled ownership
arc per port. Encode 𝑎 and 𝑏 as two labeled arcs per incidence, and store 𝑟, 𝜏, and 𝐹 as typed labels or
attribute records. The four vertex sorts and the functional arcs uniquely recover the original sets and
maps. Decoding therefore recovers 𝐻 up to an identity-preserving isomorphism. The number of structural
records and arcs is linear in the four set sizes; variable-length metadata contributes its own encoded
size. □
This encoding permits conventional graph tools without treating an edge as a software component. A specialized storage layout may omit explicit incidence vertices for binary edges if its decoder reconstructs them without ambiguity. Correctness requires
decode(encode(𝐻)) 𝐻, (8)
not equality of physical row order or object addresses.
9.5 Hierarchy and exposed interfaces
Definition 9.3 (Open module). An open module is 𝑀 = (𝐻, 𝐵, 𝛽), where 𝐵 is a finite set of named boundary endpoints and 𝛽 : 𝐵 ↩→ 𝑃 is an injective map selecting exposed owned ports. Multiple public names for one endpoint are represented as aliases, rather than separate boundary incidences.
A hierarchical module associates an internal graph with a composite node in its parent scope. The composite node owns its façade ports. An explicit boundary map relates those ports to internal endpoints. No port acquires two owners. Flattening preserves identities or supplies a total provenance map from flattened entities to hierarchical origins. Composition takes disjoint module interiors and adds typed boundary connections. It does not identify two ports with different owners as a single port. Open-graph composition and rewriting provide relevant foundations [43, 42]; exact categorical constructions depend on the chosen boundary and type encoding.
Proposition 9.4 (Ownership-preserving composition). Let two structurally valid modules have disjoint entity identities. If a composition adds only well-typed edges and incidences on permitted boundary endpoints, preserves all endpoint cardinality bounds, and does not change ownership, then total unique port ownership and the stated local structural constraints are preserved.
Proof. The disjoint union preserves each module’s ownership function without identifying its domain or
codomain elements. Added incidences reference existing ports and new edges, so referential integrity
follows from their construction. The assumptions discharge typing, cardinality, and boundary obligations
for the new records; existing records are unchanged. □
The proposition does not establish global security, deadlock freedom, or resource sufficiency. Such properties need additional composition rules or a check of the composed system.
9.6 Behavioral interpretation
The execution interpretation of a graph is a labeled transition system
⟦𝐻⟧ = (𝑋, 𝑋0 , A, −→), (9)
whose state includes component state, buffers, active calls, sessions, ownership epochs, and the se-lected topology revision. Node and edge profiles contribute transitions. Local actions interleave with communication and environmental actions; this semantics does not prescribe a single-threaded implementation.
A transition can send, admit, deliver, acknowledge, reject, crash, recover, or apply an authorized change. Internal actions may be hidden when comparing boundary behavior. I/O automata offer a suitable reference for composition, external actions, and implementation relationships [40]. Fairness, failure, and clock assumptions must be specified separately from connectivity.
Original page layout, starting at page 22
10. Network views, sparse algebra, and architectural analysis
The port hypergraph is the structural authority for executable connectivity. Many analyses require a simpler derived graph, but the projection must state what it preserves and what it discards. A graph of possible calls differs from a graph of deployments, a graph of actual invocations, and a graph of data derivations. Combining them indiscriminately produces answers that are computationally precise but semantically wrong.
10.1 A worked incidence example
Consider one publication with a sender port 𝑝 0 and two subscriber ports 𝑝 1 , 𝑝 2 . Let 𝑒 0 be the publication hyperedge and let three incidence occurrences associate those ports with their roles. For the message lane, define a tail-incidence matrix 𝑇 ∈ {0, 1} | 𝑃 | × |𝐸 | and a head-incidence matrix 𝐷 of the same shape:
1 0
𝑇 = 0 , 𝐷 = 1 . (10)
0 1
Over the Boolean semiring, 𝐴 = 𝑇 𝐷 T is the possible sender-to-receiver adjacency matrix:
0 1 1
𝐴 = 0 0 0 . (11)
0 0 0
Boolean addition means logical OR and Boolean multiplication means logical AND. Thus 𝐴𝑖 𝑗 is true
if there exists a selected hyperedge permitting the projected relationship from 𝑝 𝑖 to 𝑝 𝑗 . GraphBLAS
standardizes related sparse-algebra building blocks for graph algorithms [47].
This matrix loses edge identity, individual subscription metadata, repeated incidences, and enablement
rules. Two independent publications could yield the same 𝐴. A collective join requiring all inputs could
have the same possible-flow projection as a relationship allowing any one input to act. The matrix is
useful for possible-flow reachability, not as a replacement for the original semantics.
Do not materialize a dense |𝑃| × |𝑃| matrix for routine operation. Sparse incidence indexes can traverse
the same relationship directly. Matrix notation describes an analysis; it does not dictate storage or require
a GPU.
10.2 Reachability, strongly connected components, and domination
For a selected binary projection, reachability asks whether a path exists. Strongly connected components identify maximal groups in which every vertex can reach every other. They are useful for detecting cycles in dependencies or finding mutually dependent modules. A cycle is not necessarily a bug: event loops, controllers, and conversational protocols intentionally contain feedback. A cycle violates an invariant only in a dialect that requires acyclicity, or when its behavioral semantics make it erroneous. A vertex 𝑑 dominates 𝑣 relative to an entry 𝑠 when every path from 𝑠 to 𝑣 passes through 𝑑. A synthetic super-entry can collect several allowed ingress points. This supports a structural check for bypasses around an enforcement point. However, the graph must include all relevant execution paths, and the
enforcing operation must perform the required check on the correct authenticated request and resource. Dominance in a dependency graph is not evidence of execution dominance. An analysis result should therefore carry both a finding and a scope claim: which entries, edge kinds, code regions, and foreign systems were included; which transfer summaries were trusted; and where unknown edges remain. An unmodeled reflection or native callback can prevent a universal claim even when the visible graph has no bypass. Classical graph algorithms remain valuable without overstating their scope [48, 46].
10.3 Hypergraph-aware enablement
Suppose a workflow step needs both a payment authorization and an inventory reservation. The condition
is conjunctive. Reaching one input does not enable the step. Let 𝑅(𝑥) be the set of required input roles for
transition 𝑥, and 𝑎𝑣𝑎𝑖𝑙𝑎𝑏𝑙𝑒(𝑟) the corresponding token predicate. Then
Û
𝐸𝑛𝑎𝑏𝑙𝑒𝑑 (𝑥) = 𝑎𝑣𝑎𝑖𝑙𝑎𝑏𝑙𝑒(𝑟) (12)
𝑟 ∈𝑅(𝑥)
expresses the relevant join condition. A competing queue instead chooses one eligible receiver for an attempt; a publication creates obligations for each eligible subscription. These operations can share incidence storage while requiring different interpreters. For diagnosis, the workbench can display why a collective transition is disabled: missing reservation, expired authorization, incompatible revision, or exhausted admission credit. A single “unreachable” color discards the causal explanation. Protocol-specific explanation is more useful to both a developer and an agent than a generic topology warning.
10.4 Weighted networks and cost models
Weights can represent bytes, measured latency, expected call frequency, resource cost, or a declared
engineering penalty. Their units and interpretation matter. A latency weight is not an authorization
condition. A measured average is not a worst-case bound. A path’s costs add only when the modeled
stages actually execute serially under the chosen interpretation.
For a placement 𝜋 and hyperedge 𝑒, a simple communication surrogate is
∑︁
𝐶𝑐𝑜𝑚𝑚 (𝜋) = 𝑤 𝑒 max(0, |{𝜋(𝑜(𝑏( 𝑗))) | 𝑎( 𝑗) = 𝑒}| − 1) . (13)
𝑒∈𝐸
This counts extra occupied domains and weights them by a selected estimate. It is not an exact network bill: traffic volume, replication, routing, and compression can change the real cost. It can nevertheless rank candidate placements when used transparently and validated against observations. Optimization must obey hard constraints first. A low-latency plan that co-locates every replica in one failure domain may violate availability requirements. A cheaper route may cross a forbidden trust boundary. The result is constrained multi-objective optimization, usually solved with heuristics or bounded optimization rather than a claim of universal optimality. The planner should report its objective, constraints, feasible alternatives, and evidence quality.
10.5 Spectral methods: useful projections, limited meaning
For an explicitly chosen undirected weighted projection, let 𝑊 be symmetric with nonnegative weights,
𝐷 𝑊 its diagonal degree matrix, and 𝐿 = 𝐷 𝑊 − 𝑊 its Laplacian. For a real-valued assignment 𝑧 to
vertices,
1 ∑︁
𝑧 T 𝐿𝑧 = 𝑊𝑖 𝑗 (𝑧 𝑖 − 𝑧 𝑗 ) 2 . (14)
2 𝑖, 𝑗
The identity follows by expanding the square and using symmetry. It measures disagreement across heavily weighted neighboring vertices. Spectral embeddings can therefore help suggest clusters or layouts. The vector space here is the space of numerical vertex assignments, not the set of software systems [49]. Symmetrization can discard direction, roles, and the distinction between an AND-join and an OR-choice. A spectral cluster may be visually coherent but unsuitable as a security, deployment, or update boundary. Reaktor should treat spectral partitioning and embeddings as proposal generators, followed by semantic validation.
10.6 Views are queries with obligations
A projection should specify its entity scope, selected relations, direction, time/revision context, abstraction rules, and completeness requirements. Some views preserve identity; others aggregate several entities into one summary. Aggregated views need a drill-down mapping so that a diagnostic or proposed mutation can be traced back to actual entities. The editor can collapse a service and show one aggregate edge while retaining operation-level identities in the underlying query result. An agent can request only the state and contracts relevant to a feature. A verifier can demand a closed-world projection of all paths to a protected effect. These uses share the graph model but differ in their admissible omissions. A layout omission is acceptable for readability; a verification omission must be justified.
Original page layout, starting at page 25
11. Ports, contracts, and shared service interfaces
11.1 Two dimensions of an endpoint
An endpoint combines a signature with a protocol shape. Its role selects the endpoint’s perspective:
EndpointType = Signature × Protocol × Role. (15)
The signature describes exchanged schemas. The protocol describes permitted sequences, completion, errors, cancellation, and demand. A role may be a caller, handler, producer, consumer, authority, observer, or a named session participant. Well-formed endpoint types form the admissible subset of this product. Role compatibility is checked against the edge profile rather than inferred from a universal input/output arrow.
Profile Endpoint roles Required interpretation
Reference<T> Requires / provides Access to an interface with declared identity, lifetime, and locality.
Value<T> Source / sink A value dependency with evaluation and purity rules.
Call<Q,R,E> Caller / handler A finite request with a typed domain outcome and explicit
infrastructure failures.
Message<M> Sender / receiver One-way business delivery; admission acknowledgement is distinct
from completed processing.
Stream<T> Producer / consumer A sequence with ordering scope, demand, termination, and
cancellation.
State<S> Authority / observer A revisioned snapshot and a defined transition to subsequent
changes.
Session<Π> Protocol-defined A long-lived conversation following protocol Π.
Table 7: Standard profiles. Profiles share the same port and incidence representation; they are not distinct graph storage engines.
These profiles are extensible, but an extension must declare its structural checks, behavior, adapter requirements, and available analyses. An unknown profile may remain visible as opaque structure. It cannot silently become executable or verified. A value is not automatically a call returning a value. That lowering is valid only if evaluation, purity, failures, and lifetime are preserved. Similarly, state observation is not merely a stream: snapshot acquisition and subscription must specify whether an intervening update can be missed, which revision the snapshot represents, and how observers recover from gaps.
11.2 Language-neutral contract identity
A contract has a stable nominal identity and an immutable revision, with request, result, error, item, or frame schemas as appropriate. A compatibility relation is separate from both nominal identity and semantic-version notation. Matching major versions is a release policy, not a proof of behavioral compatibility. The wire model specifies integer ranges, nullable versus absent values, field identifiers, unknown variants, time representations, and encoding constraints. Runtime registries associate schema references with Kotlin serializers, native codecs, and foreign-language bindings. An application class name, serializer instance, HTTP path, or deployment address is not the canonical identity. For a call, the handler must accept the requests the caller can issue, and the caller must understand the outcomes the handler can produce. Schema variance is only one part of that condition. Changed authorization requirements, strengthened preconditions, altered cancellation behavior, or different error meanings can be incompatible even when the payload schema is unchanged.
11.3 Cardinality and collective operations
Binding cardinality counts a port’s logical connections. Edge arity counts incidence occurrences. Routing cardinality counts selected recipients for one invocation. Execution cardinality limits simultaneous work. These quantities are independent: one logical service binding can select one of many replicas while admitting many concurrent calls. Coordination profiles include point-to-point, anycast, broadcast, keyed routing, gather, and quorum. Partitioning does not itself define ordering or exclusive ownership. A scatter/gather call must expose an aggregate outcome, such as a keyed collection or a quorum result; it cannot retain an ordinary single-result contract while discarding outcomes implicitly. A one-way message profile can require a durable-admission receipt without claiming that its business effect has completed.
11.4 Shared API authoring
A shared service interface remains the agreement between clients, implementations, tests, and source-navigation tools. Its members describe logical operations rather than transport-specific handler classes. The following syntax is illustrative of the proposed API:
@GraphService("bestbuds.messaging")
interface MessagingApi {
@Operation("message.send")
val send: Call<SendMessage, ChatMessage, SendError>
@Operation("message.watch")
val watch: ServerStream<WatchMessages, MessageEvent, WatchError>
}
class MessagingServer(
graph: Graph,
private val repository: MessageRepository,
) : ServiceNode(graph), MessagingApi {
override val send by handles(MessagingApi::send) { request, context ->
repository.send(request, context)
}
override val watch by handles(MessagingApi::watch) { request, context ->
repository.watch(request, context)
}
}
class ChatInteractor(graph: Graph) : Node(graph) {
val sendMessage by api(MessagingApi::send)
}
A generated client and a test implementation implement the same interface. Abstract API classes remain a valid alternative. A whole-service handle corresponds to a bundle of caller ports owned by the consuming node. Member references retain source navigation and establish operation identity without duplicating a second hand-authored registry. Elaboration generates descriptors for the signature, protocol, caller and handler endpoints, source locations, and optional exposure metadata. HTTP mounting, Worker bindings, local dispatch, and FFI are realizations of the operation. The current transport-dependent ServiceEndpoint.portType and handler-backed ServiceNode are implementation seams for this separation [9]. The service contract layer is part of the graph architecture even when maintained in a separate package or build module. A common interface establishes agreement within its compilation boundary. Deployed older clients and foreign-language services still require manifest-based compatibility checks and conformance tests. Server-side validation remains mandatory for requests received from untrusted callers.
11.5 Context, effects, and failure
Business payloads are separate from invocation context. Context contains authenticated identity, authorization scope, tracing, deadlines, cancellation, and consistency tokens under explicit propagation rules. Client-supplied metadata is not an authenticated principal. Local realizations retain applicable enforcement rather than bypassing it when a network hop disappears. Domain rejection is distinct from invalid payloads, authorization failure, unavailability, cancellation, deadline expiry, and an unknown outcome. A timeout can leave a remote operation committed. Repeated invocation therefore requires an explicit idempotency contract or a caller-visible possibility of repeated effects. A raw local reference is not automatically remotely realizable. Object identity, mutable aliases, captured state, and lifetime can be essential to its meaning. A placement change must choose a supported proxy contract or fail. Effects summarized by an interface remain declared assumptions until established by implementation analysis, encapsulation, or conformance evidence.
Original page layout, starting at page 27
12. Interface contracts and implementation architecture
The architecture requires a small number of stable interfaces between authoring, analysis, storage, execution, and external providers. This section specifies those boundaries more concretely. The Kotlin fragments are interface sketches: supporting identifiers and descriptor types are opaque versioned values, and omitted implementations are not implied to exist. They are not a release-ready library or a claim of compiled conformance.
12.1 Identity, revision, and schema directories
Logical identity answers which entity; a revision answers which immutable description; a runtime handle answers which currently bound implementation. Keeping these questions separate avoids invalidating architecture references on every process restart and prevents a local array index from becoming a permanent external name. An entity identifier includes or resolves within an authority namespace. A descriptor reference identifies an immutable revision by content or registry revision. A runtime handle includes the registry/generation necessary to interpret its slot. Boundary APIs use stable identifiers; the compiler interns them into compact local indexes after validation.
data class DescriptorRef(
val authority: AuthorityId,
val identity: DescriptorId,
val revision: ContentHash,
)
data class EndpointTypeDescriptor(
val signature: DescriptorRef,
val protocol: DescriptorRef,
val role: RoleId,
)
interface ContractRegistry {
suspend fun resolve(ref: DescriptorRef): ContractDescriptor
suspend fun compare(
required: DescriptorRef,
offered: DescriptorRef,
environment: CompatibilityContext,
): CompatibilityResult
}
CompatibilityResult distinguishes compatible, incompatible with a counterexample, and unknown. It can include an explicit adapter requirement. The registry must not silently identify two nominal contracts merely because their serialized fields currently look similar. Conversely, schema-compatible revisions can remain distinct identities for auditing and release analysis. Wire schemas should support a portable core of products, sums, optional fields, bounded integers, strings, byte sequences, collections, and declared domain refinements. A field’s absent value is distinct from an explicit null when the protocol distinguishes them. Numeric units, coordinate frames, and effect semantics are additional typed metadata or refinements, not arbitrary comments. An implementation can use richer language types internally and lower them to this core at a boundary.
12.2 Graph readers expose snapshots, not mutable internals
A graph reader resolves entity records at one selected semantic revision. It offers indexes and cursors rather than requiring clients to download a complete graph. Query results retain evidence and completeness information.
interface GraphReader {
suspend fun snapshot(ref: RevisionRef): SnapshotHandle
suspend fun query(
snapshot: SnapshotHandle,
query: GraphQuery,
access: ReadAuthority,
): QueryPage
suspend fun explain(finding: FindingRef): Explanation
}
data class QueryPage(
val revision: RevisionRef,
val records: List<EntityRecord>,
val next: QueryCursor?,
val completeness: CoverageClaim,
val evidence: List<EvidenceRef>,
)
A cursor is bound to the query, revision, and access scope. Continuing it after arbitrary mutation must either retain the referenced snapshot or return a clear stale-cursor result. A federated result can carry several source watermarks; its envelope must not misrepresent them as a simultaneous snapshot of all systems. CoverageClaim is more precise than a confidence number. It can state that all declared ports in a module were returned, that a source scanner covered specific files, or that a service map contains sampled observations from a time interval. An agent cannot infer the absence of an unobserved dependency from any of those claims unless the relevant closed-world condition is established.
12.3 Selectors, traversals, visitors, and passes
The graph’s extensibility depends on a concrete interpretation mechanism. The visitor design separates four responsibilities: a selector chooses the relationships in a view; a traversal determines visit order; a visitor produces a typed result; and a pass packages those choices with dependencies and diagnostics [28]. This separation lets routing, wiring, authorization coverage, context export, and deployment analysis reuse the same structural substrate. A selected arc carries its meaning: containment, incidence with a role, route attachment, data lineage, or another declared relation. Returning only a neighboring entity would lose information needed to interpret a port hypergraph. Traversal context identifies the current entity, incoming relation, scope path, and source revision. A path through an exposed module boundary must not be confused with arbitrary permission to inspect its private implementation.
interface Visitor<R> {
fun enter(context: VisitContext): VisitDecision
fun leave(context: VisitContext) {}
fun result(): R
}
interface GraphPass<R> {
val key: PassKey<R>
val dependsOn: List<PassKey<*>>
val selector: Selector
val traversal: Traversal
fun visitor(context: PassContext): Visitor<R>
}
The types above describe the semantic API. A hot traversal can operate over primitive-index cursors and reuse context storage rather than allocate rich wrappers for every arc. DFS, BFS, post-order traversal, and
topological order have different contracts. Topological traversal requires an appropriate acyclic projection; it is not valid merely because the containing application is called a graph. A route-index pass can produce a RouteIndex; a deep-link planner consumes it; an auth-coverage pass produces findings for the same route surface; an installation plan then connects permitted ingress adapters. Similarly, wiring produces a binding report and proposed patch rather than mutating ports during a read-only walk. A pass that installs a runtime subscription returns a lifecycle-owned installation operation, not an untracked side effect. Pass dependencies form a separate analysis graph. Its nodes are analyses, not application components. Cached results identify the snapshot, descriptor versions, query dependencies, and policy scope on which they depend. Invalidation must include predicate dependencies: adding an ingress can invalidate a finding about all paths without modifying any previously visited entity. Reactive passes consume an explicit event stream and close with their owner scope. Stable traversal ordering makes fixed-snapshot results reproducible; it does not make arbitrary remote effects or concurrently observed executions deterministic. The benefit is practical: adding a new semantic aspect need not add branches to every node class or create another source of topology. A module contributes its vocabulary and passes, while the engine supplies the shared indexing, lifecycle, diagnostics, and change protocol.
12.4 Graph patches are transactions over a semantic revision
A patch contains operations such as adding nodes, ports, edges and incidences; changing attributes or descriptor references; and replacing a module region. It includes an expected base and preconditions. Derived records are recomputed or invalidated by the owning subsystem rather than directly overwritten by arbitrary clients.
data class PatchProposal(
val id: ProposalId,
val expectedBase: RevisionRef,
val operations: List<GraphOperation>,
val preconditions: List<PredicateRef>,
val sourceDelta: SourcePatchRef?,
val provenance: ProvenanceRef,
)
interface GraphWriter {
suspend fun prepare(
proposal: PatchProposal,
authority: ChangeAuthority,
): PreparedChange
suspend fun commit(
prepared: PreparedChangeRef,
approval: ApprovalRef,
): CommitResult
}
Preparation checks authorization, resolves immutable descriptors, constructs a candidate, validates its structural invariants, computes impacted obligations, and produces a reviewable result. Preparation is not a reservation of the current revision forever. Commit rechecks the expected base or revalidates the relevant read dependencies under a sound concurrency protocol. A minimal correctness-first implementation serializes expected-base validation and publication. More concurrency can be introduced through optimistic validation, but it must handle predicate dependencies. A proof that “no alternative ingress exists” depends on possible new edges, not only records that were read. Two disjoint row updates can therefore conflict semantically. Any automatic rebase must produce a newly validated candidate, not simply replay writes after an unnoticed base change.
Source-backed changes have an additional round trip. The authoring adapter produces a source patch; elaboration of the edited source produces a semantic delta; the system checks that this delta matches the approved intent within a declared equivalence. Unsupported source edits remain ordinary source changes requiring review. The graph is not authorized to overwrite unowned source regions to force a round trip.
12.5 Protocol registries and semantic extension packages
A protocol profile describes role signatures, legal state transitions, coordination rules, cancellation, completion, and required environmental capabilities. A realization provider states which profiles it implements and under what conditions.
interface ProtocolModule {
val descriptor: ProtocolDescriptor
fun validate(edge: EdgeView): List<Finding>
fun obligations(edge: EdgeView): List<PropertyObligation>
fun behavior(edge: EdgeView): BehaviorModelRef?
}
interface RealizationProvider {
val descriptor: ProviderDescriptor
fun supports(request: RealizationRequest): SupportResult
suspend fun lower(request: RealizationRequest): LoweredRegion
}
A profile must not obtain execution authority by loading a validator plugin. Validators themselves are tooling code with a trust and resource scope. Untrusted validation extensions can run in constrained processes, and their output can be advisory unless the project explicitly adopts them into its assurance boundary. Standard modules can provide direct references, unary calls, request/response streams, publication, competing work delivery, state subscriptions, actor protocols, and sessions. Less common coordination rules remain possible through versioned modules. The kernel stores the references and preserves their invariants; it does not acquire a branch for every broker product or UI framework.
12.6 Execution handles and invocation context
A compiled call endpoint resolves to a binding whose contract is already checked. The invocation carries
runtime context separately from its business payload. A generated client preserves the shared service
interface from Section 11; it does not require callers to manually construct graph commands for routine
execution.
data class InvocationContext(
val invocation: InvocationId,
val authenticatedSubject: SubjectRef,
val authority: InvocationAuthority,
val deadline: Deadline?,
val trace: TraceContext,
val consistency: ConsistencyRequirement?,
val executionView: ExecutionViewRef,
)
interface BoundCall<Q, R, E> {
suspend fun invoke(
request: Q,
context: InvocationContext,
): CallOutcome<R, E>
}
The trusted runtime constructs authenticated context from appropriate credentials and local authority. A client-provided subject field is merely input until validated. CallOutcome separates domain results from transport/infrastructure outcomes, including uncertainty about commitment. A cancellation request is not necessarily proof that execution stopped. The production ABI need not allocate this entire record for every local call. Generated bindings can use an existing scope object, direct references, or compact fields. The semantic requirement is that the relevant context is available and enforced, not that every execution passes a large generic map.
12.7 Streams and state subscriptions
A stream binding returns a scoped subscription with explicit request/cancel or another declared demand protocol. It identifies sequence scope, gap detection, terminal outcomes, and ownership of buffered frames. A receiver that cannot keep up can suspend admission, drop under a declared lossy profile, or fail the subscription; these are not interchangeable behaviors. A state subscription additionally needs a no-gap handoff from its snapshot. One valid implementation establishes a subscription at revision 𝑣, captures the corresponding snapshot, and then delivers changes after 𝑣 from a retained log. Another uses a transactional snapshot and cursor. Both must define what happens if the cursor expires during initialization.
data class StateStart<S>(
val snapshot: S,
val revision: StateRevision,
val changes: ChangeSubscription,
)
interface StateEndpoint<S> {
suspend fun start(
request: StateObservationRequest,
context: InvocationContext,
): StateStart<S>
}
The returned state is an immutable value or controlled view, not a reference that lets an observer mutate the authority’s internal object. A merged replicated state may use a causal frontier rather than one scalar revision. The chosen profile defines the revision algebra.
12.8 Lifecycle ownership
A runtime component progresses through preparation, binding, activation, draining, stopping, and retirement according to its profile. Lifecycle hooks have different permissions. A prepared candidate may resolve contracts and allocate resources without accepting production traffic. An active component may create timers and subscriptions within its owner scope. Draining prevents new admission but does not automatically cancel work whose contract requires completion. Closing a scope cancels or transfers its owned resources according to policy. A callback to a retired generation must be rejected or dispatched to a still-pinned valid generation. These obligations apply to native objects, Hermes functions, file handles, database subscriptions, and UI event handlers alike. A common lifecycle vocabulary is useful; a single universal cleanup implementation is not.
12.9 Compilation outputs and diagnostics
Compilation should return a coherent plan and source-linked findings, not only generated files. A lowered region maps each relevant logical entity to implementation bindings, artifacts, codecs, and resources. It
records the rule and version used to lower the region so that later evidence can be invalidated when that rule changes. A failed lowering can report that an operation requires lossless delivery but the selected adapter only supports a lossy profile, or that a borrowed native buffer cannot cross an asynchronous boundary. An ambiguous service binding should identify the competing providers. Such findings are useful even when no formal verifier is enabled. The central interface discipline is stable meaning with replaceable representation. Public application APIs remain small. The descriptor and provider interfaces carry the richer contracts required by compilers, tools, and proofs. The runtime specializes them into the narrow mechanisms needed at each execution boundary.
Original page layout, starting at page 30
13. Hyperedges, modules, and graph rewriting
13.1 Native hyperedges and reified components
Native hyperedges represent multi-party relationships directly. Their identity can carry policies, prove-nance, deployment mappings, and observations. Incidence metadata can represent distinct subscription filters, participant positions, or per-membership requirements. Representational reification, as in Proposition 9.2, is a storage or analysis encoding. Semantic reification introduces an actual component. A queue with durable state, administration ports, lifecycle, and an independently meaningful identity can be a node in the logical model. A publication relationship can remain a hyperedge even when its physical realization contains broker topics and subscriptions. These representations describe different abstractions rather than competing truths. Í Let 𝐾 = 𝑥 ∈𝐸 |𝐽 𝑥 |. Native edge records plus incidence records require 𝑂 (|𝐸 | + 𝐾) connectivity storage. An incidence/star encoding also requires linear storage. Neither representation is inherently faster; compact versions can compile to the same arrays. A directed clique expansion can instead Í require 𝑂 ( 𝑥 |𝑇𝑥 ||𝐻 𝑥 |) pairwise arcs and discard collective identity. It is a derived view, not the default representation. Delivering an event to 𝑘 receivers still requires the corresponding physical delivery work.
13.2 Declarative graph patches
A patch is a revision-relative value containing operations, preconditions, and provenance. Structural operations add or remove nodes, ports, edges, incidences, attributes, and semantic relations. A patch may also modify exposed interfaces, provided all affected boundary obligations are checked. Constructors do not publish architectural mutations as incidental side effects. Patch admission checks permissions separately from validity. The resulting candidate graph is validated against the current authority revision. Events are emitted after successful publication. A failed validation leaves the previous revision intact. Runtime preparation must not perform irreversible external effects before the corresponding operation plan has been authorized. Algebraic graph transformation supplies a vocabulary for matches, preserved interfaces, application conditions, and dangling references [50]. Reaktor patches can be encoded as typed incidence-graph rewrites. This does not establish confluence or behavioral preservation for arbitrary patch sequences; those are separate properties. Lemma 13.1 (Structural patch safety). Assume an initial graph satisfies Valid𝑠 . Suppose every commit checks its expected base revision, validates the entire candidate against that revision, and publishes the candidate at one serialized commit point. Rejected candidates do not mutate the published graph. Then every published graph satisfies Valid𝑠 .
Proof. The initial revision is valid by assumption. For an accepted next revision, the serialized base check prevents publication of a candidate validated against a different head. Candidate validation establishes
Valid𝑠 before publication. Rejection preserves the induction hypothesis. Induction over successful
commits proves the claim. □
The lemma specifies an implementation obligation. It does not prove that a particular validator is sound, that a storage implementation commits atomically, or that external deployments are transactional.
13.3 Concurrent editing
Concurrent proposals carry source and semantic read sets, write sets, and expected revisions. Disjoint entity writes may still conflict through global constraints, such as uniqueness or the absence of a forbidden path. A merged proposal is revalidated. For scalable editing, independent scopes may commit separately when their composition rules justify that independence. Conflict-free replication of editor state can support convergence of suitable data, but convergence alone does not preserve arbitrary architectural invariants. Invariant-confluence analysis provides a relevant criterion for identifying operations that can avoid coordination under stated merge semantics [39]. Security policy, ownership transfer, and protected release publication use explicitly coordinated authority where required.
Original page layout, starting at page 35
14. Computational semantics and flow-based programming
A graph is a representation of relationships. A program additionally defines how state changes, how values are produced, when operations are enabled, and which effects become visible. Turing completeness is a property of that executable interpretation, not of drawing nodes and arrows. Reaktor should support several computational dialects over the same structural substrate rather than make every connection obey one universal scheduling rule.
14.1 A hierarchy of executable dialects
The simplest dialect contains pure expressions and value dependencies. An expression can run once its arguments are available. When the dependency graph is acyclic, a topological ordering provides an evaluation order. Independent pure expressions can be reordered without altering a result under the specified numerical semantics. Floating-point reassociation, exception behavior, and observable resource use require separate care; mathematical equality over real numbers is not automatically equality of machine computations. An effectful dialect adds explicit sequencing, branches, loops, resource acquisition, and cancellation. A stateful dialect introduces owned state and message handling. A durable dialect adds persisted decisions, checkpoints, retryable activities, and recovery. A real-time dialect adds timing, resource, and scheduling constraints. Each dialect declares which analyses and transformations are valid. A dataflow fusion pass should not cross an externally observable transaction boundary merely because two operations are adjacent. MLIR provides an industrial precedent for extensible intermediate representations and progressive lowering across abstraction levels [51]. Reaktor’s analogous requirement is a shared structural substrate with domain-specific semantics, not adoption of a single compiler IR as the full application knowledge graph. Source code and the semantic graph need traceable mappings in both directions, while unsupported arbitrary source round-tripping remains outside the guarantee.
14.2 Kahn networks and deterministic streams
Kahn’s model describes deterministic processes connected by conceptually unbounded FIFO channels. Blocking reads and the absence of scheduling-dependent observations permit a denotational account in
terms of stream transformations and least fixed points. Formalizations connect this model to complete partial orders and machine-checked reasoning [29, 30]. The important lesson for Reaktor is that attractive properties arise from restrictions. A process that observes whether a queue is currently empty and chooses a different output can expose scheduler timing. A bounded implementation can block on a write where the unbounded model does not. Consequently, compiling a deterministic network to bounded channels requires a separate argument about buffer sizes, scheduling, or admissible deadlock behavior. Consider two processes that each attempt to send two items before receiving two. With unbounded channels both can finish their sends. With capacity one in each direction, both may block on their second send. Payload types and structural connectivity are unchanged, but progress differs. A lowering must not claim to preserve the unbounded semantics without addressing this case. A practical stream profile should therefore declare whether production is push-or demand-driven, whether buffering is bounded, what happens on overflow, and which termination events are visible. Determinism is an optional qualified property of a profile and its implementations. It is not a default consequence of Stream<T>.
14.3 Synchronous dataflow and balance equations
Synchronous dataflow (SDF) restricts actors to fixed token production and consumption rates, enabling
static scheduling analyses for appropriate signal-processing networks [52, 53]. Let a channel from actor
𝐴 to actor 𝐵 produce 𝑝 tokens per firing of 𝐴 and consume 𝑐 tokens per firing of 𝐵. A periodic balanced
schedule requires
𝑝𝑞 𝐴 = 𝑐𝑞 𝐵 , (16)
where 𝑞 𝐴, 𝑞 𝐵 count actor firings per period. For 𝑝 = 2 and 𝑐 = 3, the smallest positive integer balance is
𝑞 𝐴 = 3, 𝑞 𝐵 = 2. Across a network these constraints form Γ𝑞 = 0 for a topology/rate matrix Γ.
This is a genuine use of linear algebra: a null-space calculation describes necessary token balance.
A positive solution alone does not establish a valid bounded schedule. Initial tokens, cycles, firing
enablement, and buffer capacity still matter. Two actors in a cycle with no initial token can satisfy balance
while neither can start.
Reaktor can expose an SDF dialect for media, sensor processing, or other fixed-rate pipelines. The
compiler may compute repetition vectors, construct schedules, and allocate bounded buffers under that
dialect’s assumptions. A general web service, whose output count depends on data and remote responses,
should not be forced into the same model. It can be connected through an explicit boundary that states the
relevant rate or buffering contract.
14.4 Petri nets and resource accounting
A Petri net describes places containing tokens and transitions that consume and produce them. It is useful
for reasoning about resource availability and synchronization. In an ordinary net, a transition 𝑡 is enabled
only when every input place has enough tokens. If 𝑀 is the marking and 𝐶 the signed token-incidence
matrix, a firing changes the marking to 𝑀 ′ = 𝑀 + 𝐶·𝑡 . A vector 𝑦 with 𝑦 T 𝐶 = 0 defines a conserved
token sum 𝑦 T 𝑀 [54].
A bounded work queue offers a simple Reaktor interpretation. A capacity pool contains 𝐾 credits.
Admitting work moves one credit to the set of outstanding jobs; terminal completion returns it. The
invariant is
𝐶𝑟𝑒𝑑𝑖𝑡𝑠 + 𝑂𝑢𝑡𝑠𝑡𝑎𝑛𝑑𝑖𝑛𝑔 = 𝐾, 𝐶𝑟𝑒𝑑𝑖𝑡𝑠 ≥ 0. (17)
The token model makes a common bug visible: returning a credit both on timeout and on a later completion
can over-admit work. The implementation needs a unique terminal transition or idempotent credit return
keyed by the work identity. A client timeout is not necessarily that terminal transition.
This does not require every Reaktor application to be authored as a Petri net. A protocol module can export a Petri-net or transition-system interpretation for analysis while presenting an ordinary Kotlin API. Structural hyperedges describe participation; the interpreted transitions explain enablement and resource movement.
14.5 An explicit Turing-complete behavior dialect
A general-purpose behavior dialect can contain a finite controller, conditionals, mutable storage, and an unbounded conceptual tape. One step reads the tape symbol at the current position, selects a transition from a finite table, writes a symbol, changes the position by one, and updates the controller state. Represent the read, branch, write, and state-update operations as typed nodes with explicit control and value edges. A feedback edge enables the next step unless a halting state is reached.
Proposition 14.1 (Computational universality of the general behavior dialect). If the dialect implements the operations above with unbounded conceptual tape storage and faithfully executes each transition, then it can simulate every deterministic Turing machine.
Proof. Encode the machine’s finite transition table in the controller and its tape as the dialect’s indexed
store. The initial controller, tape, and head position encode the initial machine configuration. By
construction, one graph iteration produces the encoding of exactly the next machine configuration.
Induction on the number of iterations establishes the simulation. The graph halts precisely when the
simulated machine reaches its halting state. □
The proposition follows the standard machine model of computability [55]. It is a statement about the proposed semantics, not a claim that the current visual editor implements this interpreter. A deployed process has finite storage and execution time; computational universality is an idealized expressivity result, not a promise of unlimited resources. A less elaborate implementation can compile equivalent loops and mutable state into Kotlin or another target language. The significance is unchanged: the semantics, not the visual notation, provide universality. A directed acyclic graph whose nodes perform fixed finite operations once does not obtain the same property merely by being large.
14.6 Why general verification cannot be completely automatic
Suppose a verifier could always decide whether an arbitrary program in this general dialect eventually completes. Applying it to the simulation above would decide whether an arbitrary Turing machine halts. The general decision procedure therefore cannot exist. This does not prevent proving termination for particular programs, enforcing a restricted terminating dialect, or analyzing a bounded abstraction. The engineering response is a hierarchy. Pure acyclic computations admit straightforward scheduling checks. Restricted protocols admit finite-state exploration. Resource contracts can bound loops and queues. General code can supply specifications, proofs, tests, or conservative summaries. Unknown outcomes remain explicit. Expressivity and automatic decidability are design choices with a real tradeoff, not an objection to using formal methods. For an agent-generated transformation, the verifier should identify which class of obligation is being asked. Type compatibility may be decidable and cheap. Termination of a bounded loop may be statically checked. Preservation of an arbitrary external business effect may require a human-supplied specification or domain proof. The tool should not turn an undecidable question into an unqualified success because a test suite happened to terminate.
14.7 Multiple meanings of time
A UI animation frame, a stream element’s event time, a message-delivery attempt, a workflow checkpoint, and a control-system sample do not share one universal clock. A dialect should distinguish logical step order from wall-clock deadlines and from timestamps carried in data. An event-time window may need late-arrival handling; a deadline may require a monotonic local clock; a distributed timestamp may carry uncertainty. A simulation can virtualize time and external effects so that a failure trace is replayable. An actual deployment may remain nondeterministic. The mapping between simulated and real execution must state which events, ordering constraints, and timing bounds are covered. A repeatable simulation is valuable evidence, not proof that every real-world schedule was tested.
Original page layout, starting at page 36
15. Distributed algorithms behind the execution model
The logical graph states which components can interact. A distributed realization must additionally specify how progress, failure detection, ordering, consistency, and recovery work. Location-independent interfaces are useful only when their contracts remain honest about these differences.
15.1 Failure models are part of the contract
A crash-stop process halts and does not recover. A crash-recovery process can restart with some durable state and lose volatile state. An omission failure loses a message or response. A Byzantine participant may deviate arbitrarily from its protocol. A slow or partitioned process can be indistinguishable from a failed one to another process that has not received a response. A realization profile should name the failures it addresses. A durable queue can recover accepted messages after a worker crash without tolerating a malicious broker or corrupted storage. A signed artifact authenticates an update without ensuring its code is correct. A trusted in-process reference can be suitable within one application yet inappropriate across an untrusted plugin boundary. Broad phrases such as “fault tolerant” should be replaced by the relevant failure model and preserved properties [40].
15.2 Causality and clocks
Lamport’s happens-before relation orders events connected by local program order and message trans-mission, together with their transitive consequences [56]. Events not related by it may be concurrent. Logical clocks can respect this relation without revealing all concurrency. Physical timestamps can assist diagnosis but require clock assumptions before they can establish event ordering. A graph observation should retain the difference between observed at, occurred at according to the producer, and causally depends on. A query that joins traces, a database commit, and a deployment event solely by timestamp can invent an order that the evidence does not establish. Spanner’s use of explicitly bounded clock uncertainty is an instructive precedent for making timing assumptions visible in a consistency protocol [57]. It does not imply that a commodity mobile device, a JVM process, or a robot sensor supplies the same clock guarantees. A Reaktor clock capability must describe the available service and uncertainty rather than expose one undifferentiated now() operation to every timing analysis.
15.3 Safety, liveness, and impossibility boundaries
Safety excludes bad outcomes; liveness requires eventual progress. A consensus service may preserve agreement during a partition by declining to complete some operations. The FLP result rules out guaranteed termination for deterministic consensus in a fully asynchronous model with a possible process
failure [58]. It does not rule out practical consensus protocols with additional timing or probabilistic assumptions. Partial synchrony formalizes systems in which useful timing bounds eventually hold, or hold but are initially unknown [59]. A deployment can therefore state that a protocol preserves safety despite delay but requires eventual communication and a sufficiently stable period for liveness. These assumptions belong in verification evidence and operational health interpretation. The CAP result similarly concerns the inability to combine its specified consistency and availability conditions when communication partitions occur [60]. It should not be reduced to an unrestricted instruction to choose any two properties. Reaktor can expose the policy for an unavailable authority: reject, wait, queue a provisional write, or accept an explicitly weaker operation. It cannot make that policy unnecessary.
15.4 Linearization points and external effects
Linearizability gives concurrent operations the appearance of taking effect at individual points between invocation and response, respecting real-time precedence [61]. It is useful for a graph revision registry, an admission counter, or a shared state object. It is not synonymous with durability, serializability of a multi-object transaction, or instantaneous global observation. For a local patch registry, the successful publication of the validated revision can be the linearization point. For a database operation, the commit protocol defines the relevant durable outcome. For an external payment request, receipt of a timeout may leave the outcome unknown. A client cannot safely turn that uncertainty into “the payment failed” and initiate an unrelated second payment. The end-to-end principle explains why a lower-layer delivery success is not a complete application correctness argument [62]. A network acknowledgement can establish reception at one layer. The application needs evidence about the business effect and its durable identity. Reaktor should preserve both observations rather than collapse them into one success flag.
15.5 Quorums, replicas, and ownership
For 𝑛 replicas, two quorums of size greater than 𝑛/2 intersect. This follows because two disjoint subsets of those sizes would contain more than 𝑛 members. Intersection is a useful ingredient in replicated protocols, not a complete consensus algorithm. Terms, leader selection, log matching, committed entries, and membership changes still require rules. Raft provides a well-documented example of those rules around a replicated log [63]. Reaktor should normally bind to an established coordination service rather than implement a new consensus algorithm in every application. A placement descriptor can request an authoritative revision registry and declare its failure-domain assumptions. An adapter then identifies the concrete implementation and the scope of its guarantees. An actor directory requires similar precision. A stable address identifies the logical actor; an activation identifier identifies one running generation; a fencing epoch limits which activation can commit protected effects. A lease holder that pauses can resume after its lease has expired. Rejecting its stale epoch at the protected resource is what prevents it from continuing as an unauthorized writer. Merely removing it from a routing table is insufficient when it still holds another path to that resource.
15.6 Delivery identity, effect identity, and deduplication
A message, an attempt to deliver it, and the effect it requests need distinct identities. A publication delivered to two subscriptions creates two logical consumer obligations. Deduplicating globally by message ID could incorrectly prevent the second subscription from performing its different effect. A suitable key often includes the subscription or business-effect scope.
Consider a transactional consumer with key (𝑔, 𝑚), where 𝑔 is the effect scope and 𝑚 the message identity. The consumer transaction checks for a committed receipt, applies the business update if no receipt exists, writes the receipt, and commits both together. A uniqueness constraint prevents two concurrent transactions from committing two receipts for the same key.
Proposition 15.1 (Scoped transactional effect uniqueness). Assume the deduplication record and protected effect are committed atomically in a store that enforces the key’s uniqueness and the required transaction semantics. Assume every execution of the protected effect uses this transaction, and the receipt is retained for every permitted replay. Then at most one committed execution of the protected effect exists for each key (𝑔, 𝑚).
Proof. A committed protected effect implies a committed receipt in the same transaction. Two committed
executions would imply two successful receipt insertions for the same unique key, contradicting the store’s
uniqueness semantics. Retries that observe the receipt return its result rather than execute the effect
again. □
The proposition does not cover an external effect performed outside the transaction. It also fails if receipts expire before a valid replay or if an administrator bypasses the protected path. Those conditions should be part of the profile, retention policy, and test corpus. The outbox pattern extends the same atomicity boundary to a record of an event that must subsequently be published. The relay may publish more than once, so subscribers still need an appropriate replay policy. This is deliberate composition of narrower guarantees, not universal exactly-once execution.
15.7 Backpressure and overload
Backpressure communicates that a downstream stage cannot currently accept more work. Its effectiveness depends on where buffering occurs. Suspending one coroutine does not bound memory if upstream requests are still accepted into another unbounded queue. An end-to-end admission policy needs a budget across relevant buffers, requests, and retained payloads. A credit protocol can enforce a hard count bound under atomic accounting. If each admitted job consumes one of 𝐾 credits and exactly one terminal transition returns it, then 𝑂𝑢𝑡𝑠𝑡𝑎𝑛𝑑𝑖𝑛𝑔 ≤ 𝐾. Byte-based budgets may be more appropriate when payload sizes vary. Flow control should also address fairness: one tenant or session must not monopolize all capacity indefinitely. Retry is an additional arrival process. Under widespread failure, immediate retries can increase load on the very component that cannot make progress. A profile should declare retry budget, backoff, deadline, and terminal handling. Retry behavior can be analyzed and simulated without claiming that a particular backoff schedule proves recovery from permanent failure.
15.8 Consistency belongs to an operation or datum
A system rarely has one useful global consistency label. A message commit may need transactional authority; presence can tolerate stale observations; a draft can merge offline edits; a deployment registry may require linearizable revision publication. The graph should attach requirements to these specific objects and operations. For a projected datum, a read-your-writes token must identify a relevant committed position and a replica must establish that it has applied the corresponding changes before serving the dependent read. Comparing unrelated clocks or revision counters does not establish this. For a multi-store query, one scalar token may be insufficient; the query can require a frontier of applied positions or explicitly accept a mixed-freshness result. Conflict-free replicated data types provide convergence under their particular update and merge conditions [64]. They do not automatically preserve arbitrary global business invariants. An offline draft
and a scarce inventory reservation therefore need different contracts even when both appear as mutable values in an application.