ch:linear-types: ch:linear-types

Pairwise disjointness supplies the six facts $${\mathrm{\Delta }}_1\mathrm{\#}{\mathrm{\Delta }}_2,{\mathrm{\Delta }}_1\mathrm{\#}{\mathrm{\Theta }}_1,{\mathrm{\Delta }}_1\mathrm{\#}{\mathrm{\Theta }}_2,{\mathrm{\Delta }}_2\mathrm{\#}{\mathrm{\Theta }}_1,{\mathrm{\Delta }}_2\mathrm{\#}{\mathrm{\Theta }}_2,{\mathrm{\Theta }}_1\mathrm{\#}{\mathrm{\Theta }}_2.$$ Thus every intermediate union displayed in the problem is defined. Repeated associativity gives $$(({\mathrm{\Delta }}_1\uplus {\mathrm{\Delta }}_2)\uplus {\mathrm{\Theta }}_1)\uplus {\mathrm{\Theta }}_2={\mathrm{\Delta }}_1\uplus ({\mathrm{\Delta }}_2\uplus ({\mathrm{\Theta }}_1\uplus {\mathrm{\Theta }}_2)).$$ Commuting the middle two summands and reassociating yields $${\mathrm{\Delta }}_1\uplus ({\mathrm{\Theta }}_1\uplus ({\mathrm{\Delta }}_2\uplus {\mathrm{\Theta }}_2)).$$ For the second equation, both sides are the finite map whose domain is the disjoint union of the same four domains and whose restriction to each domain is the corresponding context. More explicitly, The first line uses the four cross-disjointness facts between the two parenthesized pairs; the last line uses them again after the permutation.

Under the singleton context $f:\mathsf{File}$, the body of $e_1$ has the derivation $$\frac{\begin{array}{c}\cdot ;u:1⊢u:1\\ \cdot ;f:\mathsf{File}⊢\mathsf{read}f:\mathsf{File}\otimes \mathsf{Bytes}\end{array}}{\cdot ;u:1,f:\mathsf{File}⊢\mathsf{let}\ast =u\mathsf{in}\mathsf{read}f:\mathsf{File}\otimes \mathsf{Bytes}}\mathrm{T}-\mathrm{OneE}.$$ Hence $\cdot ;f:\mathsf{File}⊢e_1:1⊸(\mathsf{File}\otimes \mathsf{Bytes})$. Separately, T-Close, T-LVar, and T-LolliE give $$\cdot ;f:\mathsf{File}⊢e_2=\mathsf{close}f:1.$$ The rejected rule therefore offers the same declaration $f:\mathsf{File}$ to both premises and concludes a type for $e_1{e}_2$. Call by value first evaluates the argument $e_2$, removing the live token, and beta reduction then exposes the read in $e_1$. The duplicated assumption is precisely $f:\mathsf{File}$. Removing an explicit contraction rule does not help: the unsplit application rule itself has copied its entire $\mathrm{\Delta }$ into two premises.

The body derivation is $$\frac{\begin{array}{c}{\displaystyle \frac{\phantom{X}}{\cdot ;p:A\otimes B⊢p:A\otimes B}}\mathrm{T}-\mathrm{LVar}\\ {\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{\phantom{X}}{\cdot ;y:B⊢y:B}}\mathrm{T}-\mathrm{LVar}\\ {\displaystyle \frac{\phantom{X}}{\cdot ;x:A⊢x:A}}\mathrm{T}-\mathrm{LVar}\end{array}}{\cdot ;y:B,x:A⊢y\otimes x:B\otimes A}}\mathrm{T}-\mathrm{TensorI}\end{array}}{\cdot ;p:A\otimes B⊢\mathsf{let}x\otimes y=p\mathsf{in}y\otimes x:B\otimes A}\mathrm{T}-\mathrm{TensorE}.$$ The two singleton premises of T-TensorI are $y:B$ and $x:A$; their union is the branch context supplied by tensor elimination. Applying T-LolliI discharges $p$ and concludes $$\cdot ;\cdot ⊢\mathsf{swap}:(A\otimes B)⊸(B\otimes A).$$

Suppose first that $\cdot ;\cdot ⊢\lambda x.x\otimes x:A⊸(A\otimes A)$. Inverting T-LolliI gives $\cdot ;x:A⊢x\otimes x:A\otimes A$. Inverting T-TensorI would split the singleton context as ${\mathrm{\Delta }}_1\uplus {\mathrm{\Delta }}_2=x:A$ and type one occurrence of $x$ in each premise. Each variable premise requires its entire linear context to be the singleton $x:A$, so both ${\mathrm{\Delta }}_1$ and ${\mathrm{\Delta }}_2$ contain $x$. They are not disjoint, a contradiction.

For $\lambda x.\ast$, implication inversion would require $\cdot ;x:A⊢\ast :1$. The only introduction of $\ast$ is T-OneI, whose linear premise is $\cdot$. No rule removes the unused declaration $x:A$. Hence neither displayed judgment is derivable.

Define $${\mathsf{route}}^{\prime }=\lambda z.\lambda r.\mathsf{case}z\mathsf{of}\mathsf{inl}x\Rightarrow \mathsf{inr}(x\otimes r)\mid \mathsf{inr}y\Rightarrow \mathsf{inl}(y\otimes r).$$ In either branch, T-TensorI first gives $x\otimes r:A\otimes R$ or $y\otimes r:A\otimes R$. Use T-PlusI2 in the left branch and T-PlusI1 in the right: $$\cdot ;x:A,r:R⊢\mathsf{inr}(x\otimes r):(A\otimes R)\oplus (A\otimes R),$$ $$\cdot ;y:A,r:R⊢\mathsf{inl}(y\otimes r):(A\otimes R)\oplus (A\otimes R).$$ With scrutinee context $z:A\oplus A$, T-Case takes $r:R$ as the same residual context in both alternatives. Two implications therefore give $$\cdot ;\cdot ⊢{\mathsf{route}}^{\prime }:(A\oplus A)⊸(R⊸((A\otimes R)\oplus (A\otimes R))).$$ The printed occurrence of $r$ is duplicated between alternatives, but only the selected alternative executes; this is exactly why T-Case shares, rather than splits, its residual context.

Suppose the last rule of the first derivation is $$\frac{\begin{array}{c}\mathrm{\Gamma };{\mathrm{\Xi }}_1⊢e_1:C⊸B\\ \mathrm{\Gamma };{\mathrm{\Xi }}_2⊢e_2:C\end{array}}{\mathrm{\Gamma };{\mathrm{\Xi }}_1\uplus {\mathrm{\Xi }}_2⊢e_1{e}_2:B}\mathrm{T}-\mathrm{LolliE},$$ where ${\mathrm{\Xi }}_1\uplus {\mathrm{\Xi }}_2={\mathrm{\Delta }}_1,x:A$. Exclusive membership puts $x$ in exactly one premise. If ${\mathrm{\Xi }}_1={\mathrm{\Xi }}_1^{\prime },x:A$, the induction hypothesis and the substituent $\mathrm{\Gamma };{\mathrm{\Delta }}_2⊢v:A$ give $$\mathrm{\Gamma };{\mathrm{\Xi }}_1^{\prime }\uplus {\mathrm{\Delta }}_2⊢e_1[v/x]:C⊸B.$$ The second premise is unchanged. Reapplying T-LolliE yields $$\mathrm{\Gamma };({\mathrm{\Xi }}_1^{\prime }\uplus {\mathrm{\Delta }}_2)\uplus {\mathrm{\Xi }}_2⊢e_1[v/x]e_2:B.$$ Pairwise disjointness and split algebra identify its context by $$({\mathrm{\Xi }}_1^{\prime }\uplus {\mathrm{\Delta }}_2)\uplus {\mathrm{\Xi }}_2=({\mathrm{\Xi }}_1^{\prime }\uplus {\mathrm{\Xi }}_2)\uplus {\mathrm{\Delta }}_2={\mathrm{\Delta }}_1\uplus {\mathrm{\Delta }}_2.$$ The term is $(e_1{e}_2)[v/x]$. If $x\in {\mathrm{\Xi }}_2$, the symmetric argument substitutes in the argument premise and uses ${\mathrm{\Xi }}_1\uplus ({\mathrm{\Xi }}_2^{\prime }\uplus {\mathrm{\Delta }}_2)=({\mathrm{\Xi }}_1\uplus {\mathrm{\Xi }}_2^{\prime })\uplus {\mathrm{\Delta }}_2$.

Inversion of a typing derivation for the tensor redex supplies pairwise disjoint contexts and premises $$\mathrm{\Gamma };{\mathrm{\Delta }}_v⊢v:P,\mathrm{\Gamma };{\mathrm{\Delta }}_w⊢w:Q,\mathrm{\Gamma };{\mathrm{\Delta }}_e,x:P,y:Q⊢e:C.$$ The redex is typed under $({\mathrm{\Delta }}_v\uplus {\mathrm{\Delta }}_w)\uplus {\mathrm{\Delta }}_e$: tensor introduction first types $v\otimes w$, and tensor elimination combines that result with the body premise.

Alpha-rename $x,y$ away from the substituents. Regard the body context as $({\mathrm{\Delta }}_e,y:Q),x:P$. Linear substitution with $v$ gives $$\mathrm{\Gamma };{\mathrm{\Delta }}_e\uplus {\mathrm{\Delta }}_v,y:Q⊢e[v/x]:C.$$ A second substitution with $w$ gives $$\mathrm{\Gamma };({\mathrm{\Delta }}_e\uplus {\mathrm{\Delta }}_v)\uplus {\mathrm{\Delta }}_w⊢e[v/x,w/y]:C.$$ Finally, $$({\mathrm{\Delta }}_e\uplus {\mathrm{\Delta }}_v)\uplus {\mathrm{\Delta }}_w=({\mathrm{\Delta }}_v\uplus {\mathrm{\Delta }}_w)\uplus {\mathrm{\Delta }}_e$$ by commutativity and associativity of the pairwise-disjoint union. This is the context of the redex, so the tensor root preserves its type.

Rule T-TensorI gives $$\mathrm{\Gamma };{\mathrm{\Delta }}_v\uplus {\mathrm{\Delta }}_w⊢v\otimes w:P\otimes Q.$$ Combining this with the supplied body premise by T-TensorE types the redex under $({\mathrm{\Delta }}_v\uplus {\mathrm{\Delta }}_w)\uplus {\mathrm{\Delta }}_e$.

For the reduct, first apply linear substitution to $x$: $$\frac{\mathrm{\Gamma };{\mathrm{\Delta }}_e,x:P,y:Q⊢e:C\mathrm{\Gamma };{\mathrm{\Delta }}_v⊢v:P}{\mathrm{\Gamma };{\mathrm{\Delta }}_e\uplus {\mathrm{\Delta }}_v,y:Q⊢e[v/x]:C}.$$ Then apply it to $y$: $$\frac{\mathrm{\Gamma };{\mathrm{\Delta }}_e\uplus {\mathrm{\Delta }}_v,y:Q⊢e[v/x]:C\mathrm{\Gamma };{\mathrm{\Delta }}_w⊢w:Q}{\mathrm{\Gamma };({\mathrm{\Delta }}_e\uplus {\mathrm{\Delta }}_v)\uplus {\mathrm{\Delta }}_w⊢e[v/x,w/y]:C}.$$ After fresh alpha-renaming, the simultaneous substitution is the displayed pair of successive substitutions. The context equation is $$({\mathrm{\Delta }}_e\uplus {\mathrm{\Delta }}_v)\uplus {\mathrm{\Delta }}_w=({\mathrm{\Delta }}_v\uplus {\mathrm{\Delta }}_w)\uplus {\mathrm{\Delta }}_e={\mathrm{\Delta }}_v\uplus {\mathrm{\Delta }}_w\uplus {\mathrm{\Delta }}_e,$$ so redex and reduct have the required common context and type.

On the left, T-Case uses ${\mathrm{\Delta }}_s$ for its scrutinee and the common residual $${\mathrm{\Delta }}_r,p:P,q:Q$$ for both branches. It therefore types the case at $C$ under ${\mathrm{\Delta }}_s\uplus ({\mathrm{\Delta }}_r,p:P,q:Q)$. Tensor elimination then combines this body with $t:P\otimes Q$ and concludes under $${\mathrm{\Delta }}_t\uplus {\mathrm{\Delta }}_s\uplus {\mathrm{\Delta }}_r.$$

On the right, use tensor elimination separately in the alternatives. The left one has premises $t:P\otimes Q$ under ${\mathrm{\Delta }}_t$ and $e_1:C$ under ${\mathrm{\Delta }}_r,p:P,q:Q,x:A$, so it concludes under ${\mathrm{\Delta }}_t\uplus {\mathrm{\Delta }}_r,x:A$. The right alternative similarly concludes under ${\mathrm{\Delta }}_t\uplus {\mathrm{\Delta }}_r,y:B$. Thus the outer T-Case has scrutinee context ${\mathrm{\Delta }}_s$ and the common residual $${\mathrm{\Delta }}_t\uplus {\mathrm{\Delta }}_r.$$ It concludes under ${\mathrm{\Delta }}_s\uplus ({\mathrm{\Delta }}_t\uplus {\mathrm{\Delta }}_r)$. The freshness hypotheses prevent either elimination binder from capturing a free variable of $s$ or $t$, and split commutativity and associativity give $${\mathrm{\Delta }}_s\uplus ({\mathrm{\Delta }}_t\uplus {\mathrm{\Delta }}_r)={\mathrm{\Delta }}_t\uplus {\mathrm{\Delta }}_s\uplus {\mathrm{\Delta }}_r.$$ Hence both sides have type $C$ under the stated context.

In the first configuration, T-Case places $x:A$ in the scrutinee context. Linear substitution gives $$\mathrm{\Gamma };{\mathrm{\Delta }}_0\uplus \mathrm{\Theta }⊢s[v/x]:P\oplus Q.$$ The branch premises are unchanged, so rebuilding the case yields $$\mathrm{\Gamma };({\mathrm{\Delta }}_0\uplus \mathrm{\Theta })\uplus {\mathrm{\Delta }}_r⊢\mathsf{case}s[v/x]\mathsf{of}\mathsf{inl}p\Rightarrow e_1\mid \mathsf{inr}q\Rightarrow e_2:C.$$

In the second configuration, the scrutinee is unchanged. Apply linear substitution to both branch derivations: $$\mathrm{\Gamma };{\mathrm{\Delta }}_r\uplus \mathrm{\Theta },p:P⊢e_1[v/x]:C,\mathrm{\Gamma };{\mathrm{\Delta }}_r\uplus \mathrm{\Theta },q:Q⊢e_2[v/x]:C.$$ Both alternatives therefore have the common residual ${\mathrm{\Delta }}_r\uplus \mathrm{\Theta }$, and T-Case gives $$\mathrm{\Gamma };{\mathrm{\Delta }}_0\uplus ({\mathrm{\Delta }}_r\uplus \mathrm{\Theta })⊢\mathsf{case}s\mathsf{of}\mathsf{inl}p\Rightarrow e_1[v/x]\mid \mathsf{inr}q\Rightarrow e_2[v/x]:C.$$ If the two residual contexts differed, no single ${\mathrm{\Delta }}_r$ could fill both branch premises of T-Case; the rule would therefore be inapplicable.

For the first term, implication inversion puts one declaration $f:\mathsf{File}$ in the body. Tensor inversion would split it between two premises, but inversion of each application $\mathsf{read}f$ requires a premise containing $f$. Both summands would contain the same declaration, contradicting disjointness.

For the second term, implication inversion requires $\cdot ;f:\mathsf{File}⊢\ast :1$. Inverting its only possible last rule, T-OneI, requires the empty linear context, so the declaration $f$ cannot be consumed.

For the third term, the application $\mathsf{read}f$ consumes $f$ and has type $\mathsf{File}\otimes \mathsf{Bytes}$. Tensor elimination therefore extends the body by $f^{\prime }:\mathsf{File},b:\mathsf{Bytes}$. Returning $b$ uses T-LVar under the singleton context $b:\mathsf{Bytes}$; the declaration $f^{\prime }:\mathsf{File}$ remains. Since there is no linear weakening rule, that branch premise cannot be formed. Thus all three displayed types are underivable.

The scrutinee variable has $\cdot ;z:1\oplus 1⊢z:1\oplus 1$. In the left branch, T-OneE consumes $u:1$ and a second T-OneE consumes the unit returned by $\mathsf{close}f$; the application of close consumes $f:\mathsf{File}$. Hence $$\cdot ;u:1,f:\mathsf{File}⊢\mathsf{let}\ast =u\mathsf{in}\mathsf{let}\ast =\mathsf{close}f\mathsf{in}\ast :1.$$ The right branch has the identical derivation with $v$ in place of $u$. Thus T-Case uses $f:\mathsf{File}$ as its common residual and gives $$\cdot ;z:1\oplus 1,f:\mathsf{File}⊢q(z,f):1.$$

The scrutinee contributes one use of $z$ and zero of $f$. After masking the branch binders, each branch contributes one use of $f$: it occurs only as the close argument. The case clause therefore compares equal branch counts and calculates $${\mathsf{use}}_f(q(z,f))=0+1=1.$$ For the left injection, the complete branch trace is The roots are, in order, E-InL, E-One, E-Close, and E-One. Replacing $\mathsf{inl}$ and its binder by $\mathsf{inr}$ and the right binder gives the symmetric four-step trace. Only the selected printed occurrence of $f$ runs.

One affine weakening gives the body premise $$\frac{\cdot ;\cdot {⊢}_a\ast :1}{\cdot ;f:\mathsf{File}{⊢}_a\ast :1}\mathrm{W}-\mathrm{Aff}.$$ Rule T-LolliI therefore types $\lambda f.\ast :\mathsf{File}⊸1$. Independently, T-Open, T-OneI, and T-LolliE type $\mathsf{open}\ast :\mathsf{File}$ under the empty context. A final T-LolliE derives $\cdot ;\cdot {⊢}_a\mathsf{drop}:1$.

For fresh $h$, evaluation is $$(\mathrm{\varnothing },\mathsf{drop}){⟶}^{\ast }(\{h\},(\lambda f.\ast ){\mathsf{file}}_h)⟶(\{h\},\ast ).$$ The strictly linear cleanup conclusion says that a returned unit has empty live set. The affine trace ends with live set $\{h\}$, so that conclusion does not transfer to affine typing. This is not a counterexample to theorem 18.20: its premise is the strictly linear ownership judgment $H⊩e:A$, whereas the displayed derivation uses ${⊢}_a$ and its additional weakening rule.

Use distinct assumptions $f_1,f_2:\mathsf{File}$ before contraction. The body has the derivation shape $$\frac{\begin{array}{c}\cdot ;f_1:\mathsf{File}{⊢}_r\mathsf{close}{f}_1:1\\ \cdot ;f_2:\mathsf{File}{⊢}_r\mathsf{close}{f}_2:1\end{array}}{\cdot ;f_1:\mathsf{File},f_2:\mathsf{File}{⊢}_r\mathsf{let}\ast =\mathsf{close}{f}_1\mathsf{in}\mathsf{close}{f}_2:1}\mathrm{T}-\mathrm{OneE}.$$ Rule C-Rel identifies $f_1,f_2$ with $f$, producing the body printed in $\mathsf{badClose}$; T-LolliI discharges $f$. The closed argument $\mathsf{open}\ast$ supplies the final T-LolliE premise.

For fresh $h$, the complete relevant trace is The last configuration is stuck because $h$ is no longer live.

Affine typing preserves configurations and at-most-one ownership, but cleanup fails by the drop trace. Relevant typing destroys one-owner immediately and configuration preservation at the first close; therefore iterated progress also fails. Its no-weakening fact still implies $H{⊩}_{r}v:1\Rightarrow H=\mathrm{\varnothing }$, so the trace above is not a cleanup counterexample: it never returns unit. Unrestricted typing admits both counterexamples, so one-owner, configuration preservation/progress, and cleanup all fail there.

The identity needs no structural rule: T-LVar followed by T-LolliI derives it already in ${⊢}_{\ell }$ (and the same tree is available in every regime). It uses zero weakenings and zero contractions.

The discarded function needs exactly one W-Aff, as in exercise 18.14; its inclusion-minimal regime is affine, and it is also derivable unrestrictedly. It is not linear or relevant: inversion of the implication would require a derivation of $\ast$ with $x:A$ still in the linear context, while neither regime has weakening.

For $\lambda x.x\otimes x$, start with two variable leaves under $x_1:A$ and $x_2:A$, combine them by T-TensorI, and use one C-Rel to identify $x_1,x_2$ with $x$. Thus its minimal regime is relevant, with one contraction and no weakening. For $\lambda x.(x\otimes x)\otimes x$, tensor introduction first uses three fresh declarations $x_1,x_2,x_3:A$. Contract $x_1,x_2$ and then contract the resulting declaration with $x_3$. After the two capture-avoiding identifications the body is $(x\otimes x)\otimes x$. Its minimal regime is again relevant, now with two contractions and no weakening. Both copying terms are also unrestrictedly derivable.

Neither copying term is affine or linear. Inverting their tensor trees forces two, respectively three, leaves whose contexts all contain the one declaration $x:A$; disjoint splitting cannot supply those leaves, and affine weakening cannot create a second occurrence. Hence the classifications and the stated rule counts are minimal.

Let $g:!(A⊸A)$ be linear. Bang elimination consumes $g$ and places $f:A⊸A$ in the unrestricted context. Under the additional linear declaration $x:A$, the innermost application is $$\frac{\begin{array}{c}f:A⊸A;\cdot ⊢f:A⊸A\\ f:A⊸A;x:A⊢x:A\end{array}}{f:A⊸A;x:A⊢fx:A}\mathrm{T}-\mathrm{LolliE}.$$ Apply the same unrestricted $f$ once to $fx$ and once to $f(fx)$. These are three T-UVar leaves for $f$, each with empty linear context, and one T-LVar leaf for $x$. Implication introduction discharges $x$; bang elimination rebuilds the body; the outer implication introduction discharges $g$. Hence $$\cdot ;\cdot ⊢{\mathsf{thrice}}_{!}:!(A⊸A)⊸(A⊸A).$$ The derivation stores only the permission to reuse $f$, not the numeral three: the same T-UVar rule could occur any finite number of times.

For the unwrapped term, inversion of the outer and inner T-LolliI rules leaves a single linear declaration $f:A⊸A$ for the nested application. Inversion of its two outer T-LolliE rules would have to partition that singleton among three function premises, each of which ends in T-LVar for $f$. Pairwise disjoint context splitting cannot do so. Thus the displayed linear type of the unwrapped $\mathsf{thrice}$ is underivable.

Removing $x$ is absence: the precontext no longer contains it, so neither a term nor a type may mention it. Marking $x$ by zero is contemplation: the shared precontext retains $x:S$, but a nonzero run-time subject cannot consume it. This is the case justified by zero-erasure.

Permitting an unused unit-priced input is discardability. It needs the ordered weakening rule and its factorization, splitting, and zero-reflection conditions; the rigid zero annotation alone does not justify it. Postulating that all proof inhabitants are equal is proof irrelevance. It needs an equality rule or semantic principle and follows neither from absence nor from erasure. Thus the four changes realize, respectively, clauses 1–4 of proposition 36.33; only the second is the zero-use mechanism of the erasure theorem.