Shared mutation can coexist with complete checkpoints

The broader goal is to understand when future behavior can be represented by finite rules with bounded local access and allocation. A strong sufficient statement survives a meaningful test: an unbounded tree can have arbitrarily many mutable links into a fixed finite shared core, while retaining constant-cost complete checkpoints. The statement below is conditional on the explicit real-time functional deque premise from the tree checkpoint assessment.

Consider many directory entries referring to one shared settings node. Editing that node must affect every reference in the current version. Returning to yesterday’s version must restore yesterday’s settings everywhere. Copying settings independently for each directory entry would implement the wrong behavior. Updating every reference would be expensive. Instead, references retain a finite target tag and each version retains its own interpretation of that tag.

The number of references can grow without bound. What is fixed here is the number of distinguished targets, not their incoming degree, the depth of the tree, or the amount of data reachable from them. This gives a positive case with genuine observable aliasing. It is not a general theorem eliminating mutation from arbitrary graphs.

Exact conditional statement

Fix constants $D\ge2$, $k\ge1$, $r\ge1$, and $q\ge1$, and a finite payload alphabet. A logical state consists of:

• a finite rooted tree with at most $D$ children per node, in named finite ports;
• at most $r$ distinct permanent distinguished nodes, registered under distinct names in the fixed set $\Gamma=\{1,\ldots,r\}$;
• at most $k$ moving cursors;
• a finite payload and $q$ mutable reference fields at each node. Each field is null or points to one registered distinguished node.

The distinguished nodes remain ordinary mutable tree nodes: they can have large evolving subtrees. Registration fixes their identities within a component; it does not freeze their labels or children. The tree is the supplied navigation backbone. Parent navigation is available, but arbitrary reassignment of its edges is not a primitive.

Commands read/write a payload at a cursor, move to parent or a named child, reset to the root, assign one cursor the location of another, insert a fresh leaf at a cursor, delete an unmarked leaf child, set/clear a reference field using a registered name, follow a reference field, and compare two cursor locations. A distinguished node or a node occupied by a cursor cannot be deleted. Invalid commands return a designated failure symbol and preserve the state. All commands and outputs have fixed finite alphabets. There is no external arbitrary-node handle interface.

Conditional theorem (finite shared core). Assume premise D: purely functional catenable deques of opaque bounded-arity records admit uniform worst-case bounded pointer access and allocation, using finite tags, with no mutation, unbounded arithmetic, or deferred work. Then the interface above has a deterministic immutable finite-rule realization. For each fixed $D,k,r,q$, one implementation has constants $K,A$ such that every command, on every valid history and every supplied old version, returns its answer within $K$ primitive steps and allocates at most $A$ bounded-arity records. It preserves aliasing, tree state, cursor positions and a fixed finite controller state.

The quantifiers concern this specified class, not every mutable machine. Constants are not uniform as $r$ or the other interface parameters grow. D is a classical data-structure premise with a remaining exact-machine implementation qualification, not the desired graph theorem restated as an assumption.

Representation and proof

Keep the shared targets permanently accessible

Use the compressed marked-tree representation behind Demaine, Langerman and Price’s functional trie construction, but mark all distinguished nodes in addition to the moving cursors and root. There are at most $m=k+r+1$ marks. Their connecting tree has at most $2m$ marked or branching vertices after degree-two paths are contracted. A bounded header describes this skeleton using finite indices. Each cursor and core name maps to a skeleton vertex. Coincident cursor positions map to the same index.

Store the interior of a contracted path as a deque of context frames. A frame contains its node’s finite payload and reference tags, the port continuing down the path, and its other child subtrees. Store each skeleton vertex’s current information once in the header representation. Fixed-degree child tables are finite tuples. No physical pointer-equality test is required: comparisons among currently marked locations compare finite header indices.

Every reference field stores a tag in $\Gamma$, rather than a pointer to a stale physical copy of a distinguished node. Following the field consults the current version’s core-name table and assigns the moving cursor to that marked location. A write updates that location’s authoritative information in the new header. All aliases in the new version resolve there; all aliases in the old version resolve through its unchanged header. We neither enumerate incoming references nor alter old records.

A jump must not hide a path scan

Ordinary one-edge cursor movement is handled by removing or adding a context frame at a path endpoint. A jump to an already marked core node also removes the cursor mark at its old position. Merely declaring that removal cheap would leave a gap: a long path that no longer contains a mark must become an ordinary hanging subtree without being rebuilt node by node.

For this purpose, represent a hanging subtree either as an explicit root with child representations or as $\operatorname{Spine}(Q,t)$. Here $Q$ is a nonempty deque of context frames and $t$ has an explicit root. Its meaning is the nested application of those frames to $t$. The smart constructor eliminates an empty $Q$; if its proposed endpoint is already a spine, it concatenates the two deques and keeps the explicit endpoint. Thus a spine never ends in another spine.

To expose the root of a spine, pop its first frame. That frame becomes the explicit root, and its continuing child is the remaining spine, or $t$ if the deque is empty. Only one frame is examined. The child returned need not be exposed during the same operation. This invariant prevents a chain of suspended wrappers from concealing an unbounded normalization step.

Now assign a cursor to an already marked destination. Add its role there and remove its old role. If the old vertex still has a mark, nothing structural changes. Otherwise:

1. If it has at least two skeleton children, retain it as a branch vertex.
2. If it has one skeleton child, turn the old vertex into a frame and concatenate the incoming path, that frame, and the outgoing path.
3. If it has no skeleton children, make its current contents an explicit hanging root and fold its incoming path into one spine at its skeleton parent. The parent might now be an unmarked vertex with one skeleton child; suppress it as in case 2.

The root is always retained. In case 3 there is at most one additional suppression: splicing the parent replaces one child connection at the next vertex by one connection and does not reduce that vertex’s child count. Each case changes a bounded number of deques and bounded-degree tuples. Rebuild the bounded skeleton header and its finite indices. This proves a uniform bound for jumps and cursor assignment, including an arbitrarily long abandoned path.

For a one-edge move into a hanging subtree, expose one root, add it as the new marked vertex, and remove the old cursor mark by the same rules. For a move into a contracted path, pop the relevant endpoint frame and mark it. Moving to an adjacent skeleton vertex needs only role reassignment. Parent moves use the reverse endpoint operation. These cases, payload/reference updates, and leaf edits exhaust the single-state command interface. A leaf-deletion request can check children and marks locally; it never searches for incoming aliases, since a noncore node cannot be a reference target.

All skeleton records have bounded arity. Every new record is initialized from finite tags and already available pointers, so the physical heap remains immutable and chronological. Premise D bounds each deque call. The other work is a bounded number of tuple operations and finite-header traversals. This establishes constants $K,A$, independently of path lengths and incoming degrees.

Correctness for every future command

Interpret the skeleton, its path frames, and its hanging trees as one logical tree. Interpret each reference tag through that version’s core table. The normalization cases preserve this interpretation, except for the commanded cursor move or tree edit. Reference writes change exactly the selected field; payload writes change exactly one logical node. Following a tag reaches the unique registered node. The finite index map gives correct cursor equality even when a tree path and a reference path reach the same node.

Induction on commands gives the required output sequence. Retaining the header retains the entire interpreted state. Allocations on another branch cannot affect it. The same induction therefore applies to every finite branching history, not only a single linear run. This is complete store preservation for the stated interface, not merely reuse of a control continuation.

Composition after independent preparation

There is also a precise cheap join. Prepare two components independently using a common fixed name set $\Gamma$, with disjoint sets of registered core names. Each component’s reference fields use only its own registered names. Supply their version handles and retained cursor choices, with total core/cursor counts within the fixed budgets.

Join creates a fresh root with the two input tree values as its first two children. Node occurrences from the two operands are treated as disjoint in the result. Preserve each input’s reference relations within its corresponding copy and unite their disjoint core tables. Old versions remain unchanged. The new root’s payload and fields have fixed default values.

For the representation, take the two bounded skeletons, preserve their path/hanging-tree storage, and connect their root vertices below the new root. Remap only the finite skeleton indices, not tree payload tags. Each old root remains explicit if marked or branching; otherwise absorb it into an adjacent context path by the normalization above. All changes are bounded in number. Hence this join also costs $O(1)$ work and allocation, under D. Subsequent reference writes can create links from one component into the other’s registered core, giving genuine shared interaction.

Disjointness of the registered name sets is checked in the finite headers. Conflicting registrations are rejected; silently renaming all tags in an unbounded operand is not included. The construction allows a fixed budget of shared names, not unrestricted repeated duplication of named cores. It does not reconcile conflicting edits to one original mutable identity. A global compatibility query or enumeration after joining still pays its own traversal cost.

This is a resource-preserving composition of independently prepared components under an explicit interface agreement. No global joint preprocessing or free node-address access has been inserted into the contract.

Input, history, and storage

An explicit initial tree can be encoded in preorder over the finite child ports, payloads, reference tags and core-marker tags. For fixed parameters its encoded size $N$ is $\Theta(n+1)$ for $n$ nodes, before any separately supplied cursor paths. Loading it and checking that each reference names a unique registered core takes $O(N)$ work and historical allocation. Setup cursor paths are traversed and included in $N$. A bounded number of permanent marks can be installed as the traversal reaches their nodes. Preprocessing does not solve future command sequences.

Across independently loaded inputs of total description size $N$, and $H$ actually executed commands/joins after handle acquisition,

$$T=O(N+H),\qquad S=O(N+H)$$

in local steps and bounded-arity records, including all old versions and temporary allocated records. A literal address serialization needs $O(S\log(S+2))$ bits. If version selection or input vertex names are given as unbounded strings/integers, their decoding and routing costs are additional and must be charged. Boundary width is not the resource parameter of this theorem: even a large number of incoming reference edges is allowed, whereas the shared target namespace remains fixed.

The source operations have finite outputs. There is no uncharged history scan, pointer arithmetic, randomized success condition, arbitrary external node query, reclamation requirement, or allocation deferred past the command deadline.

What this rules out as a proposed obstruction

Take a tree consisting of a root and a long chain, mark the root as one core node, and give every chain node a reference to the root. A write at the root is seen after following any of those references. The graph has unbounded incoming degree and arbitrarily many additional directed cycles, while the conditional construction applies with $r=q=1$.

The same idea works when the core node lies deep inside a branching tree. The ability to reach it through many stored links does not force us to update those links. Core identity is interpreted relative to the current version.

Thus neither the presence of mutable aliases, their number, nor incoming degree alone supplies the missing obstruction to the general compiler candidate. The controlled feature is that all exceptional targets have a fixed finite naming interface. Ordinary tree edges still have unboundedly many possible destinations, but their navigation is structured and charged.

A tempting stronger extension fails as a naive implementation: reassigning a registered tag to a different node changes what every old field carrying that tag denotes. For example, a field that originally pointed to node $a$ must still point to $a$ after an unrelated operation registers $b$. Rebinding its tag to $b$ breaks pointer semantics. A successful extension must retain older identities or prove the old name dead. This is a counterexample to silent tag reuse, not a lower bound against all representations.

Provenance, status, and next decisive statement

The Demaine–Langerman–Price paper, §2 Theorem 1, supplies the classical compressed-finger-tree mechanism. Its introduction pp3–4 explicitly distinguishes cursor navigation from arbitrary addressable-node access. We use that model distinction; we do not independently import the Fiat–Kaplan lower bound summarized there. The preceding assessment records the functional-deque literature and why its exact finite-rule transfer remains conditional. The jump normalization, finite shared-core interpretation and disjoint-name join are written reductions here, built from those classical ideas. Their novelty is not established. There is no formal verification or independent implementation review.

The result changes the next large question. A candidate worth testing is whether hierarchically scoped finite shared interfaces can replace one global finite core, allowing unboundedly many distinct shared objects while retaining local access and complete checkpoints. That is presently hypothetical. The decisive issue is maintaining identity and routing when entering, leaving, copying and joining scopes, without hiding global name repair. The tag-reuse counterexample is the first required control. A mere bounded-width picture or one failed representation would not settle that statement.

The general mutation-elimination candidate remains unresolved. No language-recognition, scaffold-to-PEG, unrestricted SAT or P-versus-NP consequence is claimed.