Using type systems to model type theories

Allen's techniques enable us to model a variety of type theories. Let us designate some models for the theories discussed earlier. We'll fix the terms and evaluation relation to include those of the richest theory; so the terms are: 0, 1, $\bullet$, ${{\mathbb{N} }}$, 0, suc(t), prd(s), add(s; t), mult(s; t), exp(s; t), R(n; t; v.b; u, v, i.h), $s \times t$, pair(s; t), prod(s; x.t), fun(s; x.t), $\lambda(x.t)$, list(t), (s.t), L(s; a; v.b; h, t, v, i.g), s+t, inl(s), inr(t), and decide(p; u.s; v.t).

There is also the evaluation relation $s\ evals\_to\ t$ which we abbreviate as $s \downarrow t$. definedness ( $\downarrow$) We consider various mappings T $_l: TS \rightarrow TS$ where l is a label such as $N, G, ML, N\!u$, etc. The most elementary ``theory'' we will examine is a subtheory of arithmetic involving only equalities over ${{\mathbb{N} }}$ built from 0, suc(t), prd(s), and add(s; t). This is modeled by T_N. The input to T_N is any pair $\langle E, \mathbf{L}\rangle$ and the output is $\langle F, \mathbf{M}\rangle$ where the only type name is N, so NFN, thus $N \in \vert F\vert$, and the only type equality is M(N) which is defined inductively. We have that s M(N)tis the least relation $N\!eq$ such that

$$s\ N\!eq\ t\ \hbox{\textit{iff}}\ \left( s \downarrow 0\ \&\... ...row suc(s')\ \&.\: t \downarrow suc(t') s' N\!eq\ t'\right).$$

The map T_N takes any $\langle E, \mathbf{L}\rangle$ to this $\langle F, \mathbf{M}\rangle$, so its least fixed point, $\mu(\mathbf{T}_N)$ is just $\langle F, \mathbf{M}\rangle$. This is the model for successor arithmetic. We see that in this model, N is a type, that s=t in N iff s evaluates to a canonical natural number and t evaluates to the same canonical number.

The rules can be confirmed as follows. First, notice that evaluation is deterministic and idempotent on the terms. As we observed, the general equality rules hold in any type system (because M(N) is in equivalence relation on canonical numbers). This follows by showing inductively that $0, suc(0), suc(suc(0)), \ldots$ are in the relation M(N), i.e. in the field of the relation. The fact that M(N) respects evaluation validates the last equality rule.

$\mu(T_N) \models 0=0$ in N

$\mu(T_N) \models s=t$ in N implies $\mu(T_N) \models suc(s)=suc(t)$in N.

The typing rule for successor is also confirmed by induction on $N\!eq$; namely, if s' L(N) t', then since $suc(s') \downarrow suc(s')$ and $suc(t') \downarrow suc(t')$, then we have suc(s) M(N) suc(t) as required for the typing rule.

In the case of N, the model $\mu(T_N)$, and the informal semantics are essentially the same. So the theory fragment for N can stand on its own with respect to the model. Even a set theoretic semantics for N will have the same essential ingredient of an inductive characterization. For instance, Frege's definition was that

$$N==\{x\ \vert\ \forall X.\: (0 \in X\ \&\ \forall y.\: (y \in X \Rightarrow s(y) \in X)) \Rightarrow x \in X\}$$

where s(x) is $\left\{z\ \vert\ \exists u.\:\left(u \in z\ \&\ z-\{u\}=x\right)\right\}.$ In ZF we can use the postulated infinite set, inf, and form $\omega ==\left\{i: in\!f\ \vert\ \forall x.\: nat\_like(x) \Rightarrow i \in x\right\}$ where $nat\_like(x)\ \hbox{\it iff}\ (0 \in x\ \&\ \forall y.\:(y \in x \Rightarrow suc(y) \in x))$ for $S\!uc(y)=y \cup \{y\}$. In both of these definitions, the inductive nature of ${{\mathbb{N} }}$ is expressed. But Frege's theory and ZF allow very general ways of using this inductive character. So far we have only used it for specifying the canonical values.

The same approach can be used to define a model for the type theory with cartesian products. In this case we denote the operator on type systems as $T_N^{\mbox{\tiny$2$ }}$. Given $T{_N{^2}}\left(\left\langle E, \mathbf{L}\right\rangle\right)=\left\langle F, \mathbf{M}\right\rangle$, if $S \in \vert E\vert$ and $T \in \vert E\vert$ then $S \times T \in \vert F\vert$, and $\mathbf{M}(S \times T)$ is $\mathbf{L}(S) \otimes\mathbf{L}(T)$. For this system, T_N² is continuous, i.e. if $\tau_0=\langle \phi, \phi\rangle$ and $T{_N{^2}}(\tau_i)=\tau_{i+1}$, then $\mu(T{_N{^2}})=\tau_{\omega}$.

In $\mu(T{_N{^2}})$ all the rules for the fragment of section  are true. Again the theory is so close to the semantics that it stands on its own. Notice that in confirming the rule for typing pairs, we rely on the fact that $\mu(T{_N{^2}})$is a fixed point.

$\mu(T{_N{^2}})$	$\models s=s'$ in $S\ \mbox{and}\ \mu(T{_N{^2}}) \models (t=t'\ \mbox{in}\ T)$ imply
$\mu(T{_N{^2}})$	$\models \ pair(s; t)= pair(s'; t')\ \mbox{in}\ S \times T.$

Note, this fact would not be true in any fixed $\tau_i$ since $S \times T$ might be defined only in $\tau_{i+1}$.

To provide a semantics for $f\!un(A; x.B)$ and $prod(A; x.\ B)$ we use the map T_ML defined in section . The model is $\mu(T_{ML})$. To prove the rules correct, we recall the meaning of sequents such as $x \in A \vdash B$ type and $x \in A \vdash s=t$ in T.

$\mu(T_{ML}) \models (x \in A \vdash B\ type)$ implies $\mu(T_{ML}) \models f\!un(A; x. B)\ type$

$\mu(T_{ML}) \models (x \in A \vdash b \in B)$ implies $\mu(T_{ML}) \models \lambda(x. b)$ in $f\!un(A; x.B)$