Classical Dependent Type Theory and Control

Proof. The two displayed rules type the opening term as $$⊢p_0:\mathrm{\exists }x:\mathbb{N}.x=1.$$ The new commuting rule, the ordinary pair projection, and the second new rule give the annotated reduction The side condition of Callcc-Term holds because $k\notin \mathsf{FV}(0)$. Reflexivity followed by conversion along this reduction therefore derives $$⊢\mathrm{refl}:\mathrm{wit}(p_0)=0.$$ The ordinary proof projection independently gives $$⊢\mathrm{prf}(p_0):\mathrm{wit}(p_0)=1.$$ Taking $B[x]:=x=0$, equality elimination applies the equation $\mathrm{prf}(p_0)$ to the payload $\mathrm{refl}$ and derives $$⊢\mathrm{subst}(\mathrm{prf}(p_0))\mathrm{refl}:1=0.$$ The calculation uses only the displayed witness/proof equations; no command or reduction of the later $\mu /\tilde{\mu }$ calculus is asserted here. ◻

Proof. Induct simultaneously on the dependent derivation and on the list of open dependencies. A variable or value rule does not mention $\star$ and rebuilds unchanged. In a regular cut, apply the induction hypotheses to its proof and context premises and rebuild Cut-$d$. A $\tilde{\mu }$ binder alpha-renames its bound proof variable outside $\mathrm{FV}(e)$ before applying the induction hypothesis. The $\mu \star$ case removes the bound occurrence of $\star$; every other continuation binder commutes with the substitution.

The only case that changes the dependency list is a nested cut. A binding $\{a\mid \mu \star .c_0\}$ is replaced by the two bindings exposed by $c_0$. The premise assigning a formula to the old binding says that its proof lies in the old compatibility class. The NEF congruence equations identify that formula with the formula of the two exposed bindings after $[e/\star ]$. Conversion-left therefore rebuilds the premise for $\widehat{\mathsf{tp}}$. The delimiter cases either substitute through the inner command by the induction hypothesis or discharge the distinguished continuation by $\widehat{\mathsf{tp}}$-Return. These are the regular, binder, dependency-extension, and delimiter rule families, so the simultaneous induction proves the displayed judgment. ◻

Proof. Induct on the reduction rule. For $⟨\mu \alpha .c_0\parallel e⟩⟶c_0[e/\alpha ]$, inversion gives a derivation of $c_0$ under $\alpha :A$ and a context derivation for $e:A$; context substitution reconstructs the conclusion. The dual $\tilde{\mu }$ root uses proof substitution. Product beta substitutes its value and proof components separately; existential and equality roots use term substitution followed by proof substitution. Each substitution is capture avoiding because the corresponding binder was chosen outside the free variables of the substituted object.

For dependent application, inversion gives an NEF proof together with the open formula family that contains it. The reduct inserts the delimiter and is typed successively by $\mu \widehat{\mathsf{tp}}$, Cut-$d$, $\tilde{\mu }$-$d$, and $\widehat{\mathsf{tp}}$; the dependency entry records the same NEF proof, so compatibility membership preserves the formula assigned to the entry. If the NEF proof is $\mu \star .c_0$, apply lemma 109.5 to type $c_0[e/\star ]$.

Rule $\widehat{\mathsf{tp}}$-Return removes a delimiter whose inner command has already produced a proof; inversion of the delimiter typing gives exactly the outer context premise. Rule $\widehat{\mathsf{tp}}$-Cong applies the induction hypothesis to the inner command and rebuilds the delimiter. Congruence for the remaining contexts applies the induction hypothesis to the selected subcommand and rebuilds its typing rule. The ordinary control, product, existential, equality, dependent-application, delimiter, and congruence cases exhaust the displayed reduction relation, proving preservation. ◻

Proof. Use mutual induction on the term, NEF-proof, NEF-command, and NEF-context grammars, with the positive translation of definition 109.8 supplying the witnesses. A variable, numeral, proof variable, or reflexivity proof beta-reduces immediately to the continuation applied to its positive translation. A lambda uses the induction hypothesis for its body under the extended target context. The pair case shows the nontrivial sequencing mechanism: For $\mathrm{prf}{p}_N$, first apply the proof induction hypothesis to the inner continuation and then beta-reduce the two continuation lambdas; the result is $k(\mathrm{prf}{p}_N^{+})$. Witness extraction and equality substitution use the term and proof induction hypotheses, respectively, and then their positive eliminator equations. In a command $⟨p_N\parallel e_N⟩$, the proof and context hypotheses meet at the same positive value. A context $\tilde{\mu }a.c_N$ uses the command hypothesis after substituting that value for $a$. Finally, $\mu \star .c_N$ uses the command induction hypothesis with the supplied continuation substituted for $\star$; because $e_N$ is generated only by $\star$ and $\tilde{\mu }a.c_N$, that continuation is used exactly at the unique terminal command. These cases exhaust the four mutually defined grammars.

The reason the statement is restricted to NEF proofs is visible in the $\mu \alpha$ clause: $[[\mu \alpha .c{]]}_{p}k=[[c{]]}_c[k/\alpha ]$ substitutes $k$ for a variable the command may use zero times or many times, so no single $p^{+}$ answers every continuation. The restriction is not to control-free proofs: $\mu \star .c_N$ is NEF and does have a positive translation, namely $c_N^{+}$, because its command may use only $\star$ and $\tilde{\mu }a.c_N$ and therefore uses its continuation exactly once. ◻

Proof. Note first what the statement is not: assigning that type to $p^{+}$ itself would be vacuous, since $p^{+}$ already has type $[[A{]]}^{+}$ and the type would then follow by applying the supplied function at $p^{+}$. The content is that the continuation-passing translation, whose ordinary type is the constant double negation $([[A{]]}^{+}\to \mathrm{\perp })\to \mathrm{\perp }$, can be refined to a parametric answer type $X$ once $p$ is NEF. lemma 109.9 is exactly what licenses the refinement: $[[p{]]}_p$ uses its continuation once, so the answer may depend on the value $p^{+}$ that it passes.

The induction is simultaneous on the NEF proof, command, and context grammars. A variable applies the supplied dependent function at that variable. A lambda rebuilds a positive product value and applies the proof induction hypothesis to its body in the extended context. A pair translates its term witness first and invokes the induction hypothesis on its NEF component; lemma 109.9 identifies the resulting answer as $X((t,p{)}^{+})$. The $\mathrm{prf}$ and $\mathrm{subst}$ cases use their positive eliminators, whose motives are obtained by substituting the positive translations into $X$. A command applies the translated context to the translated proof. The $\tilde{\mu }$ context abstracts over the positive proof value and uses the command induction hypothesis. Finally, $\mu \star .c_N$ substitutes the answer-family continuation for $\star$ and uses the command hypothesis. There is no $\mu \alpha$ case, and there could not be one: it would require manufacturing $X(p^{+})$ after an arbitrary outside continuation has already changed the result, which is the impossible step isolated by proposition 109.2. ◻

Proof. Prove the three claims simultaneously by induction on the typing derivation, strengthened to dependent contexts and their compatibility lists. A proof variable is translated at its declared positive type and then double-negated by the surrounding continuation. A context variable is the corresponding target continuation. Rule Cut becomes application of the translated context to the translated proof, producing $\mathrm{\perp }$.

For $\mu \alpha .c$, the command induction hypothesis has type $\mathrm{\perp }$ under $\alpha :[[A{]]}^{+}\to \mathrm{\perp }$; abstraction over $\alpha$ gives $[[A{]]}^{\ast }$. The dual $\tilde{\mu }$ rule abstracts over a positive proof value. Product introduction uses the proof induction hypothesis under the translated domain. Dependent product elimination uses lemma 109.10 with result family equal to the translated codomain; the occurrence of the proof argument remains visible in that family. Existential pairing translates the first-order witness and then its proof component. Witness extraction, proof extraction, reflexivity, and equality substitution commute with their positive translations and use the corresponding induction hypotheses.

In the dependent mode, $\star$ is assigned the answer-family continuation and $\widehat{\mathsf{tp}}$ receives the translated formula at the positive proof stored in the compatibility list. Rule $\mu \widehat{\mathsf{tp}}$ abstracts over that continuation; $\widehat{\mathsf{tp}}$ applies it. Weakening, exchange, conversion, and alpha-renaming follow componentwise from the simultaneous context induction. These are the variable, cut, control-binder, dependent-product, existential, equality, delimiter, and structural families, and they exhaust the displayed typing rules. ◻

Proof. The target is the intuitionistic dependent fragment of the top system in the lambda cube, with naturals, equality, and existentials translated by their strictly positive encodings. Strong normalization for the top vertex of the lambda cube says that every well-typed target term admits no infinite beta reduction; the added positive constructors have structurally decreasing eliminators, so the same reducibility interpretation extends with their canonical-value clauses.

We next prove a directed simulation. Induct on a source reduction step and expand the clauses of definition 109.8. A regular $\mu$ or $\tilde{\mu }$ root becomes beta substitution. Product, existential, equality, and dependent-application roots become one or more target beta steps followed by the positive eliminator equation. Delimiter congruence uses the induction hypothesis under the translated answer-family context. Thus every principal source step contributes a nonempty target reduction sequence.

Four administrative roots can translate to equality: the two $\mathrm{subst}$ rules, delimiter return, and congruence for reduction inside a first-order witness. Assign a command the lexicographic measure $$(n_{\mathsf{nonvalue}\text{-}\mathsf{subst}},n_{\mathsf{subst}},n_{\widehat{\mathsf{tp}}},n_{\mathsf{wit}}),$$ where the four components count, respectively, substitutions whose proof argument is not a value, all substitution forms, occurrences of the distinguished continuation, and witness eliminators. The first administrative rule decreases the first count while preserving the other three. The second preserves the first and decreases the second. Delimiter return preserves the first two and decreases the third. Witness congruence preserves the first three and decreases the fourth. Thus every administrative step strictly decreases this lexicographic tuple, so no infinite sequence can consist only of administrative roots.

Suppose a typed source command had an infinite reduction. If it contained infinitely many principal steps, directed simulation would give an infinite reduction of its target translation. If it contained only finitely many, its tail would be an infinite descending chain of the administrative measure. Both alternatives are impossible. Hence every typed command normalizes.

If a closed proof $p:\mathrm{\perp }$ existed, CPS preservation would give a closed target term $[[p]]:(\mathrm{\perp }\to \mathrm{\perp })\to \mathrm{\perp }$. Apply it to the target identity $\lambda x:\mathrm{\perp }.x$; normalization would produce a canonical inhabitant of $\mathrm{\perp }$, but the target has no constructor for $\mathrm{\perp }$. Therefore no closed source proof of $\mathrm{\perp }$ exists. ◻

Proof. For the first claim, name the demanding context $\alpha :P$, assume $h:(P\to \mathrm{\perp })\to \mathrm{\perp }$, and define $$q_{\alpha }:=\lambda a.\mu \beta .⟨a\parallel \alpha ⟩:P\to \mathrm{\perp },{\mathrm{dne}}_{P}h:=\mu \alpha .⟨h\parallel q_{\alpha }\cdot {\mathrm{abort}}_{\alpha }⟩.$$ To check $q_{\alpha }$, assume $a:P$ and extend the continuation context by $\beta :\mathrm{\perp }$. The cut $⟨a\parallel \alpha ⟩$ is typed under $\alpha :P,\beta :\mathrm{\perp }$ by weakening; $\mu$-R at $\beta$ therefore gives $\mu \beta .⟨a\parallel \alpha ⟩:\mathrm{\perp }$, and $\mathrm{\Pi }$-R gives $q_{\alpha }:P\to \mathrm{\perp }$. Rule $\mathrm{\perp }$-L types ${\mathrm{abort}}_{\alpha }$ as a context consuming $\mathrm{\perp }$ while retaining $\alpha :P$. Hence $\mathrm{\Pi }$-L types $q_{\alpha }\cdot {\mathrm{abort}}_{\alpha }$ as a context consuming $(P\to \mathrm{\perp })\to \mathrm{\perp }$. Cutting $h$ against it produces a command under $\alpha :P$, and the outer $\mu$-R closes exactly that continuation. The previously tempting tail $q_{\alpha }\cdot \alpha$ is ill typed: $\alpha$ consumes $P$, whereas the result of $h$ is $\mathrm{\perp }$.

For the second claim, unrestricted extraction would admit $p_0$ in the formula $\mathrm{wit}(p_0)=1$. Then the reductions in proposition 109.2 reconstruct a proof of $1=0$. Definition 109.3 rejects $p_0$, so the exact calculus proves the first claim while blocking the second. ◻