appendix sectionsolutions

ch:quantitative-types: ch:quantitative-types

The outer function occurrence contributes $1$ . The inner application lies in an argument scaled by $r$ , so the inner function occurrence contributes $r$ . The input lies under both argument positions and contributes $r^{2}$ . Thus the grades are $1 + r$ and $r^{2}$ . In the Boolean semiring, the function grade is true and the input grade is $r$ ; idempotent disjunction and conjunction cannot recover a call count.

exercise 54.2.

The premise of L-Prom must have a fully graded context, so $y : A$ blocks promotion. From L-Var, derive $y : A ⊢ y : A$ , use L-Der to get $y : [A]_{1} ⊢ y : A$ , and apply rank-one promotion to conclude $y : [A]_{1} ⊢ [y] : ◻_{1} A$ .

exercise 54.3.

Typing the redex ends with G-App from $Δ, x :_{r} A ⊢ t : B$ and $Θ ⊢ u : A$ , hence its context is $Δ + r Θ$ . Graded substitution derives the same context for $t [u / x]$ . This preserves a static annotation. No premise connects the semiring element to a measured number of machine steps or dynamic variable lookups.

exercise 54.4.

In the one-element semiring, $0 = 1$ . A constant body typed after zero weakening can therefore be abstracted at an arrow marked $1$ . A direct map to $A ⊸ B$ would demand that the bound variable occur linearly, but the constant body contains no occurrence. The grade $1$ has lost exact-use meaning.

exercise 54.5.

Expanding the equations gives $G [[◻_{2} (A ⊸ A)]] = (G [[A ⊸ A]] \overset{2}{\to} K) \overset{1}{\to} K,$ where $G [[A ⊸ A]] = ((G [[A]] \overset{1}{\to} G [[A]]) \overset{1}{\to} K) \overset{1}{\to} K .$ The grade $2$ is on the continuation consuming the boxed payload. Removing either continuation changes the translated type and invalidates the typing induction.

exercise 54.6.

Changing the operation performed by $p$ changes the index $e$ on $T_{e}$ and the effect-composition premise for its bind. Changing the number or mode of uses of $x$ changes $r$ on $D_{r}$ and the scalar multiplying its discharged context. Neither change determines the other.

exercise 54.7.

Let one location be targeted by two outgoing references, each with permission $1$ . Their total is $2$ , so the assignment does not satisfy the theorem’s incoming sum-one premise and is not a counterexample. It does destroy the desired unique full-permission state. Graded substitution computes context demand but has no heap-target relation summing all aliases to one location, so it cannot exclude the assignment.

exercise 54.9.

Put $F = ◻_{r} A ⊸ A$ . The source’s two application steps are $\frac{\begin{matrix} f :_{1} F ⊢_{G} f : F \\ \frac{\begin{matrix} f :_{1} F ⊢_{G} f : F \\ x :_{1} A ⊢_{G} x : A \end{matrix}}{f :_{1} F, x :_{r} A ⊢_{G} f x : A} G - App \end{matrix}}{f :_{1 + r} F, x :_{r^{2}} A ⊢_{G} f (f x) : A} G - App$ The direct translation inserts one promotion at each application: $\frac{x : [A]_{1} ⊢_{L} x : A}{x : [A]_{r} ⊢_{L} [x] : ◻_{r} A} L - Prom$ The outer application promotes the translated inner application: $\frac{f : [F]_{1}, x : [A]_{r} ⊢_{L} L [[f x]] : A}{f : [F]_{r}, x : [A]_{r^{2}} ⊢_{L} [L [[f x]]] : ◻_{r} A} L - Prom$ The outer L-App adds its independent $f : [F]_{1}$ to the second promotion’s $f : [F]_{r}$ . The two translated abstractions each use L-Let followed by L-Abs, giving $⊢_{L} L [[λ f . λ x . f (f x)]] : ◻_{1 + r} F ⊸ ◻_{r^{2}} A ⊸ A .$

exercise 54.10.

For function beta, expand CPS application, beta-reduce the outer continuation lambdas, apply the translated abstraction, and reach the translation of the substituted body. Modal beta passes the translated boxed payload to the let continuation before substituting it. Reductions underneath continuation lambdas are full-beta target steps, not source call-by-name positions.

exercise 54.11.

Let $p$ return under effect $e$ and let a discharged input be available at coeffect $2$ . Effect bind composes $e$ with the continuation effect using the effect monoid. Duplicating the input scales its discharged context using the coeffect semiring. Writing $e ∙ e^{'}$ and $2 \cdot [Δ]$ on separate derivation lines prevents either coordinate from being mistaken for the other.

exercise 54.8.

If all references to a location have total permission $1$ and one reference alone carries $1$ , then that reference is unique at that moment. A uniqueness attribute alone does not derive the fractional calculus’s multistep permission-sum invariant for new locations; heap compatibility and borrow safety are additional hypotheses.