Metatheoretic Preservation for Accepted Recursive and Corecursive Definition Packages

Theorem

Edit Issues Pull Requests Attributions Admin

Let $K_0$ be a typed proof-assistant kernel equipped with well-typed terms, a one-step reduction relation $\to_0$, definitional equality given by the conversion relation generated by $\to_0$, an inductive fragment, a coinductive fragment with finite observation contexts, and a closed empty proposition $\bot$. Assume that $K_0$ satisfies the following four metatheoretic invariants: 1. subject reduction for $\to_0$; 2. strong normalization for every well-typed term in the inductive fragment; 3. productivity for every closed well-typed coinductive term under every finite observation context; 4. consistency with respect to $\bot$, meaning that there is no closed term of type $\bot$. Let $D_1,\dots,D_n$ be a finite sequence of definition packages, and define kernels $K_i$ recursively by letting $K_i$ be the extension of $K_{i-1}$ by $D_i$ for $1 \le i \le n$. Assume that, for every $1 \le i \le n$, the package $D_i$ is well formed over $K_{i-1}$ and extends $K_{i-1}$ only by new named definitions and their accepted defining reduction rules. In particular, $D_i$ adds no axioms, no primitive constants without definitions, no independent typing rules, and no conversion or reduction rules except those generated by its accepted definitions. Assume also that every ordinary recursive definition in $D_i$ is accepted by the structural termination checker of $K_{i-1}$, and every corecursive definition in $D_i$ is accepted by the guarded productivity checker of $K_{i-1}$. Finally, assume the following soundness property of the extension discipline: for every kernel $K$ satisfying subject reduction, inductive strong normalization, coinductive productivity under finite observations, and consistency with respect to $\bot$, extension by any well-formed accepted definition package over $K$ again satisfies those four invariants, and definitional equality in the extension is exactly the conversion relation generated by the previous reductions together with the accepted defining reductions of that package. Then the sequential extension $K_n$ satisfies subject reduction, strong normalization for every well-typed term in its inductive fragment, productivity for every closed well-typed coinductive term under every finite observation context, and consistency with respect to $\bot$. Moreover, definitional equality in $K_n$ is exactly the conversion relation generated by the reductions of $K_0$ together with the accepted defining reductions introduced by $D_1,\dots,D_n$. Consequently, the sequence of packages introduces no reduction rule except an accepted defining reduction rule, and hence introduces no unchecked self-referential reduction rule.

Discussion

Proof

[proofplan] The proof is a finite induction over the sequence of accepted definition packages. At each stage we keep two pieces of data: the four metatheoretic invariants and the exact description of definitional equality as conversion generated by the accumulated accepted reductions. The base case is precisely the hypothesis on $K_0$, and the induction step is exactly the assumed soundness of the extension discipline applied to the next well-formed accepted package. [/proofplan] [step:Define the accumulated reduction data and the induction invariant] For each $1 \le i \le n$, let $\mathcal R_i$ denote the set of accepted defining reduction rules introduced by the package $D_i$. Let $\mathcal R_0$ denote the one-step reduction rules of $K_0$, equivalently the rules generating $\to_0$. For $0 \le m \le n$, define the accumulated reduction data \begin{align*} \mathcal A_m := \mathcal R_0 \cup \mathcal R_1 \cup \cdots \cup \mathcal R_m. \end{align*} For $m=0$, this means $\mathcal A_0=\mathcal R_0$. We prove by induction on $m$, for $0 \le m \le n$, the assertion $P(m)$ consisting of the following five clauses: 1. $K_m$ has subject reduction; 2. every well-typed term in the inductive fragment of $K_m$ is strongly normalizing; 3. every closed well-typed coinductive term of $K_m$ is productive under every finite observation context; 4. there is no closed term of type $\bot$ in $K_m$; 5. definitional equality in $K_m$ is exactly the conversion relation generated by $\mathcal A_m$. The first four clauses are the metatheoretic invariants, and the fifth clause records that definitional equality has acquired exactly the accepted defining reductions introduced so far. [/step] [step:Verify the base kernel satisfies the induction invariant] The hypotheses on $K_0$ state that $K_0$ has subject reduction, inductive strong normalization, coinductive productivity under every finite observation context, and no closed term of type $\bot$. These are exactly the first four clauses of $P(0)$. The statement also assumes that definitional equality in $K_0$ is the conversion relation generated by $\to_0$. Since $\mathcal A_0=\mathcal R_0$ and $\mathcal R_0$ is the reduction data generating $\to_0$, definitional equality in $K_0$ is exactly the conversion relation generated by $\mathcal A_0$. Hence the fifth clause of $P(0)$ also holds, so $P(0)$ is established. [/step] [step:Extend the invariant across one accepted package] Assume $0 \le m < n$ and assume $P(m)$. The package $D_{m+1}$ is well formed over $K_m$ by hypothesis. It adds only new named definitions and their accepted defining reduction rules, adds no axioms, no primitive constants without definitions, no independent typing rules, and no reduction or conversion rules except those generated by its accepted definitions. Its ordinary recursive definitions are accepted by the structural termination checker of $K_m$, and its corecursive definitions are accepted by the guarded productivity checker of $K_m$. By $P(m)$, the kernel $K_m$ has subject reduction, inductive strong normalization, coinductive productivity under finite observation contexts, and no closed term of type $\bot$. Therefore the assumed soundness property of the extension discipline applies to the extension of $K_m$ by $D_{m+1}$. It follows that $K_{m+1}$ has subject reduction, inductive strong normalization, coinductive productivity under finite observation contexts, and no closed term of type $\bot$. The same soundness property also states that definitional equality in $K_{m+1}$ is exactly the conversion relation generated by the previous reductions together with the accepted defining reductions of $D_{m+1}$. By the induction hypothesis, the previous definitional equality in $K_m$ is generated by $\mathcal A_m$. The accepted defining reductions of $D_{m+1}$ are precisely $\mathcal R_{m+1}$. Hence definitional equality in $K_{m+1}$ is exactly the conversion relation generated by \begin{align*} \mathcal A_m \cup \mathcal R_{m+1} = \mathcal A_{m+1}. \end{align*} Thus all five clauses of $P(m+1)$ hold. [guided] We now explain the induction step with all hypotheses visible. Suppose that $P(m)$ holds for some $m$ with $0 \le m < n$. This means that the current kernel $K_m$ already has the four metatheoretic invariants: subject reduction, strong normalization on its inductive fragment, productivity for closed coinductive terms under every finite observation context, and no closed inhabitant of $\bot$. It also means that definitional equality in $K_m$ is not mysterious: it is exactly conversion generated by the accumulated reduction data $\mathcal A_m$. The next package is $D_{m+1}$. The theorem assumes that $D_{m+1}$ is well formed over $K_m$. It also assumes a strict extension discipline: $D_{m+1}$ contributes only new named definitions and the defining reduction rules accepted for those definitions. In particular, it contributes no axiom, no primitive constant without a definition, no independent typing rule, and no separate conversion principle. This is the formal reason that the extension cannot smuggle in an unchecked proof of $\bot$ or an arbitrary self-referential computation rule. Now we use the main hypothesis of the theorem, namely soundness of the extension discipline. That soundness property applies to any kernel satisfying the four invariants and any well-formed accepted definition package over that kernel. The kernel $K_m$ satisfies the four invariants by $P(m)$, and the package $D_{m+1}$ is well formed and accepted by the hypotheses just recalled. Therefore the extension $K_{m+1}$ again has subject reduction, inductive strong normalization, coinductive productivity under finite observation contexts, and no closed term of type $\bot$. It remains to track definitional equality. Let $\mathcal R_{m+1}$ be the set of accepted defining reduction rules introduced by $D_{m+1}$. The soundness property says that definitional equality after extension is generated by the previous reductions together with these new accepted defining reductions. The previous reductions generate exactly $\mathcal A_m$ by the induction hypothesis, and adding the reductions of $D_{m+1}$ gives \begin{align*} \mathcal A_m \cup \mathcal R_{m+1}. \end{align*} By the definition of accumulated reduction data, \begin{align*} \mathcal A_m \cup \mathcal R_{m+1} = \mathcal A_{m+1}. \end{align*} Thus definitional equality in $K_{m+1}$ is exactly conversion generated by $\mathcal A_{m+1}$. This proves every clause of $P(m+1)$. [/guided] [/step] [step:Apply finite induction to reach the final kernel] The base case proves $P(0)$, and the induction step proves $P(m)\implies P(m+1)$ for every $m$ with $0 \le m < n$. By finite induction, $P(n)$ holds. Unpacking the first four clauses of $P(n)$, the kernel $K_n$ has subject reduction, every well-typed term in its inductive fragment is strongly normalizing, every closed well-typed coinductive term is productive under every finite observation context, and there is no closed term of type $\bot$. [/step] [step:Identify the final definitional equality and exclude unchecked reduction rules] The fifth clause of $P(n)$ states that definitional equality in $K_n$ is exactly the conversion relation generated by \begin{align*} \mathcal A_n = \mathcal R_0 \cup \mathcal R_1 \cup \cdots \cup \mathcal R_n. \end{align*} Here $\mathcal R_0$ is the original reduction data of $K_0$, and each $\mathcal R_i$ for $1 \le i \le n$ is precisely the set of accepted defining reduction rules introduced by $D_i$. Therefore definitional equality in $K_n$ is exactly the conversion relation generated by the reductions of $K_0$ together with the accepted defining reductions introduced by $D_1,\dots,D_n$. Since each extension contributes no reduction or conversion rules except those generated by its accepted definitions, the accumulated reduction data contains no additional rule beyond $\mathcal R_0$ and the accepted defining reductions $\mathcal R_1,\dots,\mathcal R_n$. In particular, the sequence introduces no unchecked self-referential reduction rule. This proves the theorem. [/step]

What brings you to Androma?

Start with a route through the knowledge graph.