appendix sectionsolutions

ch:dependent-control: ch:dependent-control

The left rule is $\frac{\begin{matrix} Γ ⊢ q : A ∣ Δ \\ Γ ∣ e : B [q / a] ⊢ Δ \end{matrix}}{Γ ∣ q \cdot e : Π a : A . B ⊢ Δ} Π - L .$ Cutting $f$ against the resulting context forms $⟨ f ∥ q \cdot e ⟩ : (Γ ⊢ Δ)$ . When $f = λ a . p$ , its principal cut decomposes into the two cut commands $⟨ q ∥ \tilde{μ} a . ⟨ p ∥ e ⟩ ⟩ : (Γ ⊢ Δ) .$ The inner cut places the function body against $e$ ; the outer cut supplies its argument. The first call-by-value root $⟨ V ∥ \tilde{μ} a . c ⟩ ⟶ c [V / a]$ requires the argument premise $q = V$ , a proof value (and, for dependency, an admissible NEF proof).

Exercise 109.2.

The variable $a$ , lambda $λ a . a$ , and positive pair $(0, refl)$ are NEF by the variable, lambda, and pair/value clauses. They may respectively be substituted in $X (a)$ , $X (λ a . a)$ , and $wit ((0, refl)) = 0$ , provided the surrounding families have the displayed domains. The fourth accepted proof is $q_{⋆} : = μ ⋆ . ⟨ a ∥ ⋆ ⟩ .$ Its command is a NEF command using the one admitted continuation, so the $μ ⋆ . c_{N}$ clause accepts it. If $a : A$ and $X : A \to U$ , it may occur in the formula $X (q_{⋆})$ .

The proof $μ α . c$ is not NEF. It would require an unrestricted $μ α . c$ production, distinct from the displayed $μ ⋆ . c_{N}$ production. Replacing $α$ textually by $⋆$ does not make the result NEF unless $c$ is also generated by $c_{N}$ , so that every context in it is either $⋆$ or $\tilde{μ} a . c_{N}$ . Without that command restriction, a throw can still resume an external context after a dependent formula has fixed its proof occurrence.

Exercise 109.3.

For $P = Π a : A . B (a)$ , $\begin{aligned} [[P {]]}^{+} & = Π a : [[A {]]}^{+} . [[B (a) {]]}^{*}, \\ [[P {]]}^{*} & = ((Π a : [[A {]]}^{+} . [[B (a) {]]}^{*}) \to ⊥) \to ⊥ . \end{aligned}$ The continuation captured by ${dne}_{P}$ therefore has target type $[[P {]]}^{+} \to ⊥$ . To place the resulting proof in a family $X (-)$ , fix a source proof $r : P$ . Then lemma 109.10 would require its continuation-passing translation to have type $Π X : ([[P {]]}^{+} \to U) . (Π u : [[P {]]}^{+} . X (u)) \to X (r^{+}) .$ The proof produced by ${dne}_{P}$ binds an unrestricted continuation by $μ$ , so the premise that $r$ be NEF is unavailable and the positive term $r^{+}$ required in the conclusion is not defined. That missing premise, rather than ordinary CPS typing at $[[P {]]}^{*}$ , is the precise obstruction.

Exercise 109.4.

At the capture site, $p_{0}$ is assigned $\exists x : N . x = 1$ . The witness projection follows the ordinary return and records $0$ , so the surrounding dependent cut expects $prf (p_{0}) : 0 = 1$ . Forcing the proof invokes the captured continuation with $(1, refl)$ . The proof projection of that pair is $refl : 1 = 1$ . The reduction has therefore changed the term named in the cut formula from the previously observed $0$ to the thrown witness $1$ , without rebuilding the surrounding formula. The exact failed preservation premise is the attempted typing of $refl$ at $0 = 1$ .

Exercise 109.5.

Values form a proper subclass of NEF proofs. A positive projection such as $prf ((0, refl))$ is NEF but is not a value. Normal proofs and NEF proofs are otherwise incomparable in the displayed control language. A normal suspended $μ$ -proof has no redex until it is cut against a context, but is not NEF; an exact witness is $μ α . ⟨ a ∥ α ⟩$ . Conversely the displayed positive projection is NEF and is not normal, because for every context $e$ its enclosing command takes the step $⟨ prf (0, refl) ∥ e ⟩ \overset{P r f - P a i r}{⟶} ⟨ refl ∥ e ⟩ .$ Thus $Value ⊊ NEF$ , while NEF and normal proofs are incomparable. Proof values are closed under reduction because none of their grammar productions is a reduction head. NEF proofs are closed under the displayed reduction rules by the NEF cases used in theorem 109.6; in particular no rule introduces an unrestricted continuation. Normal proofs are closed vacuously: by definition no reduction starts from one. These closure facts do not turn either values or normal proofs into a substitute for NEF.

Exercise 109.6.

The product clause sends a positive argument $a : [[A {]]}^{+}$ to the computation type $[[B (a) {]]}^{*}$ ; the proof occurrence therefore remains visible in the target family. The NEF translation supplies exactly the family-indexed term needed to substitute that $a$ in $[[B (a) {]]}^{*}$ . During dependent-pair elimination, $\hat{tp}$ consumes the answer family after the first-order witness has been fixed, and only then passes the NEF proof to the ordinary continuation. If delimitation is removed while NEF is retained, the CPS clause for dependent elimination would have to give one ordinary continuation both the pre-projection family and the post-witness family. Those answer types differ by witness substitution, so the translated continuation application cannot be typed. The missing target judgment is the continuation at the fixed family $X ([[t {]]}^{+})$ , formerly supplied by the delimiter.

Exercise 109.7.

Operational equality accepts the control root $⟨ μ α . c ∥ e ⟩ ⟶ c [e / α]$ ; neither extensional dependent type theory nor proof irrelevance even has that control command in its signature. Equality reflection in extensional type theory accepts $m \equiv n : A$ from a proof $p : m =_{A} n$ ; control reduction alone does not turn an arbitrary identity proof into a reduction, and proof irrelevance does not identify the data $m, n$ . Proof irrelevance accepts $p \equiv q : P$ for arbitrary proofs $p, q$ of one proposition $P$ ; intensional operational conversion need not reduce the two proofs to the same term, and extensional equality reflection without a proof-irrelevance axiom does not identify them. Each equation therefore uses a rule specific to its named regime.