ch:ownership-borrowing: ch:ownership-borrowing

The complete state trace is The steps use Share-begin, Share-nest, Read, Share-end, Read, and Share-return, in that order. Freshness holds because $\alpha \ne \beta$, and each end command names the top lifetime.

Use Ex-begin at fresh $\alpha$, Ex-reborrow at fresh $\beta$, Write with any closed $v:A$, Ex-pop at $\beta$, and Ex-return at $\alpha$. This derives No sharing rule has an exclusive state in its premise. Ending $\alpha$ while $\beta$ is active matches neither Ex-pop, whose conclusion must remove the top suffix $\beta$, nor Ex-return, whose premise has a singleton exclusive stack.

With fresh $k$, Move concludes $$\mathcal{L};\mathrm{\Omega },h:\mathsf{O}(A)⊢\mathsf{move}h\mathsf{as}k\Rightarrow \mathcal{L};\mathrm{\Omega },h:\mathsf{D},k:\mathsf{O}(A).$$ Inverting Read and Write requires the named state to belong to their displayed live-state sets; $\mathsf{D}$ belongs to neither. Inverting Drop requires $h:\mathsf{O}(A)$, also absent. The destination has exactly that owned state, so Read applies to $k$.

Activating $[b:\sigma {]}_{\mathsf{S}}^n$ gives the borrow a kind at region level $n$. Returning that borrow would therefore require both ${\mathsf{L}}_n\le \mathrm{kind}(\tau )$ and the Region premise $\mathrm{kind}(\tau )\le {\mathsf{L}}_{n-1}$. The stratified kind order does not have ${\mathsf{L}}_n\le {\mathsf{L}}_{n-1}$, so the premises cannot be solved. A closure containing the borrow has a kind at least as restrictive as the captured binding; it produces the same incompatible inequalities. The argument uses the Affe kind level, not lexical scope inspection of result syntax.

First take $\mathrm{\Gamma }=a:\mathsf{Array}A$, with $a$ unique and consumed by the update. There is no other root for the array, so overwriting its representation is observationally equivalent to the pure replacement. Second take $\mathrm{\Gamma }=a:\mathsf{Array}A,b:\mathsf{Array}A$, allow $a$ and $b$ to denote the same array, consume $a$, and leave $b$ unused. The path is affine because neither handle is used twice. It does not establish absence of the alias $b$; a surrounding context or later lazy evaluation could still observe that value. In-place replacement needs the first environment’s uniqueness fact, not only a use count.

Borrow $m:{\mathsf{Mut}}^{\alpha }a$ at $\beta$ to obtain $$m^{\prime }:{\mathsf{Mut}}^{\alpha \wedge \beta }a\otimes {\ell }_{\beta }:{\mathsf{Lend}}^{\beta }({\mathsf{Mut}}^{\alpha }a).$$ Ending $\beta$ consumes ${\mathsf{Now}}^{\beta }$ and returns the persistent evidence $e_{\beta }:{\mathsf{End}}^{\beta }$. Reclamation consumes the linear lender ${\ell }_{\beta }$, uses $e_{\beta }$, and recovers $m$. Ending $\alpha$ similarly consumes ${\mathsf{Now}}^{\alpha }$. The outer reclamation consumes the outer linear lender and uses ${\mathsf{End}}^{\alpha }$ to recover the original owner. The two mutable borrowers have already been consumed by their respective scope computations, so no borrower survives either reclamation.

Denotational strong confluence and leak freedom of a safe final mutative configuration are proved. Progress of safe mutative configurations is conjectured. Preservation of safety and behavior uniqueness are conditional on the association-bisimulation conjecture; the latter also uses the proved denotational diamond. Strong confluence of the mutative semantics is unsupported: neither the published theorem nor the stated conditional corollary has that conclusion.

The observer can see every deque empty after the delayed worker has removed a task but before it publishes the two children. An emptiness test then reports termination although two tasks will shortly become available. With an outstanding-task counter, removing the parent does not make the count zero: the parent remains outstanding until publication accounts for its children, so the observer cannot finish during the gap. The repair does not prove that the core borrowing API is pure, and it does not establish the association bisimulation conjecture.

Let the initial states be $b_1:\mathsf{O}(A),b_2:\mathsf{O}(B)$. The command sequence produces lifetime stacks $ϵ,\alpha ,\alpha \beta ,\alpha \beta ,\alpha ,ϵ,\gamma ,ϵ,ϵ$. The states of $b_1$ are respectively $\mathsf{O},{\mathsf{S}}_{\{\alpha \}},{\mathsf{S}}_{\{\alpha ,\beta \}},{\mathsf{S}}_{\{\alpha ,\beta \}},{\mathsf{S}}_{\{\alpha \}},\mathsf{O},{\mathsf{X}}_{\gamma },\mathsf{O},\mathsf{D}$; $b_2$ changes from $\mathsf{O}(B)$ to $\mathsf{D}$ at the move and fresh $k$ receives $\mathsf{O}(B)$. The runtime makes exactly the same mode changes and moves the $B$-payload, so agreement holds after each command. Replacing ${\mathsf{endS}}_{\beta }{b}_1$ by ${\mathsf{endS}}_{\alpha }{b}_1$ fails because $\alpha$ is not the top lifetime.

Without destination freshness, move into an existing owned $k$ has two candidate payloads for one target entry; the unique-result clause of lemma 46.4 fails. Without the top condition, ending the outer lifetime of ${\mathsf{X}}_{\alpha \beta }(A)$ can leave a runtime inner view whose static stack no longer has its enclosing scope, breaking agreement and the final no-dangling argument. Without Affe’s result-kind premise, may return the region-level borrow; the owner can then resume while the escaped borrow remains reachable, so the source containment step used in the nonescape argument fails.

Suppose $M{\bowtie }_{A}D$ and $M{⟼}_{\mathsf{m}}{M}^{\prime }$. The forward half of the conjectured bisimulation supplies $D^{\prime }$ with $D{{⟼}_{\mathsf{d}}}^{\ast }{D}^{\prime }$ and $M^{\prime }{\bowtie }_A{D}^{\prime }$. The last judgment is the definition of safety for $M^{\prime }$, so safety is preserved conditionally.

For behavior uniqueness, mere existence of associations permits one mutative state to associate with unrelated denotational states, or two mutative outcomes to associate with one state without being equal. The diamond joins denotational reductions only. Bisimulation is needed to transport each mutative execution into that diagram and transport the joined observations back; the result remains conditional because that bisimulation is conjectural.

One possible five-row separation is Affine use separates a one-use program from one that duplicates $a$. Uniqueness separates an in-place pure update from the same update with a live alias. Ownership separates transfer/drop authority from a read-only handle. An exclusive borrow separates mutation through the top view from an attempted simultaneous shared view. The points-to assertion separates a command with the owned heap cell in its footprint from a command whose precondition lacks that cell. These judgments are not translations of one another.

The sharing let has nodes $c=C$ and $p=P(c,c)$, rooted at $p$. Counting the root edge, $p$ has one incoming reference and $c$ has two. The copied expression has $c_1=C$, $c_2=C$, and $p=P(c_1,c_2)$. Each of the three nodes has one incoming reference. Node renaming cannot turn one two-referenced node into two nodes, so the rooted graphs are not isomorphic.

Give $a$ type $\delta$. The $C$-equation gives $\alpha =\delta$ and the bound root type $T\delta$. The two argument positions of $P$ give $\beta =T\delta$ twice; the sharing interface is the equation equating the type of each occurrence of $x$ with that single bound-root type. The result is $U(T\delta )$. Up to renaming $\delta$, this solution is most general.

Correcting a unique list of unique elements changes only the outer spine attribute, giving a shared list whose element attribute remains unique. Such a type need not be the result of any constructor scheme; it is the temporary shared view used at contraction. Correcting a unique list of already shared elements likewise changes only the spine and leaves the elements shared.

Type $C(a)$ at $\sigma$, bind $x:\sigma$, and present the body first with two variables $y:[\sigma ],z:[\sigma ]$. The $P$-scheme types $P(y,z)$; Contr substitutes $x$ for both variables, and Share joins the binding. In the denotation, the $C$-root has two incoming $P$-edges, so definition 47.10 checks its corrected type. Assigning both edges the uncorrected unique type would assert one incoming reference while displaying two.

For a unique spine and shared elements take $b=\mathsf{u}$, $a=\mathsf{m}$. The scheme condition is the allowed edge $\mathsf{u}\le \mathsf{m}$. For a shared spine and unique elements it becomes $\mathsf{m}\le \mathsf{u}$, the unique forbidden edge. Reflexive-transitive closure therefore accepts the first problem and rejects the second.

Consume the cells headed by $3,1,4,2$ in order. Once the pivot cell is removed, the tail reference is the sole incoming reference to the next spine cell. Start with empty accumulators. Relink the $1$-cell onto the low accumulator, the $4$-cell onto the high accumulator, and the $2$-cell onto the low accumulator. The accumulators are then $2::1::[]$ and $4::[]$; reversing the low accumulator gives $1::2::[]$. Each relink has one incoming spine reference and retains a tail edge at the list-tail type. With a shared input spine, the first matched cell already lacks the unique outer attribute, so condition 2 of definition 47.18 blocks the first relink.

Let $\eta$ send each pattern-interface node to its matched host node. Rule typing gives the same attributed root type on the left and right interfaces under $\eta$. For an interface node whose reference count remains one, its original local inequality is unchanged. If the right side introduces a second reference, its rule derivation uses contraction, so both outgoing positions demand $[T_G(n)]$. Internal replacement equations are typed by the right-side rule derivation; host equations are unchanged. Reconstructing a source expression may choose different lets or a different presentation of a cycle, so completeness yields an expression with the same graph denotation as the parser’s reduct, not necessarily the same syntax.

Enumerate first-order instances of the principal conventional solution in increasing substitution size. For each instance, generate the finite attribute graph, compute its transitive closure, and report the symbolic attribution exactly when the forbidden edge is absent. Exact conventional generation proves the first phase sound; lemma 47.15 and theorem 47.16 prove every reported attribution sound. The conventional principal theorem factors known typings through one solution, but it supplies neither a finite bound on instances nor a decision that no attributable instance exists. Unrestricted enumeration is therefore only semidecidable.

$x$ overlaps each of $x.0,x.1,x.0.1$, with $x$ the shorter prefix. $x.0$ overlaps $x.0.1$, with $x.0$ the shorter prefix. $x.0$ is separated from $x.1$, and $x.1$ is separated from $x.0.1$. These are all six unordered pairs.

After moving $x.0.1$, the overlapping paths $x$, $x.0$, and $x.0.1$ are unreadable. The separated siblings $x.0.0$ and $x.1$ remain readable. Assigning a fresh box to $x.0.1$ removes the only partial marker, so all five listed paths are readable again.

At block exit the local binding $y$ is removed, so the ordinary output environment can be empty and hence vacuously well formed. The result type is nevertheless . Adding fresh makes well-formedness inspect that borrow; its referent is absent after the block, so the judgment fails.

For ${\tau }_1$, the dependency graph is $x\to y\to z$. One ranking is $\varphi (x)=2,\varphi (y)=1,\varphi (z)=0$. For ${\tau }_2$, the graph contains $x\to y\to x$, so the inequalities would require both and . Lookup beginning at $\ast x$ follows the borrow to $y$, then the borrow back to $x$; the obligation rooted at $x$ repeats.

The whole place $x$ overlaps both loans. Its shared use conflicts with the unique $x.1$-loan; its unique use conflicts with both. At $x.0$, a shared use is permitted because the only overlapping loan is shared, while a unique use is rejected. At $x.1$, both shared and unique uses conflict with the overlapping unique loan.

With empty $\mathrm{\Theta }$, $r$ occurs in no stored type, so collection replaces its loan set by $\varnothing$. When $\mathrm{\Theta }$ contains a component type mentioning $r$, collection retains $\{\mathsf{uniq}x\}$. Tuple construction needs the latter result: the already evaluated first component still holds the unique borrow, so the attempted second unique borrow must be rejected.

For move, safe abstraction locates a uniquely owned value; runtime destructive read writes undefined and typing strikes the same owner type. For mutable borrow, ownership safety establishes absence of an overlapping loan before the runtime creates a location value; the anonymous result binding records its referent. For block exit, runtime recursively drops the latest frame and typing removes the same lexical bindings; borrow invariance rules out a returned reference to any removed local. None of these frozen-core cases has a projection rule, so they do not prove the named-field extension.

Type the first sequence component from $\mathrm{\Gamma }$ to ${\mathrm{\Gamma }}_1$. The second component is typed from ${\mathsf{gc}\text{-}\mathsf{loans}}_{\mathrm{\Theta }}({\mathrm{\Gamma }}_1)$, not directly from ${\mathrm{\Gamma }}_1$. A reduction inside the first component preserves the same continuation $\mathrm{\Theta }$, so a region mentioned by an already evaluated component cannot be cleared. Oxide’s value-preservation-under-drop/collection lemma re-establishes the typing of those temporaries after collection. Apply the induction hypothesis to the stepping component, then rebuild the sequence rule with the preserved $\mathrm{\Theta }$, rewritten result type, and residual output union.