Free Assembly: A Calculus of Composition by Name

Lachlan Douglas — July 2026

Abstract

A logical, or rules-based, system has a form and any number of instances. The form is the system's parts and how they connect, one and abstract, settled from the parts' declarations before anything is built. Each instance is built from the form, concrete, part by part, each part after those it draws on. Each part states what it requires and what it provides, and the form follows from the declarations. The form also fixes the order in which an instance is built. That order is partial, and a substrate may take two parts that wait on each other for nothing in either order or at once (§7). The form itself is assembled from parts set side by side, and the order of assembly makes no difference. This paper gives the form's assembly its calculus. The operator ⊕ unions the parts and re-derives the wiring by name-matching over the whole union at once. A requirement with two candidate providers is an error. A requirement with none stays open. By-name merging is associative when the composite is a function of the union and incompleteness is permitted, and its wiring is frame-local when the pair determines the edge and ambiguity is refused. A pairwise merge takes its order from the bracketing, and the whole union has no bracketing to take one from.

Compositions form an algebra under ⊕, a cancellative partial commutative monoid of the shape separation logic gives its heaps. Uniqueness-or-error governs the exclusively keyed settled values as well as the wiring, the accumulating kinds collecting losslessly instead. A target configured twice is refused as a requirement provided twice is, so the operator selects among nothing. Composition being by disjoint union, a composite together with one operand determines the other. Composing with disjoint parts never disturbs a wiring already derived by name or a value already settled, the frame property. Normalisation takes every declaration to one outcome, a normal form or a defined error, whatever order the parts were assembled in.

Two characterisations follow. The first says what can be known early. When normalisation is a procedure that halts on every declaration, the finitary case, what the composition settles can be determined from its declaration. That is this paper's answer to what a system is in form. Once the substrates include a universal machine, whether it halts when run cannot be determined. Normalisation and operation fall on opposite sides of the decidable/undecidable line. The coincidence is contingent. It fails once the declarations' values are written in a Turing-complete language.

The second says that normalisation needs no notion of time. Step-indexing is the apparatus for self-referential state, and the calculus cannot express any. A reference is an address and ranges over no predicate on configurations, so the carrier cannot occur within itself. Self-reference enters only with an extension, reflection, a reference that reads the normal form it is part of. Read extensionally, reflection leaves the carrier equation with no solution in Set, and step-indexing is one standard repair. The two results are linked. The finitary calculi are a proper subclass of the predicative ones. A calculus with extensional reflection, its references predicates over composites, loses both results at once. With reflection written in finite syntax, expressive enough to carry every partial computable predicate, it loses the decidable normalisation alone. A calculus with a Turing-complete configuration language loses the same and nothing more.

Past a delegation boundary, building and running belong to external substrates. ⊕ is the parallel complement to the sequential calculus of Fettke and Reisig, which joins modules end to end through directed interfaces. Under the encodings §8 quantifies over, no commutative restriction of their operator reproduces ⊕; that no encoding at all embeds it is argued rather than proved.

1 The two strata, and the two modes of composition

Consider systems, parts connected to work together. A pump and its pipes are a system. So are a shop and its suppliers, and a program and its database.

Some systems are governed by rules. In a rules-based system, stated rules say what a part can be, how parts may connect, and what the whole may do. A chess position is rules-based. A database under its schema is rules-based. A fleet of containers under an orchestrator is rules-based. Call such systems logical.

Designing a system involves many decisions. This paper is about two of them: which parts to use, and how the parts connect. Call the connections the wiring. Parts and wiring together are the system's composition. A common record of a composition is a diagram, with boxes for the parts and lines for the wiring. For a logical system, the composition can settle what the system is in form. Settled means decided in advance. Once the composition is recorded, any question about what the system is in form can be answered from the record, before a single part exists. Assembling the instance then adds no decisions. Build the parts, and wire them as recorded.

For a logical system, the composition can be written down in full, every part named, and what each part requires and provides stated. Call such a record a declaration, a declared composition. A declaration is itself rules-based. It is finite, and stated rules say what may appear in it, so a machine can read one. The machine normalises the connections, pairing each requirement with the part that provides it. That normalising needs nothing but the declaration, so it can happen before the system is assembled. That is the special feature of a logical system, and §10 gives the condition under which a system has it. Call the normalising, done in that early position, normalisation (§4).

All of this can be made exact. The composition becomes a mathematical object. Combining compositions becomes an operator. The claims above are proved in §§3 to 5: assembly order cannot matter (§3, §4), normalisation terminates with one settled outcome (§4, §5), and the line between what that outcome settles and what only running shows is placed exactly (§5). This paper presents that mathematics, a calculus called free assembly, whose operator ⊕ assembles parts and normalises their wiring.

The system that results exists twice over. The form is what the declaration normalises to: one, abstract, and settled before anything is built. An instance is a concrete system built from the form, and one form may be built many times. The two are assembled from different materials, the form from declarations, an instance from built parts.

The composition is the paper's answer to what a logical system is in form. What the system is in operation, once an instance is assembled and running, is its operation. Build a part a different way, and the composition is unchanged. Wire the parts differently, and it is a different composition. The two answers are distinct. It calls them the system's two strata. The compositional stratum holds what the system is in form. The operational stratum holds what it is in operation. Normalisation completes at the normalisation point, where the form stands settled. The strata meet later, at the operation point, where a realised instance begins to run. The calculus stops at the first of these. The settled form may then stand, normalised and not yet handed over. At the delegation boundary, a normalised composition is handed to a substrate, something external that builds and runs the system (§7).

The stages a system passes through, and the three crossings §§4, 5 and 7 place on them. A declaration assembles and normalises to a normal form (§3, §4). Past the delegation boundary a substrate realises an instance from that form (§7). The instance's own running begins at the operation point. Everything left of that point is what the system is in form, and is settled by reading the declaration; whether the running halts, to the right of it, is not (§5).

This paper distinguishes two modes of composition, because a system is assembled twice, as an instance and as a form. One mode joins parts in sequence. The output of one part becomes the input of the next. Order matters, since A-then-B and B-then-A are, in general, different systems. This is the mode an instance's dataflow exhibits. Category theory writes it as g ∘ f, and Fettke and Reisig recently gave it a calculus over declared modules [Fettke–Reisig], so that mode is, to that extent, settled. The mode that settles a form is the question that remains. It sets parts side by side. Each part declares what it requires and what it provides. The wiring pairs each requirement with a provider. Order contributes nothing. Assembling A beside B and assembling B beside A yield the same form.

Call the first mode sequential and the second parallel. Both compose declarations, and they differ in how they match: by label and ordinal position, between two adjacent interfaces, against by name over the whole union at once. The parallel mode is the one that settles a form, and it composes up to the normalisation point, where the form stands assembled. Sequence is what lies past that point, in the dataflow the built thing runs on. Free assembly is a calculus of the parallel mode. In algebraic terms, the parallel mode is commutative. Section 3 shows it is also a separating composition, in the sense separation logic gives the word. Two composites join only when their parts do not overlap. Section 8 shows that, under the encodings it quantifies over, no commutative restriction of the sequential operator reproduces the parallel mode, and argues it is no fragment of the sequential one.

By-name parallel composition has been given algebras before. In Bracha's Jigsaw, modules merge by name. The merge is commutative and associative, and a name defined twice is an error [Bracha]. In Cardelli's linksets, program fragments link by name. The linking is confluent and terminating [Cardelli]. Both algebras are partial. Some pairs have no combination. Neither derives the wiring from the whole assembly at once. Neither obtains a separating monoid (§3), a frame property (wiring derived on the union survives further composition, §3), nor a delegation boundary (§7). The parallel mode has all three here. The frame property holds of ⊕. The abstract binding of §4 consults more than a pair and stands outside it (Prop 4.8).

Terminology: part, component, module. The field has no settled name for the unit of composition. Fettke and Reisig range over "modules, or components, parts, constituents" within a single sentence [Fettke–Reisig]. This paper sorts the three names by a single axis, information hiding. A part is the general term, any unit of composition that bears an interface of ports, the named points where it requires or provides connections. Section 3 treats parts as the resources of a separation algebra.

A component is a part wired transparently. Every dependency of a component is visible at its interface, and nothing is hidden [Szyperski]. A module is a part that seals an internal composition behind its interface [Parnas]. Both kinds bear an interface. They differ in sealing alone. The calculus of this paper is flat. Every part is wired in one carrier, and no part hides an interior. Every part here is therefore a component. A composite reused as one sealed unit would be a module, and modules are out of scope.

The development below speaks of parts, the general term, because ⊕ composes by one rule whether or not a part hides an interior. None of this corrects Fettke and Reisig. Their "module" is the broad composable-unit sense standard across the field. The three-way split only adds precision to it.

One discipline governs the calculus: static well-formedness. A required port may be wired to at most one provider, and a configurable slot may be set by at most one part. Two candidate providers for one requirement is an error, and so is a second part configuring a slot. A requirement with no candidate stays open and a slot no part configures is unset, and §2 permits both. Whether a composition is well-formed is settled by reading the declaration, the criterion deduced, not measured.

The claim, and its scope. The contribution is the securing discipline behind the wiring mechanism, four clauses in two pairs. Associativity is secured by two: the composite is a function of the union, and incompleteness is permitted, of an unmet requirement, an unset target and key, and a dangling fragment alike. The frame property is secured by two more: the requirement–part pair determines the edge and nothing else in the set does, and ambiguity is refused, of a requirement and of a target alike (§2, §3). Dropping any one costs its property. Drop the first and associativity goes with it (Remark 8.1). Drop the second and associativity goes as well. A requirement that two parts leave open and a third closes makes one bracketing undefined where the other is defined, so permitting the count of none is what leaves well-formedness downward closed (Remark 3.6). Drop the third and a derived edge can turn on what else the set holds, an edge that reads the pair to choose a candidate and the whole set to choose the port among them being enough, so it need not survive restriction. Drop the fourth and the frame property fails, since a disjoint frame can re-rank (Prop 4.8). With the discipline come the two characterisations it affords (§5, §6). (𝒞, ⊕, ∅), the algebra §3 builds, composes parts by disjoint union and settles values under one uniqueness rule for the exclusive kinds and lossless collection for the accumulating; normalisation runs as a finite chain of total functions (§4).

The scope is this. The calculus is static, and everything in it happens before anything runs. Operation is delegated to substrates, and the paper models no running behaviour beyond what Proposition 5.1 imports from its universal substrate. Section 9 locates the discipline against the prior by-name operators, and §5 and §6 carry their own prior art.

The non-embedding from the sequential calculus is argued model-theoretically. No refused functor is exhibited. The decidability result is where the line falls, and no new undecidability is proved. Its undecidable side is imported from the chosen universal substrate, Turing's (§5). A further claim, that composition is prior to computation as such and grounds it, is not made here.

The terms above are used throughout, in these senses.

2 The calculus

Four things make up the calculus. A part is the unit that declares what it requires and what it provides. A configuration is a set of parts together with their wiring and their settled values. Satisfaction and well-formedness are the discipline the wiring is derived from. The operator ⊕ composes configurations by re-deriving everything on the union. Definitions 2.1 to 2.5 build them in that order, and Definition 2.6 closes with the composite, the element of the carrier §3 takes up. A part carries two sorts of declared data, ports for the wiring and fragments for the settled values, and each sort gets its own derivation.

Fix a countable set Λ of names. 𝒩 = Λ*, the finite paths of names, is the set of addresses, the empty path the root. Addresses are hierarchical by construction. The prefix order on 𝒩 is containment.

Definition 2.1 (Part). A part is a triple m = (ι, P, F). The address ι ∈ 𝒩 locates the part. P is a finite set of ports. F is the part's fragment map, described after the ports. Write id(m) = ι. A set of parts is identified when its members have pairwise-distinct addresses.

Ports. A port has a polarity in {!, ?} and a mode in {named, abstract}. Polarity ! marks a provided port and polarity ? a required one. A provided port carries a name in Λ, and the provided ports of one part carry pairwise-distinct names. A required port's mode fixes what it carries. An abstract required port carries a name, its role (§4). A named required port carries a reference, a nonempty path in 𝒩; a one-segment path is read as a plain name.

port	polarity	carries
provided	!	a name in Λ, pairwise-distinct within the part
self-port	!	no name; matched by address alone (Def 2.3)
required, named	?	a reference, a nonempty path in 𝒩
required, abstract	?	a name, its role (§4)

The self-port. Besides its declared ports, every part bears one canonical provided self-port. The self-port stands for the part as a whole. It carries no name, counts among the part's provided ports, and is matched by address alone (Def 2.3).

Fragments. A fragment is a value the part contributes, drawn from a fixed first-order set V of values, taken throughout with a computable coding and decidable equality, so that a declaration is finite data and §5's finitarity is well-typed. Every fragment carries a target address in 𝒩, naming the part that receives it, and belongs to a configuration kind. Keys are drawn from a fixed first-order set 𝒦. The kind fixes how the fragment is collected and how far it may reach (Def 2.3). An exclusive kind is tagged with a key, and its target address is the declaring part's own address ι or an address extending ι by one segment: a part configures itself or one of its constituents, and reaches no further. An exclusive fragment is an instruction, and instruction follows containment; an accumulating fragment is data, which a target may collect from anywhere. An accumulating kind carries no key, and its target may be any address. The map F assigns to each configuration kind a finite set of the part's fragments of that kind. F is key-injective: within one part, at most one fragment per target and key. A part carries at most one accumulating fragment per kind and target, so within one collector the contributions have pairwise-distinct source addresses (Def 2.3).

For an instance of all of this: a part at the address data/store carries one provided port of name store. Call this one store, after the last segment of its address. A part data, at the top-level address data, carries one exclusive fragment keyed endpoint whose target address is data/store. data holds store as its constituent, which is how far an exclusive fragment reaches. A part service, at the top-level address service, carries a named required port of reference store and a provided port of name api. Each is a part in full, an address with its ports and its fragment map, and Example 4.6 completes the three into a composition.

Named ports bind by reference (a point-to-point requirement wired directly by ⊕, to a provided port matched by name or to a part matched by address); abstract ports bind by role (a non-local requirement bound by the normaliser, §4). Only named ports participate in ⊕.

Definition 2.2 (Configuration). A configuration is a triple C = (M, W, Γ). M is an identified finite set of parts. W ⊆ M? × M! is a wiring, relating the required ports M? to the provided ports M!. A port is located by the part carrying it: M? is the set of pairs (m, r) with m ∈ M and r a required port of m, written m.r, and M! likewise. Two parts declaring the same port are therefore two elements, and the owner of a port is recoverable from it (Def 4.1). Write M?* for the named required ports. ⊕ populates the edges at named required ports (Def 2.3), and the normaliser populates those at abstract ones (§4). Γ holds the settled values, a partial map assigning a fragment or a set of fragments to a target and kind, with a key besides for the exclusive kinds. A target is a part in its capacity as the recipient of configuration. Whether Γ holds what the parts determine is Def 2.6's question rather than this one. Where it does, an exclusive kind's entry is the one fragment declared for that target and key, and an accumulating kind's is the set of the fragments of that kind addressed to the target. Each fragment retains its source address (Def 2.3). Write ‖C‖ = M.

Definition 2.3 (Satisfaction, well-formedness, and the derived wiring).

Satisfaction. A part p satisfies a named required port r iff r has polarity ? and one of two matches holds. The match by name: p carries a provided port whose name is r's reference, a one-segment reference being read as a name. The match by address: r's reference is a segment-aligned suffix of p's address, so the reference a/b matches the addresses a/b and ⋯/a/b and no other. Satisfaction is a property of the pair alone; no ambient set enters it. A part does not satisfy its own required port, so the owner is excluded from the satisfier count. A part matching in both ways is one satisfier; two parts are two.

Well-formedness. An identified part-set M is well-formed, wf(M), iff two counts are at most one. Every named required port in M must be satisfied by at most one part of M. Every pair of a target and an exclusive key must be configured by at most one part of M. A count of none is permitted in both cases. A requirement satisfied by no part is open; a target and key no part configures is unset. A count of two or more is the error ⊕ refuses; call the discipline uniqueness-or-error. It governs the wiring and the settled values alike. The two matchings feed one count, so a reference matching one part's provided name and another part's address is ambiguous like any other double provision.

The derived wiring. On a well-formed M, the wiring function w returns the derived wiring w(M) ⊆ M?* × M!, one edge per satisfied requirement r. When the match is by name, the edge runs to the satisfying part's provided port of the referenced name. When the match is by address and not by name, the edge runs to the satisfying part's self-port. A part matching both ways takes the by-name edge. w is defined on well-formed sets only.

Besides ports, each part carries configuration fragments through its map F (Def 2.1), of two kinds.

Exclusive kinds. An exclusive kind (a configure) is keyed, and reaches the declaring part itself or one of its constituents and no further (Def 2.1). For a target t and key k, a configurer of (t,k) is a part carrying a k-fragment addressed to t. On a well-formed M there is at most one, so the configuration function γ, which yields Γ as w yields W, records it and has nothing to choose between. Two configurers of one (t,k) is the error wf refuses, on the same ground as a doubly satisfied requirement: the declaration does not say which governs, and the calculus refuses rather than choosing silently. A (t,k) no part configures is unset, and what a receiving part does absent an instruction is its own affair, past the delegation boundary (§7).

Accumulating kinds. An accumulating kind (a contribution) carries no key, and is collected per kind by the addressed target. Every part carrying such a fragment contributes it to the collector that its target address keeps for that kind, and the contributing part may sit anywhere, ancestor or not. γ keeps every such fragment; no winner is chosen, so the collection is lossless. The kept fragments form a set, their source addresses pairwise distinct (Def 2.1). No order is imposed on them. A consumer needing one computes it from the sources the collector carries, and which order to compute is a matter for the substrate (§7).

kind	reach	keyed	γ keeps
exclusive	the declaring part or one of its constituents	yes	the one fragment declared for that target and key
accumulating	the part the fragment addresses, anywhere	no	every fragment addressed to that target, each tagged with its source

Dangling fragments. A fragment of either kind whose target address is the address of no part of M is dangling: it reaches no target, and γ passes over it. Dangling is not ill-formedness. A wider union may supply the part addressed, so refusing it pairwise would make ⊕ depend on the order of assembly, and a singleton part that configures a constituent would not be a composite, as data alone would not in Example 4.6. Like a cyclic wiring (§7), a dangling fragment in the assembled whole is settled at normalisation, which yields a defined error and no normal form. Addresses are unique in an identified set, so no ambiguous target arises.

γ is thus a total function, and it selects among nothing. Where a fragment reaches a target, γ records it; no fragment is ever dropped in favour of another.

On the parts above: service's required port is satisfied by store twice over, by the name of the port store provides and by store's address, the reference store being a segment-aligned suffix of data/store. That is one part, so one satisfier, and the set is well-formed. data satisfies nothing, providing no port of that name and bearing an address the reference does not end.

Lemma 2.4 (Downward closure of wf). If M' ⊆ M and wf(M), then wf(M'). Proof. Both counts fall under a subset. A named required port r ∈ M' is also in M, and its satisfiers in M' are a subset of those in M, which number at most one. A target and key configured in M' is configured in M, and its configurers in M' are likewise a subset of those in M. ∎

Definition 2.5 (Free assembly). For C₁=(M₁,W₁,Γ₁), C₂=(M₂,W₂,Γ₂) with id(M₁)∩id(M₂)=∅ and wf(M₁∪M₂): C₁ ⊕ C₂ = (M₁∪M₂, w(M₁∪M₂), γ(M₁∪M₂)). Both the wiring and the settled values are re-derived on the union. ⊕ is undefined on address collision or ¬wf(M₁∪M₂). The empty configuration is ∅ = (∅,∅,∅).

The operands' wirings are discarded, and the composite's wiring is re-derived on the whole union. This global re-derivation is the defining move of free assembly, and it keeps ⊕ associative, since no match is internalised pairwise, so no bracketing can consume one. Composition is at the level of parts. One composes parts and normalises the whole.

Definition 2.6 (Composite). C is a composite iff wf(‖C‖), W = w(‖C‖), and Γ = γ(‖C‖): its wiring and its settled values are exactly what its part-set determines. Let 𝒞 be the set of composites. Equality on 𝒞 is by parts, in full: address, ports, and fragment map, with W and Γ agreeing wherever the parts do, being functions of the part-set.

3 ⊕ as a separating composition

Composition under ⊕ has the algebra of a separation logic heap. Theorem 3.1 gives the monoid laws, cancellation among them; Proposition 3.2 says that the settled values of anything that normalises determine the fragments they came from; Proposition 3.3 gives the frame property, of the wiring and of the settled values alike; Corollary 3.4 settles decomposition. The section closes on what cancellativity supplies and what it does not.

Theorem 3.1. (𝒞, ⊕, ∅) is a cancellative partial commutative monoid. Proof. Equations between possibly-undefined composites are read as Kleene equality: both sides defined and equal, or both undefined.

• Closure. A defined C₁⊕C₂ has wiring w(M₁∪M₂) and settled values γ(M₁∪M₂), hence a composite, in 𝒞.
• Commutativity. ∪ and ∩ are symmetric, so definedness is symmetric; M₁∪M₂=M₂∪M₁, and w and γ being functions of the union give equal results.
• Associativity. Each side is defined exactly when the addresses are pairwise disjoint and wf(M₁∪M₂∪M₃). The full-union condition is the same on both sides, and Lemma 2.4 supplies the binary well-formedness each side also needs along the way. When defined, both sides equal (M₁∪M₂∪M₃, w(M₁∪M₂∪M₃), γ(M₁∪M₂∪M₃)), since w and γ depend only on the union. For γ there is nothing further to check: on a well-formed union each target and key has at most one configurer, so γ gathers the fragments declared and selects among none.
• Unit. For C∈𝒞, C⊕∅ = (‖C‖, w(‖C‖), γ(‖C‖)) = C since C is a composite.
• Cancellativity. If C₁⊕C₃ = C₂⊕C₃ (both defined), then M₁∪M₃ = M₂∪M₃ with id(M₃) disjoint from both, so M₁ = (M₁∪M₃)∖M₃ = M₂, and W and Γ follow (Def 2.6).

∎

⊕ is partial (Def 2.5), the partiality being address collision and uniqueness-or-error (Def 2.3), the second covering a doubly configured target as well as a doubly satisfied requirement.

Proposition 3.2 (the settled values determine the declared fragments). Let wf(M) hold and no fragment of M dangle, every one addressing a part of M (Def 2.3). Then from γ(M) the fragment map of every part of M can be read off, so a composite's settled values and its declared fragments determine each other. Every normal form meets the hypothesis, normalisation refusing a dangling fragment (Def 4.2). Proof. Each fragment retains its source address (Def 2.2). For an exclusive kind, wf admits at most one configurer of each target and key, and γ records that fragment with its source, so the k-fragments of every part are recovered by reading Γ and grouping by source. For an accumulating kind, γ keeps every fragment and the sources are pairwise distinct within a collector (Def 2.1), so the same reading recovers them. Under the hypothesis γ passes over nothing, so no fragment of M is absent from γ(M) and none is added. ∎

Cancellation costs nothing here. Disjointness lets set subtraction read M₁ = (M₁∪M₃)∖M₃ (Theorem 3.1), and W and Γ follow the parts, being functions of the part-set (Def 2.6). Remark 8.1 sets the associativity against the pairwise by-name merge that loses it.

Cancellative is short of invertible. ⊕ has no inverse, no part that un-provides another. Like addition on the naturals, it cancels and does not undo.

Separating composition. Separation logic's resources form a partial commutative monoid, the canonical instance being heap composition h₁*h₂, defined iff dom(h₁)∩dom(h₂)=∅ [Reynolds; Calcagno–O'Hearn–Yang]. Free assembly is the same shape, with address-disjointness in the role of domain-disjointness. It cancels as the heap does, since disjoint union forgets nothing. (𝒞, ⊕, ∅) is a separation algebra in the sense of Calcagno–O'Hearn–Yang, meeting the cancellativity axiom that the design space of Dockins, Hobor and Appel marks as optional [Calcagno–O'Hearn–Yang; Dockins–Hobor–Appel].

The calculus-specific content is the wiring w and the configuration function γ layered over the resource monoid, the structure that turns disjoint resources into a connected, configured system.

Proposition 3.3 (Locality of the derived form). Let M' ⊆ M with wf(M). (i) w(M') = w(M) ∩ (M'?* × M'!). (ii) to every target in M', γ(M') assigns what γ(M) assigns it, restricted to the fragments whose source lies in M'; to a target outside M' it assigns nothing. Proof. Lemma 2.4 gives wf(M'), so both derivations are defined on each side. (i) Satisfaction is a property of the requirement–part pair alone (Def 2.3), and the pair determines the edge's port, so the edges within M' are exactly the edges of M whose requirement and satisfying part both lie in M'. (ii) A fragment is declared by a part and addressed to an address, and γ records it exactly when that address is a part of the set γ is given (Def 2.3). A fragment recorded by γ(M') has its source and its target in M', hence in M, so γ(M) records it too. A fragment of γ(M) whose source and target lie in M' is declared in M' and addressed within M', so γ(M') records it. Well-formedness leaves γ no choice of which fragment to record for a target and key, so the two agree. ∎

Proposition 3.3 is the calculus's frame property, and the two clauses say one thing of the two halves of the derived form: each derived item depends on the pair it relates and on nothing else in the set. Taking M=‖C‖∪‖D‖, M'=‖C‖, clause (i) gives w(‖C‖) ⊆ w(‖C⊕D‖). Composition with a disjoint frame never disturbs an established wiring; no new wiring rebinds a port of C already wired, and new edges attach only to C's open required ports or to its provided ports. This is the wiring analogue of separation logic's frame rule, the locality on which local reasoning would rest; the calculus proves the locality and builds no program logic over it.

Clause (ii) reads the same way for the settled values. A disjoint frame cannot displace an established value, since a second configurer of one target and key leaves the union ill-formed and C⊕D undefined. It can only set a target and key that C left unset, add its own fragments to a collector C had begun, or supply the part that a fragment of C was addressed to. Every fragment recorded for C is recorded again for C⊕D, from the same source. Extension can settle what was unset, and cannot alter what was settled.

The abstract binding of §4 is the one stage that is not frame-local (Prop 4.8), and the failure is not peculiar to the nearest-enclosing rule. Any ranking that strictly prefers a nearer candidate re-ranks when an extension supplies one, so no binding discipline that consults proximity in that way can be frame-local. Proposition 4.8 proves the nearest-enclosing instance; the general statement is the same one line read of any such ranking. That literature proves coherence and stability under type substitution, resolution being unchanged when a term acquires a more specific type [Schrijvers et al.]. Proposition 4.8 concerns extension of the composition rather than of a type, and neither property reduces to the other. The frame property belongs to what ⊕ derives, the wiring and the settled values, and not to what bind adds.

Corollary 3.4 (unique decomposition). In (𝒞, ⊕, ∅) the indecomposable elements are exactly the singleton composites, and every composite is the join of the singletons of its parts, uniquely. Proof. Let C be a composite with at least two parts and M' a non-empty proper subset of ‖C‖. Both M' and its complement are well-formed (Lemma 2.4) and address-disjoint, so the composites they determine compose to C, and C is decomposable. A singleton admits no such split, ∅ being the unit. A decomposition into indecomposables is a set of singletons whose part-sets union to ‖C‖, and ⊕ unions part-sets disjointly, so the set is exactly the singletons of ‖C‖. ∎

Remark 3.5 (teardown and refactoring without subtraction). Cancellativity supplies no subtraction operator, and nothing needs one. Because the normal form is a function of the part-set (Corollary 4.3), removing a part is re-normalisation of the smaller set, and no inversion of ⊕ is involved. Refactoring reasons one level up: two part-sets are interchangeable in a context C exactly when C⊕A and C⊕B normalise alike, agreeing in wiring and settled values. Normalising alike is coarser than A = B: two parts differing only in a provided port that nothing in the context requires normalise alike, since w draws an edge only for a satisfied requirement (Def 2.3), and differ as declarations. The coarser, observational equality is the property refactoring wants.

Remark 3.6 (what the discipline secures, in general). Theorem 3.1 and Proposition 3.3 use nothing of w and γ but two facts about them. Let P be any predicate on identified finite part-sets that is downward closed, and f any function defined on the sets satisfying P. Write M₁ ⊗ M₂ = (M₁∪M₂, f(M₁∪M₂)), defined when the addresses are disjoint and P(M₁∪M₂) holds. Then (⊗, (∅, f(∅))) is a cancellative partial commutative monoid, by Theorem 3.1's proof read with f for (w, γ) and P for wf. Closure and the unit are immediate. Commutativity follows from the symmetry of ∪ and ∩, associativity from P's downward closure supplying the binary conditions each bracketing needs, and cancellativity from disjoint subtraction. Where f is in addition local, f(M') being what f(M) assigns within M', the frame property follows by Proposition 3.3's proof read the same way. This calculus is the instance P = wf, f = (w, γ).

So §1's discipline is this lemma's hypotheses in the calculus's own terms. The composite being a function of the union is f being a function at all, and it buys the algebra. An unmet requirement being permitted is P's downward closure, and it buys associativity. Two things leave f local, and the lemma above takes locality as a hypothesis rather than deriving it. Candidacy reads the requirement–part pair and nothing else in the set (Def 2.3). Ambiguity is refused rather than ranked, where a discipline that ranked candidates would re-rank under a disjoint frame, as binding does (Prop 4.8). A variant calculus, over a different fragment regime or a different ranking, inherits both by checking the three hypotheses.

4 Normalisation: assembly and binding

After assembly, named ports are wired and the values are settled by γ (Def 2.3); the abstract required ports (matched by role) remain. A normaliser N = bind, applied once, discharges them. The calculus assumes part-preservation: neither ⊕ nor N introduces new parts or ports.

Definition 4.1 (Binding). A candidate for an abstract required port r is a provided port that carries r's name and belongs to a part other than r's own, the owner being excluded as it is for named ports (Def 2.3). A scope is an address prefix, and its region is the set of parts whose addresses it prefixes. Let ≺ rank, for each abstract r, its candidates as a function of C's structure (parts + containment). bind(C) keeps the parts and adds wiring, taking each abstract r in turn. With no candidate, r stays open. With a unique ≺-minimal candidate, that candidate is wired. With a non-unique minimum, bind(C) is undefined, which is an error. The calculus fixes ≺ as the nearest-enclosing-scope ranking, which is the discipline of scope-directed implicit resolution [Oliveira et al.; Schrijvers et al.]. Walk the containment chain outward from r's owning part, beginning at the owner's parent scope. The first enclosing scope whose region contains any candidate wins. Outer scopes are not consulted. Every candidate in the winning scope's region ranks ahead of every candidate outside it, and candidates within the winning scope tie. So bind wires r when the winning scope holds exactly one candidate, errs when it holds several, and leaves r open when no scope on the chain holds any. The provider need not enclose r; the scope encloses, and the provider sits anywhere within its region. This fixed choice makes the normal form canonical and unique. That the choice is structural, a function of the assembled parts and containment, matters separately. Any structural ranking would yield a deterministic bind, so the determinacy results below turn on structurality alone. The particular rule decides only which normal form is the canonical one.

An instance of the walk: let the port's owning part sit at a/b/p and carry an abstract required port, and let the one part providing that name sit at a/q. The walk starts at the owner's parent scope, a/b, whose region holds no candidate; it steps out to a, whose region holds a/q; that scope wins and the candidate binds. Proposition 4.8 takes up the same arrangement.

bind is a function of C, part-preserving, and idempotent. The configuration function γ that ⊕ carries (Def 2.3) is likewise a function of the part-set and part-preserving, and it selects among nothing: on a declaration that normalises, every declared fragment reaches the settled Γ and can be read back from it (Prop 3.2). bind only adds wiring. Normalisation therefore consumes nothing. Every stage is a function of the whole declaration, and the declaration survives normalisation intact.

Definition 4.2 (Assembly and normalisation). For finite identified S with wf(⋃S), A(S) composes the singletons under ⊕ in any order; by Theorem 3.1 this is (⋃S, w(⋃S), γ(⋃S)), independent of order and bracketing. (N ∘ A)(S) is the normal form of S. The name is the rewriting tradition's [Church–Rosser], and the sense is the one that carries over: an outcome reached whatever order the parts were taken in, and unique. Normalisation here is a function rather than a rewrite relation, so a normal form is what the function returns rather than a term to which no rule applies. Normalisation ends with two global checks on the assembled whole: no fragment of either kind may dangle, every one addressing a part of ⋃S (Def 2.3), and the dependency relation the derived wiring induces must be acyclic (§7). Either failing is a defined error and yields no normal form. On an S that is not identified, or whose union is not well-formed, the map returns the refusal of Def 2.5 as its defined error, so that it is defined on every finite S.

Corollary 4.3 (Determinacy of normalisation). For every finite identified S with wf(⋃S), (N ∘ A)(S) is a well-defined function of S, returning a normal form or one of the defined errors of Def 2.3, Def 4.1 and §7. Under the canonical ranking of Def 4.1, the outcome depends only on the parts composed; assembly order, bracketing, and normalisation scheduling contribute nothing. Proof. By Theorem 3.1, A(S) is determined by S alone, and N is a function with no internal schedule. The errors are determined with it: a non-unique ≺-minimum, a dangling target address, and a cyclic dependency relation are all properties of the assembled parts. ∎

The normal form is also a certificate: reaching it witnesses that the composition is determinate, settled by its parts alone; the uniqueness-or-error discipline leaves normalisation nothing to choose, since it wires, errs, or leaves open. The certificate covers the composed whole as it stands. Composing further parts re-derives the wiring and may re-rank a binding (§3), and the extended whole requires a fresh certificate.

A normal form in which bind has bound an abstract port carries wiring beyond w(‖C‖) and so is not an element of 𝒞 (Def 2.6). The exclusion is deliberate. 𝒞 is the carrier of assembly, closed under ⊕ (Theorem 3.1). The normal form is normalisation's output, what the delegation boundary later hands over (§7). It enters further ⊕ only through its part-set. Def 2.5 accepts a normal form as an operand, discards its wiring along with the rest of the operand wiring, and re-derives on the union. Hence bind(C) ⊕ D = C ⊕ D. The bindings are shed by composition and re-made only by the next normalisation. Composition proceeds from parts alone. To extend a composite, compose the part-sets and re-normalise (Def 4.2). A normal form remains a configuration triple, finite and first-order exactly as §6 treats the carrier; what it gives up is only membership in the algebra.

Normalisation consults nothing outside the declaration. Ports, references, fragments, and containment are declared data, and no value produced by realisation or operation enters w, γ, or bind. Normalisation is therefore a function of the declaration alone, which is §1's criterion made a property of the map.

Remark 4.4 (single pass). Part-preservation makes N single-pass, since binding exposes no new ports, so one pass saturates.

Remark 4.5 (generation is staged rather than forbidden). Part-preservation does not outlaw generative module systems, functors, or macros; it stages them. Such expansion is a prior elaboration that produces the part-set, after which normalisation runs part-preserving over the result: expansion first, then the part-preserving pass. Excluded is generation interleaved with normalisation, where normalising a part creates further parts needing normalisation. That interleaved case is the self-referential one whose absence §6 names, and it admits a precise condition: generation that is well-founded (each added part strictly smaller than its emitter in a fixed well-founded order) terminates, an ordinary inductive construction. Termination alone does not restore order-independence: two generators whose outputs depend on what is already present can terminate under every interleaving and still produce different part-sets, so the confluent core survives only when the generation steps also commute. Unbounded generation is computation, and belongs past the normalisation point as any other non-terminating act does.

Example 4.6 (a data service). Take the three parts of §2, store, data and service, and add two more, at the top-level addresses seed and catalog. data's endpoint fragment has the value ⟨127.0.0.1, 7000⟩. seed requires one named port with reference store. catalog carries an accumulating fragment of kind records whose target address is data/store, with the value [⟨A-100, Widget, 9.99⟩, ⟨A-101, Gadget, 12.50⟩]. Let S be these five.

Assembly unions the parts and re-derives on the union (Def 2.5). Both service's and seed's required ports carry the reference store, each satisfied by the one part store as §2 showed, and the match by name takes the edge. So w(⋃S) = {(service.?store, data/store.!store), (seed.?store, data/store.!store)}, both wirings found in one global pass and present in neither operand. γ(⋃S) records the one configurer of (data/store, endpoint), which is data, and collects the records list into data/store's collector for that kind. The two fragments reach their target by different routes. data may configure store because store is its constituent; catalog sits in another branch and reaches the same target because an accumulating fragment may address any part. No abstract port remains, so N = bind adds nothing, and (N ∘ A)(S) = (⋃S, w(⋃S), γ(⋃S)) is the normal form, its Γ giving (data/store, endpoint) ↦ ⟨127.0.0.1, 7000⟩ and (data/store, records) the collector holding catalog's one contribution, the list [⟨A-100, Widget, 9.99⟩, ⟨A-101, Gadget, 12.50⟩]. Composing the five in any order yields the same normal form (Corollary 4.3): the wiring is re-derived on the union rather than accumulated pairwise, so no order exposes or withholds a match. Had store also carried an endpoint fragment addressed to itself, the set would have two configurers of one target and key, and ⊕ would refuse it (Def 2.3). Refusal reaches the wiring the same way. Add a part cache at a top-level address, providing a port of name store: service's requirement then has two satisfiers, wf fails on the union, and every bracketing of the six parts is equally undefined.

The normal form of Example 4.6. Both required ports ?store, on service and seed, are re-derived on the union to the single provided !store of data/store (the solid arrows); neither wiring is present in any operand. data's exclusive endpoint fragment, which reaches data's constituent, and catalog's accumulating records contribution, which reaches across a branch, normalise by kind into Γ (the dashed arrows and box). service's !api has no consumer. Any assembly order gives this same form (Corollary 4.3).

Remark 4.7 (equivariance: by name means by equality). Nothing in the calculus reads inside a name segment. Every definition consults Λ and 𝒩 through segment equality and path structure alone. Satisfaction compares a reference with a carried name, or matches it as a segment-aligned address suffix (Def 2.3). Well-formedness counts satisfiers. A fragment of either kind matches its target address against a part's address, and an exclusive one is counted per key. Depth, prefix and suffix are path structure, indifferent to which segments compose the path. The whole construction is therefore equivariant under renaming of segments. Take an injective renaming π of the name segments, applied to names directly and to addresses, references and target addresses segment-wise, so that path structure is preserved. Then π·(C₁ ⊕ C₂) = π·C₁ ⊕ π·C₂, with definedness preserved in both directions, and (N ∘ A)(π·S) = π·(N ∘ A)(S). The normal form is a function of the pattern of sameness and distinctness among the declared segments and of the shape of the paths they compose, never of the segments themselves. This is the sense of by name in the title, the sense that the nominal tradition gives the word [Pitts]: a name is an atom bearing only equality, and the calculus uses no more of it. Equivariance holds under every injective renaming, with no clause excepted, since a collector is a set and imposes no order for a renaming to disturb (Def 2.3).

Proposition 4.8 (binding is not frame-local). Under the nearest-enclosing ranking of Def 4.1 there are composites C and disjoint D, every composition and binding defined, in which an abstract port bound by bind(C) binds to a different provider in bind(C ⊕ D). Proof. Take the arrangement after Def 4.1: owner at a/b/p, unique candidate at a/q, winning scope a. Let D add, at a fresh address under a/b, one part providing the port's name. The walk now stops at a/b, the nearer scope, and binds its candidate. ∎

5 Decidability: the decidable/undecidable line, placed

The first characterisation says what can be settled by reading a declaration: normalisation is decidable, operation is not, and the line between them falls in one place. Stating it needs a class of calculi, since the coincidence is contingent: the base calculus exhibits it, and the variations of this section and §6 are the calculi that lose it.

Throughout this section and §6, a composition calculus is the calculus of §2 with two points of variation: a reference discipline (§6), and an evaluation stage, a partial computable function that normalisation applies to the declarations' configuration fragments in the course of normalising. The base calculus has the trivial stage, and a configuration language is an evaluation stage by another name (Remark 5.2); a language that computes the part-set itself, rather than fragment values, is generative elaboration, staged before normalisation as in Remark 4.5.

Call a composition calculus finitary when its normalisation map, from a finite declaration of parts to a normal form or a defined error, is a total computable function. The calculus of §2 is finitary. Whether the union is well-formed is a finite count (Def 2.3), and Def 4.2 returns that refusal as the map's outcome. On a finite part-set there are finitely many requirements and candidate providers, the structural ranking is a finite computation, and γ gathers finitely many fragments and selects among none. The acyclicity check of §7 is a search of a finite relation. So the whole halts with a normal form or a defined error.

Proposition 5.1 (the embedding, and the placement of the line). Let a calculus be finitary, with a delegation boundary that delegates the normal form to external substrates, and let the substrates include a deterministic universal machine. Such a calculus realises the machine. Take V infinite and decidable, so that it carries a computable coding of machine-input pairs. A declaration carries the machine's program and input as fragments and delegates the transition function across the boundary (§7), so the running artifact is the universal runner applied to the normal form (Remark 7.1). Normalisation is total computable by the definition of finitarity, so the set of declarations whose normalisation returns a normal form is Δ⁰₁. Among the declarations realised on the universal substrate, the set whose operation halts is Σ⁰₁-complete, so operation sits strictly above normalisation in the arithmetical hierarchy. Proof. Machine-input pairs map computably to such declarations, the standard m-reduction from the halting set of a universal machine. Determinism makes "the operation halts" a well-defined predicate of the declaration, and a finite run witnesses it, so the set is Σ⁰₁; were operation decidable, halting would be. The strict inclusion Δ⁰₁ ⊊ Σ⁰₁ is classical. ∎

The proposition is §1's claim made precise. What the system is in form, its composition, is computed from the declaration; whether a realised instance halts is not decidable from it. The two fall on opposite sides of the Δ⁰₁/Σ⁰₁ line. Everything past the delegation boundary belongs to substrates, the realisation of the form as well as the running of what is realised (§7).

Remark 5.2 (scope). Normalisation-finitary is a real restriction. A configuration language that is itself Turing-complete is not finitary, and for it "normalisation" can be undecidable; such a system has, by the criterion of §1, moved that work out of the compositional stratum and into computation, which is exactly where the undecidability lives.

Remark 5.3 (entailment rather than the engineered phase distinction). The decidable half alone is familiar, and so is the engineered way of securing it: strong normalisation gives decidable conversion, and the static phase of a staged or two-level language is kept decidable by stipulation, restricting the language until it terminates [Davies–Pfenning; Nielson–Nielson; Turner-TFP]. Shipped configuration languages adopt exactly this rationale when they bar Turing-completeness outright, making termination a design guarantee [Dhall; CUE; Starlark]. The contribution is the coincidence: the line falls out of order-invariant finitary structure. Computation is not barred to secure it. It is delegated across the boundary of §7, drawn on independent grounds and stated before termination is in question, and normalisation halts because what would not halt is on the far side. A calculus that admits a Turing-complete configuration language takes that work back across the boundary and loses the result (Remark 5.2). And the line falls between composition and operation, where the engineered line falls between type-checking and evaluation.

6 Atemporality: normalisation needs no step-indexing

Program logics for running, self-referential state standardly employ step-indexing, the apparatus of guarded recursion and the later modality ▷, to solve recursive domain equations whose recursion variable occurs negatively and to take fixpoints over non-terminating computation [Iris; America–Rutten; Birkedal et al.]. Normalisation requires none, and the reason is structural. Its carrier admits no negative self-occurrence.

Proposition 6.1 (the carrier is first-order; predicative). The carrier 𝒞 is an ordinary set, presenting no recursive domain equation in which it occurs negatively. Proof. Take the constituents in turn, by Definitions 2.1–2.2 and 2.6. A composite is a triple on a finite, identified, well-formed set of parts. A part is a tuple of an address in 𝒩, a finite set of ports, and a finite fragment map. The wiring W is a finite relation on ports, and the settled values Γ (Def 2.2) a finite map to first-order fragments and finite sets thereof. A port is a tuple over the fixed first-order sets of polarities {!,?}, modes {named, abstract}, names Λ, and references 𝒩. A key is drawn from 𝒦.

Every constituent is therefore built by finite product, coproduct, and the finite-powerset functor over those fixed sets. The calculus has two pointers, a named port's reference and a configuration fragment's target address, and both are first-order (𝒩). Containment is carried by the hierarchical addresses (§2), so a scope is a region of the one flat part-set and no part stores a configuration. The carrier therefore contains no occurrence of itself, and in particular none in a function domain or under a contravariant power. It is first-order: a plain set with no recursive domain equation, defined with no appeal to guarded recursion. (Were scopes instead modelled as parts that nest a composite, the carrier would occur once and covariantly: an ordinary inductive datatype, and a fortiori the initial algebra of a strictly positive finitary functor [Adámek]. Covariant self-reference is harmless and the conclusion is unchanged.) ∎

The distinction turns on variance, and self-reference alone is harmless. A covariant occurrence would be an ordinary inductive datatype. What no set construction solves is a negative occurrence. This yields the framework-independent statement that, for carriers of this section's form, predicativity is the absence of negative self-occurrence, of which "needs no step-indexing" is the same statement relative to one framework.

Normalisation adds no recursion of its own. N ∘ A is a finite composition of total, single-pass, part-preserving functions (§4). Assembly is the order-independent ⊕-fold (Corollary 4.3) and N = bind saturates in one pass (Remark 4.4). N ∘ A is computed once and never approached as a fixpoint, so no well-founded recursion, and a fortiori no step-indexing, is invoked.

To state the predicative/impredicative line as an equivalence rather than a single trigger, write the carrier as a functor of its reference discipline. By Definitions 2.1–2.6 a composite is built from the fixed first-order sets by finite product, coproduct, and finite powerset. Those sets are the addresses 𝒩, the names Λ, the polarities {!,?}, the modes {named, abstract}, and the first-order fragment values. Two codomains join them: the one a named port draws its reference from, and the one a configuration fragment draws its target from (Def 2.1). Both are 𝒩 so far. Only the reference codomain is varied below, the target being the poorer pointer and varying identically (Remark 6.4). Collect the fixed part as a finitary polynomial functor K, strictly positive in its argument. What varies is the reference discipline, which Def 6.2 makes precise as a difunctor. The base calculus draws references from the constant 𝒩. A covariant discipline admits references to sub-configurations. Reflection admits references that are predicates over composites, so a requirement may read "bind to the provider for which P holds of the normal form." The carrier then solves the equation Def 6.2 gives it.

Definition 6.2 (reference discipline). A reference discipline gives the admissible references when the carrier is X. Take it as a difunctor R : Set^op × Set → Set, written R(X⁻, X⁺), generated by R ::= B | X⁺ | (X⁻ → D) | R × R | R + R | 𝒫 R, where B ranges over fixed countable first-order sets, those of §2 among them, D over fixed sets, X⁺ is the covariant carrier argument, and 𝒫 is finite powerset. Both B and D are required nonempty. An empty D would let the classification below call a discipline covariant that is not, since X ↦ (X → ∅) is not covariant; an empty B would let a product carrying a contravariant factor collapse to ∅, and a constant discipline solves its carrier equation whatever the factor was. Product, coproduct, and powerset are covariant, and X⁻ → D is the sole entry at which the carrier occurs contravariantly. Its codomain is fixed because a reference denotes: it picks out a part to wire to, and it does not compute a composite. A discipline drawing references from X⁻ → X⁺ would be a different object, and the reflexive equation D ≅ [D→D] lies outside the grammar for that reason, as the repairs cited above lie outside Set. The carrier equation of R is 𝒞 ≅ K(R(𝒞, 𝒞)), with K the fixed constructor collected above. Call R covariant when its derivation uses no X⁻ → D with |D| ≥ 2, and predicative when its carrier equation has a solution in Set. Covariance is read off a derivation, and no functor admits derivations of both kinds, since the injection of Proposition 6.3(ii) would then apply to it. Every result below quantifies over disciplines generated by this grammar, and over the carrier equations they determine. Def 2.3 reads a reference as a path and Def 4.1 a role as a name, so for a discipline drawing references from anywhere but 𝒩 those definitions need supplementing. Call a discipline resolved when it comes with a total computable interpretation of its references into 𝒩. Satisfaction, well-formedness and binding are then defined as in §2 and §4. The interpretation is required computable because one that is not leaves a normalisation map that is total and not computable, which Prop 6.6 would otherwise count as finitary. Claims about the carrier below hold for every discipline of the grammar; claims about normalisation are stated for the resolved ones.

The obstruction that a contravariant occurrence raises is classical. When a set X must contain a distinct element for each predicate on X, Cantor's theorem is violated, since 2^X then injects into X. The same obstruction arose in domain theory, in the reflexive equation D ≅ [D → D], and the repairs are standard: Scott's inverse-limit domains [Scott], metric-space models [America–Rutten], and guarded solutions in the topos of trees [Birkedal et al.], the last being step-indexing, the apparatus of [Iris]. Each repair solves the equation in a category with more structure than Set. What remains to determine is which reference disciplines of the grammar above raise the obstruction at all.

Proposition 6.3 (predicativity iff covariant references). Let R be a reference discipline (Def 6.2). Its carrier equation has a solution in Set iff R is covariant, and reflection is the minimal discipline of the grammar that is not. (i) Let R be covariant. The diagonal X ↦ K(R(X,X)) is then a finitary covariant endofunctor, and its initial algebra is the colimit of 0 → F0 → F²0 → ⋯ [Adámek]. The carrier is a plain set: non-recursive when R is constant, an inductive datatype when R is covariant-recursive, computed with no guarded recursion either way. (ii) Suppose R uses its contravariant argument into a codomain of size at least 2, as reflection does with R(X⁻, X⁺) ⊇ (X⁻ → 2). The equation is then mixed-variance and the Cantor obstruction above applies. Distinct predicates p : 𝒞 → 2 are distinct references, hence distinct ports, and K injects distinct port-tuples, which gives an injection 2^𝒞 ↪ 𝒞. The carrier equation is read here over the raw solution set rather than over the well-formed carrier, wf being defined only for a resolved discipline (Def 6.2) and extensional reflection admitting no resolution. A solution requires a category with more structure than Set, and the repaired settings cited above supply one. (iii) In the base calculus the carrier enters the equation only through R, every other constituent of K ranging over a fixed first-order set. The least codomain for which the contravariant occurrence obstructs a set solution is 2, the degenerate X⁻ → 1 ≅ 1 being covariant. Reflection is therefore the minimal feature that forces the carrier out of Set. The carrier is predicative iff its reference discipline is covariant, which is the no-negative-occurrence criterion made precise. Proof. (i) A covariant discipline uses only the finite constructors, so the diagonal is finitary and covariant and has an initial algebra [Adámek]. For a resolved discipline the well-formed carrier is a decidable subset of it (Defs 2.3, 2.6), and normalisation is computed once (§4), with no fixpoint approached.

(ii) Fix a port's other fields. Distinct references then give distinct ports, and K injects distinct port-tuples, so (𝒞 → 2) ↪ K(R(𝒞,𝒞)) ≅ 𝒞 and |𝒞| ≥ 2^|𝒞|, which is impossible in Set. Where the contravariant space sits nested under 𝒫, ×, or +, the same injection composes with a singleton or a fixed choice of the other coordinates. For |D| ≥ 2 a two-element subset of D gives (𝒞 → 2) ↪ (𝒞 → D). Guarding yields a contractive functor with a unique fixpoint in the topos of trees [Birkedal et al.].

(iii) Immediate from the grammar, the carrier occurring only within R. ∎

Remark 6.4 (the criterion is field-uniform). Proposition 6.3 varies the reference codomain, but the same criterion governs every field. Each field of a part or configuration (Defs 2.1–2.2) has a codomain through which the carrier may enter; the wiring W and the settled values Γ add no contravariance, being a relation on ports and a map out of the fixed address set. So the carrier is predicative iff no field uses the carrier contravariantly into a codomain ≥ 2. In the base calculus every field but the reference is a fixed first-order set, so the reference is the only field a discipline can non-trivially widen, and reflection is the minimal violation; widening any other field to 𝒞 → 2 (fragment values, say) breaks predicativity identically. The reference is singled out only as the more expressive of the calculus's two cross-part pointers, the natural site for the widening; a target address widened the same way breaks predicativity identically.

The trigger is specifically impredicative reflection, where the predicate ranges over all configurations, including reflective ones. Stratified reflection lets a level-r predicate range only over configurations below level r. Each reference stays first-order in a lower universe, and R stays covariant in the current carrier, since the predicate ranges over a lower universe already fixed. By Proposition 6.3(i) the construction climbs an ordinary hierarchy 𝒞₀ ⊂ 𝒞₁ ⊂ ⋯ with no step-indexing. The cost is that no top level reflects on itself. This is exactly the predicative/impredicative line of type theory. No reflection, or stratified reflection, leaves the carrier predicative and time-free; impredicative reflection forces the recursive domain equation and the temporal apparatus.

Reflection's failure is itself a compositional fact, read from the reference discipline by §1's criterion, deduced and not measured. What fails is the carrier, and predicativity is the condition that secures it. The predicativity result of Proposition 6.1 stands on its own.

The predicativity characterisation now meets the decidable/undecidable line of §5, and the two are not independent.

Proposition 6.5 (the two costs of reflection). A reflective reference admits two readings. On the extensional reading, a reference is an arbitrary predicate p : 𝒞 → 2, the discipline of Proposition 6.3(ii). The carrier equation then has no solution in Set, so predicativity fails, and with no set carrier finitarity fails with it. On the syntactic reading, references are written in finite syntax, so only countably many predicates are expressible. Two stipulations fix that reading: the full syntactic discipline expresses every partial computable predicate, and normalisation evaluates the predicate of every reference it normalises. The contravariant argument then lands in a fixed countable set, R is covariant, and by Proposition 6.3(i) the carrier stays a plain set, so predicativity holds. What fails is halting. The expressible predicates of the full syntactic discipline are arbitrary partial computable functions, and the second stipulation obliges normalisation to run every predicate it meets. A reflective reference's predicate is evaluated on the normal form that the evaluation itself helps determine, so normalisation reads its own output, and its result satisfies a partial computable fixpoint equation in that result, an equation neither shown to have a solution nor shown to have only one. Among the expressible predicates are divergent ones, and a declaration whose reference carries one makes normalisation diverge on it. Finitarity fails either way, since a map that is undefined, multi-valued, or divergent on some declaration is not total computable. Syntactic reflection therefore occupies the same cell as a Turing-complete configuration language (Remark 5.2): predicative and not finitary. A deployed system sits in it. The NixOS module system evaluates a fixpoint in which a module reads the merged configuration it helps determine, and a reference that reads its own output is what makes evaluation diverge there [Dolstra–Löh–Pierron]. On either reading the form is no longer settled by reading its declaration alone. Proof. The extensional half is Proposition 6.3(ii), and a carrier outside Set supports no total computable normalisation map between sets. For the syntactic half, the expressible predicates form a fixed countable set, so R is covariant and Proposition 6.3(i) gives the set carrier; the expressible predicates include divergent partial computable functions, and a declaration whose reference carries one makes normalisation diverge on it. ∎

Proposition 6.6 (finitarity nests in predicativity). A calculus whose reference discipline is of the form above and resolved (Def 6.2) is finitary iff it is predicative and its normalisation map halts on every finite declaration; in particular every finitary calculus is predicative, properly. Proof. (⟹) Let the calculus be finitary. Finitarity makes the normalisation map total computable (§5), hence a function between sets, so both its domain and its codomain are sets. Were the discipline contravariant into a codomain of size at least 2, the carrier equation would have no solution in Set (Proposition 6.3(ii)), and no such sets would exist. On the extensional reading in particular, even the declarations normalisation consumes carry references in 𝒞 → 2, so neither domain nor codomain would be a set. The syntactic reading raises no such obstacle; there declarations stay finite, and Proposition 6.5 shows the cost falls on finitarity instead. So the discipline is covariant, and by Proposition 6.3 the carrier is a set, the predicative case. A total computable map on finite declarations halts. Finitary therefore entails predicative and halting.

(⟸) Let the discipline be predicative and resolved. Then 𝒞 is a set (Proposition 6.3(i)), so normalisation is a genuine function between sets. Its assembly-and-bind core N ∘ A is a finite composition of total part-preserving steps (§4). Finitarity is the further condition that the whole map halts on every finite declaration, the evaluation stage applied to the declarations' fragments included (§5). The normalisation map is then total computable, hence finitary.

(Properness) Predicativity does not give halting on its own. A predicative calculus may carry a normalisation stage that diverges with no contravariant occurrence of the carrier: a Turing-complete configuration language (Remark 5.2), whose references are drawn from 𝒩 itself, so the interpretation is the identity and the discipline is resolved. Its carrier stays a first-order set, yet normalisation need not halt: predicative and not finitary. Syntactic reflection diverges the same way (Proposition 6.5), and its interpretation is partial rather than total, so it lies outside the resolved class quantified over here. ∎

The proper gap between the finitary and the predicative classes holds exactly the halting-only failures, of which syntactic reflection and the Turing-complete configuration language are the two exhibited (Propositions 6.5, 6.6; Remark 5.2).

7 Realisation, operation, and the delegation boundary

A normal form specifies a system completely and canonically. Running the specified system is a further act. Two stages are delegated across the delegation boundary (§1) to substrates the calculus treats as external oracles.

Realisation directs a substrate to make the form actual (build an image, provision a resource, register each part). Operation is the running of the realised system. Normalisation settles the form, realisation makes an instance of it, and operation runs that instance. Both lie past the delegation boundary, and they differ in kind. Realisation is the substrate's making of the system; operation alone is the system's own act. The delegation boundary is what makes the calculus applicable to real systems.

The substrate builds what the declaration specifies. Past the operation point the instance's running is its own, and the calculus says nothing about it. The two sides of that point differ in what is counted. The form is one and is normalised once; instances are many, and each instance crosses into operation separately. Realisation is the step that produces an instance from the one form, and §5 places the running of that instance beyond decision.

A substrate is an opaque relation from normal-form regions to outcomes. Determinism is not assumed of it, since runtime nondeterminism is what the delegation boundary exists to delegate. The calculus is parametric in the available substrates. Which substrate realises a part is itself declared data, a configuration fragment like any other, and it drives the dispatch.

Realisation is itself an assembly, of the instance rather than the form, and it needs an order, which ⊕ does not carry. The order it needs is fixed by the form. A required port wired to a provided one puts the provider before the consumer, so the wiring induces a dependency relation on the parts, and the schedule is any linear extension of it. Its reverse governs teardown. The form determines that relation completely and leaves free exactly the orderings between parts that depend on neither, which a substrate may take in either order or at once. A collector's presentation is delegated the same way. The form carries each contributed fragment with its source address and imposes no order on the set (Def 2.3), so a substrate that concatenates them fixes an ordering convention of its own, computed from those sources.

A wiring may close a loop, and then no linear extension exists. Whether it does is decidable by reading, so it is settled at normalisation rather than discovered when a schedule is drawn: a declaration whose dependency relation is cyclic yields a defined error and no normal form, as a dangling fragment does (Def 2.3).

A double provision is refused earlier and by a different route. Each satisfaction is a property of a requirement and a part alone (Def 2.3), and no wider union takes a satisfier away, so a second satisfier, once present, stays. wf counts satisfiers, and ⊕ is undefined on a union that holds two: the composition never happens. A cycle admits no such test. It is a property of the whole derived wiring, where wf counts satisfactions that are themselves pair-local and is downward closed for that reason (Lemma 2.4), which is the locality Proposition 3.3's proof reads. Putting both under one name would make wf two conditions of different kinds. An early check would also refuse too much. bind adds edges (§4), and a disjoint frame can re-rank a binding (Prop 4.8), so an edge that closes a loop in one composite need not survive into the normal form of a wider union. The check therefore falls after binding, on the assembled whole, on the normal form the composite would otherwise have been.

A normal form may still carry open required ports, so a composition is legitimately partial: complete as a specification, partial as a closed system.

The normal form of Example 4.6 realises region by region. data/store goes to a key-value process listening at 127.0.0.1:7000 and holding the records its collector settled, service to an HTTP server on port 8080 serving that store, and seed to a one-shot writer that opens the store and writes its first key. data and catalog go to nothing, their fragments already settled into Γ. The schedule is any linear extension of the wiring, a provider before its consumer. The substrate is opaque to the calculus here. The same normal form could be realised by clerks keeping a ledger and answering queries by hand, or by a mix of process and clerk, and ⊕ could not tell which, realisation lying wholly on the far side of the delegation boundary. Which substrate realises a region lies beyond the form.

Remark 7.1 (the run as operation stage). The delegation boundary is also where the undecidability of Proposition 5.1 enters. A machine's description is itself a realised form, so a normal form whose region delegates a transition function to a universal substrate realises a universal machine. Write N ∘ A for the normalisation map of §4 and U for the universal runner the substrate supplies. The artifact is M = U((N ∘ A)(S)), and (N ∘ A)(S) is the determinate description, fixed without running. So a machine's run is the operation stage of the composed system whose description normalisation fixed.

8 The parallel complement to the sequential calculus

The immediate neighbour is the composition calculus of Fettke and Reisig [Fettke–Reisig], whose operator is the sequential one, modules joined end-to-end through directed interfaces, a non-commutative, cancellative algebra generalising concatenation. Fettke and Reisig isolated the calculus of the sequential mode. This paper isolates the calculus of the parallel one, which is the mode that settles a form. Their claim, and their title, is that the sequential operator composes modules once and for all. The disagreement here is with the scope of that claim and with nothing inside it. They isolated the sequential mode and axiomatised it, and that stands. The parallel mode is a second mode of module composition, and Proposition 8.2 shows that no restriction of their operator reproduces ⊕ under any encoding this section quantifies over. Their own diagnosis marks the border. They found by-name merging non-associative and read that failure correctly, and Remark 8.1 locates it in the pairwise merge rather than in by-name matching, so the road they turned back from is the one this calculus takes.

Fettke and Reisig reached the sequential operator by rejecting a by-name merge that is not associative. When three modules share a label, a pairwise merge internalises and consumes the first match, so the result depends on the bracketing. ⊕ is a different by-name operator that avoids exactly this. Feature algebra gives an independent instance of the same diagnosis [Apel–Lengauer–Möller–Kästner]. Its superimposition merges tree nodes by name, keeps each merged node available to a later merge, and is associative. It is not commutative, because overlapping terminals are merged in the order of composition, and its authors note that forbidding that overlap would make it commutative. In both calculi a by-name merge that consumes no match is associative, and they part on whether overlap is ordered or refused. Re-deriving the wiring on the whole union (Def 2.5) consumes no match, so a shared name normalises identically under any bracketing; and a requirement with two providers, the genuinely ambiguous case, is refused under uniqueness-or-error rather than wired order-dependently. So the form's side has a by-name operator, and interaction survives it. The price is that ambiguity is refused where the pairwise merge would silently choose within it. (A shared name that fans in to one provider is wired by re-derivation; one that fans out to two providers is the refused case, where associativity holds in the partial-monoid sense, both bracketings being equally undefined.)

Remark 8.1 (why the pairwise merge fails). The failure Fettke and Reisig found is structural, and their diagnosis is correct. A pairwise merge consumes its match, so the bracketing decides which match is consumed first, and the result depends on the bracketing. Order is what their operator carries and ⊕ does not: a pairwise merge takes its order from the bracketing, and a re-derivation over the whole union has no bracketing to take one from. By-name normalisation belongs before the normalisation point, to the system as declared, and no order exists there to import. Theorem 3.1's associativity turns on exactly this choice, and the pairwise merge shows the property is lost without it.

Proposition 8.2 (no commutative restriction of the sequential operator is ⊕). A positional sequential operator is commutative on a pair of parts exactly where they do not interact, that is, where their interface labels are disjoint and the composition is mere juxtaposition. This is Fettke and Reisig's own commutativity criterion [Fettke–Reisig, Thm 5]. Their operator commutes on a pair, M·N and N·M being interface-equivalent, iff M and N are not entangled, where entangled means sharing a gate label (their Def 12). Their commutativity is taken up to interface equivalence throughout, and ⊕'s holds on the nose; the argument below uses only the failure of their commutativity, which the weaker notion already gives. ⊕, by contrast, is commutative wherever it is defined. Its domain includes pairs that do interact through a single-provider wiring, and it refuses the multi-provider case. Under any encoding identifying parts with modules, and shared names and matched references with shared gate labels, the sequential operator's commutativity regime excludes every pair ⊕ wires. Proof. Suppose, under such an encoding, that ⊕ were the restriction of the sequential operator to a sub-domain D on which the latter is commutative. Then D would contain no interacting pair, the sequential operator being non-commutative on those. But every wired composite of ⊕ is an interacting pair, so ⊕'s wiring could never arise on D. Hence no commutative restriction of the sequential operator reproduces ⊕. ∎

The broader claim, that ⊕ is no fragment of the sequential operator under any encoding, is argued rather than proved: simulating by-name matching inside a positional operator demands a global gate-index assignment, which destroys the locality the frame property rests on (Prop 3.3). A sequentialisation of a normal form is any linear extension of its dependency relation (§7), one form to many sequences with none canonical; a functor would have to select one, and no selection is canonical. A formal non-embedding awaits both operators in one setting, the question left unanswered in §10.

Compare Moller's theorem that the parallel merge of CCS has no finite equational axiomatisation over the sequential operators without auxiliary operators [Moller; Milner–Moller], a far stronger result about bisimulation congruence, and a separation of the two modes reached in a different setting. Process algebra's expansion law, which appears to express a finite parallel composition through sequential composition and choice, is no counterexample. It is a schema, one instance per pair of head normal forms, infinitely many equations rather than a finite axiomatisation; and the finite axiomatisations that do exist adjoin exactly those auxiliary operators, the left and communication merges, which Moller's result shows cannot be finitely eliminated. Exhibiting a formal functor relating the two settings would still illuminate; in process algebra the reductive claim is settled in the negative [Moller].

9 Related work

The separating monoid, the frame property, and the sequential/parallel complementarity are each prior art. The separating monoid and the frame property come from separation logic [Reynolds; O'Hearn; Calcagno–O'Hearn–Yang]. The categorical accounts of interconnection by gluing along shared interfaces pair a sequential product with a parallel one: hypergraph categories, structured cospans [Baez–Courser], and wiring-diagram operads [Spivak]. Against the gluing accounts, ⊕ is deliberately the separating counterpart, connecting without merging. The new element is the re-derivation of the binding relation from required-to-provided name normalisation under a uniqueness-or-error discipline, where trace theory takes the independence relation as primitive and separation logic takes the resource keys as given. Earnshaw, Nester, and Román type the trace's actions. Each action carries declared inputs and outputs rather than a bare name, and the traces so typed present effectful categories, with a commuting tensor of the free ones [Earnshaw–Nester–Román-Traces]. The typing governs the sequencing while the commutations come from elsewhere, from the presentation within a system and from the commuting tensor they construct across two systems; ⊕ derives the wiring from the names and refuses the double provision.

Closest by aim is institutional model theory [Goguen–Burstall], which treats any logical system abstractly and composes theories within one. Signatures glue by colimit and the satisfaction condition holds truth invariant under the gluing, composition prior to and untouched by interpretation. It works a level above this calculus and leaves the gluing abstract, where ⊕ composes parts within one flat carrier by name normalisation and settles the result under a uniqueness-or-error discipline; the shared shape is composition-before-interpretation, the difference is the level of abstraction and the determinacy.

Several mechanisms sit closer, and each differs. Module systems with by-name linking include MixML [Dreyer–Rossberg], which is directional and non-commutative where ⊕ is commutative, and Ancona–Zucca's confluent module-operator calculus [Ancona–Zucca], oriented to type soundness and not to a separating monoid. Backpack, MixML's descendant, comes closer [Kilpatrick et al.]. Its mixin-linking pass computes a wiring diagram over a whole unit, matching requirements against provisions and permitting unfilled holes, with no separating monoid or frame property proved of it. On the securing discipline, the nearest prior is the trait. A trait sum flattens its operands into one whole, and a method defined by two operands is an error the composer must normalise rather than a silent override, so the sum is commutative and associative [Schärli et al.; Ducasse et al.]. Two of the four clauses are therefore two decades old, and they were adopted there for the reason given here, that a composite computed from the whole imports no order from its bracketing. Traits carry no addresses, so no part plays a resource and no separating monoid arises. They carry no configuration at all, so an algebra of settled values under the same discipline is not in question. No frame property is available to them, the flattening reading the whole composite where the frame property holds of a wiring relation preserved under extension. On the by-name axis, the nearest priors are two formalisations of by-name combination. Bracha's Jigsaw merge [Bracha] is a commutative and associative by-name combination of modules with definition conflicts as errors, but it binds by fixpoint over a shared name space, with no wiring relation, no addresses, and no frame property. Cardelli's linkset merge [Cardelli] is a by-name link operation proved confluent and terminating under an export-disjointness partiality, but binary and substitution-consuming, and it states no associativity law, frame property, or algebra of settled values.

By mechanism, the nearest prior is the unification of a configuration language: CUE combines values commutatively, associatively and idempotently over a lattice, order-independently by construction, with conflict as an error [CUE]. The combination is total where ⊕ is partial, it unifies values where ⊕ derives a wiring relation between declared ports, and addresses are not resources it composes, so no separating monoid or frame property arises. So an associative by-name operator has precedent. The clauses of the securing discipline have precedent, in traits above all, and the symmetric concatenation of record calculi refused a conflict earlier still [Harper–Pierce]. The NixOS module system carries the clauses over addressed parts already: independent modules contribute to hierarchically addressed option paths, the merge is order-independent, an option that does not merge and is defined twice is an error, and list-typed options collect losslessly [Dolstra–Löh–Pierron]. It meets a double definition by priority, discarding all but the lowest value and refusing only on a tie, which is the ranking Prop 4.8 prices. What no prior mechanism has is the discipline as a proved algebra, refusing where that one ranks, over parts that are address-disjoint resources. That is what makes the monoid separating, and it makes the derived form frame-local in both its halves, the wiring and the settled values, each of them governed by one uniqueness-or-error (Prop 3.3). The separating monoid, the frame property, and the delegation boundary come with the discipline, the first an instantiated standard shape, the last an architectural stance. Two engineering practices remain, dependency injection [Fowler] and a linker's global symbol resolution, and ⊕ gives proved laws to the pattern both exhibit, no encoding of either being offered here. A linker resolves in one pass over a flat table. Compile-time injection does more, computing the binding graph from the union of the declared modules, taking qualifiers as keys, refusing a duplicate binding, and collecting multibindings losslessly, which is the two fragment kinds again. What none of them carries is an associativity law, a frame property, an algebra of settled values, or a delegation boundary. The Concurrent Views Framework [Dinsdale-Young et al.] layers a reification map over a commutative resource monoid, the nearest analogue of wiring-over-a-monoid with a delegation boundary, but its extra structure is interference for concurrency soundness, where ⊕'s is static by-name wiring.

Feature-oriented software development composes features by superimposition, merging feature structure trees by matching nodes' names and types [Apel–Lengauer–Möller–Kästner; Apel–Kästner–Lengauer]. Its introduction sum, also written ⊕, is associative and idempotent, and it is not commutative, because overlapping terminals are merged by language-specific rules. Free assembly refuses the overlap (§8). Two parts at one address do not compose and a key configured twice is refused, so the operator commutes, and an idempotent composition cannot cancel, since i ⊕ i = i ⊕ ξ would give i = ξ. Refinement survives the choice and moves to the receiving part. A part that accepts refinement keeps a collector, every contribution addressed to it is kept with its source (Def 2.3), and the precedence among them is a rule the receiver applies to the collected set, which stays order-independent. In feature composition the later feature overrides, and the result depends on the order in which features are composed. Superimposition merges structure and derives no wiring between parts.

Delta-oriented programming applies deltas that add, modify and remove program elements by name, in an order a partial order constrains [Schaefer et al.]. A product line is unambiguous when every compatible total order yields the same product, a property checked of each product line [Schaefer–Bettini–Damiani]. Here order-independence holds of every composite (Corollary 4.3), a conflict that a delta product line resolves by ordering is refused, and deltas that remove form no cancellative monoid.

On uniqueness of the normal form, the unique-decomposition theory for partial commutative monoids [Milner–Moller; Luttik–van Oostrom] is the structural twin; ⊕'s unique normal form comes from global name-matching (Corollary 4.3). A decomposition order plays no role, and the strict-compatibility and Archimedean conditions of that theory are not assumed, so the distinction is the mechanism. Decomposition itself is settled by Corollary 3.4, the indecomposables being the singletons and the decomposition unique. In the operadic setting a wiring diagram is already a normal form because the symmetric-monoidal laws hold on the nose [Patterson–Spivak–Vagner]; ⊕'s determinacy is instead a fact about computed wiring (Corollary 4.3). The delegation boundary is in the lineage of functorial semantics [Lawvere]. Coordination languages (Reo [Arbab], BIP) and the process calculi (CCS/CSP/π) carry by-name parallel composition too, but on the behavioural, runtime side; ⊕ is their static counterpart.

The categorical setting for two interacting composition products, one sequential and one parallel, is the duoidal (2-monoidal) category [Aguiar–Mahajan]. Its interchange is generally non-invertible, and recent work uses that for an explicit account of sequential-versus-parallel process composition [Cranch–Struth; Earnshaw–Hefford–Román]. Concurrent Kleene algebra's exchange law is its order-theoretic ancestor [Hoare–Möller–Struth–Wehrman]. Read against §1, the pairing is a pairing of the two modes. The sequential product is the one that carries order, the parallel product the one that settles a form, and the interchange is where the two meet. ⊕ is the partial, separating parallel product of that pairing, and its normaliser is by-name binding under uniqueness-or-error. The duoidal and produoidal accounts work with total products and a unit-coincidence normalisation, where this calculus has a partial separating tensor and a by-name binding step. None of that structure is claimed here; §3 treats (𝒞, ⊕, ∅) directly as a partial commutative monoid.

Earnshaw, Nester, and Román have since axiomatised the partial case, monoidal categories graded by a partial commutative monoid, where each morphism carries a grade and the tensor of two morphisms is defined exactly when their grades combine [Earnshaw–Nester–Román]. The gradings they single out as well behaved are the cancellative ones, the class in which Theorem 3.1 places (𝒞, ⊕, ∅). The roles differ. There the monoid grades a category of processes; here the monoid is the carrier, the composed configurations, with the wiring layered over it (§3).

The phenomenon of §1, boxes wired to boxes before the system exists, is the subject of architecture description languages, which formalise a system from its components and connectors [Medvidovic–Taylor]. These are closest to the motivation here, and they typically carry no proved-law operator, no confluent normalisation, and no delegation boundary. Among practical systems, purely-functional deployment normalises a declared composition to a normal form before realising it, which is the normalise-before-run pattern of §5 [Dolstra]. Nix and Bazel work this way, and each is a single substrate scoped to build and configuration, and ⊕ generalises the pattern to substrate-agnostic composition across all planes, with an explicit parallel operator and proved laws. Declarative infrastructure tools, Terraform, Helm, and Crossplane, likewise normalise before applying, but on a single plane and, for the platform-bound ones, a single platform; the present calculus spans planes and treats such tools as substrates across the delegation boundary.

10 Conclusion and scope

The contribution is two properties of by-name parallel composition and the discipline that secures them. The discipline has four clauses in two pairs. The first pair yields associativity (Theorem 3.1, Remark 8.1), and with it determinate normalisation (Corollary 4.3). The composite is a function of the union, so it cannot depend on the order its parts arrived in; and an unmet requirement is permitted, which leaves well-formedness downward closed, the hypothesis Remark 3.6 names. The second pair yields the frame property (Prop 3.3). Candidacy is a property of the requirement–part pair alone, so no ambient set enters a derived edge; and ambiguity is refused. A discipline that met a double provision by ranking the candidates would be determinate too, and it would re-rank when a disjoint frame supplied a better one, exactly as binding does (Prop 4.8), so no established wiring would survive extension. Refusal also leaves γ nothing to discard, which is why the settled values of anything that normalises determine the fragments they came from (Prop 3.2). Cancellation follows from disjointness of the operands. The algebra is a cancellative partial commutative monoid in the sense of separation algebras, and the frame property holds of the wiring and of the settled values alike. The two characterisations nest. The finitary class, on which normalisation and operation split across the decidable/undecidable line, lies properly inside the predicative class, and reflection is the exit the calculus's own pointers afford (Propositions 5.1, 6.3, 6.6, and Remark 6.4 on what else a widened field would do). ⊕ is the parallel complement to the sequential calculus of Fettke and Reisig (Prop 8.2), and the delegation boundary is the claim's scope (§7).

The scope is exactly the concessions of §1. Prop 8.2 is proved for the encodings it quantifies over, by a model-theoretic argument that exhibits no refused functor; the question of a functor relating the two settings is unanswered. Earnshaw, Nester, and Román propose, as a direction, grading by a "partial duoid", grades combining partially under both the sequential and the parallel product [Earnshaw–Nester–Román]. A graded setting with exactly those two partial products is one in which that question could be posed. Its two partial products are the two strata's algebras.

Conjecture 10.1 (partial-duoid interchange). The two products are these. The parallel product is ⊕ on the composites, the cancellative partial commutative monoid of Def 2.5 and Theorem 3.1. The sequential product is the composition of modules of [Fettke–Reisig], written · as in Prop 8.2. An encoding of the kind Prop 8.2 quantifies over brings it to one carrier, identifying parts with modules, and shared names and matched references with shared gate labels. A partial duoid is read here as one set bearing both partial monoid structures, the parallel one commutative, related by an oriented interchange law: whenever a ⊕ b, c ⊕ d, and (a ⊕ b) · (c ⊕ d) are defined, then a · c, b · d, and (a · c) ⊕ (b · d) are defined and the two composites are equal. The orientation runs from sequential composition of parallel pairs to parallel composition of sequential pairs, the direction of the duoidal interchange [Aguiar–Mahajan] and of concurrent Kleene algebra's exchange law [Hoare–Möller–Struth–Wehrman]. [Earnshaw–Nester–Román] propose the partial duoid as a direction and do not develop it, so this reading is one candidate transcription, and the unit coherences are left aside.

Under no such encoding do ⊕ and · satisfy the law, in this orientation or its reverse. Nothing here establishes that. The expected obstructions are the two §8 locates. Re-derivation on the right side is global and can meet a double provision that the split on the left keeps apart, a requirement in a with one provider in b and another in d, so the right side need not be defined where the left side is. A match consumed by · on one side can be wired otherwise by ⊕ on the other, so where both sides are defined the composites can still differ. Whether a restriction of · to the quadruples on which consumption and re-derivation agree remains a partial monoid, and whether its pair with ⊕ then satisfies the law, is open. The established results end earlier. Prop 8.2 shows that no commutative restriction of · is ⊕, and the non-embedding of §8 is argued rather than proved.

The conjecture is where the unexhibited functor of §8 would live. A functor from the parallel setting to the sequential one must choose a sequentialisation of each form, and §7 gives one form many schedules with none canonical, so a functor would have to select one. In a category graded by such a duoid no schedule need be chosen. Both products belong to one structure, and the comparison between the two modes is the interchange family itself, one instance per quadruple. Confirmed, the conjecture would give the argued non-embedding formal support beyond Prop 8.2. Refuted, it would make the complementarity of §8 a structure, the two calculi the two products of one partial duoid.

Further directions of the calculus itself include dynamic reconfiguration, mobility, and failure, each a run-time matter or a succession of recompositions rather than a move of ⊕. One direction lies on the theory rather than the calculus. Impredicative reflection is repairable at the ω-indexed level of the topos of trees (Proposition 6.3), and whether a graded family of reflective features induces a transfinite hierarchy of indexing heights is left unanswered [Svendsen–Sieczkowski–Birkedal].

The concessions of §1 describe the class the results characterise. The calculus applies to the systems its own condition picks out, and the theorems draw the consequences of that condition rather than those of a class independently arrived at. A system has a compositional layer this calculus captures exactly when it is finitary: a finite composition of interface-bearing parts (§2) whose form is settled by its declaration and read from it, its normalisation halting (§5). The properties named separately above are facets of this one condition rather than independent restrictions. Finiteness and a halting normalisation are its finitary clause; deduced, not measured is that same criterion; and predicativity, freedom from negative self-occurrence, follows by Proposition 6.6, finitarity entailing it.

The condition is therefore single, and it fails in three ways. A Turing-complete configuration language breaks termination (Remark 5.2). Wiring that turns on runtime values breaks the deduced-not-measured clause (§1, §4). Reflection breaks predicativity on the extensional reading, by leaving no carrier, and termination on the syntactic one (Propositions 6.3, 6.5). Each costs the purely compositional layer. The class so drawn is narrow in principle. It holds the systems that can be specified before they are built, and how much of what is deliberately constructed falls inside it is not a question this paper settles. Outside it are the systems whose form is settled only in the course of their making, of which the calculus claims nothing.

References

• [Adámek] J. Adámek. Free Algebras and Automata Realizations in the Language of Categories. Commentationes Mathematicae Universitatis Carolinae 15(4):589–602, 1974. (initial algebra of a finitary functor as the colimit of the initial chain)
• [Aguiar–Mahajan] M. Aguiar, S. Mahajan. Monoidal Functors, Species and Hopf Algebras. CRM Monograph Series 29, American Mathematical Society, 2010.
• [America–Rutten] P. America, J. Rutten. Solving Reflexive Domain Equations in a Category of Complete Metric Spaces. Journal of Computer and System Sciences 39(3):343–375, 1989. doi:10.1016/0022-0000(89)90027-5.
• [Ancona–Zucca] D. Ancona, E. Zucca. A Calculus of Module Systems. Journal of Functional Programming 12(2):91–132, 2002. doi:10.1017/S0956796801004257.
• [Apel–Kästner–Lengauer] S. Apel, C. Kästner, C. Lengauer. FeatureHouse: Language-Independent, Automated Software Composition. ICSE 2009, pp. 221–231. doi:10.1109/ICSE.2009.5070523.
• [Apel–Lengauer–Möller–Kästner] S. Apel, C. Lengauer, B. Möller, C. Kästner. An Algebra for Features and Feature Composition. AMAST 2008, LNCS 5140, pp. 36–50. doi:10.1007/978-3-540-79980-1_4. (introduction sum a non-commutative idempotent monoid; commutativity given up to permit the superimposition of terminals)
• [Arbab] F. Arbab. Reo: A Channel-based Coordination Model for Component Composition. Mathematical Structures in Computer Science 14(3):329–366, 2004. doi:10.1017/S0960129504004153.
• [Baez–Courser] J. C. Baez, K. Courser. Structured Cospans. Theory and Applications of Categories 35(48):1771–1822, 2020.
• [Birkedal et al.] L. Birkedal, R. E. Møgelberg, J. Schwinghammer, K. Støvring. First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees. Logical Methods in Computer Science 8(4:1), 2012. doi:10.2168/LMCS-8(4:1)2012.
• [Bracha] G. Bracha. The Programming Language Jigsaw: Mixins, Modularity and Multiple Inheritance. PhD thesis, University of Utah, 1992. (a by-name module merge proved commutative and associative, with definition conflicts as errors)
• [Calcagno–O'Hearn–Yang] C. Calcagno, P. W. O'Hearn, H. Yang. Local Action and Abstract Separation Logic. LICS 2007, pp. 366–378. doi:10.1109/LICS.2007.30.
• [Cardelli] L. Cardelli. Program Fragments, Linking, and Modularization. POPL 1997, pp. 266–277. doi:10.1145/263699.263735. (a by-name linkset merge under export-disjointness, proved confluent and terminating)
• [Church–Rosser] A. Church, J. B. Rosser. Some Properties of Conversion. Trans. AMS 39(3):472–482, 1936. doi:10.1090/S0002-9947-1936-1501858-0. (the normal form of the rewriting tradition: unique, and reached in any order)
• [Cranch–Struth] J. Cranch, G. Struth. Interacting Monoidal Structures with Applications in Computing. arXiv:2411.03821, 2024.
• [CUE] M. van Lohuizen et al. CUE: Configure, Unify, Execute. cuelang.org, 2018–. (lattice/unification-based configuration; order-independent, conflict-is-error)
• [Davies–Pfenning] R. Davies, F. Pfenning. A Modal Analysis of Staged Computation. Journal of the ACM 48(3):555–604, 2001. doi:10.1145/382780.382785.
• [Dhall] The Dhall configuration language. Language standard, dhall-lang.org, 2017–. (a total, non-Turing-complete configuration language; guaranteed termination as design rationale)
• [Dinsdale-Young et al.] T. Dinsdale-Young, L. Birkedal, P. Gardner, M. Parkinson, H. Yang. Views: Compositional Reasoning for Concurrent Programs. POPL 2013, pp. 287–300. doi:10.1145/2429069.2429104.
• [Dockins–Hobor–Appel] R. Dockins, A. Hobor, A. W. Appel. A Fresh Look at Separation Algebras and Share Accounting. APLAS 2009, LNCS 5904, pp. 161–177. doi:10.1007/978-3-642-10672-9_13.
• [Dolstra] E. Dolstra, M. de Jonge, E. Visser. Nix: A Safe and Policy-Free System for Software Deployment. LISA 2004, pp. 79–92.
• [Dolstra–Löh–Pierron] E. Dolstra, A. Löh, N. Pierron. NixOS: A Purely Functional Linux Distribution. Journal of Functional Programming 20(5–6):577–615, 2010. doi:10.1017/S0956796810000195; ICFP 2008, pp. 367–378. (configuration fragments merged from independent modules onto hierarchically addressed option paths; a non-mergeable option defined twice is an error; list-typed options accumulate; priorities rank)
• [Dreyer–Rossberg] D. Dreyer, A. Rossberg. Mixin' up the ML Module System. ICFP 2008, pp. 307–320, doi:10.1145/1411204.1411248; journal version A. Rossberg, D. Dreyer, ACM TOPLAS 35(1):2, 2013, doi:10.1145/2450136.2450137.
• [Ducasse et al.] S. Ducasse, O. Nierstrasz, N. Schärli, R. Wuyts, A. P. Black. Traits: A Mechanism for Fine-Grained Reuse. ACM Transactions on Programming Languages and Systems 28(2):331–388, 2006. doi:10.1145/1119479.1119483.
• [Earnshaw–Hefford–Román] M. Earnshaw, J. Hefford, M. Román. The Produoidal Algebra of Process Decomposition. CSL 2024, LIPIcs vol. 288, art. 25. doi:10.4230/LIPIcs.CSL.2024.25. arXiv:2301.11867.
• [Earnshaw–Nester–Román] M. Earnshaw, C. Nester, M. Román. Monoidal Categories Graded by Partial Commutative Monoids. arXiv:2603.16375, 2026. (the tensor of morphisms defined when their grades combine in the grading monoid; cancellative monoids as the well-behaved gradings; a "partial duoid" grading proposed as a direction)
• [Earnshaw–Nester–Román-Traces] M. Earnshaw, C. Nester, M. Román. Resourceful Traces for Commuting Processes. CSL 2026, LIPIcs vol. 363, art. 28. doi:10.4230/LIPIcs.CSL.2026.28. arXiv:2507.18246. (Mazurkiewicz traces with typed actions presenting effectful categories; the commuting tensor product of free ones)
• [Fettke–Reisig] P. Fettke, W. Reisig. Once and for all: how to compose modules — The composition calculus. ISoLA 2024, LNCS 15220, Springer, pp. 173–190. arXiv:2408.15031.
• [Fowler] M. Fowler. Inversion of Control Containers and the Dependency Injection pattern. 2004.
• [Goguen–Burstall] J. A. Goguen, R. M. Burstall. Institutions: Abstract Model Theory for Specification and Programming. Journal of the ACM 39(1):95–146, 1992. doi:10.1145/147508.147524. (any logical system treated abstractly; theories glue by signature colimit, the satisfaction condition holding truth invariant under change of notation)
• [Harper–Pierce] R. Harper, B. Pierce. A Record Calculus Based on Symmetric Concatenation. POPL 1991, pp. 131–142. doi:10.1145/99583.99603. (commutative record merge with conflict refused)
• [Hoare–Möller–Struth–Wehrman] C. A. R. Hoare, B. Möller, G. Struth, I. Wehrman. Concurrent Kleene Algebra. CONCUR 2009, LNCS 5710, Springer, pp. 399–414. doi:10.1007/978-3-642-04081-8_27.
• [Iris] R. Jung, R. Krebbers, J.-H. Jourdan, A. Bizjak, L. Birkedal, D. Dreyer. Iris from the Ground Up: A Modular Foundation for Higher-Order Concurrent Separation Logic. Journal of Functional Programming 28:e20, 2018. doi:10.1017/S0956796818000151.
• [Kilpatrick et al.] S. Kilpatrick, D. Dreyer, S. Peyton Jones, S. Marlow. Backpack: Retrofitting Haskell with Interfaces. POPL 2014, pp. 19–31. doi:10.1145/2535838.2535884. (mixin linking computes a wiring diagram over a whole unit; holes may go unfilled)
• [Lawvere] F. W. Lawvere. Functorial Semantics of Algebraic Theories. PhD thesis, Columbia University, 1963.
• [Luttik–van Oostrom] B. Luttik, V. van Oostrom. Decomposition Orders—Another Generalisation of the Fundamental Theorem of Arithmetic. Theoretical Computer Science 335(2–3):147–186, 2005. doi:10.1016/j.tcs.2004.11.019.
• [Medvidovic–Taylor] N. Medvidovic, R. N. Taylor. A Classification and Comparison Framework for Software Architecture Description Languages. IEEE Transactions on Software Engineering 26(1):70–93, 2000. doi:10.1109/32.825767.
• [Milner–Moller] R. Milner, F. Moller. Unique Decomposition of Processes. Theoretical Computer Science 107(2):357–363, 1993. doi:10.1016/0304-3975(93)90176-T.
• [Moller] F. Moller. The Nonexistence of Finite Axiomatisations for CCS Congruences. LICS 1990, pp. 142–153. doi:10.1109/LICS.1990.113741.
• [Nielson–Nielson] F. Nielson, H. R. Nielson. Two-Level Functional Languages. Cambridge University Press, 1992.
• [O'Hearn] P. W. O'Hearn, J. C. Reynolds, H. Yang. Local Reasoning about Programs that Alter Data Structures. CSL 2001, LNCS 2142, pp. 1–19. doi:10.1007/3-540-44802-0_1.
• [Oliveira et al.] B. C. d. S. Oliveira, T. Schrijvers, W. Choi, W. Lee, K. Yi. The Implicit Calculus: A New Foundation for Generic Programming. PLDI 2012, pp. 35–44. doi:10.1145/2254064.2254070. (scope-directed implicit resolution: nearest scope wins, ambiguity within it an error)
• [Parnas] D. L. Parnas. On the Criteria To Be Used in Decomposing Systems into Modules. CACM 15(12):1053–1058, 1972. doi:10.1145/361598.361623. (information hiding: a module seals an internal secret behind its interface)
• [Patterson–Spivak–Vagner] E. Patterson, D. I. Spivak, D. Vagner. Wiring Diagrams as Normal Forms for Computing in Symmetric Monoidal Categories. ACT 2020, EPTCS 333:49–64, 2021. doi:10.4204/EPTCS.333.4. arXiv:2101.12046.
• [Pitts] A. M. Pitts. Nominal Sets: Names and Symmetry in Computer Science. Cambridge University Press, 2013. doi:10.1017/CBO9781139084673. (names as atoms bearing only equality; equivariance).
• [Reynolds] J. C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. LICS 2002, pp. 55–74. doi:10.1109/LICS.2002.1029817.
• [Schaefer et al.] I. Schaefer, L. Bettini, V. Bono, F. Damiani, N. Tanzarella. Delta-Oriented Programming of Software Product Lines. SPLC 2010, LNCS 6287, pp. 77–91. doi:10.1007/978-3-642-15579-6_6.
• [Schaefer–Bettini–Damiani] I. Schaefer, L. Bettini, F. Damiani. Compositional Type-Checking for Delta-Oriented Programming. AOSD 2011, pp. 43–56. doi:10.1145/1960275.1960283. (unambiguity: every total order compatible with the application order yields the same product)
• [Schärli et al.] N. Schärli, S. Ducasse, O. Nierstrasz, A. P. Black. Traits: Composable Units of Behaviour. ECOOP 2003, LNCS 2743, Springer, pp. 248–274. doi:10.1007/978-3-540-45070-2_12. (a flattening sum, commutative and associative, with a doubly defined method an error)
• [Schrijvers et al.] T. Schrijvers, B. C. d. S. Oliveira, P. Wadler, K. Marntirosian. COCHIS: Stable and Coherent Implicits. Journal of Functional Programming 29:e3, 2019. doi:10.1017/S0956796818000242. (coherence and stability under type substitution for nested implicit scoping)
• [Scott] D. S. Scott. Continuous Lattices. In F. W. Lawvere (ed.), Toposes, Algebraic Geometry and Logic, Lecture Notes in Mathematics 274, Springer, 1972, pp. 97–136. doi:10.1007/BFb0073967. (the reflexive domain D ≅ [D→D] solved by an inverse-limit construction, a mixed-variance equation with a domain solution)
• [Spivak] D. I. Spivak. The Operad of Wiring Diagrams: Formalizing a Graphical Language for Databases, Recursion, and Plug-and-Play Circuits. arXiv:1305.0297, 2013.
• [Starlark] The Starlark configuration language. github.com/bazelbuild/starlark. (a deterministic, non-Turing-complete Python-like configuration dialect)
• [Svendsen–Sieczkowski–Birkedal] K. Svendsen, F. Sieczkowski, L. Birkedal. Transfinite Step-Indexing: Decoupling Concrete and Logical Steps. ESOP 2016, LNCS 9632, Springer, pp. 727–751. doi:10.1007/978-3-662-49498-1_28.
• [Szyperski] C. Szyperski. Component Software: Beyond Object-Oriented Programming. Addison-Wesley, 1998 (2nd ed. 2002). (a component is a unit of composition with contractually specified interfaces and explicit context dependencies)
• [Turner-TFP] D. A. Turner. Total Functional Programming. Journal of Universal Computer Science 10(7):751–768, 2004. doi:10.3217/jucs-010-07-0751.

AI language models assisted in the drafting of this work; the author is solely responsible for its content.