Complete checkpoints through nested ownership

Our broader goal is to understand which future behaviors have representations maintained by finite rules with bounded local access and allocation. The strong statement tested here is a compositional one: can one constant-cost checkpoint construction support arbitrarily many shared identities by being nested inside itself?

There is a precise positive answer for an access discipline. Each region owns its children; a computation enters one child, operates there, and returns one level. References within a region may share its mutable core, but live references do not escape to another region. Under the real-time deque premise of the finite shared-core construction, complete checkpoints remain constant-cost, independently of the number of regions and nesting depth. Components can reuse local names and be repeatedly composed without global renaming.

The qualification is consequential: returning one level is one operation. Returning to the outermost region from depth $d$ takes $d$ returns in this implementation. A saved value from a child is not a live alias to its future state. The theorem below preserves those contracts rather than adding an unproved fast global access operation.

The statement

Fix one finite shared-core interface, with fixed bounds on tree degree, local cursors, reference fields and distinguished local targets. Extend each local tree node by a fixed number of owned child slots. A nonempty slot contains another region of the same kind. Logical child occurrences have unique owners, so the ownership structure is a finite tree. Its size and depth are unbounded. Each region has its own local core namespace $\{1,\ldots,r\}$, cursor tuple and finite local control state.

Ordinary reference fields point only to distinguished targets in their own region. They never contain pointers into a different region. These local targets remain permanent within that region, as in the shared-core contract. A child slot may be reached through several local aliases to its containing node, but the slot itself is the child’s unique owning location.

There is one active region. Commands comprise the local shared-core operations plus:

• Enter: at a ready local cursor and fixed slot, suspend the parent’s local state and activate the child, restoring its saved local cursors and control.
• Return: replace the suspended parent’s selected child value by the current region’s updated value, then reactivate that parent.
• Create, discard, copy: create a fixed initial child in an empty slot, discard a child, or copy a suspended child’s entire value into another ready slot. Copy creates independent logical occurrences, preserving sharing inside each copied region.
• Graft: from two supplied root-focused component versions, create a fixed wrapper region owning copies of them in two slots. Its output is root-focused. The inputs may use identical local core names.
• Checkpoint and resume: retain or restore a supplied complete focused-state version.

A root-focused component has no suspended parent regions; its local cursors need not be at its local tree root. Deleting a local leaf may discard its owned child values, but cannot delete a local core or cursor location. Invalid commands return a fixed failure symbol. Ordinary command arguments and outputs are finite; version capabilities are supplied separately. Finding a version by an unbounded name is charged separately. No command exports a live child-node handle, mutates an inactive region behind its owner, or treats a complete root normalization as one return.

Conditional closure theorem. Under deque premise D, this interface has one deterministic immutable finite-rule implementation and constants $K,A$ such that every valid command, at every depth and on every supplied prior version, completes within $K$ primitive steps and allocates at most $A$ bounded-arity records. The constants depend on the fixed local interface, not the number of regions, shared identities, aliases, or executed commands.

This is a sufficient compilation statement for the specified behavior. It is not a necessary condition for persistence, nor a claim that general ownership types automatically supply these bounds.

Proof: keep the active region and its context

First extend the local implementation to carry child-version pointers as opaque payloads. This needs an argument because the original labels were finite. A child slot is a tagged option containing one immutable pointer. Local path frames and explicit nodes copy that pointer without inspecting its contents, comparing addresses, or following it. Reading/replacing a slot at a ready cursor uses the same bounded reconstruction as a finite payload update. Each record acquires only a fixed number of fields. The shared-core proof and its deque premise therefore remain applicable. Enter is the separate operation that interprets the pointer as another local-state header.

Write a complete state as $(h,z,c)$: an active local-state header $h$, an immutable stack $z$ of parent contexts, and fixed finite outer controller state $c$. A parent context contains:

$$\operatorname{Frame}(p,i,a,z'),$$

where $p$ is the suspended parent header, $i$ its cursor index, $a$ the selected child-slot index, and $z'$ the rest of the stack. Both indices range over fixed finite sets. The suspended cursor cannot move while its child is active.

The interpretation plugs the active region into the designated slot of the top parent context, then plugs that reconstructed parent into the next context, and so on. This recursive interpretation is a correctness definition, not an operation executed at every command. The saved parent’s old child field is the hole occupied by the active descendant. It is not a second independently observable current child.

A local operation transforms $h$ and leaves $z$ unchanged. Enter reads the chosen child header, allocates one parent-context record, and makes that child active. Return performs one local slot replacement in $p$, using the current $h$, and pops one context. Create installs a fixed-size initial local header; discard installs null. Copy reads one suspended child header and installs that pointer in another slot. The logical interpretation treats the two child occurrences as independent, although their current immutable storage is shared.

Every operation invokes a bounded number of already costed local operations and stack constructors. Thus it has uniform work and allocation bounds. New contexts point only to available older headers; a returned parent header is allocated after its updated child. Nothing requires mutation or late filling of an old record.

For correctness, assume the interpretation matches the source ownership tree before a command. A local update changes only the active region. Enter changes which region is active without changing the interpreted tree. Return performs exactly the replacement designated by the top hole. Copy gives two initially equal but separately owned occurrences; a later return updates only the selected owner slot. These cases establish the invariant by induction. Retaining $(h,z,c)$ retains the entire state, so the induction applies to arbitrary branching histories as well.

The no-escape rule is used at a specific point: while a child is active, no operation can inspect the suspended parent’s old child field as a competing current view. Access to the parent requires Return, which first installs the updated child. That is why one-hole contexts suffice.

Repeated composition and identities

Graft allocates a fixed wrapper header and inserts the two supplied root-focused headers into its two child slots. It performs no traversal of either operand. All names remain local: name 1 in one operand denotes that operand’s core node, while name 1 in the other denotes a different node. Enter chooses the region header through which the name is interpreted. There is no global renaming pass or unbounded numeric scope identifier.

The same component may be grafted twice. Its immutable storage may be shared initially, but the result contains two logical owned occurrences. Updating one through its owner leaves the other unchanged. Internal aliases still agree within each occurrence. Arbitrarily many distinct mutable identities can therefore be represented, even though every individual region uses the same finite name set.

This is composition of values with encapsulated internal sharing. It does not merge two versions of one live identity or preserve an external alias spanning both operands. Compared with a flat shared-core join, it permits repeated reuse of local names but restricts cross-region live references. These are different, explicit composition contracts.

A component at depth $d$ must make $d$ Returns before it is an eligible root-focused Graft input. The bound does not conceal this cost in publication, normalization, or a later query. Checkpointing the focused state itself remains constant-time at every depth.

Resource accounting

For an explicitly encoded initial hierarchy, let $N$ count its finite-port local trees, local core markers, reference tags, region delimiters and any supplied setup paths. The local budgets are fixed. Traverse that description and prepare its regions in $O(N)$ work and historical records. Each independently supplied component pays for its own preparation; Graft uses their prepared root-focused handles.

For $H$ executed local operations, scope transitions, copies, grafts and checkpoints after handle acquisition,

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

in bounded-local steps and bounded-arity records, including all historical contexts and temporary allocations. At depth $d$, the current context stack uses $O(d)$ records, created by the preceding charged Enters. Literal serialization of all pointer addresses uses $O(S\log(S+2))$ bits. A straight finite-command stream has $\Theta(H)$ command bits; serialized version identifiers add their actual input length and routing work. No unit-cost unbounded name manipulation is included.

Repeated value copies can make the logical unfolding much larger than the retained representation. Enumeration or a global query must pay for the observations it requests. There is no exponential-in-boundary-width lower bound here, and no free query obtained from a cheap join.

Two controls against overgeneralization

Escaping live handle. Let a parent own child $C$, whose local shared bit is 0. Suppose another location stores an exported handle that promises live access to that same child. Enter $C$, change its bit to 1, and return. The construction replaces the owner’s child pointer, but an exported pointer to the old child header still reads 0. The promised live semantics require 1. Calling that old pointer a checkpoint changes the contract; it does not repair the live-alias implementation. A different representation might succeed, so this is not an impossibility theorem.

Containment alone. Merely placing all state behind one owner does not make a general mutable computation easier. At each command boundary, any finite-register local machine can store its register tuple in a fixed-size owner record and expose only that record through the external interface. Loading those registers, executing its bounded command and storing them again adds constant overhead. The internal graph can still be arbitrary. Consequently, a general compiler justified only by this single-owner boundary property would already imply the broad mutation-elimination candidate C. This reduction concerns that weak external-interface property, not every formal ownership type system or every intermediate stack-graph definition of domination.

The positive theorem instead combines a specifically costed local kernel with unique ownership, no escaping live references and explicit scope traversal. Its value is a closure result: the kernel’s bound survives unbounded nesting and repeated value composition. The global theorem was not assumed in the local premise.

Classical comparison and strategic consequence

The context construction is a specialization of Gérard Huet’s The Zipper, published in JFP 7(5), 1997, 549–554. We inspected the primary note’s introduction and §§1–2.2. Its general list-of-siblings version explicitly charges upward movement by the number of preceding siblings; its fixed-arity version and remembered-position variant avoid that reconstruction. Here the parent is a costed local header with a saved slot, so Return uses one bounded slot replacement rather than scanning siblings.

The local aliasing mechanism depends on the shared-core proof, in turn using classical compressed-finger-tree ideas and explicit deque premise D. The exact machine implementation of that deque is still not certified here. This is a written conditional construction using classical techniques. Novelty is unestablished; no formal verification or independent implementation review is claimed.

The construction supports a more useful principle than a global bound on the number of shared identities: complete local representations can compose through a controlled access interface. It still falls short of a foundational characterization. The next decisive test is whether an independently specified interface can admit escaping live references or multiple independently active scopes without turning snapshot consistency into an unbounded lookup obligation. The old-header counterexample must survive any proposed repair. Another routine nesting variant would not answer that question.

See the candidate portfolio. Candidate C remains unresolved. There is no new scaffold-recognition, PEG, unrestricted SAT, or P-versus-NP claim.