ch:computational-type-theory: ch:computational-type-theory

The pair $p$ is canonical as soon as its outer pair constructor is visible. Neither $(\lambda x.0)\mathrm{\Omega }$ nor $1+2$ is evaluated to establish that fact. The first spread performs $$\mathsf{spread}(p;x,y.x){⟶}^{\ast }(\lambda x.0)\mathrm{\Omega }{⟶}^{\ast }0.$$ The first contraction inspects only the outer constructor of $p$; the second substitutes $\mathrm{\Omega }$ into a body in which the bound variable does not occur. Thus no step evaluates $\mathrm{\Omega }$. The second spread performs $$\mathsf{spread}(p;x,y.y){⟶}^{\ast }1+2{⟶}^{\ast }3.$$ Here the left component, including its occurrence of $\mathrm{\Omega }$, is discarded. Only the selected right component is evaluated.

If $S(m,n)$, then $|n-m|=|m-n|=1$, so $S$ is symmetric. It is not transitive: $S(0,1)$ and $S(1,2)$ hold, whereas $S(0,2)$ does not. Its PER domain would be $$\{m\in \mathbb{Z}\mid S(m,m)\}=\{m\in \mathbb{Z}\mid 0=1\}=\varnothing .$$ The empty domain does not repair the failure of transitivity on arguments outside that domain; $S$ is therefore not a PER.

Write $T(m,n)$ when $2$ divides $m-n$. Reflexivity follows from $2\mid 0$, symmetry from $2\mid d\Rightarrow 2\mid -d$, and transitivity from closure of divisibility under addition: $$2\mid (m-n),2\mid (n-k)⟹2\mid (m-k).$$ Hence $T$ is an equivalence relation, in particular a PER, and $T(m,m)$ holds for every integer. Its domain is all of $\mathbb{Z}$.

Integer addition gives $2+1\Downarrow 3$, while the canonical integer $3$ evaluates to itself. Thus $R_{\mathbb{Z}}(2+1,3)$ holds by (91.1). The witness $\mathsf{axiom}$ also evaluates to itself, so all three conjuncts of (91.4) hold. Therefore $${\mathsf{Mem}}_i(\mathsf{axiom};{\mathsf{Eq}}_{\mathsf{Int}}(2+1,3)).$$ Evaluation is used first to compute the two endpoints and then to expose the canonical equality witness; integer equality is used to see that both endpoints compute to the same integer.

For ${\mathsf{Eq}}_{\mathsf{Int}}(2,3)$, the endpoints are distinct canonical integers. Determinism rules out an integer $z$ to which both evaluate, so $R_{\mathbb{Z}}(2,3)$ is false. Equation (91.4) therefore assigns the empty member relation to this equality type, independently of the proposed witness. It has no member.

Apply (91.11) in each case: Root contraction of $\mathrm{\Omega }$ reproduces $\mathrm{\Omega }$, so it does not evaluate to any integer. The existential in (91.11) has no witness, and $\mathrm{\Omega }$ is not a member. Divergence and convergence to a negative integer are distinct reasons for rejection.

Take the two raw representatives $$r:=0,s:=(\lambda z.z)0.$$ Both evaluate to $0$ and are therefore equal in $\mathbb{N}$. On the abstract two-element set $\{r,s\}$, this is the total PER. Write $t{\equiv }_{\mathsf{raw}}s$ for literal equality of raw syntax. Define a total, representation-sensitive assignment on every closed representative $t$ by Thus $B(r)=\mathsf{Int}$ and $B(s)=\mathbb{N}$. Every closed instance is a type, so a test that substitutes one representative at a time accepts it. Pointwise functionality also compares the equal substitutions $[r/x]$ and $[s/x]$ and would require $${\mathsf{TyEq}}_i(\mathsf{Int},\mathbb{N}).$$ This is false: $-1$ belongs to the integer PER but not to the natural-number PER. The pair $[r/x]{\equiv }_{x:\mathbb{N}}[s/x]$ therefore exposes the failure. Such source-spelling inspection is not a valid functional Nuprl family; the example isolates exactly what the two-substitution condition excludes.

At input $n$, successor has raw output $n+1$ in the set type $$\mathsf{Inc}(n)=\{m:\mathbb{N}\mid {\mathsf{Eq}}_{\mathbb{N}}(m,n+1)\}.$$ The predicate is inhabited by $\mathsf{axiom}$, but (91.5) relates the ambient members themselves and does not pair them with predicate evidence. At $n=2$, the result is therefore the program $2+1\Downarrow 3$.

For the dependent pair $$\sum _{m:\mathbb{N}}{\mathsf{Eq}}_{\mathbb{N}}(m,n+1),$$ the dependent-pair specification uses $(n+1,\mathsf{axiom})$. At $n=2$, beta contraction gives $$s2{⇝}_0(2+1,\mathsf{axiom}).$$ This pair is canonical before either component is evaluated. Projecting its first component and demanding a natural numeral gives $2+1\Downarrow 3$; the second projection gives $\mathsf{axiom}$. Thus its observed components are $3$ and $\mathsf{axiom}$, although lazy evaluation does not reduce under the pair constructor merely to expose the outer value. Equation (91.3) retains both components, whereas (91.5) uses only inhabitance of the predicate relation. This accounts for the visible $\mathsf{axiom}$ in exactly one result.

Define the relation program where is signed integer remainder. At every old-system level $i$, equality formation derives ${\mathsf{Ty}}_i(E_3(m,n))$. If equal integer representatives replace $m,n$, their computed values are unchanged, so both instances normalize to the same canonical equality type ${\mathsf{Eq}}_{\mathsf{Int}}(r,0)$, where $r$ is their common signed remainder. Thus ${\mathsf{TyEq}}_i$ relates the two instances, proving the functionality clause. The condition ${\mathsf{Inh}}_i(E_3(m,n))$ holds exactly when $r=0$, so it is equivalent to $3\mid (m-n)$, and the other admissibility clauses are Thus $E_3$ is admissible at every old-system level.

As candidate endomaps $\mathsf{Int}/E_3\to \mathsf{Int}/E_3$, successor respects the quotient because $$(m+1)-(n+1)=m-n.$$ Absolute value does not. The representatives $1$ and $-2$ are equal modulo $3$, since $1-(-2)=3$, but their absolute values are $1$ and $2$, whose difference is not divisible by $3$.

For function transitivity, assume $R_{\mathrm{\Pi }}(f,g)$ and $R_{\mathrm{\Pi }}(g,h)$ and take $R_A(a,c)$. The PER laws give $R_A(c,c)$. Instantiating the first function relation at $(a,c)$ and the second at $(c,c)$ gives $$R_B^{a,c}(fa,gc),R_B^{c,c}(gc,hc).$$ The middle application is $gc$. Functionality identifies $R_B^{a,c}$ with $R_B^{c,c}$, and transitivity in that common fiber relates $fa$ to $hc$. Symmetry reverses the domain relation and then uses symmetry in the identified fiber.

For pairs, write the two premises as Determinism of evaluation gives $(b,v)=(b^{\prime },v^{\prime })$, hence $b=b^{\prime }$ and $v=v^{\prime }$. Base transitivity gives $R_A(a,c)$; functionality puts the two component relations in the fiber $R_B^{a,c}$; fiber transitivity then gives $R_B^{a,c}(u,w)$.

The need for functionality is witnessed by a finite countermodel. Give $\{0,1\}$ the total base PER and take four distinct results $u,v,w,z$. Let the nontrivial equivalence classes of the four fiber PERs be With $f(0)=f(1)=u$, $g(0)=w$, $g(1)=v$, $h(0)=w$, and $h(1)=z$, the four fiber checks show $R_{\mathrm{\Pi }}(f,g)$ and $R_{\mathrm{\Pi }}(g,h)$. But the $(0,1)$ check for $R_{\mathrm{\Pi }}(f,h)$ asks that $u$ and $z$ lie in one class of the $(0,1)$ fiber, which they do not. Likewise, $$(0,u)R_{\mathrm{\Sigma }}(1,v),(1,v)R_{\mathrm{\Sigma }}(1,z),$$ but the first and last pairs are not related. Every displayed fiber is a PER; the failure is precisely that equal base inputs do not identify the fiber PERs.

Write $$\sigma =(a,u,g),\tau =(a^{\prime },u^{\prime },g^{\prime })$$ for substitutions into the three hypotheses. They are equal exactly when the left-to-right construction yields together with the type equalities that make the second components legitimate. The first hypothesis is functional because $\mathbb{N}$ is closed. For the second, equality of $a,a^{\prime }$ makes ${\mathsf{Eq}}_{\mathbb{N}}(a,a)$ and ${\mathsf{Eq}}_{\mathbb{N}}(a^{\prime },a^{\prime })$ equal types. The third type is closed, so it is functional independently of the prefix.

For the extract $fn$, (91.14) becomes $${\mathsf{TyEq}}_i(\mathbb{N},\mathbb{N})\text{and}{\mathsf{MemEq}}_i(ga,g^{\prime }{a}^{\prime };\mathbb{N}).$$ The last conjunct in the definition of equal substitutions is a function-PER relation; its instance at the related arguments $a,a^{\prime }$ gives the member equality.

After replacing the last hypothesis by $f:\prod _{x:\mathbb{N}}{\mathsf{Eq}}_{\mathbb{N}}(x,n),$ functionality requires the additional cross-fiber obligation $$\begin{array}{c}{\mathsf{TyEq}}_i({\mathsf{Eq}}_{\mathbb{N}}(x,a),{\mathsf{Eq}}_{\mathbb{N}}(x^{\prime },a^{\prime })),\\ \text{whenever }{\mathsf{MemEq}}_i(x,x^{\prime };\mathbb{N})\text{ and }{\mathsf{MemEq}}_i(a,a^{\prime };\mathbb{N}).\end{array}$$ An equal pair of substituted functions must in addition return equal $\mathsf{axiom}$ witnesses in those fibers. In fact the modified function type has no closed member: a member would have to inhabit ${\mathsf{Eq}}_{\mathbb{N}}(x,a)$ for every natural $x$, including one whose numeral is different from the numeral denoted by $a$. The context may still be proved functional, but it admits no closed substitution for its final hypothesis.

Put These are old-system programs; in particular, the quotient is not used in the definition of $E$. Let $p,q\in \mathrm{dom}(R_A)$. Sigma inversion gives evaluations of $p$ and $q$ to canonical pairs whose two components belong to the integer PER. Spread followed by addition therefore evaluates each sum to a canonical integer. The old equality-type generator then proves ${\mathsf{Ty}}_i(E(p,q))$ for every old-system level $i$.

It remains to check functionality for arbitrary program representatives, not only written pairs. Suppose $R_A(p,p^{\prime })$ and $R_A(q,q^{\prime })$. Sigma inversion and the integer PER identify the two component values of $p,p^{\prime }$ and those of $q,q^{\prime }$. Hence $\mathsf{sum}(p)$ and $\mathsf{sum}(p^{\prime })$ evaluate to the same integer, as do the two sums from $q,q^{\prime }$. The equality generator consequently gives $${\mathsf{TyEq}}_i(E(p,q),E(p^{\prime },q^{\prime })).$$ Moreover, $${\mathsf{Inh}}_i(E(p,q))⟺\mathsf{sum}(p)\text{ and }\mathsf{sum}(q)\text{ evaluate to the same integer}.$$ Reflexivity, symmetry, and transitivity of integer equality establish admissibility clauses (2)–(4). Thus all four clauses hold on the entire Sigma-PER domain.

Three nontrivial equalities in $A/E$ are $$(0,3)E(1,2),(-1,5)E(4,0),(7,-2)E(0,5).$$

Use the lazy programs at the signatures printed in the exercise: First projection does not respect $E$: the $E$-equal programs $(0,3)$ and $(1,2)$ produce the unequal integers $0$ and $1$. Sigma inversion shows that $\mathsf{total}p$ evaluates to an integer whenever $p$ is a member of $A$. It also shows that $\mathsf{swap}p$ evaluates to a pair of integer components, hence is a member of $A$ and therefore of $A/E$ by quotient reflexivity. Total respects $E$ by its defining condition. Swapping respects $E$ because $$a+b=c+d⟹b+a=d+c.$$ If swapping instead had the unquotiented pair type as codomain, the same representatives would be a counterexample: $(3,0)$ and $(2,1)$ are not componentwise equal. The codomain equality is therefore part of the congruence claim.