Uniqueness graphs and place calculi

Chapter 47: graph-denotation uniqueness

The frozen expression grammar has variables, fixed-arity symbols, nonrecursive sharing lets, simultaneous recursive lets, and left-linear constructor cases. The denotation clauses apply to case-free expressions; top-level cases in function definitions generate one rewrite rule per alternative. The result is a finite rooted equation graph whose equations, including garbage equations, are retained. A source step is defined exactly by one graph-rewrite step.

Conventional graph typing assigns one scheme instance to every symbol equation. Uniqueness graph typing refines each incident type with attributes $\mathsf{u}\le \mathsf{m}$. In the root-extended graph, one incoming reference checks $T_G(n)\le {\sigma }_i$; more than one checks $[T_G(n)]\le {\sigma }_i$. Correction must be defined. Source contraction is $$\frac{B,y:[\sigma ],z:[\sigma ]⊢E:\tau }{B,x:\sigma ⊢E[y:=x,z:=x]:\tau }\mathrm{Contr}.$$ Sharing and subsumption retain every premise of their source rules:

$B⊢E:\sigma$$B,x:\sigma ⊢E^{\prime }:\tau$

$B⊢\mathsf{let}x=E\mathsf{in}{E}^{\prime }:\tau$

$B⊢E:\sigma$$\sigma \le \tau$

$B⊢E:\tau$

The cycle rule corrects recursive interfaces receiving multiple incoming edges.

Conventional inference generates finite first-order equations and uses a most general unifier. Attribute inference is a separate finite inequality closure. Its principal result is relative to a fixed conventional solution. It rejects precisely a closure deriving $\mathsf{m}\le \mathsf{u}$; there is no full principal uniqueness theorem in the frozen system.

An update may reuse a matched node only with one incoming reference, outer attribute $\mathsf{u}$, a fitting declared layout, and correctly typed retained outgoing edges. This rule decides eligibility; it does not add a machine-store semantics.

Chapter 48: Featherweight Rust

The core left values are $w::=x\mid \ast w$. A copy reads without changing the store; a move returns the value and replaces the selected owner position by $\partial T$. Moving through a borrow is not a rule. Assignment drops the old target before writing; block exit drops the top lexical frame.

The flow judgment is $\mathrm{\Gamma }⊢⟨t:T{⟩}_{\ell }^{\sigma }⊣{\mathrm{\Gamma }}^{\prime }$. A unique access requires no overlapping live borrow. A shared access requires no overlapping live mutable borrow. Borrow invariance checks the result type by extending the output with a fresh anonymous binding.

The termination repair requires an injective $\varphi :\kappa \to \mathbb{N}$ with . Recursive place operations use the lexicographic measure $(\varphi (\mathsf{root}(w)),d(w))$. Move and drop delete dependency edges; declaration adds a highest-ranked fresh vertex; assignment reranks the finite updated path above its new dependencies.

Chapter 48: Oxide v4

Oxide v4 uses numeric places $\pi$, dereferencing place expressions $p$, reference types , and loans $\omega p$. Its judgment is $\mathrm{\Sigma };\mathrm{\Delta };\mathrm{\Gamma };\mathrm{\Theta }⊢e:\tau \Rightarrow {\mathrm{\Gamma }}^{\prime }$. $\mathrm{\Gamma }$ is an ordered sequence of frames containing variables and concrete regions; a concrete region maps to a finite loan set.

Ownership safety $\mathrm{\Delta };\mathrm{\Gamma };\mathrm{\Theta }{⊢}^{\omega }p\Rightarrow L$ rejects every overlapping loan for a unique use and every overlapping unique loan for a shared use. Reborrows carry an exclusion obligation for the suspended parent. ${\mathsf{gc}\text{-}\mathsf{loans}}_{\mathrm{\Theta }}(\mathrm{\Gamma })$ empties exactly the concrete regions absent from all types in $\mathrm{\Gamma }$ and $\mathrm{\Theta }$. The $\mathsf{shift}$ and $\mathsf{framed}$ reductions pop only the latest runtime and static frame. Region rewriting and output-environment union are parts of preservation and may not be replaced by equality.