Eliminating mutation may require changing how data is routed
Working argument, 4 October 2026.
Imagine reading a row of bits, then returning those same bits in a previously chosen order. A mutable implementation can keep two linked routes through the same cells: one route for writing, another for reading. The routes do not depend on whether the incoming bits are zero or one.
Can an immutable implementation retain that independence and still run just as quickly? Under the finite-register model below, the answer is no. This narrows a powerful possible compilation theorem: constant-overhead mutation elimination, if it exists in our broader finite-data model, cannot always preserve data-oblivious routing.
The broader goal remains to characterize future behavior maintained by finite rules, bounded local access and bounded allocation. The result here concerns all implementations within an explicitly restricted immutable class. It does not refute candidate C, whose implementations may organize memory according to incoming values.
Contents
The stronger statement being tested
Consider the following strengthening of C:
Every finite-data local mutable machine with payload-independent routing has a constant-overhead immutable realization whose routing remains independent of those payloads.
Here routing includes allocation shape, pointer selection, field selection, traversal, command completion and control flow. It is not enough to remove conditional branches while retaining a bit-indexed pointer lookup.
We give a written refutation of this strengthening. The argument adapts the chronological counting method in Pippenger’s Pure versus Impure Lisp, Section 4. The replacement hypothesis is structural independence from the current binary payload, rather than his unbounded alphabet of fresh atoms. Novelty has not been established; this is not a formally verified or independently reviewed proof.
Exact immutable model
Fix one deterministic finite program with a fixed number of registers, a finite set of node tags and payload symbols, and a fixed bound on record arity. A primitive reads one bounded record component, copies a register, allocates one bounded record, performs one of a fixed finite set of Boolean operations, or reads/writes one stream symbol. Constant-sized batches change only constants.
Registers and fields can carry pointers or finite payloads. Every field is fixed at allocation and points only to an older record, if it is a pointer. A primitive cannot compare physical addresses, perform address arithmetic, invoke an arbitrary stored function at unit cost, or inspect an unbounded scalar. There is no ambient mutable table or late-filled field. All recursion and navigation use the same fixed-register machine and charged records.
A phase starts from any prepared heap and register state, then receives fresh input bits and produces them in a specified permutation. Input bits are payloads. We call the implementation payload-oblivious during that phase if, after fixing the initial state and phase length, its structural instruction sequence is the same for all payload vectors. Finite Boolean gates and copied payload values may differ in value, but not in which gate, register, field or pointer route is used. In particular, fresh payloads cannot select a pointer, choose an allocation plan, control a loop or change the stopping time.
This is a precise restriction, not a claim about all functional programs. The program can choose its structural instructions using the permutation or any other information available before the phase. It may have different instructions on different phases. Previous payloads are fixed when analyzing the next phase. Correctness still requires every possible current payload vector.
Preparation may be arbitrarily large for the single-phase lower bound. The program and its register bound are fixed independently of and the permutation. A separately hardwired program with registers is outside this uniform claim.
Why prepared immutable memory cannot supply a fresh payload
Call every record existing at phase entry old. An old record cannot contain a pointer to a record allocated during the phase. Following fields inside old memory therefore never discovers a newly read payload. Old memory can supply routing instructions, old pointers and finite constants. The fresh input dependency must be carried by registers or newly allocated records.
This fact permits a finite description of a phase’s behavior. Record each executed primitive and each finite response obtained by reading old memory. A returned old pointer needs only an old-pointer marker: its future dereferences have their own recorded responses. No physical identity test can distinguish the markers. Reads of new records are determined by their earlier construction, so their pointer relationships do not need separately encoded addresses. Fresh input reads are symbolic variables , and finite payload computations are the recorded gates.
For a fixed program there is a constant such that at most such descriptions have length at most , absorbing the finitely many initial control/payload states and the fixed register tuple into . Initial pointer registers are marked old or missing. Null tests, node kinds and all old finite values are included in the description.
Each description determines at most one Boolean input/output function. To reconstruct it, start with the old markers and symbolic inputs, build every new record according to the recorded primitive, and supply the recorded finite responses whenever old memory is inspected. The absence of identity tests is essential. The absence of old-to-new pointers is essential too. Payload-obliviousness makes the same description valid for all current inputs, rather than just one execution.
Single-phase obstruction
For a permutation of , let
There are distinct Boolean functions of this form. If two permutations differ at an output position, an input with a single one distinguishes them. Thus a fixed payload-oblivious immutable program cannot correctly implement more than of these functions in at most phase steps, regardless of the prepared heaps used for those permutations.
Consequently, some permutation requires
This is not an output-length argument: only bits are returned. It is a restriction on how a bounded-register immutable machine can apply a prepared routing pattern to new payloads without using their values to choose structure.
Repetition charges the entire preparation
There is a fixed mutable finite-data machine that constructs cells linked in the order . A unary description of lets it traverse that list and install a second route through the cells. Each unary symbol causes only bounded local work. Creating the cells, processing the unary indices and delimiters takes commands. Correctness is required on valid permutation descriptions; the machine can have any fixed bounded-step behavior on malformed descriptions.
In each subsequent phase, the machine reads bits while following the first route and overwriting the corresponding finite payload fields. It then follows the second route, returning one bit on each of dummy commands. It can echo the input bit during the loading half. The phase boundaries are tracked by route endpoints, not by an unbounded integer primitive. Each command takes constant local work. Routing in these phases is independent of the payload bits, and even the source’s incoming pointer degree is bounded by a constant.
Fix any correct payload-oblivious immutable simulator. Consider phases, with every preceding payload fixed to zero when analyzing a particular phase. For each phase , let contain the permutations on which its cost is at most . The single-phase description argument still applies to the entire heap present at that phase, so
Choose . For sufficiently large , this is positive and . The union of the easy sets has size at most . One permutation lies outside every easy set. For that same permutation, all phases on the actual all-zero payload history cost more than each.
The complete finite-alphabet command sequence has encoded length
The lower bound includes all phase work; any target preparation adds to it. It therefore refutes a uniform constant-overhead compiler preserving this obliviousness property, even with amortized total time as its conclusion. The incoming-degree promise alone cannot replace the missing model hypotheses.
There is no claim that an unrestricted immutable implementation must be slow on all-zero inputs. Detecting their special values and taking a different route is precisely an option excluded here. The theorem quantifies over payload-oblivious implementations, not every representation permitted by C.
Why this does not prove the unrestricted binary separation
Two concrete tests locate the remaining gap.
Encoding the old symbolic example changes its cost. Replacing distinct opaque atoms by fixed-width distinct binary names needs width at least . The resulting input/output length is , so the numerical symbolic lower bound would be only linear in that new length even if it transferred. It does not transfer automatically: bit inspection permits operations absent from the symbolic model. This closes that direct encoding route, not every binary lower-bound argument.
A prepared truth table defeats the oblivious description argument. For any fixed Boolean map , prepare a full binary decision trie whose leaf for points to the ready output list . Each input bit chooses one edge, and each output command follows one list cell. Every command costs with immutable records. The route now depends on the fresh payload.
For , a simple finite-rule enumeration builds the trie and output lists in local work and total historical allocations; the final reachable table needs records. Traversal and enumeration stacks are included in the historical bound. This construction is not a solution to C: its preparation is exponentially larger than the source’s prologue. It is a control showing why arbitrary prepared storage and value-sensitive routing invalidate the oblivious counting step. Ready output lists may contain only pre-existing zero and one values; their outputs need not preserve the identity of newly received bit occurrences.
Primary literature and what was actually checked
- Pippenger, Pure versus Impure Lisp, author report TR95-23, Section 4, report pp.6-9: the chronological description/counting strategy and repeated-phase selection are adapted here. Its original separation uses fresh opaque atoms, not our binary obliviousness hypothesis. The finite-alphabet qualification is explicit on p.8. The present proof must therefore stand on its separately stated description argument.
- Bird, Jones and de Moor, A Lazy Pure Language versus Impure Lisp, sections “A real-time on-line lazy implementation” and “Lazy versus normal-order”: their transposition construction shares a repeatedly used computation. The evaluator replaces a shared closure by its result. An eager normal-order translation repeats work; their note explains this explicitly. The stated aggregate bound, including its treatment of the prologue, is not by itself a worst-case command bound in our immutable-at-allocation model.
- Driscoll, Sarnak, Sleator and Tarjan, Making Data Structures Persistent, Section 2.3.2, printed pp.94-96, and Section 3.3: the inspected algorithms fill extra fields, update copy/predecessor information and navigate using version metadata. Their analysis supplies amortized update costs. Section 6, p.122, states a write-once/pure-LISP consequence, but does not furnish here a verified bounded-local immutable-at-allocation online translation. We have not imported that consequence as a proof of C or claimed the classical persistence theorem false.
The shared issue is concrete: a pre-existing location that later leads to a freshly computed value violates the chronological premise of this proof. Lazy closure updates and late filling cannot be silently treated as ordinary immutable construction. This observation alone is not a semantic lower bound against alternative representations.
What this teaches about the larger statement
The proposed universal theorem must allow a change in computational strategy. Preserving a mutable program’s payload-independent access pattern is too strong, even for bits and a simple fixed permutation task. If C is true, its compiler must sometimes use values to reorganize access, or use another mechanism outside the restricted class proved impossible here.
There is a second consequential simplification. Excluding an explicit pointer-equality instruction does not substantially weaken the mutable source class in C. Give every source node one extra scratch bit, zero between commands. To compare non-null pointers and , set the bit at , read the bit at , then clear the bit at . The answer is one exactly when the pointers coincide, and all scratch bits are restored. Missing pointers are handled separately. Every original transition still takes bounded work, with a finite label enlargement and fixed finite initialization. Thus C is equivalent, up to constants, to its version allowing source pointer equality. No address arithmetic follows from this argument.
The target cannot use the same trick on immutable records. A successful simulator must represent the required identity behavior by another means. This does not itself refute C: a whole-state representation may retain relationships between its registers. Nor does C grant a free operation comparing arbitrary externally supplied object handles; obtaining and routing those handles remains charged. The distinction between whole-program realization and preserving an opaque component interface is therefore another essential test of a proposed foundational theorem.
The next question is whether that freedom suffices with only linear preparation and allocation, and uniform command deadlines. A complementary literature comparison concerns reuse of partial computations: which benefits arise from an immutable snapshot, which require a mutable memo table, and which require exposing a continuation that an otherwise opaque component would not provide? These are candidate structural distinctions for the broader characterization, not a claim that a sharper permutation bound alone will settle it.