No Feedback: A Logical System Is Not a Process

Lachlan Douglas — July 2026

Abstract

This paper asks two questions of a made thing: what it is in form, and what it is in operation, once it acts. The two meet at one boundary, the operation point, and where the thing computes, its operation is a computation. Every made thing traverses an arc from its making to its acting, and where on that arc its form becomes settled, its identity point, divides made things. On one kind of arc the form is shaped during the making, by feedback, as a tree's is. On the other it is entailed by the declared parts, settled before the making that realises it and before the operation that exercises it, and altered by neither; the priority there is one of ground and not of time. That arc has a single mark: operation cannot constitute its own composition. Three conditions follow, on the making, the revealing and the operating. A fourth condition secures the set of forms they are stated over. Where they hold, and where the substrate is a deterministic universal machine, what a thing is in form can be determined from its declaration and whether its operation halts cannot, so the boundary falls on the decidable/undecidable line. Many fields hold something settled apart from something that varies over it, and the paper sorts those separations by the condition each secures, stated so that a tradition's own results can refute a placement. The settled form is placed last. It is a type, its made things are tokens, and it is real with none of them made. An artefact's dual nature follows from where its identity point falls, and the identity objection to realist structuralism, asked of a composition, picks out its duplicated parts.

1 Two questions about a made thing

A thing must be something before it can do anything, and whatever it does something to must also be. Being is presupposed by action. Aristotle gave the thought in Greek, that a thing's action follows from what it actually is; the scholastics fixed it in the Latin under which it is still cited, agere sequitur esse. The principle is general, true of anything made, but the theory it has received is uneven, and most uneven for the systems built to compute. What such a system is in operation, when it runs, has a deep and finished account in computability. What it is in form, how its parts are put together, has been theorised only in scattered pieces and never as one account, though it is the structure that an engineer draws before any code runs and keeps long after.

Computation has received abundant attention, and the attention has gone to other questions. Turing's analysis and the computability tradition account for a machine in operation; the mechanistic account says what makes a physical process a computation at all [Piccinini]; the method of levels of abstraction fixes the grain at which a system is described as computing [Floridi]; the implementation debate is over when a physical system runs a given computation [Chalmers]. Each takes a computation as given and asks after its nature, its grain, or its physical realisation. None asks after the composition, the decidable structure a system is assembled into before it computes at all.

This paper takes the composition for its subject, together with the boundary at which the composition gives way to the running. The near side of that boundary is what the philosophy of computer science calls the computational artefact under its abstract aspect [Turner]; the boundary itself lies within the artefact's dual nature, where abstract structure gives way to concrete running.

The nature of a made thing is asked after directly in one place, the metaphysics of artefacts. That tradition locates the ground of what a thing is in its maker. For some the ground is intention. The artefact is what a maker intends to make of its kind [Thomasson; Hilpinen]. For others it is constitution. The thing is made of its material without being identical to it [Baker]. On the common point, that the made depends on its maker, this paper agrees. It departs on two counts. The dependence it needs runs to the parts and the normalising; intention is displaced rather than absent: it belongs to the discipline of reading, which §3 concedes is presupposed, and not to the artefact. And the layer it isolates is finer than the artefact taken whole, the composition, settled and decidable before the thing runs, real as a type rather than conferred by a maker's intention (§9).

Turner's cut, a specification against its implementation, carries an operational norm. The implementation is correct, or it malfunctions, against what it was meant to do. A literature now maps the ways a computation can go wrong, sorting miscomputations from hardware fault to design error [Fresco–Primiero], and it has pressed the norm to a fine point: software understood as a type can misfunction in a limited sense and cannot dysfunction [Floridi–Fresco–Primiero]. Its operational verdicts measure a doing against an intent, and its design-level ones measure one representation against another. Constitution carries a norm of a different kind. A declaration either normalises to a form or fails with a defined error, and for the calculi §5 characterises, which of the two it does is decidable and independent of intent. An illogical declaration does not malfunction; it fails to yield a composition at all. The failure removes the subject of the operational norms, since where nothing normalised there is nothing whose behaviour could be measured, and its operational verdicts begin on the far side of that one, presupposing a system that succeeded in being one. A system can only miscompute once it has succeeded in being a system.

A made thing's composition is what it is in form. Its operation is its own act, once it is, and what it is in operation is the course of states its realised instance passes through while it acts. The form fixes what that course can be, the acts it allows and, where it declares a mode, the chances within that mode, and the form does not change as the course runs. Where the thing is assembled from declared parts, its composition is those parts and their wiring. For a system built to compute, the operation is a computation. Composition and operation meet at one boundary, the operation point: on the near side what the thing is in form, settled before the thing acts, on the far side what it is in operation, which in general only its running discloses. This paper gives the foundations of that boundary. It asks what a made thing is, such that the boundary falls where it does (§2); why the composition is prior to the operation (§3); and exactly when the boundary is sharp (§4–§6). It answers the objection from systems that rewrite their own declarations (§7), places many fields as instances of the one line (§8), and closes on the metaphysics that lies beyond the structure (§9). The concrete calculus, and the proofs to which the account points, are the companion [FA].

The single principle is this. The operation point is sharp, the composition decidable from its declaration and prior to the operation, exactly when operation cannot feed back to constitute the composition: when the made's own act adds nothing to what the made is. Stated at this generality the principle restates the definition of the logical arc, since §2 defines that arc as the case where nothing of the thing's own acting enters the form. The principle's content lies in the conditions of §5, which it grounds. Decidability from the declaration requires three conditions, and the principle grounds the two that belong to the arc (§5). Each condition has mathematics of its own, as does the predicativity beneath all three.

2 The arc, and where the form is settled

Every made thing traverses an arc. It is projected, held as a possibility; realised, made actual as a particular thing; and it acts, fully itself in the world. Two crossings join the stages, the essence, where the thing's nature is settled, and being, where it is and so can act. On each arc there is one identity point, where the whole of what the thing is becomes settled, and where it falls divides made things.

For most made things it falls late. A creature is shaped in its gestation. A building takes shape against its site and its weather. A tree must grow before its form is settled. Such a thing acts while it is still being made, and that loop, feedback, settles a real part of what it finally is. These are the nutritive arcs, after Aristotle's word for the soul that grows by intake. On a nutritive arc the form is temporal during its realisation, settled only at the making's end. The process tradition, which takes reality to be temporal becoming [Whitehead; Bergson], describes these arcs. Whitehead keeps an atemporal ingredient of his own, the eternal objects that ingress into an occasion. He refuses to let it stand alone. By the ontological principle nothing is a reason apart from an actual entity, so the eternal objects are pure potentials, deficient in actuality, held in the primordial nature of one. The division drawn here declines that last move, and his system is the sharpest statement of what declining it costs. The thing is built in a loop, and to freeze an instant destroys it, because the reality there is the loop.

In one case feedback is absent. The form is entailed by the declared parts, settled by them the way a conclusion is settled by its premises, with nothing of the thing's own acting entering. There the identity point falls early, at the essence, and the form is atemporal: settled before either of the temporal processes that flank it, the realisation that makes it real and the operation that runs it, and altered by neither. This is the logical arc.

Every made thing traverses one arc, and where its identity point falls divides made things. On the logical arc it falls early, at the essence, so the form is settled before the realisation that makes it actual and before the operation that runs it, and altered by neither. On the nutritive arc it falls late, essence and being running together in the one making, because the thing acts while it is still being made and that feedback settles a real part of what it finally is. The second crossing, being, is the operation point.

Revealing the form, normalising the declaration to it, is itself a computation that takes steps, but the revealing does not settle the form; it reveals the form the declaration already settled, as finding a proof reveals what the axioms already entail. The steps take time; the form is timeless. Compiled software instantiates this case: the logic is held in place by a compiler that refuses whatever will not normalise.

Two crossings follow. On the nutritive arc the late identity point ran essence and being together, both settled in the one making. On the logical arc the form is settled at the essence, and then, realised as a particular instance, the thing comes to being, where it can act. The operation point is the second crossing, where the realised instance gives way to its operation. The distinction at this crossing is Aristotle's first and second actuality. The realised instance, formed and not yet acting, possesses its form; the operation exercises it; the operation point is the seam between possession and exercise [Aristotle, De Anima II]. Both are actualities of the one thing, and so both are ways it is, the first what it is in form and the second what it is in operation. In software these are familiar: the form revealed at compile time, the instance minted at instantiation, the running at runtime, with the operation point between the instance and its run. They are not confined to software. A statute traverses the same arc, in force from enactment, and no case decided under it rewrites a clause. What a clause settles is fixed by its text under a practice of reading, and that practice is the presupposition §3 takes up rather than one this example escapes.

On the logical arc the two are apart, the form settled at the essence long before the instance acts at being. So one form can be realised many times. It is a type, settled at the essence, its realisations the instances that come to being, the distinction §9 turns on. The logical arc has no loop to freeze; time belongs to the flanking processes, the realising and the operating, and in neither is the form altered.

Within the logical arc the form may still be light or heavy, a free choice that leaves the arc untouched. A light form settles little and leaves much to the operation; a heavy form determines nearly all of what the thing is in operation. Both are logical, since each is settled at the essence and altered by neither flank. What the weight of the form settles is the character of the thing's operation.

A system's mode, probabilistic or deterministic, is among the things a declaration may fix, and where it fixes one the mode is settled at the essence with the rest of the form. The running then discloses no new fact about that mode, the run drawing a particular outcome within it. The light probabilistic form and the heavy deterministic one are two ends of a single axis, the measure of how much the form determines and how much it delegates, and every point along it is logical.

3 Constitutive priority

That the composition is prior to the operation is easily misread as a claim about time, and it is not. On the logical arc the form stands to its running as premise to conclusion; the order is ground to consequence, and no lapse of time is part of it. The distinction is old. Aristotle separates priority in being from priority in time, and holds that a thing may be prior in substance even where a particular's own coming-to-be precedes it in time [Aristotle, Metaphysics Θ.8]. Only the distinction among priorities is borrowed. Θ.8 gives priority in substance to actuality as exercise, and it gives it on teleological grounds: the capacity is for the sake of the activity, sight for the sake of seeing. That is a priority of end. The priority argued here is a priority of presupposition, which Aristotle's first actuality supplies [Aristotle, De Anima II]. Seeing requires that sight already be possessed. Both orderings hold of the one pair and they run opposite ways, which is why the first actuality of §2 carries the direction taken here. Priority in account Aristotle gives to the exercise, and that placement is accepted. A capacity is defined through its exercise, sight through seeing.

The operational descriptions are still unlocated. A specification, a semantics, a test each describe a doing, because the account of a made thing is operational in content. The account is written at design time, before the thing exists. The actuality it involves is the designer's; the system, not yet made, contributes none. So the orderings separate. The operation is prior in account, the composition is prior in being, and the operation comes last in act. The misreading is the compression of the three into one, a description of the doing taken for the doing.

The remaining priority, in being, is kin to what contemporary metaphysics studies as grounding, a determination that is not causal and need not be temporal [Fine; Schaffer]. The kinship is claimed and nothing more. Grounding is usually regimented over facts, and the relata here are a form and its operation, so it has no place in that regimentation. The priority is constitutive, with a definite computational content. The form is prior to the operation, and is not merely earlier in time. For the same reason it is not the trivial point that a function needs its argument first, a point temporal through and through. On the side where the form is settled there is no first in time, only what settles what.

That the priority is not temporal does not make it no priority. The relation is a dependence, and the dependence runs one way. Settle what a thing is in form, and what it can be in operation is fixed so far as the form determines it: the acts it allows, and, where the form declares a mode, the chances within that mode. What the form delegates stays past the boundary, a substrate's own nondeterminism with it [FA, §7]. A particular act draws from what the form allows, and adds nothing to it. Settle only the behaviour, and what the thing is in form stays underdetermined, one behaviour being carried by many structures, as one and the same service is delivered by differently wired systems. So what a thing is in operation depends on what it is in form, and what it is in form does not depend on what it is in operation. The two are asked separately, and the second answer rests on the first.

The asymmetry rests on two premises. One direction is that being is presupposed by action. Every step of the acting rests on a form already settled, agere sequitur esse. The other is the single principle, and on the logical arc it holds by definition. Where operation cannot feed back to constitute the composition, nothing the running does returns into what the form is, so what it is in form does not in turn depend on what it is in operation. Presupposition forward and no feedback back together make the dependence one-way. The regress below gives that dependence a further mark, since the descent through makers terminates, so the relation is well-founded as well as asymmetric. Well-founded asymmetric non-temporal dependence is the shape grounding theorists work with, and the kinship claimed above is claimed on that ground. The stronger identification is not made here: determination on its own falls short of grounding, as Socrates and his singleton show, each necessitating the other while the grounding runs only from member to set [Fine]. Where feedback is present the second direction fails, the thing's own activity while it is still being made enters the form, and the order is then neither temporal nor constitutive but absent. The nutritive arc is that case, with form and operation folded into one loop. The boundary is sharp in exactly the case where the dependence is wholly one-way.

Constitution is what the maker leaves, the parts and the normalising that settle the form, what a thing is in form; operation is the made's own act, once it is. Two acts flank the form: the maker's making before it, and the made's acting after. The normalising between them is neither act; it is the finitary reading that reveals the form the parts settled. Which act the priority favours depends on the side it is viewed from. From the maker's side, the maker's act produces the form and is prior in time. From the made's side, the form is given to the thing's own running, presupposed by every step of it, and prior in being. The maker's doing becomes the made's form.

The universal machine, the engine of computation itself, shows the priority in miniature. Handed a description, it reads from it the machine it is to run. Well-formedness of the description is settled by a finite and decidable check; the per-step consultation that follows belongs to the running. In the standard construction, the structure it read is consulted at every step of the running and altered by none of it, presupposed continuously, never read once and left behind. The priority here is constitutive. The structure that was read is never a phase the running leaves behind, and non-termination lives only in the running, never in the reading. So the universal engine of computation contains the operation point in its own operation. Everything the machine does is computation, and a provable line divides it: on one side the decidable reading of the constitution, on the other the undecidable running.

If the form is the residue of a maker's act, the maker had a form of its own, and the question is whether this climbs without end. It does not. The descent in production-stage is well-founded. Von Neumann's construction already shows the base of it: the constructor and its description must be given before any reproduction runs, so self-reproduction is not self-creation [von Neumann; McMullin]. The homunculus regress has the same shape and the same resolution, a base case at which the descent stops. So does the standard reading of quines: the recursion theorem produces a fixed point within an already-given system, never a thing from nothing [Kleene]. The descent from any made thing terminates in a structure no in-system computation produced, a given relative to the system, the programmer, the physics, an axiom. It is not a cosmological given, a structure produced by nothing whatever; the regress shows composition at the bottom of every chain of computation taken within a system, which is all the priority needs.

Wittgenstein raises a further question, and it concerns the declaration rather than the maker. A rule does not determine its own application. Any continuation of a series can be brought into accord with the rule under some interpretation, so the rule by itself does not say which continuation is correct. What says so is a practice, a way of going on that its followers are trained into [Wittgenstein, §§185–242]. Kripke draws a sceptical conclusion from this. No fact about the sign's user fixes what the sign means, and the appearance of such a fact comes from agreement in use [Kripke]. If nothing fixes what a declaration says, then a declaration settles nothing, and what a thing is depends on how its declaration is used.

That question is about the reading, and a reading is assumed throughout. Normalisation is a fixed procedure from a declaration to a form. Every claim above holds of a system for which such a procedure is already in place. None of them says what makes it that procedure. The maker regress above reaches this case too. A normaliser is a structure no in-system computation produced, a given relative to the system, as the programmer and the axiom are. The sceptical argument survives that reply untouched. It asks what establishes a way of reading, and the argument here takes such a way for granted.

One case seems to resist, the living thing that appears to make itself. The appearance has a worked-out theory, autopoiesis, on which a living system is a network of processes that produces the very components that realise it, so that its identity is the work of its own operation [Maturana–Varela]. The theory's own distinction supplies the materials for an answer, and the answer has to be argued, since one of its sentences runs the other way. Maturana and Varela hold a system's organisation apart from its structure. The organisation is the set of relations that makes the system one of its kind; the structure is the components and the relations that realise it on a particular occasion. An autopoietic system holds its organisation constant through structural change, and a system that loses its organisation does not take on a new identity; it disintegrates. So what the network produces is structure. The organisation is what it holds constant. An invariant held constant across its realisations is exactly what the account means by a form. The continual production of components is realising, unending here where elsewhere it is done once. Against that reading stands the definition itself, on which an autopoietic machine "continuously generates and specifies its own organization through its operation" [Maturana–Varela, p. 79]. Taken strictly, that sentence asserts the feedback the principle denies. Taken with the invariance claims of the same work, where a system that loses its organisation dies rather than becomes another thing [Maturana–Varela, p. 112], what the operation generates and specifies is the components realising the organisation, and the organisation is what that production conserves. The second reading is the one taken here, and it is an interpretation rather than a report. On it the living thing is an instance of the account rather than a counterexample to it, its unusual feature being that its realising never stops. This has a consequence for the arc. §2 puts the settling of a nutritive form at the making's end, and a living making has no end. What carries the identity is the organisation, constant from the origin. The particular structure goes on being realised for as long as the thing lives. Where the organisation itself changes, one unity has disintegrated and another has begun, the earlier thing's operation acting as the maker of the later, never one thing constituting itself. The shape is the succession of §7, though a living succession passes through no declaration, so the test §7 sets is not met there and nothing is claimed of it.

The general move the appearance invites, letting a thing's running settle what it is, has a Lamarckian analogue one remove away, where what the individual's running settles is the constitution of its lineage. The correction is Weismann's germ-plasm barrier, which sequesters the individual's acquisitions from its lineage and leaves adaptation to selection among individuals [Weismann]. The barrier is drawn where a germ line is sequestered early, so it holds of animals and not of plants, whose gametes come from somatic tissue; what the example carries is the shape of the correction and not its reach. Darwin himself allowed the inheritance of acquired characters, so the barrier is later than the theory it secures [Darwin].

So operation, taken strictly, does not form the self. A thing's running sustains it but does not constitute it. What its making settles is constitution; on the nutritive arc that includes the thing's own forming activity, which belongs to the making there and never to operation. The clean operation point is the limit where the maker is entirely external to it, the parts and the normalising do all the constituting, and the thing's own act adds nothing to what it is in form. Operation cannot constitute its own composition. The split between making and operating tracks constitution, so at this generality the sentence demarcates rather than reports a discovery, as §1 already conceded of the principle. Three claims give the principle content beyond the demarcation. The logical arc is not empty, which the companion calculus establishes. The test of §7 decides, case by case, whether a system's reconstitution passes through a declaration. And §6 gives the coincidence. The rest of the paper makes the demarcation exact.

4 Decidable from the declaration

To say the composition is decidable from its declaration is to say two things. First, that the form is entailed by the declared parts, settled by them alone the way a conclusion is settled by its premises, with nothing of the making or the running entering. Entailment is atemporal: the form is settled at the essence (§2) and unmoved through realisation, and that is what makes the form prior. Second, that the revealing terminates, so the form is not merely entailed but knowable in finite time; this makes it decidable. Together they make the made thing knowable without redoing its making.

The first of the two calls for exactness about order. A form entailed by the parts alone cannot depend on the sequence in which the parts were put together, since the sequence belongs to the making. Trace theory is the mathematics of that independence. It presents a construction as a sequence of steps, marks the pairs of steps that do not interact, and counts two sequences as one construction when they differ only in the order of non-interacting steps. An object settled by the parts alone comes out the same under every such reordering, and order-invariance, defined below, is that sameness made formal.

A construction is presented by a build, a finite sequence of steps β ∈ Step*, with a symmetric irreflexive independence relation I ⊆ Step × Step, (s,s′) ∈ I meaning neither step produces what the other consumes. The congruence ~ generated by s·s′ = s′·s for (s,s′) ∈ I quotients Step* to the trace monoid, the free partially commutative monoid on (Step, I) [Cartier–Foata], and a ~-class is a trace, which corresponds to a labelled partial order, its dependence graph. A denotation ⟦·⟧ assigns objects to builds. An object is order-invariant when its denotation factors through the trace, β ~ β′ implying ⟦β⟧ = ⟦β′⟧, so it depends on the partial order of the build and not the linearisation. At the pole where I holds of every pair of distinct steps, every pair of steps commutes, so an order-invariant object is a function of the multiset of steps. That pole is full parallelism. The by-name composition operator ⊕ of [FA] sits there by construction, and more narrowly still: each of its steps composes a distinct part, so the multiset carries no repetition, and the object is a function of the set of steps.

What else a form might depend on, besides the declaration, is the subject of §5.

5 Three conditions, and the precondition

On the logical arc the form is entailed by the declared parts (§2). Entailment leaves no opening. What the premises entail is settled with the premises, and nothing that happens later revises it. A calculus built on the arc has the same character: its normalisation reads declared data, ports and references and fragments and containment, and no value produced by the realising or the operating is available to it at all [FA, §4]. So the question §2 leaves is what a declaration must be for a form to follow from it.

The answer is three conditions: one for the realising that makes the form actual, one for the revealing that takes the declaration to it, and one for the operating that exercises it. The realising and the operating are the two acts that flank the form on the arc; the revealing is neither (§3). Each condition has been studied in isolation in some field of its own. A fourth property, predicativity, is of a different kind. It secures a carrier of forms to speak of, and it stands beneath the three rather than beside them.

First, the realising. Part-determinacy says the form is a function of the declared set of parts. Its canonical face is order-invariance, the form factoring through the trace; the wider condition is that the form is a function of the parts alone, with the schedule, the timing, and the maker's identity contributing nothing. Where part-determinacy holds, the realising makes actual a form the parts already settled, and the form is atemporal across its making. Where it fails, the form was settled in the course of the building, as the order of assembly or the path the maker took enters the result. That is the nutritive arc of §2, and the failure is not a logical form gone wrong. It is a form of the other kind.

Second, the revealing. Finitarity says the normalisation map, from a finite declaration to a normal form or a defined error, is a total computable function. Where it holds, the form the declaration entails can be read from it in finite time. Where it fails, either the reading is not total, or it is total and not computable; the paragraph below separates the two. Where it is not total, on some declarations it never returns. The standard case is a configuration language that is itself Turing-complete, and "what the thing is" then inherits the undecidability of "what a program does" [Turing; Rice; FA, Remark 5.2]; there no procedure decides which declarations return, though non-totality does not give that in general.

The failure comes in two kinds, and only one is a failure of knowing. Where a value is computed by something that never stops, nothing is settled for a reading to miss, and the declaration determines no form. Where the reading is instead total and not computable, the form is settled and no procedure finds it. There the failure is knowability alone. Nothing of the making or the running has entered the declaration, and what it entails, it entails with or without a reading that returns. Rice's theorem seems to stand in the way here, since every non-trivial semantic property of a program is undecidable, and the form might seem to be such a property. The exemption that keeps the near side decidable is Rice's own. The form is the intensional object, the wiring the declaration normalises to, and identity of forms is equality of those normal forms. Two forms with the same behaviour are still two forms. Rice makes the semantic property undecidable and leaves the syntactic one alone; the form is settled on the syntactic side, which is why deciding the form does not decide what an instance of it does.

Third, the operating. Staticness says a binding's result is a function of the declared structure alone, deduced, not measured [FA, §4, §10]. Where it holds, every question about the form is answered by reading. Where it fails, no form was declared. A record that leaves a binding to be settled by a value only its own running produces, a distribution estimated from that running or a probed live state, has declared no form at that binding, and what it leaves to measurement it does not constitute. The running has not reached back into the form. There was no form for it to reach.

The three can be put as questions about one declaration, and the companion's worked example answers them [FA, Example 4.6]. Take a store, a service that requires it, and a seed that fills it. For part-determinacy, write the three down in any order and ask whether the form differs; it does not, the wiring being derived from the whole set at once. For staticness, a service that requires the store is wired by reading, and a service that requires whichever replica answers fastest is not: nothing in the declaration says which, and only a run would, so that binding declares no form. For finitarity, pairing each requirement with its provider is a search of a finite relation and it halts, which a declaration whose values are computed by a Turing-complete language forfeits.

The three share one question, and it is the one to carry away. Can this be answered by reading the declaration, or only by watching the system run? What reading settles is constitutional. What only watching settles was never declared.

Beneath the three, the carrier. Each condition is stated of a form, and the forms must be drawn from somewhere: a set of forms, the carrier, into which normalisation is a function. Predicativity is used here in a stipulated sense, narrower than the classical one and kin to it in that a reflective reference quantifies over a totality it belongs to. It is the condition under which that set exists, and it holds when the carrier admits no negative self-occurrence, so that normalisation is an ordinary function between sets and needs no temporal apparatus. A declaration's parts refer to one another through the names and references they declare, and what a reference may say is a design choice. Suppose the choice admits a requirement conditioned on a predicate over the whole composite, a reference whose evaluation reads the very forms it helps make up. Call such a reference reflection. A concrete case is a part whose requirement reads: bind to the provider that nothing else in the finished composition uses. To resolve it, normalisation would have to read the normal form it is still producing. What it costs depends on how the references are read. On the extensional reading, a reference is a predicate over the composites themselves. The carrier must then solve an equation in which it occurs negatively, into a codomain of at least two values [FA, Def 6.2]. That equation has no solution in Set: distinct predicates demand distinct references, so 2^𝒞 injects into 𝒞, against Cantor. A solution is recovered only outside Set, by a stratified construction the well-founded constitutional layer was free of: the step-indexing of guarded recursion, whose index is read as time [FA, Prop 6.3; Iris], or the approximation-indexed inverse limit of domains [Scott]. On a syntactic reading of references the cardinality obstruction lapses, and the cost reappears as non-termination, the second condition's territory [FA, Prop 6.5].

The three conditions sort into two of the arc and one of knowability, and the precondition stands beneath all three. Part-determinacy and staticness are two faces of one requirement, that the parts alone settle the form: the first fails where the making settles it, the second where nothing settles it. Finitarity is a requirement on knowability wherever a form is settled at all, which is the case where the reading is total and not computable; where the reading diverges there is no form to be ignorant of. Predicativity is not a fourth condition of the same sort; it is what secures the carrier over which the three are stated. A form meeting all three, over such a carrier, is a function of its declared parts and of the normaliser that reads them. The normaliser is fixed once for a calculus and is the given §3 concedes, so within one calculus the parts alone settle the form; across calculi one declaration has as many forms as there are disciplines to read it. Its maker is wholly other.

6 The characterisation

The characterisation below says what secures a form and what secures its reading. Read as a definition it is close to one: that a form is decidable from its declaration means that the declaration alone settles it and that the settling can be read in finite time. The content lies elsewhere. It lies in where each condition is grounded. The two temporal conditions are grounded in the arc's flanking stations and the third in knowability, with predicativity beneath them as the condition of a carrier (§5).

The characterisation. Predicativity secures a carrier of forms. Where a reference ranges over the compositions themselves, the carrier would have to hold a distinct member for every property of itself, and no set does; such a reference has nothing to refer to. Over a carrier predicativity secures, three conditions say that the declared parts alone settle the form and that the settling can be read. Part-determinacy: the form is a function of the declared set of parts, so the realising makes actual a form the parts already settled. Staticness: every binding is deduced from declared structure and not measured, so nothing of the form is left for the operating to settle. Finitarity: the revealing terminates. The first two are grounded in the arc, the third in knowability. Part-determinacy and staticness give the first of §4's two requirements, that the form is entailed by the declared parts with nothing of the making or the running entering; finitarity gives the second, that the revealing terminates. So the three suffice, and they do so by what they assert rather than by any further argument. What is open is whether they are all of them: the enumeration follows the arc's stations, and that those stations are exhaustive is not argued here.

The three do not contribute in the same way. Finitarity is the normalisation map's totality and computability, and staticness is its dependence on declared structure alone, so those two carry the decidability. Part-determinacy carries the other half, that the form is entailed by the parts and not settled in the course of the making: a form can be computed from its declaration in finite time and still fail it, the declaration's order having entered the result. Predicativity is not a fourth condition of the same sort, since it is what lets the normalisation map exist as a function between sets in the first place.

When all three hold over a predicative carrier, the normalisation map is a total computable function of the declaration, so the composition is decidable, Δ⁰₁. Where a substrate is a deterministic universal machine, the halting of what is realised on it is Σ⁰₁-complete, the far side being the halting problem [Turing]. That is the decidability coincidence [FA, Prop 5.1]. The line the theorem draws falls at the essence, between the declaration with everything deducible from it and everything that only running decides. In the statute's terms the line falls between what the text settles and what only a case decides. The operation point of §2, the crossing at being, is where a realised instance meets that line. Realisation itself is delegated to substrates and left unmodelled [FA, §7]. So the coincidence is claimed for the form, and of an instance the only claim is that its running lies on the far side.

An engineering boundary between what a thing is in form and what it is in operation, and a logical boundary between what a finite procedure can settle and what it cannot, fall on one line. The alignment has an antecedent. The phase distinction of Harper, Mitchell and Moggi already holds a static stratum decidable while the dynamic stratum it precedes is not, in the module systems where the two phases were formalised for type checking [Harper–Mitchell–Moggi].

A nearer neighbour still is partial evaluation. Binding-time analysis divides a program's inputs into the static ones, known now, and the dynamic ones, known only when the program runs, and the program is then specialised on the static part [Jones–Gomard–Sestoft]. Davies and Pfenning give the same division a modal type discipline, the type □A typing the code one stage constructs for a later stage to run [Davies–Pfenning]. The static side there is computation done early. What binding-time analysis holds back is work that could have been done now, and Davies and Pfenning's boxed code is made at one stage for another to run, which is the succession of §7 rather than a constitution. And the division answers to a classification the user supplies. The analyst declares which inputs count as known, and the analysis then propagates that classification through the program under a congruence constraint, so the division of the program is computed while the division of the inputs is chosen. Here nothing is classified per program: once the declaration discipline is fixed, what the declared parts settle they settle, and no division of the work is offered to an analyst. The discipline is itself a choice, made once for the calculus, so what is exhibited is a calculus in which the two boundaries fall together rather than two boundaries characterised apart and found to coincide.

The coincidence generalises the phase distinction from a type system to the whole of constitution. What it adds beyond that antecedent is knowability. Given the no-feedback conditions, constitution by the parts alone still does not make a form readable, and finitarity is what does, so a form settled by its declared parts and finitarily revealed is a form a finite procedure can settle. The direction of priority, that the composition is prior to the computation, is the argument of §3 and does not rest on decidability; a difference in decidability is a difference in kind, and on its own it grounds nothing. The composition falls on the decidable side of a provable line and the operation on the undecidable side, and the side §3 calls prior is exactly the side that a finite procedure can settle. The result does not prove the priority; it locates the line along which the priority runs.

The same diagonal cuts both sides. On the far side, the undecidability runs on the universal machine's self-application; that is the diagonal Turing and Rice turn against it. On the near side, the carrier admits no such self-reference; that is the diagonal Cantor turns against a set required to hold a distinct element for each predicate on itself, and predicativity is its absence. The instruments differ, cardinality on one side and computability on the other, and their unity is a theorem. Lawvere's fixed-point theorem derives the Cantor, Russell, Gödel and Tarski diagonals as instances of one construction in a cartesian closed category [Lawvere], and the same scheme yields Turing's halting argument and Rice's theorem [Yanofsky]. The single axis is inherited from that theorem, and its placement at the operation point is the application made here. The constitution is decidable because no self-reference enters it and its revealing halts (§5). The operation is undecidable because computation admits self-application and need not halt. So the operation point is the line between what a finite procedure can settle and what it cannot. The absence of impredicative self-reference secures the carrier that line is drawn over. It does not draw the line by itself, the finitary calculi being a proper subclass of the predicative ones [FA, Prop 6.6]. A Turing-complete configuration language leaves the carrier an ordinary set while the revealing fails to halt.

Whether the three conditions and the precondition are all the ways a form can fail to be essence-settled and knowable is more than the paper proves, though the arc says why they should be. The arc has exactly two acts flanking the form, the making before it and the operating after, and one non-act between them, the revealing; beneath all three lies the carrier the forms are drawn from. A failure of constitution can enter only through an act, a failure of knowability only through the revealing, and a failure of the domain only through the carrier. On that reading the enumeration follows the arc's own shape rather than a list of the failures met so far. What is missing is an argument that the arc's stations are themselves exhaustive, and none is offered here. The depth in each is borrowed. That a carrier whose references range over it has no ordinary solution is impredicativity and the stratified construction it forces [FA, Prop 6.3; Iris]. That a making-shaped form is the failure of confluence is rewriting [Newman]. That the operation the form gives way to is undecidable is the halting problem, generalised to every non-trivial semantic property [Turing; Rice]. That an operation-read form is the deduced-not-measured line is [FA, §10]. That an unbounded revealing forfeits decidability is [FA, Remark 5.2]. What is new is the arrangement, and §5 states it.

7 Systems that rewrite their own declarations

A system that rewrites its own declaration while it runs looks like the principle's outright refutation. An autoscaler edits its own composition; a model is retrained on the traces of its own operation. If the look were right, operation would be constituting, and it would be doing so in the systems now most discussed. The answer is a succession of compositions. Each stage emits a declaration, the declaration normalises finitarily to a form, and the running of one stage acts as the maker of the next. The companion calculus names that shape and stops there, placing dynamic reconfiguration among the successions of recomposition rather than the moves of ⊕ [FA, §10]; the account of the succession is this paper's. Within any one stage the form is closed against that stage's own running, so the principle holds stage by stage. The reach the counterexample points to crosses stages, from one composition's operation into the next composition's making, and a maker was always permitted to be a prior operation; the maker's doing becomes the made's form (§3).

A system that rewrites its own declaration is a succession of compositions rather than a refutation of the principle. Within a stage the form is closed against that stage's own running, which is the arrow shown grey. Across stages the running of one is the maker of the next, and the crossing passes through a declaration. That is what the test below requires, and what a process rewriting its configuration in memory fails.

What decides whether the succession reading applies is a fact about the system, once declaration is fixed as the artifact a stage is realised from, under a normaliser settled before the stage runs. Given that, the reading applies exactly when each stage emits such a declaration and it normalises finitarily, so that there is a settled form at every stage. The fixing is the presupposition §3 concedes and does not remove; what it does remove is any choice left to an analyst afterwards. A pipeline that checkpoints a weights file and redeploys meets the test, the checkpoint its declaration and the redeploy its realisation. A tree meets no such test, since its growth never passes through a declaration; there the arc is nutritive and the principle makes no claim. The tree is not the only failing case. A process that rewrites its own configuration in memory, passing through no declaration between one configuration and the next, fails the test. The account then places a system built to compute off the logical arc. Since a stage is individuated by its declaration, that the form is closed against its stage's own running holds by the definition of a stage; what the test asserts, and what can fail, is that declarations normalising finitarily exist at every reconstitution. A declaration is more than a state written down. Its form must admit instances beyond the one that followed, since a form admitting exactly one is settled in that making and is nutritive by the division of §2. Serialising a configuration between two moments meets the letter and not that, so under the criterion every boundary is checkable, one composition at a time, and the principle does not hold by bookkeeping alone. What the succession leaves undetermined is what persists across it, and that is the two-identities question §9 raises and does not answer: the type's identity against the token's, and when a change of declaration is a revision of one thing and when it is the birth of another.

8 Many fields, one boundary

Many mathematical theories, developed for unrelated reasons, each hold a settled layer apart from something that varies over it, and most divide constitution from operation. On its own the recurrence proves little. Every model of computation separates a fixed structure from the executions that run over it, and that separation is the definitional shape of a model, so among the computational traditions below the recurrence is one convention met many times. Nor can the survey serve as independent evidence for the three conditions and the precondition, since both were abstracted from these same literatures and the cases are sorted by the taxonomy they illustrate. The survey's content is the classification itself. Each tradition is placed under one condition, or under the precondition. A placement is correct when the tradition's own central result asserts that condition of the tradition's objects:

• for part-determinacy, an invariance of the object under the order or the path of its construction;
• for staticness, a constitution held apart from the running and presupposed by every judgement about it;
• for finitarity, a decidability bought by bounding the revealing;
• for the precondition, a requirement that what constitutes be given from outside what it constitutes, a carrier barred from holding what ranges over it or a constructor given before anything it constructs.

A placement fails if the tradition's results show the condition does not hold of its objects, or if what they secure is one of the other three. A failed placement refutes the sorting offered here; a tradition whose separation answered to none of the four would be a counterexample to the taxonomy itself.

Two traditions outside computation, the state functions of thermodynamics and the well-founded hierarchy of sets, do not inherit the definitional shape. Thermodynamics is placed by the shape of a condition rather than by dividing constitution from operation. The reach of the classification over these two is the part of the claim least owed to convention, and it is the part most open to challenge.

Thermodynamics places by the shape of a condition alone, both sides of its cut lying in the system's own history, so it does not divide constitution from operation. Ergodic theory is the hardest case in the taxonomy, its settled layer being read off the running; it places because reading is not settling (§2), and finitarity fails there, no procedure deciding in general what a system's attractors are. Separation logic's staticness holds of the resource algebra and not of any heap, since heaps mutate as the program runs and what no run alters is the composition structure every judgement is stated over. The arithmetic threshold bounds expressive power rather than the revealing of any form, so it places at one remove, the fragment that stays decidable being the one held short of what buys full computation.

A monadic bind lets the rest of a computation depend on a value the run produces, where an applicative functor closes that off by design [Moggi; Wadler], and the interfaces sort by how much structure each settles in advance [Lindley–Wadler–Yallop]. Aczel's anti-foundation, which readmits the cycle well-foundedness bars, marks exactly what the ban secures [Aczel].

Further traditions fall under the same three conditions and the precondition without adding a distinct mechanism, and a clause apiece records them. Part-determinacy is illustrated again by true concurrency, which treats the partial order of events as real and the interleavings as observations of it [Pratt; Winskel], and by the monoidal categories whose diagrams are invariant under any order of evaluating their boxes [Joyal–Street]. Staticness is illustrated again by Petri net theory, which holds the net apart from its marking, the places and transitions fixed while the token game runs over them [Petri; Reisig]. The precondition is secured again by the hierarchies built to bar self-reference. Russell's theory of types and Tarski's stratified languages are two [Russell; Tarski]. Database theory imposed stratified negation to keep a program's meaning well-defined [Apt–Blair–Walker], then found weaker repairs, the well-founded and stable-model semantics giving a defined meaning to programs that are not stratified [Van Gelder–Ross–Schlipf; Gelfond–Lifschitz]. The placement survives the correction and is narrowed by it. What the tradition bars is an undefined answer at a cycle rather than the cycle itself, and the later semantics pay for admitting it, the well-founded one with a third truth value and the stable one with a model that need not be unique. Domain theory is the contrary case and earns its place by being one: rather than barring the self-reference it solves D ≅ [D→D] by a limit construction [Scott], the repair §5 names, and pays for it with a carrier that is no longer an ordinary set. Finitarity is illustrated again by the strong-normalisation results that buy decidable conversion with termination [Girard–Taylor–Lafont].

The map is uneven. Four of the worked cases fall under part-determinacy, which is why order-invariance stands across the literature as the signature of the stratum; the other two conditions and the precondition carry two apiece. Every condition bears more than one independent tradition.

No field names what the four have in common, and only rewriting reaches two of them, confluence answering to part-determinacy and strong normalisation to finitarity. All three conditions are met, severally, across unrelated literatures, and the precondition beneath them is met too. The covering shows that each answers a difficulty some field met on its own ground, and it leaves the exhaustiveness of the three exactly as open as §6 leaves it.

9 The keystone: the form as type

One question the account does not answer: what is the settled form? Is it a real made thing, a structure that genuinely is? Or is it the abstract denotation of an operational making, a convenient cross-section of a process? On the second answer only the process is real. Everything proved stands either way, and the answer given here is not a position taken for form's sake. Two results come with it. One is that the dual nature of a computational artefact, which the literature assumes, follows from where the identity point falls, the place on the arc at which the whole of what a thing is becomes settled (§2). The other is that the identity objection troubling realist structuralism, asked in this domain, picks out a feature the parallel mode was built to describe. The type/token distinction the arc already draws supplies the answer: the dichotomy is a category error.

The dichotomy has two terms, concrete particular and shadow, and the form is neither, because its level is the type, which the dichotomy omits. Normalising a declaration yields a normal form, a determinate form held in the abstract. Realising that form under an identity yields an instance, a concrete thing in the world, and one form admits many instances, each minted under its own identity. The made things are the tokens; the form is the type they instantiate. To ask whether the type is a concrete thing or a fiction is the wrong question, as it would be of a number. One relation of type to token belongs wholly to the declaration: a part definition reused at several addresses is a type, and those uses are its tokens. Both stand before normalisation. Form and instance is the relation that crosses into realisation.

A kindred dispute in the philosophy of computer science asks whether a program is an abstract object or a concrete one [Moor; Irmak]. The type/token answer is the field's own settlement, and Turner's dual-nature thesis frames the current debate in just those terms [Turner; Angius–Primiero–Turner]. The duality at issue is his, the abstract specification against the concrete implementation. It is not the duality the same phrase names in the Delft programme, where a technical artefact is a physical structure under an intentional function [Kroes–Meijers; Houkes–Vermaas]. Nothing here touches that one. An identity point settles when a form is fixed, and says nothing of what the thing is for. What the arc contributes is a ground for Turner's cut. The logical arc settles the form at the essence, before any realisation, so the abstract aspect names the type, settled at the essence, and the concrete aspect names the token minted at realisation. The dual nature is then a consequence of where the identity point falls, and the nutritive arc, which lacks the early identity point, is exactly where the duality fails to appear.

This separation of type from token is the mark of the logical arc, and just what the nutritive arc lacks. There the form is settled in the one making, by feedback, inseparable from the single instance it produces, so a nutritive form genuinely is this making's, and the denotation answer fits it. The logical form, settled before any realisation (§2), pre-exists every instance and stands identical across all of them, which a making's shadow could never do.

Early settling is not what makes the form separable. The form is a normal form: the declaration normalises to it, it is unique, and it is a function of the declared parts alone, which is the part-determinacy of §5 [FA, Cor 4.3]. Reaching it consults no instance, so it belongs to no one making, and every instance is an instance of it. The nutritive form admits no such presentation. It can be read only off the thing that grew, so there is nothing to hold apart from that thing. The logical form transcends its making, and that is what makes it separable.

The form is real, then, as a type is real, a determinate object with identity conditions, the equality of normal forms, open to inspection, to versioning and to ownership, standing in the abstract with no instance yet realised. It is neither concrete particular nor fiction. Its place is exactly the structuralist's, between a system and a structure [Shapiro]. A system is a collection of objects standing in relations; a structure is the abstract form of a system, keeping the interrelations and ignoring whatever feature of the objects leaves them untouched. A form is a system. It keeps the addresses its parts carry, and those are what a structure ignores, since renaming them leaves the wiring as it was [FA, Remark 4.7]. The structure is what all the renamings of one form share.

Both are abstract. The structure's reality is what the ante rem thesis is for, where a system with identity conditions is the sort of thing anyone who accepts a finite labelled graph already accepts. The two levels are what let the next two questions be kept apart. Addresses tell one form from another [FA, Def 2.6]. What tells two positions apart within one form is a question about the structure, and it is the subject of the objection below.

A standing objection to that position must be met, since where positions bear no properties but structural ones it is close to decisive. Ante rem structuralism is charged with lacking identity conditions for its objects. A structure with a non-trivial automorphism has positions that share every structural property, as the two square roots of minus one share theirs, and positions indiscernible by structure alone cannot be told apart, so the view cannot say which object a given position is [Keränen].

A form's positions bear one property that is not structural: the address each part carries, which Def 2.6 makes constitutive of which form this is [FA, Def 2.6]. The objection therefore does not reach a form directly. It reaches the structure a form presents when names are taken to bear only equality, which is how the calculus reads them [FA, Remark 4.7].

Two questions have to be kept apart before the objection can be answered. One asks when two forms are the same form. The account settles that by equality of normal forms, and every part is separately addressed, so a form built from two like parts is a form of two parts, and the decomposition of its part-set is unique [FA, Cor 3.4]. The other asks what tells two positions within one form apart. Keränen's charge is about the second, and only the second.

The escape offered in the literature is rigidity. A structure is rigid when its only automorphism is the identity, so that no permutation of its positions returns the same structure. A rigid structure has no indiscernible positions and never faces the charge. The debate after Keränen turns on the structures that are not rigid, and on whether weak discernibility rescues them [Shapiro 2008; Ladyman; Ketland]. Here indiscernibility is settled by the form's automorphisms, the permutations of its positions that leave the wiring and the containment as they were. Two positions of a finite form share every structural property exactly when some automorphism carries one to the other. Take a structural property to be one those two relations fix, with no position named. An automorphism preserves every such property, which gives one direction. A finite form with a distinguished position has a description in those relations that fixes it up to automorphism, so two positions answering to the same descriptions are carried one to the other, which gives the other. A renaming of segments is a different thing, and the addresses it moves are no part of the structure. The criterion reads the wiring, which is derived from the form, and the form is a function of the declared parts alone, with the order and layout of the declaration contributing nothing [FA, Cor 4.3]. It does not read the names, a name being an atom bearing only equality, and the wiring being equivariant under any injective renaming of the segments [FA, Remark 4.7; Pitts].

Where no automorphism carries one position to the other, the wiring separates them and the objection does not arise. Where one does, the two are duplicates, alike in their interfaces and interchangeable in the form.

One configuration is refused before either case is reached. Two positions each requiring the other close a cycle in the dependency relation, and a declaration whose dependency relation is cyclic is refused at normalisation with a defined error and no normal form [FA, §7]. What the rules refuse is a cycle, of any length, and that is not the weakly discernible pair. Weak discernibility holds where some formula is true of the pair and false of a position taken with itself [Ladyman; Ketland], which two like subsystems standing side by side satisfy by having disjoint dependencies. Such a form is acyclic and normalises.

The duplicates are interchangeable, and that is a verdict rather than a gap in the account. What makes such positions two is the addresses they carry, which the form's identity includes and the structure it presents does not. Weak discernibility reaches some of these pairs, two like subsystems being discerned by their disjoint dependencies, and it does not reach the pair alike in everything and connected to nothing. In both the addresses are what makes them two. Neither such position ever depends on the other. Were one to, applying the automorphism again and again would carry that dependence around its orbit and close a cycle of the orbit's length, which the rules refuse. So neither produces what the other consumes, nothing orders them, and a schedule may run them in either order or at once. For such a pair, structural indiscernibility, independence and parallelism are one fact under three descriptions; independence alone is weaker, and holds of parts the wiring does separate. Keränen's objection, applied to compositions, picks out exactly the duplicated parts, and a form's symmetries measure how much duplication it holds. Duplication is not a defect in a composition; it is what the parallel mode was built to describe.

A cheaper ontology suggests itself. If identity is equality of normal forms, the form might be an expression-type, and the settled ontology of syntactic types would supply its identity conditions without any structural commitment [Wetzel]. It would supply the wrong ones. Distinct writings of one declaration normalise to one normal form, differing in the order and layout in which their parts were set down, and one expression under different declared values normalises to distinct forms. Identity is by normalised structure, and normalisation is a function of the declaration rather than of its text. Nor do the name segments, taken as marks, individuate the positions. Renaming every segment consistently leaves the wiring and the containment untouched, so what a mark is contributes nothing; the pattern of distinctness among the addresses is what the form's identity carries, and that survives any renaming.

The distinction does real work, and the plainest evidence is that systems that compile and deploy already depend on it, named or not. A container image is a type and the running container a token, individuated by the environment it is launched into, which is the relation that crosses into realisation. A content-addressed build derivation, shared unchanged across everything that depends on it, is a type of the other relation, the one lying wholly on the declaration's side [Dolstra]. The reusable parts are the universals; the deployed individual is the particular, its identity conferred at realisation by its environment and not carried by the parts, which are shared identical across instances. None of these systems was built to make the point, so they can serve as evidence; the companion calculus [FA] only regiments what they already embody.

This refutes the second of the two answers the section opened with, that the form is the denotation of the making that produced it. A shadow of one making cannot be pried loose and instantiated, identical, as many tokens. It does less to the deeper opponent, a process-nominalism for which the form's sameness across instances is itself an abstraction over the many makings; against that it shifts the burden rather than settling it. What remains of the keystone question is that standing debate over universals, where the logical form is an unusually strong case for the realist, a checkable governable structure in place of a bare predicate.

Plato and Aristotle divided on one point, whether a form can stand apart from the things that have it [Plato; Aristotle, Metaphysics A.9, M.5]. Aristotle's objection was that a separated form is idle: it explains nothing about the things that have it, and it causes no motion and no change. Against horses and bronze that holds. The form here is not idle, though what it does is govern rather than push. It is prior to every instance rather than abstracted from any, and every realisation answers to it: a build is checked against it, and the check is what fails when the build is wrong. Two writings of one declaration, differing in the order and layout their parts were set down in, normalise to one form [FA, Cor 4.3], so what a realisation answers to is the form and neither writing. His own account of a form preceding its instances does not fit either. In Z.7 the form pre-exists in the soul of the maker, and an author did write the declaration the form follows from [Aristotle, Metaphysics Z.7]. But nobody holds a normal form. It is computed rather than conceived, and beyond a trivial size no mind surveys it. The argument from idleness fails here, and two objections stand in its place. One is Aristotle's own: a universal is a such and never a this, and so does not stand apart from its particulars [Aristotle, Metaphysics Z.13, Z.16]. The other is a nominalism about abstract objects at large. Both belong to the standing debate the residue above names.

The dissolution puts a sharper distinction in its place, the two identities. The type has one identity, the specification owned and versioned. Each token carries another, minted at realisation. How the two relate is settled in the declaration. It is the identity-and-copy question recent work has begun to formalise for computational artefacts: when two tokens of one type are the same artefact, and when a change to the specification ends one type and begins another [Angius–Primiero]. Their criterion is behavioural, identity and exact copyhood by bisimulation, where the criterion here is equality of normal forms and §5 holds that two forms with the same behaviour are still two forms. The two answers disagree, and the disagreement is the deduced/measured line falling between them. That work sits within the finer program ontology the field now maps [Angius–Primiero–Turner]. The type/token cut placed here is offered as the structure those accounts can be set against. The type's identity is the equality of normal forms, decidable and owned, where the token's is conferred at realisation by its environment. Which changes end one token and begin another the maker declares, marking what cannot change without the instance being made anew, and the realising reads that mark. The relation is settled by a constitutional act, which is §3's priority applied to identity. The residue is the standing debate above, which the results do not depend on.

10 Scope

The paper claims a foundation, the arc (§2); a principle, stated in §1 and argued in §3; a characterisation (§6); and a recast keystone (§9). The characterisation's conditions are not claimed exhaustive, only to cover the cases found here and in the cited work (§6), and the per-condition proofs are FA's. The decidability coincidence is claimed for the form; for the instance the claim is only that its running lies on the far side (§6).

One limit lies at the light end of the weight axis (§2). The cut falls in the same place at every weight, since what a thing is in form is its constitution whether heavy or light. What thins as the form lightens is the constitution's purchase on particular behaviour. The lightest forms are of this kind, an inference harness given a set of tools. Reading the constitution there shows that the behaviour is delegated, and shows where: which harness, which tools, and under which mode. The chances within the mode are the substrate's, and lie past the boundary. Those are also the systems the succession criterion of §7 bears hardest on, since a harness that retrains or rewrites itself is on the account's ground only insofar as it passes through declarations that normalise finitarily, and each such pass is a checkable boundary. The boundary is in full force at every weight, and the lightest systems, which are the ones now most discussed, are the systems in which what the thing is and what it does are most easily run together.

The keystone resolves by recategorisation (§9), leaving in its place the standing debate over universals. The new claim is the unification. What a made thing is in form is the layer that its own operation cannot reach. On the logical arc the parts alone settle the form, so the layer stands whatever order the thing was put together in, and that stratum is the one the fields surveyed above each found a feature of.

References

• [Aczel] P. Aczel. Non-Well-Founded Sets. CSLI Lecture Notes 14, Stanford, 1988. (the anti-foundation axiom: sets admitting membership cycles)
• [Angius–Primiero] N. Angius, G. Primiero. The Logic of Identity and Copy for Computational Artefacts. Journal of Logic and Computation 28(6):1293–1322, 2018. (formal identity and copy relations for computational artefacts)
• [Angius–Primiero–Turner] N. Angius, G. Primiero, R. Turner. The Philosophy of Computer Science. Stanford Encyclopedia of Philosophy. plato.stanford.edu/entries/computer-science/. (survey of the program-identity debate and the finer ontologies)
• [Apt–Blair–Walker] K. R. Apt, H. A. Blair, A. Walker. Towards a Theory of Declarative Knowledge. In J. Minker (ed.), Foundations of Deductive Databases and Logic Programming, Morgan Kaufmann, 1988, pp. 89–148. (stratified negation and the standard model; perfect models are Przymusinski's, in the same volume)
• [Aristotle] Aristotle. Metaphysics, Book Θ (potentiality and actuality; Θ.8, the kinds of priority distinguished, in account, in time, and in being); Z.7 (the form pre-existing in the soul of the maker); A.9 and M.5 (the critique of the separated forms, that they explain nothing and cause no change); Z.13 and Z.16 (no universal is a substance, and none exists apart from its particulars); De Anima II (the nutritive soul; first and second actuality); the scholastic axiom agere sequitur esse.
• [Baker] L. R. Baker. The Ontology of Artifacts. Philosophical Explorations 7(2):99–111, 2004. (the constitution view: an artefact constituted by its material without being identical to it).
• [Bergson] H. Bergson. Creative Evolution. Trans. A. Mitchell, Henry Holt, 1911.
• [Carathéodory] C. Carathéodory. Untersuchungen über die Grundlagen der Thermodynamik. Mathematische Annalen 67(3):355–386, 1909. doi:10.1007/BF01450409. (axiomatic thermodynamics; state functions as exact differentials)
• [Cartier–Foata] P. Cartier, D. Foata. Problèmes combinatoires de commutation et réarrangements. LNM 85, Springer, 1969. doi:10.1007/BFb0079468.
• [Chalmers] D. J. Chalmers. A Computational Foundation for the Study of Cognition. Journal of Cognitive Science 12(4):325–359, 2011. doi:10.17791/jcs.2011.12.4.325. (the implementation relation: when a physical system implements a computation).
• [Church] A. Church. An Unsolvable Problem of Elementary Number Theory. American Journal of Mathematics 58(2):345–363, 1936. doi:10.2307/2371045. (undecidability of arithmetic; with [Presburger], the threshold at multiplication)
• [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.
• [Clausius] R. Clausius. Über verschiedene für die Anwendung bequeme Formen der Hauptgleichungen der mechanischen Wärmetheorie. Annalen der Physik 201(7):353–400, 1865. doi:10.1002/andp.18652010702. (entropy introduced as a function of state)
• [Darwin] C. Darwin. On the Origin of Species. John Murray, 1859. (adaptation as a property of the lineage; use-inheritance allowed, the barrier being Weismann's and not Darwin's).
• [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. (a modal type discipline for the staging of computation)
• [Dolstra] E. Dolstra. The Purely Functional Software Deployment Model. PhD thesis, Utrecht University, 2006. (content-addressed derivations as reusable, shared build artifacts).
• [FA] Free Assembly: A Calculus of Composition by Name (companion paper; the decidability coincidence, Prop 5.1; reflection as the minimal feature forcing the carrier out of Set, Prop 6.3; the by-name operator ⊕).
• [Fine] K. Fine. Guide to Ground. In F. Correia, B. Schnieder (eds.), Metaphysical Grounding, Cambridge University Press, 2012, pp. 37–80.
• [Floridi] L. Floridi. The Philosophy of Information. Oxford University Press, 2011. (the method of levels of abstraction).
• [Floridi–Fresco–Primiero] L. Floridi, N. Fresco, G. Primiero. On Malfunctioning Software. Synthese 192(4):1199–1220, 2015. doi:10.1007/s11229-014-0610-3. (software as a type can misfunction in a limited sense and cannot dysfunction)
• [Foundation] The axiom of foundation (regularity) of Zermelo–Fraenkel set theory; see T. Jech, Set Theory, 3rd millennium ed., Springer, 2003. (the cumulative hierarchy; no infinite descending membership chain)
• [Fresco–Primiero] N. Fresco, G. Primiero. Miscomputation. Philosophy & Technology 26(3):253–272, 2013. doi:10.1007/s13347-013-0112-0. (a taxonomy of the ways a computation can go wrong)
• [Gelfond–Lifschitz] M. Gelfond, V. Lifschitz. The Stable Model Semantics for Logic Programming. ICLP/SLP 1988, pp. 1070–1080. (a defined meaning for programs that are not stratified; the model need not be unique)
• [Girard–Taylor–Lafont] J.-Y. Girard, P. Taylor, Y. Lafont. Proofs and Types. Cambridge University Press, 1989. (strong normalisation; decidable conversion bought with termination)
• [Harper–Mitchell–Moggi] R. Harper, J. C. Mitchell, E. Moggi. Higher-Order Modules and the Phase Distinction. POPL '90, pp. 341–354. doi:10.1145/96709.96744.
• [Hilpinen] R. Hilpinen. Artifact. Stanford Encyclopedia of Philosophy, Winter 2011 edition. plato.stanford.edu/archives/win2011/entries/artifact/. (the entry at the undated URL is now Beth Preston's). (an artefact as an object intentionally made to serve a purpose, the maker's intention constitutive).
• [Houkes–Vermaas] W. Houkes, P. E. Vermaas. Technical Functions: On the Use and Design of Artefacts. Springer, 2010. doi:10.1007/978-90-481-3900-2. (function ascription and design in the dual-nature programme).
• [Iris] R. Jung et al. Iris from the Ground Up: A Modular Foundation for Higher-Order Concurrent Separation Logic. JFP 28:e20, 2018. doi:10.1017/S0956796818000151.
• [Irmak] N. Irmak. Software is an Abstract Artifact. Grazer Philosophische Studien 86(1):55–72, 2012.
• [Jones–Gomard–Sestoft] N. D. Jones, C. K. Gomard, P. Sestoft. Partial Evaluation and Automatic Program Generation. Prentice Hall, 1993. (binding-time analysis: a program's inputs divided into static and dynamic, and the program specialised on the static part)
• [Joyal–Street] A. Joyal, R. Street. The Geometry of Tensor Calculus, I. Advances in Mathematics 88(1):55–112, 1991. doi:10.1016/0001-8708(91)90003-P.
• [Keränen] J. Keränen. The Identity Problem for Realist Structuralism. Philosophia Mathematica 9(3):308–330, 2001. doi:10.1093/philmat/9.3.308. (ante rem positions with only structural properties lack identity conditions under a non-trivial automorphism)
• [Ketland] J. Ketland. Structuralism and the Identity of Indiscernibles. Analysis 66(4):303–315, 2006.
• [Kleene] S. C. Kleene. Introduction to Metamathematics. North-Holland, 1952.
• [Kripke] S. A. Kripke. Wittgenstein on Rules and Private Language. Harvard University Press, 1982. (the sceptical argument about rule-following and the communal solution)
• [Kroes–Meijers] P. Kroes, A. Meijers. The Dual Nature of Technical Artefacts. Studies in History and Philosophy of Science 37(1):1–4, 2006. doi:10.1016/j.shpsa.2005.12.001. (the artefact as physical structure under an intentional function; a different duality from Turner's).
• [Ladyman] J. Ladyman. Mathematical Structuralism and the Identity of Indiscernibles. Analysis 65(3):218–221, 2005. (weak discernibility as the reply for non-rigid structures)
• [Lawvere] F. W. Lawvere. Diagonal Arguments and Cartesian Closed Categories. In Category Theory, Homology Theory and their Applications II, Lecture Notes in Mathematics 92, Springer, 1969, pp. 134–145. Reprinted in Reprints in Theory and Applications of Categories 15, 2006, pp. 1–13. (one fixed-point construction behind the Cantor, Russell, Gödel and Tarski diagonals)
• [Lindley–Wadler–Yallop] S. Lindley, P. Wadler, J. Yallop. Idioms are Oblivious, Arrows are Meticulous, Monads are Promiscuous. Electronic Notes in Theoretical Computer Science 229(5):97–117, 2011. doi:10.1016/j.entcs.2011.02.018. (the three interfaces sorted by how much structure each settles in advance)
• [Maturana–Varela] H. R. Maturana, F. J. Varela. Autopoiesis and Cognition: The Realization of the Living. Boston Studies in the Philosophy of Science 42, D. Reidel, 1980.
• [Mazurkiewicz] A. Mazurkiewicz. Trace Theory. LNCS 255, Springer, 1987, pp. 279–324.
• [McBride–Paterson] C. McBride, R. Paterson. Applicative Programming with Effects. Journal of Functional Programming 18(1):1–13, 2008. doi:10.1017/S0956796807006326. (an applicative computation's shape is fixed before any of it runs)
• [McMullin] B. McMullin. John von Neumann and the Evolutionary Growth of Complexity: Looking Backward, Looking Forward. Artificial Life 6(4):347–361, 2000. doi:10.1162/106454600300103674.
• [Moggi] E. Moggi. Notions of Computation and Monads. Information and Computation 93(1):55–92, 1991. doi:10.1016/0890-5401(91)90052-4. (effects reified as a monad over pure values)
• [Moor] J. H. Moor. Three Myths of Computer Science. British Journal for the Philosophy of Science 29(3):213–222, 1978. doi:10.1093/bjps/29.3.213.
• [Newman] M. H. A. Newman. On Theories with a Combinatorial Definition of "Equivalence". Annals of Mathematics 43(2):223–243, 1942. doi:10.2307/1968867.
• [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.
• [Petri] C. A. Petri. Kommunikation mit Automaten. PhD thesis, Technische Hochschule Darmstadt, 1962; issued as Schriften des IIM Nr. 2, Bonn.
• [Piccinini] G. Piccinini. Physical Computation: A Mechanistic Account. Oxford University Press, 2015.
• [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)
• [Plato] Plato. Phaedo 100b–101c (participation in the forms) and Parmenides 130a–135c (the difficulties of separation). Standard editions, e.g. J. M. Cooper (ed.), Complete Works, Hackett, 1997.
• [Pratt] V. Pratt. Modeling Concurrency with Partial Orders. Int. J. Parallel Programming 15(1):33–71, 1986. doi:10.1007/BF01379149.
• [Presburger] M. Presburger. Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. Comptes Rendus du I Congrès des Mathématiciens des Pays Slaves, Warsaw, 1929, pp. 92–101. (decidability of arithmetic with addition alone)
• [Reisig] W. Reisig. Understanding Petri Nets: Modeling Techniques, Analysis Methods, Case Studies. Springer, 2013. doi:10.1007/978-3-642-33278-4.
• [Reynolds] J. C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. LICS 2002, pp. 55–74. doi:10.1109/LICS.2002.1029817.
• [Rice] H. G. Rice. Classes of Recursively Enumerable Sets and Their Decision Problems. Transactions of the American Mathematical Society 74(2):358–366, 1953. doi:10.2307/1990888. (every non-trivial semantic property of a program is undecidable; syntactic properties exempt)
• [Russell] B. Russell. Mathematical Logic as Based on the Theory of Types. American Journal of Mathematics 30(3):222–262, 1908. doi:10.2307/2369948. (the type hierarchy barring self-application)
• [Schaffer] J. Schaffer. On What Grounds What. In D. Chalmers, D. Manley, R. Wasserman (eds.), Metametaphysics, Oxford University Press, 2009, pp. 347–383.
• [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).
• [Shapiro] S. Shapiro. Philosophy of Mathematics: Structure and Ontology. Oxford University Press, 1997. (ante rem structuralism: structures as real objects with identity conditions).
• [Shapiro 2008] S. Shapiro. Identity, Indiscernibility, and ante rem Structuralism: The Tale of i and −i. Philosophia Mathematica 16(3):285–309, 2008.
• [Tarski] A. Tarski. The Concept of Truth in Formalized Languages. Trans. J. H. Woodger, in Logic, Semantics, Metamathematics, Clarendon Press, 1956, pp. 152–278 (Polish original 1933; German translation 1935). (the stratified hierarchy of languages barring semantic self-reference)
• [Thomasson] A. L. Thomasson. Artifacts and Human Concepts. In E. Margolis, S. Laurence (eds.), Creations of the Mind: Theories of Artifacts and Their Representation, Oxford University Press, 2007, pp. 52–73. (artefactual kinds settled by the maker's substantive intention).
• [Turing] A. M. Turing. On Computable Numbers, with an Application to the Entscheidungsproblem. Proceedings of the London Mathematical Society s2-42(1):230–265, 1937. doi:10.1112/plms/s2-42.1.230. (the universal machine; the printing problem and the Entscheidungsproblem shown undecidable, halting being the standard later formulation)
• [Turner] R. Turner. Computational Artifacts: Towards a Philosophy of Computer Science. Springer, 2018. doi:10.1007/978-3-662-55565-1. (the dual nature of computational artefacts, abstract specification and concrete implementation).
• [Van Gelder–Ross–Schlipf] A. Van Gelder, K. A. Ross, J. S. Schlipf. The Well-Founded Semantics for General Logic Programs. Journal of the ACM 38(3):619–649, 1991. doi:10.1145/116825.116838. (a unique three-valued model for any normal program)
• [Weismann] A. Weismann. Das Keimplasma: eine Theorie der Vererbung. Gustav Fischer, 1892. (the germ-plasm barrier: the individual's acquisitions are sequestered from its lineage)
• [von Neumann] J. von Neumann. Theory of Self-Reproducing Automata. Ed. A. W. Burks. University of Illinois Press, 1966.
• [Wadler] P. Wadler. The Essence of Functional Programming. POPL 1992, pp. 1–14. doi:10.1145/143165.143169. (monads structuring effects in a pure language)
• [Walters] P. Walters. An Introduction to Ergodic Theory. Graduate Texts in Mathematics 79, Springer, 1982. (invariant measures held apart from the orbits that run over them)
• [Wetzel] L. Wetzel. Types and Tokens. MIT Press, 2009. (the standing ontology of types, including expression-types)
• [Whitehead] A. N. Whitehead. Process and Reality. Corrected ed., Free Press, 1978 (originally 1929).
• [Winskel] G. Winskel. Event Structures. LNCS 255, Springer, 1987, pp. 325–392.
• [Wittgenstein] L. Wittgenstein. Philosophical Investigations. Trans. G. E. M. Anscombe, Blackwell, 1953. (rule-following: a rule does not determine its own application, §§185–242)
• [Yanofsky] N. S. Yanofsky. A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points. Bulletin of Symbolic Logic 9(3):362–386, 2003. doi:10.2178/bsl/1058448677. (Lawvere's scheme extended to the halting problem and Rice's theorem)

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