ch:coeffects: ch:coeffects

The two accesses require $\{(?\mathsf{width},\mathsf{int})\}$ and $\{(?\mathsf{height},\mathsf{int})\}$; the constant requires empty. The inner addition takes the union of height with empty, and the outer addition unions width with that result. Since $R{\wedge }_{\mathsf{c}}S=R\cup S=R{\oplus }_{\mathsf{c}}S$, condition $F$ is reflexivity of subset inclusion.

Take the discrete preorder on $\{a,u,b\}$ and set $\mathsf{use}=u$. Neither $a\le u$ nor $u\le a$ holds, so use is neither greatest nor least. Consequently the first step of both pointed substitution proofs is unavailable. This only blocks those proofs; it is not a counterexample to preservation.

The body $x+x$ contracts $⟨1⟩$ and $⟨1⟩$ to the latent scalar $2$. The argument $y+y$ has vector $⟨2⟩$. Application scales it to $2\times ⟨2⟩=⟨4⟩$. The two additions occur inside the separate body and argument derivations; multiplication occurs only at application.

Flat call-by-value substitutes an argument at $\mathsf{use}$ and retains the receiving scalar. Top-pointed call-by-name first uses $s\le \mathsf{use}$ and has the same conclusion. Bottom-pointed call-by-name concludes at $r⊛s$ and needs equality, commutativity, and idempotence of the three flat operations. Structural substitution replaces the bound variable’s vector cell $r$ by $r⊛S$; its unique position removes the need for pointedness.

Let $\rho (?w)=4$, $\rho (?h)=7$, and take $(\rho ,(4,7))\in D_{R\cup S}(\mathsf{int}\times \mathsf{int})$. The split image is $(\rho {|}_R,4)\in D_R(\mathsf{int})$ and $(\rho {|}_S,7)\in D_S(\mathsf{int})$. For the separate forgetting square, $${\mathrm{res}}_{\varnothing }^R({\mathrm{res}}_R^{R\cup S}(\rho ,(4,7)))=((\rho {|}_R){|}_{\varnothing },(4,7))=(\rho {|}_{\varnothing },(4,7)),$$ because restriction composes by intersection. The path through $S$ is $${\mathrm{res}}_{\varnothing }^S({\mathrm{res}}_S^{R\cup S}(\rho ,(4,7)))=((\rho {|}_S){|}_{\varnothing },(4,7))=(\rho {|}_{\varnothing },(4,7)).$$ Hence the square commutes in $D_{\varnothing }(\mathsf{int}\times \mathsf{int})$.

The least vector is $⟨3,1⟩$: the maximum offsets for $x$ and $y$ are $3$ and $1$. At time $3$, the three reads are $\rho (x{)}_1$, $\rho (y{)}_2$, and $\rho (x{)}_0$, in syntax order.