A trace is not a machine

Multiple realisation begins with a useful refusal. A function need not be chained to one material recipe. A valve can be brass, ceramic or a flexible membrane. Addition can be carried by silicon transistors, relays, gears or carefully arranged fluid channels. In philosophy of mind, Putnam used variation across possible organisms to challenge the claim that a mental kind must be identical to one neural kind; Fodor extended the anti-reductionist pressure to the special sciences. Putnam 1967; Fodor 1974.

That refusal is not permission to ignore material organisation. A ceramic disc counts as a valve because pressure differences move it in ways that regulate flow. A painted circle on the pipe does not become a valve because an observer can label “open” and “closed” regions on its surface. Substrate independence is independence from irrelevant material detail, not independence from causal detail.

The phrase “same computation” often slides across three different claims. Two devices may calculate the same mathematical function, such as parity, while using different algorithms. They may implement the same stateful algorithm while differing in clock rate, energy use or fault behaviour. They may also be interchangeable in one operating environment. These claims form a ladder. A lookup table and a long-division routine can return the same quotients without traversing the same intermediate states. A cycle-accurate emulator can preserve a processor’s instruction transitions yet miss a hard real-time deadline. This paper focuses on the middle relation, then asks what must be added before replacement is justified.

The abstraction therefore sets the burden. If the target is merely the Boolean function XOR, many gate arrangements qualify. If the target includes hazards between gate changes, fewer qualify. If the target includes the chemistry of a neuron, a silicon circuit may preserve a computational role while failing the biological specification. Asking whether “the substrate matters” before naming the invariant invites a verbal dispute. Multiple realisation is always multiple realisation of a specified organisation.

This is why the universal-implementation challenge is serious. If state classes may be invented after the whole history is known, almost any sufficiently varied physical trajectory can be redescribed as a run of almost any finite machine. Searle used the apparent ubiquity of such descriptions to question whether computation is intrinsic to physics. The practical answer developed here is not that labels are forbidden. Every measurement uses labels. It is that the labels must be fixed independently enough to survive interventions that the observed history did not dictate. Searle 1990.

The rock that follows instructions after the fact

Suppose a rock cools through a unique sequence of microstates between noon and one o’clock. After observing the sequence, we divide those microstates into two disjunctive classes and call them A and B. The labels alternate perfectly. Have we discovered a two-state machine?

The right answer is yes, if the earlier claim was that the rock implemented the A-to-B transition rule. The actual sequence did not carry that rule. We supplied it by choosing labels after seeing the sequence. Chalmers’s response to Putnam’s triviality construction makes this distinction explicit: implementation must support counterfactual transitions and mirror formal transitions that did not happen on the chosen run, rather than only material conditionals along that run. Chalmers 1996.

This does not make implementation mysterious. It makes it experimental. Ask what variables can be measured, set and perturbed; ask which transitions follow; ask whether the same classification works before and after the intervention. The next step is to say exactly what must commute.

flowchart TD
  A["The replay box"] --> B["A trace is not a machine"]
  B --> C["The relation that must survive"]
  C --> D["Where substitution breaks"]
  D -. "re-test" .-> A
  classDef first fill:#0a1424,stroke:#D95545,stroke-width:2px,color:#e6f3ff
  classDef step fill:#0a1424,stroke:#3f7da0,stroke-width:1px,color:#e6f3ff
  class A first
  class B,C,D step

The relation that must survive

Imagine replacing a relay controller one component at a time. The first relay becomes a transistor circuit. The next becomes an optical switch. Eventually no original material remains. At every step, engineers can place the controller in each relevant state, apply each admissible input and verify the successor state and output. The replacement feels continuous because the tested organisation remains continuous.

The decisive object is not a material part or an output list. It is an intervention-bearing transition structure. We need a mapping from physical states to abstract states, plus evidence that physical evolution respects the abstract rule throughout the relevant test envelope.

The smallest useful formalism

Let the abstract computation be a deterministic transducer. It has abstract states Q, inputs U, outputs Y, a transition rule δ and an output rule λ. The physical candidate has physical states X, physical inputs I, physical evolution F and physical readout G. Three maps connect the levels: φ_Q classifies physical states, φ_U classifies physical inputs, and φ_Y decodes physical outputs.

Read the first line from left to right. Start with a physical state and input. Let the device evolve. Then classify the resulting physical state. The result should match what the abstract rule predicts after classifying the starting state and input. The second line makes the same demand of the output. The two routes should agree within a declared tolerance when the system is noisy or analogue. Horsman and colleagues express a related idea through commuting physical and abstract evolutions; Stepney and Kendon make the representation relation and tolerated error explicit. Horsman et al. 2014; Stepney and Kendon 2021.

The deterministic equation assumes that the same mapped state and input lead to the same successor within tolerance. Remove that assumption and the object of comparison must change. A noisy device may need transition distributions rather than single successors. An adaptive device may require a state that includes its update rule or parameter version. A concurrent device may perform several invisible internal steps before an observable event, so a strict step-for-step comparison becomes too strong. Formalism clarifies the choice only after the modeller decides which physical variations count as noise, hidden state or part of the computation.

The equations compress the claim, but they do not choose the right variables. A mischievous analyst can still invent φ after observing the device. Three additional disciplines make the mapping evidential rather than decorative.

Coverage, causality and factorisation

Coverage asks whether every abstract state and input relevant to the claim has a physical representative inside the declared envelope. A controller does not implement a four-state specification merely because two visited states map cleanly. Unreached states may be tested by direct state setting, carefully constructed histories or a validated lower-level model. If none is possible, the claim must remain at a weaker grade.

Causal relevance asks whether mapped variables make the predicted difference. If two physical states are both labelled B, perturbing irrelevant dust on the casing should not count as setting B. Conversely, if changing a voltage band changes the next mapped state exactly where δ says it should, the voltage is more than correlated with the computation. It participates in the transition.

Factorisation matters when the abstract state contains several variables. Suppose a controller state is a pair [door, alarm]. The formal model permits the door bit to vary while the alarm bit stays fixed. If the physical mapping represents each pair by an indivisible, post-hoc class with no corresponding independent variation, the realiser may match the flat state table while failing the compositional claim. Chalmers introduced combinatorial-state automata partly to block arbitrary whole-state mappings; Godfrey-Smith similarly presses for physically grounded parts and groupings. The adequacy of any exact independence requirement remains debated, especially for integrated analogue systems.

How much testing changes the answer

The difference between a trace and a transition structure can be counted. Take every deterministic three-state, two-input Mealy machine with a binary output. There are 6⁶ = 46,656 possible tables because each of six state-input pairs can choose one of three successor states and one of two outputs. Pick one target machine and test candidates only through outputs from the initial state.

The remaining pair matters. One table uses the internal labels B and C in the opposite order, but the mapping swaps them back. Every transition and output relation is preserved. A test that demanded literal state names would reject a genuine multiple realisation. Good implementation tests are strict about relations and permissive about representation.

Where substitution breaks

The formal condition still leaves three practical choices exposed: where the system ends, which physical grouping is privileged, and what the word “same” excludes. These are not editorial details. They determine whether a replacement is a realiser, a dependent component or merely a convenient model.

The memory outside the box

The answer depends on the candidate boundary. The terminal alone does not preserve the state transition because its next response is not determined by a local state. The coupled terminal-service system may do so. Calling the terminal a “computer” in ordinary speech is harmless; claiming local computational equivalence for safety certification is not. State, clock, input transduction and output effect must sit somewhere in the declared realiser.

Boundary choice changes the proposition, not the physical events. Under the local boundary, unplugging the cable is an intervention on the environment and the terminal has no successor-state rule of its own. Under the coupled boundary, the same unplugging is an internal link failure that the larger candidate must model. A third boundary might include the door motor and its position sensor because the controller’s next state depends on a completed physical effect. Each boundary can be legitimate for a different question. What is illegitimate is beginning with the terminal, discovering the missing state, and silently expanding the candidate until the test passes.

A useful boundary dossier names four items before testing: where persistent state resides, which clock orders transitions, where inputs become typed symbols, and where outputs become effects. It also records external dependencies whose failure can change the abstract transition. This turns the familiar claim “the cloud service is part of the system” into a testable statement about state and causal closure rather than an architectural slogan.

The grouping problem

Even counterfactual transitions do not uniquely select a computational description. A physical gate with three voltage bands can sometimes be coarse-grained in more than one way. Under one partition it behaves like AND; under another it behaves like OR or NAND. Shagrir uses constructions of this kind to argue that a physical system may simultaneously implement distinct automata under different groupings, even when each grouping respects causal transitions. Shagrir 2012.

This is a genuine boundary on any simple mapping theory. The practical response is not to pretend that one grouping is written into nature in capital letters. It is to expose the warrant for the grouping. Circuit theory may privilege voltage thresholds because they are engineered noise margins and because downstream components respond to them. A biological model may privilege ion-channel states, population rates or spike timing for different explanatory tasks. Piccinini adds the organised function of producing strings according to a general rule; Horsman’s framework adds a representation relation and a compute cycle. Piccinini 2007; Horsman et al. 2014.

The audit therefore freezes the grouping before the outcome is known and asks whether it remains stable under nearby conditions. Do the same voltage bands predict transitions on another unit, after mild noise, and under a different input order? Do downstream components respond to those bands as the model assumes? Could a rival partition pass the same tests while supporting a materially different claim? A mapping that survives replication and perturbation has more warrant than one tailored to a single run, even though no finite test proves that it is the only possible description.

Time, noise and the abstraction envelope

The answer follows the specification. If time is absent from the abstract machine, both realise the same untimed transition system, while only one is operationally substitutable. If deadlines, synchronisation or rates are part of the formal object, the slow device fails the computation claim itself. The same applies to stochastic transitions, tolerated analogue error, resource bounds and irreversible side effects. Equivalence is indexed to what the abstraction says must be preserved.

This indexing prevents two opposite mistakes. One is substrate chauvinism, which treats every physical difference as computationally decisive. The other is implementation magic, which calls every difference irrelevant once outputs look similar. An explicit envelope says which perturbations, timings and physical variations the claim survives, and which remain outside it.

stateDiagram-v2
  [*] --> Claim
  state "The rock that follows<br/>instructions after the fact" as Claim
  state "The smallest useful formalism" as Test
  state "Coverage, causality and<br/>factorisation" as Revision
  Claim --> Test: expose mechanism
  Test --> Decision: evidence survives
  Test --> Revision: rival survives
  Revision --> Claim: narrow or rebuild
  Decision --> [*]

The realiser-substitution lab

The practical contribution is an evidence ladder and a test harness. The ladder prevents a weak observation from silently turning into a strong substitution claim. It is not a universal consciousness score or a metaphysical verdict. It is a disciplined answer to a narrower engineering question: what has this candidate demonstrated about the computation it is claimed to realise?

Six grades, one monotonic rule

G0, trace resemblance: one recorded run matches. This licenses regression triage or demonstration, not substitution. G1, input-output conformance: a declared family of input histories yields the expected outputs from the initial condition. This may support black-box compatibility within that family. G2, state-transition conformance: mapped internal states and every relevant state-input branch agree with the abstract table.

G3, intervention-preserving realisation: the candidate states can be set or reached independently enough to test the branch claims, and the mapped variables are causal difference-makers. G4, compositional realisation: any claimed substate structure, concurrency or modular composition also survives the relevant interventions. G5, operational substitutability: boundary, timing, error, reset, resource and side-effect invariants required by the use case are preserved.

The monotonic rule is simple: never make a grade-N decision using grade-(N−1) evidence. A G1 result can be valuable. It becomes dangerous only when translated into a G3 or G5 claim without the missing tests.

Apply the ladder from the decision backwards. A visual demonstration may need only G0. Replacing an API implementation whose contract is deliberately stateless may need G1 plus error semantics. Replacing a persistent controller requires state witnesses, so G2 is the minimum. Claiming that a different physical mechanism realises the same computation requires G3 because the mapped states must be manipulable difference-makers. A modular architecture needs G4 when independent subcomponents and interleavings are part of the claim. Safety or financial execution usually needs G5 because deadlines, duplicate effects, reset behaviour and recovery are not optional decoration.

The smallest useful audit needs one abstract table, one declared boundary, one physical-state map and one intervention per relevant branch. Run it first on a deliberately bad replay candidate. If the replay reaches G2, the test harness is too weak. Then run a known realiser and record every failed assumption. This negative control prevents an impressive interface from becoming evidence of an untested mechanism.

What the checker actually tests

The checker encodes an abstract state table, a candidate’s physical states, the physical-to-abstract map, physical transitions, state-settability flags and an operational envelope. It begins with the same fixed trace used by the replay box. It then attempts every abstract state-input pair. Where a candidate provides a physical model, the checker searches for a mapping witness and reports the first mismatch. Finally, it asks whether the declared boundary contains the state and whether the timing budget is met.

A positive G3 result permits the claim that the candidate realises this finite-state transducer under the tested mapping and envelope. A positive G5 result permits operational substitution for the listed invariants. A negative result does not show that the device computes nothing. It may show that the candidate implements a different computation, that the boundary is wrong, that the state abstraction is too coarse, or that the evidence cannot support the requested grade.

The browser lab uses synthetic transition tables so that the logic remains inspectable. To apply the instrument to hardware or software, replace the table lookup with an adapter that can initialise a physical state, deliver one typed input, observe the successor state, capture the output and read back the outcome through a path independent of the command. Freeze firmware, model, configuration and mapping versions in the result. When a state cannot be set directly, document the input history used to reach it and the assumptions that make that history a valid surrogate intervention.

Run the audit under nominal conditions first, then widen one envelope dimension at a time. Add timing jitter, sensor noise, process restart, network loss or a competing input. The first failed branch is more useful than an aggregate percentage because it identifies which claimed relation broke. Repeating the same happy path thousands of times can estimate reliability on that path, but it cannot manufacture evidence for an unvisited fault state.

The instrument cannot decide whether the chosen abstraction is scientifically privileged. It can expose its cost. A finer abstraction demands more states, interventions and boundary commitments; a coarser one may hide precisely the failure that matters. The smallest defensible implementation is therefore not the most detailed model available. It is the least detailed model whose omitted distinctions cannot change the decision under review.

from __future__ import annotations

from dataclasses import dataclass, replace
from itertools import product
from typing import Dict, Mapping, Sequence, Tuple

AbstractState = str
PhysicalState = str
Input = int
Output = int
Transition = Tuple[PhysicalState, Output]


@dataclass(frozen=True)
class AbstractMachine:
    states: Tuple[AbstractState, ...]
    inputs: Tuple[Input, ...]
    initial: AbstractState
    table: Mapping[
        Tuple[AbstractState, Input],
        Tuple[AbstractState, Output],
    ]


@dataclass(frozen=True)
class Candidate:
    physical_states: Tuple[PhysicalState, ...]
    initial: PhysicalState
    mapping: Mapping[PhysicalState, AbstractState]
    table: Mapping[Tuple[PhysicalState, Input], Transition]
    settable: frozenset[PhysicalState]
    boundary_complete: bool
    latency_ms: int
    compositional_verified: bool = True


def audit(
    abstract: AbstractMachine,
    candidate: Candidate,
    deadline_ms: int,
) -> Tuple[str, Tuple[str, ...]]:
    """Return the highest warranted grade and its supporting witnesses."""
    notes: list[str] = []

    mapped = set(candidate.mapping.values())
    if mapped != set(abstract.states):
        missing = sorted(set(abstract.states) - mapped)
        return "G1", (f"State coverage is incomplete: {missing}.",)

    for p_state, a_state in candidate.mapping.items():
        for inp in abstract.inputs:
            key = (p_state, inp)
            if key not in candidate.table:
                return "G1", (f"Missing physical branch {key!r}.",)

            physical_next, physical_out = candidate.table[key]
            if physical_next not in candidate.mapping:
                return "G1", (
                    f"Successor {physical_next!r} has no abstract mapping.",
                )

            actual = (candidate.mapping[physical_next], physical_out)
            expected = abstract.table[(a_state, inp)]
            if actual != expected:
                return "G1", (
                    f"Witness: {p_state!r} mapped to {a_state!r}, "
                    f"input {inp} produced {actual}, expected {expected}.",
                )

    notes.append("G2: every mapped state-input branch commutes.")

    unsettable = set(candidate.physical_states) - set(candidate.settable)
    if unsettable:
        return "G2", tuple(
            notes + [f"Unsettable mapped states: {sorted(unsettable)}."]
        )
    notes.append("G3: every mapped state is intervention-accessible.")

    if not candidate.compositional_verified:
        return "G3", tuple(
            notes + ["Claimed substate composition is not verified."]
        )
    notes.append("G4: composition is verified, or no non-trivial composition is claimed.")

    if not candidate.boundary_complete:
        return "G4", tuple(
            notes + ["The declared boundary omits required state or control."]
        )
    if candidate.latency_ms > deadline_ms:
        return "G4", tuple(
            notes
            + [
                f"Latency {candidate.latency_ms} ms exceeds "
                f"the {deadline_ms} ms deadline."
            ]
        )

    return "G5", tuple(
        notes + ["G5: boundary and operational deadline pass."]
    )


def enumerate_trace_lookalikes(
    target: AbstractMachine,
    trace: Sequence[Input],
) -> int:
    """Count all 3-state, 2-input, binary-output tables matching one trace."""
    choices = tuple(product(target.states, (0, 1)))
    pairs = tuple(product(target.states, target.inputs))

    def outputs(
        table: Dict[Tuple[str, int], Tuple[str, int]],
    ) -> Tuple[int, ...]:
        state = target.initial
        result: list[int] = []
        for inp in trace:
            state, out = table[(state, inp)]
            result.append(out)
        return tuple(result)

    expected = outputs(dict(target.table))
    survivors = 0
    for assignments in product(choices, repeat=len(pairs)):
        table = dict(zip(pairs, assignments))
        survivors += outputs(table) == expected
    return survivors


def enumerate_history_survivors(
    target: AbstractMachine,
    max_depth: int = 5,
) -> Dict[int, int]:
    """Count candidates matching every input history at each exact depth."""
    if max_depth < 1:
        raise ValueError("max_depth must be at least 1")

    choices = tuple(product(target.states, (0, 1)))
    pairs = tuple(product(target.states, target.inputs))

    def outputs(
        table: Dict[Tuple[str, int], Tuple[str, int]],
        history: Tuple[int, ...],
    ) -> Tuple[int, ...]:
        state = target.initial
        result: list[int] = []
        for inp in history:
            state, out = table[(state, inp)]
            result.append(out)
        return tuple(result)

    counts: Dict[int, int] = {}
    for depth in range(1, max_depth + 1):
        histories = tuple(product(target.inputs, repeat=depth))
        expected = {
            history: outputs(dict(target.table), history)
            for history in histories
        }
        survivors = 0
        for assignments in product(choices, repeat=len(pairs)):
            table = dict(zip(pairs, assignments))
            survivors += all(
                outputs(table, history) == target_output
                for history, target_output in expected.items()
            )
        counts[depth] = survivors
    return counts


def example() -> None:
    target = AbstractMachine(
        states=("A", "B", "C"),
        inputs=(0, 1),
        initial="A",
        table={
            ("A", 0): ("A", 0),
            ("A", 1): ("B", 0),
            ("B", 0): ("C", 1),
            ("B", 1): ("A", 0),
            ("C", 0): ("B", 1),
            ("C", 1): ("C", 0),
        },
    )

    relay = Candidate(
        physical_states=("low", "mid", "high"),
        initial="low",
        mapping={"low": "A", "mid": "B", "high": "C"},
        table={
            ("low", 0): ("low", 0),
            ("low", 1): ("mid", 0),
            ("mid", 0): ("high", 1),
            ("mid", 1): ("low", 0),
            ("high", 0): ("mid", 1),
            ("high", 1): ("high", 0),
        },
        settable=frozenset({"low", "mid", "high"}),
        boundary_complete=True,
        latency_ms=8,
    )
    slow_emulator = replace(relay, latency_ms=220)

    for name, candidate in (
        ("relay", relay),
        ("slow emulator", slow_emulator),
    ):
        grade, notes = audit(target, candidate, deadline_ms=100)
        print(f"{name}: {grade}")
        for note in notes:
            print(f"  - {note}")

    trace = (1, 0, 1, 1, 0, 0)
    survivors = enumerate_trace_lookalikes(target, trace)
    print(f"tables matching only the demo trace: {survivors:,}")

    depth_counts = enumerate_history_survivors(target, max_depth=5)
    print(
        "tables matching every history at depths 2 to 5: "
        + ", ".join(
            f"d{depth}={depth_counts[depth]:,}"
            for depth in range(2, 6)
        )
    )


if __name__ == "__main__":
    example()

Choose Download Python checker, then run python3 realiser_substitution_audit.py. The example should report G5 for the relay, G4 for the slow emulator, 3,852 tables matching the demonstration trace, and the depth counts plotted in Figure 5. Change the state table, boundary flags or deadline to audit another synthetic candidate.

The downloadable checker is intentionally small. It assumes deterministic finite-state machines, explicit state mappings and exact outputs. It should not be applied unchanged to continuous dynamics, probabilistic programs, quantum processes, learning systems whose transition law changes during the test, or concurrent systems where internal steps require a weak observational equivalence. Formal methods such as bisimulation provide richer back-and-forth relations for those settings. Hennessy and Milner 1985.