ch:trusted-kernels: ch:trusted-kernels

The four rules are the direct $\mathrm{\Sigma }$-counterparts of the annotated $\mathrm{\Pi }$-rules:

The final equality premise in each term rule compares the supplied expected type $C$ with the type computed from the annotations and elaborated subterms. No such premise belongs in Pre-Sg, whose output is itself a type.

Determinism is syntactic at the outermost constructor. The heads $\mathsf{Sg}$, $\mathsf{pair}$, $\mathsf{fst}$, and $\mathsf{snd}$ are pairwise distinct and each appears in the conclusion of exactly one rule. Once that rule is selected, all recursive inputs and the result-equality query are fixed; therefore no second rule can elaborate the same constructor in the same mode.

Choose de Bruijn indices for bound variables and a Gödel coding of finite lists and finite rooted ordered trees. Because the signature is recursive, we can effectively code every operator and rule name and decide whether a number is such a code. Decode a natural number $n$ as a candidate tree whose nodes carry:

1. a rule name and one of the five judgment forms;

2. codes for its context and constituent raw expressions; and

3. an ordered list of immediate subtrees.

Let $\mathsf{Der}(n)$ hold precisely when a bottom-up check accepts this tree. At a node the checker verifies the rule’s arity, matches the conclusion and premises against the corresponding recursive rule schema, and checks all side conditions. Raw substitution, lifting of de Bruijn indices, equality of alpha-classes, list membership, and freshness are recursive operations, so $\mathsf{Der}$ is a decidable predicate. The accepted numbers, in numerical order, are an effective enumeration of all derivations, possibly with harmless duplicate derivations.

Suppose total decision procedures $\mathsf{decTyEq}$ and $\mathsf{decTmEq}$ are given. On a derivation $d$ of $\mathrm{\Gamma }⊢A\mathsf{type}$, define the decidable predicate $$P_{\mathrm{\Gamma },A}(n)⟺\{\begin{array}{l}\mathsf{Der}(n),\\ \mathrm{root}(n)=\mathrm{\Gamma }⊢A_n\mathsf{type},\\ \mathsf{decTyEq}(A,A_n)=\mathsf{yes}.\end{array}$$ The equality decider receives the input formation derivation $d$ and the formation derivation decoded from $n$. Put $$\mathrm{nfTy}(d):=\mu n.P_{\mathrm{\Gamma },A}(n).$$ Unbounded minimization of a recursive predicate is partial recursive. It is total on the stated domain because the code of $d$ itself satisfies the predicate, by reflexivity.

For terms, let $d$ derive $\mathrm{\Gamma }⊢a:A$. Define $Q_{\mathrm{\Gamma },a,A}(n)$ to say that $n$ is a derivation of some $\mathrm{\Gamma }⊢b_n:B_n$, that the type decider accepts $A\equiv B_n$, and that, after converting the decoded derivation of $b_n:B_n$ to $b_n:A$, the term decider accepts $a\equiv b_n:A$. A positive answer from the type decider can be turned effectively into an equality derivation: dovetail the recursive enumeration until a derivation of $A\equiv B_n$ appears. This secondary search terminates exactly in the positive branch, after which the conversion tree is computably assembled. Thus $Q$ is decidable, and $$\mathrm{nfTm}(d):=\mu n.Q_{\mathrm{\Gamma },a,A}(n)$$ is partial recursive and total on typing derivations, since the code of $d$ itself is a witness.

It remains to verify the classifying properties. If $A\equiv A^{\prime }$, then by symmetry and transitivity a candidate $A_n$ is equal to $A$ exactly when it is equal to $A^{\prime }$. Hence $P_{\mathrm{\Gamma },A}$ and $P_{\mathrm{\Gamma },A^{\prime }}$ have the same accepted indices and their least indices coincide. Conversely, a common accepted least index provides $A\equiv A_n\equiv A^{\prime }$, so $A\equiv A^{\prime }$. The term argument is identical after the classifier conversions: candidates for two judgmentally equal terms form the same set, and a common candidate gives the desired equality by symmetry and transitivity.

Finally suppose the same raw term has converted typings $$\mathrm{\Gamma }⊢a:A,\mathrm{\Gamma }⊢a:A^{\prime },\mathrm{\Gamma }⊢A\equiv A^{\prime }\mathsf{type}.$$ If $b_n:B_n$ is admissible for the first search, then $A^{\prime }\equiv A\equiv B_n$, and conversion of the term equality $a\equiv b_n:A$ gives $a\equiv b_n:A^{\prime }$. Thus it is admissible for the second search; the converse is symmetric. The candidate sets, and hence the least term index, are independent of which converted classifier was supplied. This completes every computability and totality obligation suppressed in the proposition.

Despite the exercise label, the requested extension is by coproducts. Add the type and universe-code rules

The universe-code rule is separate:

The two introduction forms check against an expected coproduct:

Soundness of $\mathrm{unSum}$ includes a derivation $C\equiv A+B$; it is the implicit conversion that validates the returned constructor at the original expected type. Universal coherence says that these $A,B$ agree with the components of every other coproduct presentation of $C$.

Retain an explicit motive in the surface eliminator and write it as ${\mathsf{ind}}_{+}(z.\tau ;e_{\ell },e_r;e)$. Its synthesis rule is

For termination, the head constructor chooses one rule. Every recursive query is on a proper subexpression: the summands, injected term, scrutinee, motive, or one of the two branches. Calls to $\mathrm{unSum}$ and $\mathrm{unUniv}$ are total by hypothesis, and all substitutions only construct expected types. Hence the same lexicographic (mode, expression-size) argument as for the original rules terminates.

For soundness of Syn-SumInd, the induction hypotheses give Soundness of $\mathrm{unSum}$ gives $D\equiv A+B$, so conversion yields $s:A+B$. The primitive coproduct eliminator then derives $$\mathrm{\Gamma }⊢{\mathsf{ind}}_{+}(f,g,s):C[s/z],$$ which is exactly the synthesized output judgment. No unstated inversion of $D$ is used; all such information is supplied by the coherent $\mathrm{unSum}$ call.

Put $\mathrm{\Gamma }:=\cdot$, $A:=\mathbb{N}$, $a:=\mathsf{0}$, $\tau :=\mathbb{N}$, and $e:=\mathsf{0}$. Then $\mathrm{\Gamma }⊢\tau \Leftarrow \mathsf{type}⇝A$ and $\mathrm{\Gamma }⊢e\Leftarrow A⇝a$ are the two base rules. Use the annotated eliminand $$q:=(\mathsf{refl}(e):{\mathsf{Id}}_{\tau }(e,e)).$$ Rule Syn-Ann first checks ${\mathsf{Id}}_{\tau }(e,e)$ as a type. Its three queries are $$\mathrm{\Gamma }⊢\tau \Leftarrow \mathsf{type}⇝A,\mathrm{\Gamma }⊢e\Leftarrow A⇝a,\mathrm{\Gamma }⊢e\Leftarrow A⇝a,$$ followed by Ty-Id. It then checks $\mathsf{refl}(e)$ at the resulting core type. Here $\mathrm{unId}$ returns $(A,a,a)$; the single recursive query checks $e$ against $A$ and returns $a$, and the two conversion tests $a\iff a:A$ are reflexive. Thus $$\mathrm{\Gamma }⊢q\Rightarrow {\mathsf{Id}}_A(a,a)⇝{\mathsf{refl}}_a.$$

Put $\mathrm{\Delta }:=\mathrm{\Gamma },x:A,y:A,p:{\mathsf{Id}}_A(x,y)$. Rule Ty-$\mathbb{N}$ elaborates $\tau$ to $A$ in every displayed context, so Ty-Id checks the surface motive ${\mathsf{Id}}_{\tau }(x,y)$ by $$\mathrm{\Delta }⊢\tau \Leftarrow \mathsf{type}⇝A,\mathrm{\Delta }⊢x\Leftarrow A⇝x,\mathrm{\Delta }⊢y\Leftarrow A⇝y.$$ It returns $C(x,y,p):={\mathsf{Id}}_A(x,y)$. After substituting $x=z$, $y=z$, and $p={\mathsf{refl}}_z$, the required branch type is ${\mathsf{Id}}_A(z,z)$. A second use of Chk-Refl gives $$\mathrm{\Gamma },z:A⊢\mathsf{refl}(z)\Leftarrow {\mathsf{Id}}_A(z,z)⇝{\mathsf{refl}}_z.$$ Its queries are $$\mathrm{unId}(\mathrm{\Gamma },z:A,{\mathsf{Id}}_A(z,z))=(A,z,z),\mathrm{\Gamma },z:A⊢z\Leftarrow A⇝z,$$ followed by the two reflexive conversion tests $z\iff z:A$. Thus the branch call has no suppressed algorithmic premise. All premises of Syn-$J$ are now present. With ${\tau }_C(x,y,p):={\mathsf{Id}}_{\tau }(x,y)$ and $c(z):={\mathsf{refl}}_z$, its output is $$\mathrm{\Gamma }⊢\mathsf{J}(x.y.p.{\tau }_C;z.\mathsf{refl}(z);q)\Rightarrow {\mathsf{Id}}_A(a,a)⇝{\mathsf{J}}_{A;a;a}(x.y.p.C;z.c;{\mathsf{refl}}_a).$$ The annotation is essential: reflexivity is an introduction and therefore does not synthesize by itself.

Fix $a:A$ and define $${\mathsf{Sing}}_A(a):=\sum _{x:A}{\mathsf{Eq}}_A(x,a).$$ Its canonical introduction and underlying-value projection are $${\mathsf{sing}}_a:=(a,{\mathsf{refl}}_a):{\mathsf{Sing}}_A(a),\mathsf{out}(u):={\mathsf{pr}}_1(u):A.$$ For arbitrary $u:{\mathsf{Sing}}_A(a)$, the second projection has type $${\mathsf{pr}}_2(u):{\mathsf{Eq}}_A(\mathsf{out}(u),a).$$ One use of Eq-Reflect therefore gives the defining judgmental equality $$\mathsf{out}(u)\equiv a:A.$$

For eta, $\mathrm{\Sigma }$-eta first gives $$u\equiv ({\mathsf{pr}}_1(u),{\mathsf{pr}}_2(u)).$$ The defining equality compares the first components ${\mathsf{pr}}_1(u)\equiv a$. Rule Eq-Uniq gives $${\mathsf{pr}}_2(u)\equiv \mathsf{refl}:{\mathsf{Eq}}_A({\mathsf{pr}}_1(u),a),$$ where the reflexivity classifier is converted along the equality of first components. Dependent pair congruence now yields $$({\mathsf{pr}}_1(u),{\mathsf{pr}}_2(u))\equiv (a,{\mathsf{refl}}_a).$$ Composing with $\mathrm{\Sigma }$-eta proves $$u\equiv {\mathsf{sing}}_a:{\mathsf{Sing}}_A(a).$$ Thus the encoding has the expected point, projection equation, and judgmental singleton eta law.

After the first two declarations, let $a:=\mathsf{suc}(\mathsf{suc}(\mathsf{0}))$. The defined context contains $$D(c)=(\mathbb{N},a),D(p)=({\mathsf{Id}}_{\mathbb{N}}(a,a),{\mathsf{refl}}_a).$$ In the third declared type, both occurrences of $c$ elaborate by Syn-Var-Def to $a$, so the type elaborates to ${\mathsf{Id}}_{\mathbb{N}}(a,a)$. Its body $\mathsf{refl}(c)$ checks at this type: the endpoint elaborates to $a$, and Chk-Refl returns ${\mathsf{refl}}_a$. Hence the updated map stores $$D(q)=({\mathsf{Id}}_{\mathbb{N}}(a,a),{\mathsf{refl}}_a).$$ If a recursive query is made under a fresh local declaration $y:B$, the entry for $c$ does not become a variable. It returns the weakening $a^{\uparrow y}:\mathbb{N}$ in the enlarged context; similarly the entries for $p$ and $q$ return the weakened term ${\mathsf{refl}}_{a^{\uparrow y}}$.

The hypotheses $e_K$ and $e_S$ are needed only for the two generating steps. Applying them to encoded arguments produces terms of the appropriate extensional equality types, and Eq-Reflect turns those terms into the judgmental equations encoding SK-K and SK-S.

Everything used to close those equations is already built into judgmental equality. If the induction derivation of $t\sim u$ ends in reflexivity, use term-equality reflexivity on $⌜t⌝:X$. If it ends in symmetry or transitivity, apply the corresponding structural rule to the induction hypothesis or hypotheses. In the application case, the two induction hypotheses are combined by congruence of the context variable $app:X\to X\to X$, yielding $$⌜tv⌝=app⌜t⌝⌜v⌝\equiv app⌜u⌝⌜w⌝=⌜uw⌝:X.$$ Thus reflexive, symmetric, transitive, and congruence closure are rules of the ambient judgmental equality, not additional assumptions in ${\mathrm{\Gamma }}_{\mathsf{SK}}$. The context need hypothesize only the two nonstructural generating equations.

Write $r_t:={\mathsf{eqrefl}}_{⌜t⌝}$. If $⌜t⌝\equiv ⌜u⌝:X$, then Eq congruence gives $${\mathsf{Eq}}_X(⌜t⌝,⌜t⌝)\equiv {\mathsf{Eq}}_X(⌜t⌝,⌜u⌝)\mathsf{type}.$$ The conversion direction is the tree $$\frac{\begin{array}{c}{\displaystyle \frac{{\mathrm{\Gamma }}_{\mathsf{SK}}⊢⌜t⌝:X}{{\mathrm{\Gamma }}_{\mathsf{SK}}⊢r_t:{\mathsf{Eq}}_X(⌜t⌝,⌜t⌝)}}\mathrm{Eq}-\mathrm{I}\\ {\mathrm{\Gamma }}_{\mathsf{SK}}⊢{\mathsf{Eq}}_X(⌜t⌝,⌜t⌝)\equiv {\mathsf{Eq}}_X(⌜t⌝,⌜u⌝)\mathsf{type}\end{array}}{{\mathrm{\Gamma }}_{\mathsf{SK}}⊢r_t:{\mathsf{Eq}}_X(⌜t⌝,⌜u⌝)}\mathrm{Conv}.$$ The second premise is the Eq-congruence judgment displayed just above; its nonreflexive endpoint premise is the assumed $⌜t⌝\equiv ⌜u⌝:X$. Conversely, reflection is the one-step tree $$\frac{{\mathrm{\Gamma }}_{\mathsf{SK}}⊢r_t:{\mathsf{Eq}}_X(⌜t⌝,⌜u⌝)}{{\mathrm{\Gamma }}_{\mathsf{SK}}⊢⌜t⌝\equiv ⌜u⌝:X}\mathrm{Eq}-\mathrm{Reflect}.$$ Thus the term-typing query and the SK equality query are equivalent, with no appeal to an unannotated surface $\mathsf{refl}$.

Application synthesizes $\mathsf{app}(f,a;A,B)$ after normalizing the type of $f$ and inverting its $\mathrm{\Pi }$ head; the independent check rechecks $f$, checks $a:A$, and substitutes $a$ into $B$. Natural elimination records the motive $k.C$, zero branch, and step branch $n:\mathbb{N},y:C[n/k]⊢s:C[\mathsf{suc}(n)/k]$; rechecking repeats these three premises and returns $C[m/k]$. Identity elimination records $x,y,p.C$ and the reflexive branch after $y,x,p$ are replaced by $x,x,{\mathsf{refl}}_x$. Normalization occurs only before head inversion; constructor inversion chooses the rule; context conversion transports a checked branch when its reconstructed type is judgmentally, but not syntactically, the stored annotation.