Linear and Affine Type Systems

Proof. These are finite-map calculations. Disjointness makes membership exclusive. The two bracketings have the same domain and assign the same type to each member. For the refinement clause, let ${\mathrm{\Xi }}_{ij}$ be the restriction of ${\mathrm{\Delta }}_i$ to $\mathrm{dom}({\mathrm{\Delta }}_i)\cap \mathrm{dom}({\mathrm{\Theta }}_j)$. The two given partitions make the four domains pairwise disjoint and their row and column unions give the displayed equations. Any other four contexts with those equations have the same domains and types, so the refinement is unique. ◻

Proof. The three load-bearing splits are visible in these judgments: The first two conclusions use T-LolliE; the third uses T-LolliE for close and then T-OneE. Now T-TensorE combines the second conclusion with the third: its scrutinee owns exactly $f:\mathsf{File}$, and its body owns exactly $f^{\prime }:\mathsf{File},b:\mathsf{Bytes}$. Thus the body of the outer let has type $\mathsf{Bytes}$ under $f:\mathsf{File}$. The let abbreviation is an application; its function premise abstracts $f$, and its argument premise is the first displayed conclusion. Their split is $\cdot \uplus (u:1)$, so one final T-LolliI over $u$ gives the claimed type.

For any $h\in \mathsf{Tok}$, the informative part of the trace is The rule names on the arrows identify every core segment and every file step. ◻

Proof. Permutation is finite-map equality. For weakening, induct on typing and add $x:B$ to each unrestricted premise, renaming binders when necessary. A linear weakening would derive $\mathrm{\Gamma };y:C,z:B⊢y:C$, but no rule consumes $z$. Direct inspection of the last rule proves the impossibility; the exact-use induction below extends this last-rule contradiction by proving that every derivable term consumes each linear assumption exactly once. ◻

Proof. Induct on typing. At T-UVar, the selected variable is $x$, when the second premise concludes, or another variable, when the rule reapplies. For a split rule apply the hypotheses to all premises: the substituted value contributes no linear context. Both alternatives of T-Case receive the substitution and retain the same residual context. Bang introduction remains legal because the value has empty linear context. In the T-LolliI case, alpha-rename its binder $y$ away from $x$ and the free variables of $v$, apply the induction hypothesis to $\mathrm{\Gamma },x:A;\mathrm{\Delta },y:C⊢e:D$, and reapply T-LolliI to the resulting premise $\mathrm{\Gamma };\mathrm{\Delta },y:C⊢e[v/x]:D$. The other binders use the same freshness convention, after which the final rule reapplies. ◻

Proof. Induct on the first derivation. At T-LVar, the distinguished variable is $x$, ${\mathrm{\Delta }}_1=\cdot$, and the second premise concludes. In a binary multiplicative rule, exclusive membership puts $x$ in one premise. For example, if the last rule is T-LolliE, write its conclusion split as ${\mathrm{\Sigma }}_1\uplus {\mathrm{\Sigma }}_2={\mathrm{\Delta }}_1,x:A$. Exclusive membership gives exactly one of $${\mathrm{\Sigma }}_1={\mathrm{\Sigma }}_1^{\prime },x:A\text{or}{\mathrm{\Sigma }}_2={\mathrm{\Sigma }}_2^{\prime },x:A.$$ In the first case, the induction hypothesis changes the function premise to $\mathrm{\Gamma };{\mathrm{\Sigma }}_1^{\prime }\uplus {\mathrm{\Delta }}_2⊢e_1[v/x]:C⊸B$, while the argument premise retains context ${\mathrm{\Sigma }}_2$. Reapplying T-LolliE gives context $$({\mathrm{\Sigma }}_1^{\prime }\uplus {\mathrm{\Delta }}_2)\uplus {\mathrm{\Sigma }}_2=({\mathrm{\Sigma }}_1^{\prime }\uplus {\mathrm{\Sigma }}_2)\uplus {\mathrm{\Delta }}_2={\mathrm{\Delta }}_1\uplus {\mathrm{\Delta }}_2.$$ In the second case, the function premise retains ${\mathrm{\Sigma }}_1$, and the induction hypothesis changes the argument premise to $\mathrm{\Gamma };{\mathrm{\Sigma }}_2^{\prime }\uplus {\mathrm{\Delta }}_2⊢e_2[v/x]:C$. The rebuilt context is $${\mathrm{\Sigma }}_1\uplus ({\mathrm{\Sigma }}_2^{\prime }\uplus {\mathrm{\Delta }}_2)=({\mathrm{\Sigma }}_1\uplus {\mathrm{\Sigma }}_2^{\prime })\uplus {\mathrm{\Delta }}_2={\mathrm{\Delta }}_1\uplus {\mathrm{\Delta }}_2.$$ Tensor introduction uses this exclusive-membership calculation. So does each elimination rule whose displayed premises split the context.

For T-Case, if $x\in {\mathrm{\Delta }}_0$, substitute only in the scrutinee. If $x\in {\mathrm{\Delta }}_r$, substitute in both branch premises. This duplicates syntax between alternatives, not along an execution; both branches retain the same enlarged residual context. Bang introduction cannot be final because its linear context is empty. Bang elimination is another split. Injections use their sole premise, and binders are renamed fresh. These cases exhaust the rules. ◻

Proof. Alpha-rename $x,y$ away from each other’s substituent. Regard the first premise as $\mathrm{\Gamma };(\mathrm{\Delta },y:B),x:A⊢e:C$. Because ${\mathrm{\Delta }}_1$ is disjoint from both $\mathrm{\Delta }$ and $y$, linear substitution gives $$\mathrm{\Gamma };\mathrm{\Delta }\uplus {\mathrm{\Delta }}_1,y:B⊢e[v/x]:C.$$ The second substitution, using ${\mathrm{\Delta }}_2$, gives $$\mathrm{\Gamma };\mathrm{\Delta }\uplus {\mathrm{\Delta }}_1\uplus {\mathrm{\Delta }}_2⊢e[v/x][w/y]:C.$$ The freshness choices and $y\notin \mathsf{FV}(v)$ give $e[v/x][w/y]=e[v/x,w/y]$. Associativity from lemma 18.2 gives $(\mathrm{\Delta }\uplus {\mathrm{\Delta }}_1)\uplus {\mathrm{\Delta }}_2=\mathrm{\Delta }\uplus ({\mathrm{\Delta }}_1\uplus {\mathrm{\Delta }}_2)$ for the displayed context. ◻

Proof. Prove both clauses simultaneously by induction on typing, alpha-renaming each new binder away from the queried $z$. The two variable rules give one for the selected linear variable and zero for an absent variable. In every multiplicative split, exclusive membership puts a linear $z$ in exactly one premise. Its induction hypothesis gives use count one there; because $z$ is absent from every other premise context, their induction hypotheses give use count zero.

In T-Case, a variable from ${\mathrm{\Delta }}_0$ contributes one in the scrutinee and zero in both branches. A variable from ${\mathrm{\Delta }}_r$ contributes zero in the scrutinee and one in each branch. Thus the partial case clause is defined and has value one in either placement. If $z$ is absent, all three uses are zero. Bang introduction has empty linear context; bang elimination is another split, with its bound variable masked in the body. The one-premise rules and introductions follow from their displayed structural clauses. This also proves that every use invoked in the theorem is defined. ◻

Proof. For the first claim, inspect the core value grammar and invert the final typing rule. There is no subsumption to obscure the outer constructor, and a closed variable is impossible. For the second, invert a witnessing template from definition 18.19. A value template at function type is a lambda or one of the three primitive constants. The only template value at $\mathsf{File}$ is a linear placeholder $x_h$, and the closing substitution turns it into ${\mathsf{file}}_h$; distinct placeholders and tokens give uniqueness. ◻

Proof. Proceed simultaneously by structural induction on $E$ and inversion of the outer typing derivation. At the hole, the whole derivation is the designated subderivation. Each application and tensor frame selects one of the two premises of its unique syntax-directed outer rule; each tensor, unit, case, or bang-elimination frame selects its scrutinee premise; and an injection frame selects its sole premise. The induction hypothesis decomposes that premise and fixes $\mathrm{\Theta },B$; the untouched premises and their original context split then reconstruct the outer derivation. A case context changes only its scrutinee, so the common branch context is unchanged. These constructors exhaust the evaluation-context grammar, and there is no context beneath a bang because T-BangI accepts only a value. Replacing the designated premise and reversing this induction proves recomposition. ◻

Proof. Contextual steps use lemma 18.16. For beta, invert implication elimination and introduction, then apply linear substitution and split associativity. For tensor, invert tensor elimination and introduction, then apply two-variable substitution. For unit, inversion says that $\ast$ contributes the empty context.

For a left sum root, injection inversion gives $\mathrm{\Gamma };{\mathrm{\Delta }}_0⊢v:A$, and the selected branch has $\mathrm{\Gamma };{\mathrm{\Delta }}_r,x:A⊢e_1:C$; linear substitution restores ${\mathrm{\Delta }}_0\uplus {\mathrm{\Delta }}_r$. For the right root, replace $\mathsf{inl},v,x,e_1,A$ by $\mathsf{inr},v,y,e_2,B$; the same substitution argument restores the same split. For bang, introduction inversion gives an empty linear context; elimination puts $x:A$ in $\mathrm{\Gamma }$, so unrestricted substitution concludes. ◻

Proof. Induct on typing. A closed derivation cannot end in a variable rule. For application, step the function and argument in order; when both are values, the function is a lambda by canonical forms, so beta applies. For $e_1\otimes e_2$, step $e_1$, then $e_2$; two values form a tensor value. An injection steps its payload; an injected value is a value. Each elimination first steps its scrutinee. At a value scrutinee, canonical forms gives the matching tensor, injection, unit, or bang introduction, so the corresponding root rule applies. A bang introduction is already a value.

If a closed typed term reaches $e^{\prime }$, repeated preservation gives $\cdot ;\cdot ⊢e^{\prime }:A$. Progress therefore excludes a stuck nonvalue $e^{\prime }$. ◻

Proof. Choose the witnessing template for the premise. Substitution of file tokens for variables changes no constructor in the evaluation-context spine, and the active term $\mathsf{open}\ast$ contains no token. The template therefore factors as $E_0[\mathsf{open}\ast ]$, with $E_0$ closing to $E$.

The hole has type $\mathsf{File}$ under the empty linear context: both $\mathsf{open}$ and $\ast$ have empty linear context and application unions those two empty maps. Replace that subderivation by $$\cdot ;x_h:\mathsf{File}⊢x_h:\mathsf{File}.$$ Induction outward through $E_0$ adds the fresh singleton to the unique multiplicative premise containing the hole. For a case scrutinee it is added to ${\mathrm{\Delta }}_0$, leaving the common branch context unchanged. An application or tensor frame places the hole in its left or right premise; tensor, unit, and bang elimination place it in the scrutinee premise; an injection places it in its payload premise; and a case frame places it in its scrutinee premise. Each frame therefore adds the singleton only to the premise containing the hole. No evaluation context descends under bang, so the induction has no T-BangI case. The rebuilt template has the old placeholders together with $x_h$, and its closing substitution is $E[{\mathsf{file}}_h]$. ◻

Proof. Induct on the evaluation context. At the hole, use the unique placeholder whose closing image is ${\mathsf{file}}_h$. Each context constructor corresponds to one typing premise and retains its original split. If the hole is the scrutinee of a case, exact use puts $x_h$ in the scrutinee context and the absent-variable clause of theorem 18.14 gives zero uses in both branches. Reduction never enters an unselected branch. The other split constructors are simpler: exclusive membership places $x_h$ only in the premise containing the hole.

For read, T-LolliE, T-Read, and T-LVar type the active redex. The replacement is typed by T-TensorI from the same linear placeholder and the closed T-Bytes value. For close, the active T-LolliE consumes the sole placeholder; replacing its unit result by T-OneI therefore removes that singleton from the witnessing context. Context replacement rebuilds the outer derivation. ◻

Proof. For progress, induct on the typing derivation of the template while following the corresponding closed term. The core cases repeat theorem 18.18. At a value-headed application, the extended canonical-forms clause gives either a lambda, when beta applies, or one of the three primitives. Its unique declared domain and the argument canonical-form clause force $\ast$ for open and a live ${\mathsf{file}}_h$ for read or close, so the corresponding configuration root applies.

At a core root, template substitution preserves every context split. For read and close, lemma 36.22 replaces the active placeholder while preserving the surrounding template. For open, lemma 36.21 gives directly $$H\cup \{h\}⊩E[{\mathsf{file}}_h]:A$$ from $H⊩E[\mathsf{open}\ast ]:A$ and $h\notin H$. Thus the reconstructed template has exactly one path to each live token. For every $h\in H$, the placeholder $x_h:\mathsf{File}$ belongs to the template’s linear context, so theorem 18.14 gives ${\mathsf{use}}_{x_h}(e_0)=1$. Pairwise distinct placeholders and the closing substitution map only that $x_h$ to ${\mathsf{file}}_h$. Read preserves the same occurrence, open adds the fresh occurrence proved above, and close removes precisely its selected occurrence.

At result type $1$, canonical forms gives $v=\ast$. If $H$ were nonempty, exact use would force a file-placeholder occurrence in that unit value, a contradiction. ◻

Proof. Implication substitutes an argument into a lambda body. Tensor substitutes both components; unit removes the empty proof; either sum introduction selects one branch; and bang uses unrestricted substitution because its introduction had empty linear context. These are precisely the root cases of theorem 18.17.

For example, tensor introduction immediately followed by tensor elimination has the typed principal contraction $$\begin{array}{c}\frac{\begin{array}{c}{\displaystyle \frac{\begin{array}{c}\mathrm{\Gamma };{\mathrm{\Delta }}_v⊢v:A\\ \mathrm{\Gamma };{\mathrm{\Delta }}_w⊢w:B\end{array}}{\mathrm{\Gamma };{\mathrm{\Delta }}_v\uplus {\mathrm{\Delta }}_w⊢v\otimes w:A\otimes B}}\mathrm{T}-\mathrm{TensorI}\\ \mathrm{\Gamma };{\mathrm{\Delta }}_n,x:A,y:B⊢n:C\end{array}}{\mathrm{\Gamma };({\mathrm{\Delta }}_v\uplus {\mathrm{\Delta }}_w)\uplus {\mathrm{\Delta }}_n⊢\mathsf{let}x\otimes y=v\otimes w\mathsf{in}n:C}\mathrm{T}-\mathrm{TensorE}.\end{array}$$ The term contracts to $n[v/x,w/y]$. The two-variable instance of linear substitution derives $\mathrm{\Gamma };{\mathrm{\Delta }}_v\uplus {\mathrm{\Delta }}_w\uplus {\mathrm{\Delta }}_n⊢n[v/x,w/y]:C$; the split displays which resources travel with each value. ◻

Proof. Invert tensor elimination and then T-Case. Its two branches have one common residual context. Combine that context with the context of $n$, apply tensor elimination separately in both alternatives, and rebuild the outer case. Split associativity identifies the conclusion contexts. ◻

Proof. Induct on the first derivation, with the statement strengthened over every finite $n$. Alpha-rename each rule binder away from the $x_i$ and the free variables of the $v_i$. At T-LVar, either the selected variable belongs to $\mathrm{\Delta }$, when the rule reapplies, or it is the sole $x_i$, when the corresponding substituent derivation is the conclusion. The unrestricted variable and constant cases are one line each: T-UVar reapplies under the substituted unrestricted context, while a constant has no variable premise to transform.

For a multiplicative rule, exclusive membership partitions the $x_i$ between its premises. Apply the induction hypothesis to each part and use the pairwise disjointness of the ${\mathrm{\Theta }}_i$ to rebuild the conclusion. The common-refinement clause of lemma 18.2 gives a partition of the reassociated split with each $x_i$ in the same premise. For T-Case, send variables from the scrutinee context only to the scrutinee; send variables from the residual context, with the same substituents, to both alternatives. Only one alternative contributes to the conclusion context, so each ${\mathrm{\Theta }}_i$ still occurs once. The one-premise rules follow directly. T-BangI can be final only when $n=0$, because its linear context is empty.

It remains to treat the added structural rules. Suppose W-Aff adds $z:C$. If $z$ belongs to $\mathrm{\Delta }$, apply the induction hypothesis to the premise and restore the weakening. If $z=x_k$, omit $x_k$ and $v_k$ from the induction hypothesis; the term does not contain $x_k$. Then apply W-Aff once for every declaration of ${\mathrm{\Theta }}_k$. This adds exactly the missing context and proves the affine case. The same calculation handles weakening in ${⊢}_u$.

Now suppose C-Rel contracts $z_1:C,z_2:C$ to $z:C$. If $z\in \mathrm{dom}(\mathrm{\Delta })$, apply the induction hypothesis to the premise and contract $z_1,z_2$ again. If $z=x_k$, take two fresh renamings ${\mathrm{\Theta }}_k^1,{\mathrm{\Theta }}_k^2$ of ${\mathrm{\Theta }}_k$, and let $v_k^1,v_k^2$ be the corresponding renamings of $v_k$. Apply the induction hypothesis to the strict premise with the substitution list $$x_1\mapsto v_1,\dots ,x_{k-1}\mapsto v_{k-1},z_1\mapsto v_k^1,z_2\mapsto v_k^2,x_{k+1}\mapsto v_{k+1},\dots ,x_n\mapsto v_n.$$ Its contexts are pairwise disjoint by the fresh renamings. For every declaration $q:C_q$ in ${\mathrm{\Theta }}_k$, apply C-Rel to the corresponding pair $q^1:C_q,q^2:C_q$. After all these contractions and renaming back to $q$, the duplicated context ${\mathrm{\Theta }}_k^1\uplus {\mathrm{\Theta }}_k^2$ has become ${\mathrm{\Theta }}_k$, and the term is $$e[v_k^1/z_1,v_k^2/z_2][q/q^1,q/q^2{]}_{q\in \mathrm{dom}({\mathrm{\Theta }}_k)}=e[v_k/z_1,v_k/z_2].$$ This is precisely the substitution instance of the contraction conclusion. No weakening is used. The unrestricted case admits the same contraction calculation, and these cases exhaust the derivation. ◻