Complete checkpoints for locally navigated trees

The broader question is when future behavior can be maintained by finite rules with bounded local access and allocation. A powerful positive statement is already known: a tree can support several movable cursors, persistent updates, and copies of subtrees between versions without paying for its depth on every operation. This is a classical result, not a new FPRD theorem. It provides a substantial control for the proposed general mutation-elimination principle.

Imagine two cursors in a very deep directory tree. Changing a label near one cursor should be visible if the other cursor reaches that same location. We also want to retain the previous tree, return to it, and copy a directory from it into a different version. Copying the entire root-to-cursor path at each change would make depth expensive. The construction below avoids that repeated traversal.

The strong statement and its exact interface

Demaine, Langerman and Price, Confluently Persistent Tries for Efficient Version Control, Algorithmica 57 (2010), 462–483, author full text, §2 Theorem 1, give a functional trie with a fixed number of fingers. Finger movement, leaf insertion/deletion, and subtree copying/removal cost

$$O(\log(\Delta+2))$$

in time and fresh space per operation, where $\Delta$ measures degrees of the directly involved nodes. The harmless +2 makes the constant-degree reading explicit. Their introduction specifies copying between arbitrary versions and propagating a selected subset of source fingers, subject to the fixed finger budget. Their functional model never changes an old cell after allocation.

Fixed-interface specialization. Fix constants $D,k$, a finite node-label alphabet, and $D$ child ports. Maintain rooted trees of degree at most $D+1$ with at most $k$ cursors per version. Permit the paper’s local cursor moves, finite-label observations/updates, leaf edits, and subtree copies/removals; invalid moves return a fixed failure result. The endpoints of every operation are already supplied version handles and cursor indices. Preserve all old versions. The imported construction gives constant worst-case time and allocation per such operation in its functional data-structure model; the constants depend on $D,k$, not depth, logical tree size, or history length.

Fixed finite ports remove the paper’s assumption that potentially long edge labels can be compared in constant time. A node label is constant information. Copying propagates fingers only as specified by the source interface; it is not a request to preserve arbitrarily many externally stored node handles. Invalid endpoint configurations can be rejected using the fixed-size local interface.

Version handles are capabilities supplied to the operation. Finding an old version by an unbounded integer, looking up a pathname, or positioning a cursor is additional work. In particular, a path of length $d$ still requires $d$ local moves. No free address arithmetic or global name lookup is implicit.

Why the construction works

The key is the small tree connecting the cursors. Add its branch vertices and the root to the marked vertices. With $k$ fingers there are at most $2k+1$ such vertices. Contract intervening paths to obtain a constant-size skeleton, called the hand in the paper. Store each contracted path as a functional catenable deque. Store the hanging subtrees separately. At each path vertex, a dictionary holds the adjacent hanging components; its operations cost logarithmic time in the local degree, hence constant time at fixed $D$.

A cursor move transfers a bounded number of vertices between a path and a hanging subtree, or creates/removes a marked branch vertex. If two cursors meet, the skeleton records their coincidence. Updating the constant-size skeleton refreshes every cursor representation in the new version. Thus several cursors do not carry stale independent copies of an updated location. Edits and copies likewise change a bounded number of these local structures. Path endpoints can be removed and paths concatenated without scanning their interiors because of the catenable-deque primitive.

This is the actual §2 mechanism, including its nontrivial deque dependency. A plain linked path or an ordinary one-ended zipper is not a substitute: joining long path contexts could otherwise reintroduce unbounded work. We have inspected the theorem and this construction; this article does not claim a separately verified implementation of it.

Complete state, branching, and input accounting

The version representation contains the tree and its cursor configuration. A fixed finite controller state can be included in the version header. A client built from these operations therefore has complete snapshots of that state, rather than only a saved control continuation. Any private data outside this representation requires its own persistence argument.

Start with a one-node tree and a fixed cursor configuration. After $H$ operations, including cursor positioning, the construction retains $O(H+1)$ records and performs $O(H+1)$ work, even when later operations use old supplied versions. Cross-version subtree copy is included. An explicit initial finite-port tree with $n$ nodes can instead be loaded by a traversal in $O(n)$ local operations; initially put the cursors at the root. Loading separately supplied cursor paths costs their total length as well.

Let $N$ be the actual encoded initial description and supplied setup paths. A preorder finite-port/finite-label encoding has $N=\Theta(n)$ for the tree. A representation using named vertices or binary version indices has larger encoded input and must charge their decoding/routing; it does not inherit free random access. With the handles already routed, initial storage and work $O(N)$ give retained storage

$$S=O(N+H)$$

in bounded-arity pointer records. Serializing all record addresses explicitly uses $O(S\log(S+2))$ bits. Source preprocessing, temporary historical allocations, snapshots and subsequent operations are included; garbage collection is unnecessary for this all-history upper bound. Logical tree size can grow far faster than storage through repeated subtree copying. That is compression of tree values, not constant-time enumeration of their contents.

A read at a cursor has a finite output alphabet. Enumerating a subtree, following a supplied long path, or answering a global compatibility query is not a constant-time primitive. In composition language, local subtree grafting is cheap after preparation and endpoint positioning; a deferred global query still pays its actual cost.

The finite-rule bridge: what is established and what remains

To translate the construction literally into the campaign’s immutable bounded-local machine, the needed premise is precise:

Deque premise D. There is a uniform purely functional catenable deque of opaque fixed-arity records whose endpoint operations and concatenation use a fixed number of pointer dereferences, finite-tag tests and initialized record allocations, with no mutation, unbounded arithmetic, or hidden deferred work.

Conditional consequence. D implies a finite-control bounded-local implementation of the fixed-$D,k$ tree interface above. Replace fixed-degree dictionaries by finite port tables, represent the skeleton by a bounded header, and expand each bounded sequence of deque and constructor operations into finitely many machine steps. Skeleton indices range over a fixed finite set. All old pointers are read-only; each new record points to already available records. Snapshots retain the bounded header. Every operation invokes only a bounded number of primitives, so the work and allocation constants are uniform over histories. This is a resource-composition argument, not a claim that a general functional-language evaluator already has these costs.

The premise has substantial classical support: Kaplan and Tarjan’s real-time catenable deques underlie the relevant functional data-structure literature. A particularly useful modern source is Viennot, Wendling, Guéneau and Pottier, Verified Purely Functional Catenable Real-Time Deques, introduction §§1.1–1.3 and §9.2.2. Their OCaml implementation has worst-case constant-time operations and no recursive function definitions; pointers identify where the next repair is required. This is strong evidence for the desired bounded-local mechanism.

Two qualifications matter. Their tested OCaml implementation is not formally verified, and their separately verified Rocq implementation currently retains runtime indices and does not have the same constant-time bound. The authors explicitly state that no formal connection between the implementations is established. We inspected the introduction and representative core-code structure, not the full module dependency and arithmetic/callback closure of the implementation. Accordingly, this note retains D as an explicit premise for the exact finite-rule transfer. The imported trie theorem itself is unconditional in its published model. No verified compiler or new scaffold/PEG recognition theorem is asserted.

Copying is not mutable aliasing

Suppose two distinct child ports contain copies of a one-node tree labeled 0. Change the node reached through the first port to 1, then read the node reached through the second. The copy contract returns 0. A mutable graph in which both ports point to the same cell returns 1. Immutable physical sharing in the functional construction implements the first behavior; it must not be mistaken for the second.

This does not require every cursor to have an exclusive object: two cursors at the same tree occurrence are explicitly supported and see coherent updates. The useful distinction is between several access positions in a tree value and multiple structural paths denoting one mutable cell. The general mutable-machine candidate permits the latter. It is neither proved nor refuted by the trie theorem.

Cross-version copying also supplies no automatic reconciliation of conflicting updates, identity-preserving graph joins, or SAT compatibility test. Independently prepared tree values can be grafted at ready endpoints; their interaction has the specified copy semantics. Those semantics explain why this positive composition result can coexist with much harder composition contracts.

What this changes

A useful foundational characterization must accommodate deep trees, several coherent cursors, and even cross-version value composition. Small depth, one cursor, and exclusive cursor ownership are not necessary conditions. Conversely, a generic assertion that all persistence is cheap cannot be inferred from this example.

The next decisive test is whether a comparably explicit interface can support a bounded amount of structural mutable aliasing while retaining complete constant-cost snapshots. The alias must be semantically observable, its creation and routing charged, and the target allowed to choose its representation. A failure of one tree layout would not be an impossibility theorem. This tests a meaningful boundary of the strong positive statement; merely tightening the tree constants would not.

Status: imported classical theorem, inspected proof mechanism, explicit resource specialization and a conditional finite-rule consequence. No new lower bound, originality claim, formal verification, or independent implementation review. See the candidate portfolio for the still-hypothetical general statement.