appendix sectionsolutions

ch:optimal-sharing: ch:optimal-sharing

Before closure, each occurrence of $x, y, z$ has a width-three named bus. The application in $x x$ combines its two $x$ -buses with the lower fan of the application diagram. The outer abstraction feeds that combined bus back through its abstraction fan. In $λ x . λ w . x$ , the inner binder $w$ is absent and its dead branch ends at a void; the free $x$ -bus crossing that scope receives a bracket. The designation of which component is left, middle, and right—and hence which component carries calls, offsets, and commands—depends on the source’s bus convention.

exercise 42.2.

The premise $G (M) ⟶_{GAL}^{*} G_{1}$ establishes reachability by convention 42.3, definition 42.4. Clause 3 of theorem 42.6 supplies uniqueness of the caught label at distinct rightmost-fan redexes. Clause 2 supplies $R (G_{1}) ⟶_{β}^{*} R (G_{2})$ ; the displayed two $⟶_{β}$ arrows exhibit that closure. A closure of rightmost-fan steps would omit bracket, croissant, and other fan interactions. Absence of a rightmost-fan redex would then not be GAL graph normality, so the beta-normal readback conclusion would not follow.

exercise 42.3.

The values are $K_{0} (3) = 3, K_{1} (3) = 2^{3} = 8, K_{2} (3) = 2^{8} = 256.$ The main theorem relates a linear parallel-family count to first-class-machine time; Corollary 5.4 relates that count to a nonelementary number of local Lamping interactions; Corollary 5.6 relates parallel-family and ordinary-beta counts. None supplies elapsed time for a named build. Moving a local-step count into that column requires, at minimum, a verified implementation-cost model and a fixed machine; an empirical claim additionally requires a pinned build and measurement protocol.

exercise 42.4.

With $R_{a} = (λ y . y) z$ , the certificate is $⟨ (u_{a}, v_{a}), a, R_{a} R_{a} ⟶_{β} z R_{a} ⟶_{β} z z ⟩ .$ The endpoints are the facing rightmost-fan ports of the worked GAL step, the middle field is its caught label, and the final field is a nonempty verified ordinary-beta path. Its closure is $R_{a} R_{a} ⟶_{β}^{*} z z$ .

exercise 42.5.

The two hypotheses for GAL Theorem 3 are $G (P) ⟶_{GAL}^{*} G$ and $G ⟶_{GAL}^{*} G^{'}$ . Both use the full six-scheme relation. The conclusion is $R (G) ⟶_{β}^{*} R (G^{'})$ . Graph normality of a reachable $G$ gives beta-normality of its readback. The source supplies only the access-path sketch following Theorem 3, which relies on readback invariance under non-rightmost reductions. GAL then qualifies the result: normal order avoids entering subterms later found useless.

exercise 42.6.

Choose endpoint identifiers $1, 2$ with opposite rightmost tags, a fresh label $7$ , and the valid path $(λ x . x) y ⟶_{β} y$ . Store the two identifiers in two unrelated graph records. The syntactic checker accepts every field, but there is no single reachable $G$ in which they are facing fan ports. The missing premise is the GAL reachability/incidence hypothesis, so theorem 42.6 cannot be instantiated and acceptance is not an optimality proof.

exercise 42.7.

Ten is a semantic family count, ten thousand is a local graph-interaction count, and eight milliseconds is a wall-clock observation. A simulation relates families to graph steps; a representation-specific cost model relates graph steps to machine work; a fixed build, machine, scheduler, and protocol relate that work to elapsed time. Without those relations, no one of the three numbers determines either other number.