A.4 Basic metatheory
This section discusses the meta-theoretic properties of the type theory presented in \autorefsec:syntax-informally, and similar results hold for \autorefsec:syntax-more-formally. Figuring out which of these still hold when we add the features from \autorefsec:hott-features quickly leads to open questions, as discussed at the end of this section.
This rule, together with the defining equations for the defined constants form rewriting rules that determine reduction steps for a rewriting system. These steps yield a notion of computation in the sense that each rule has a natural direction: one simplifies by evaluating the function at its argument.
Moreover, this system is confluent, that is, if simplifies in some number of steps to both and , there is some to which both and eventually simplify. Thus we can define to mean that and simplify to the same term.
(The situation is similar in \autorefsec:syntax-more-formally: Although there we presented the computation rules as undirected equalities , we can give an operational semantics by saying that the application of an eliminator to an introductory form simplifies to its equal, not the other way around.)
It is straightforward to show that the system in \autorefsec:syntax-informally has the following properties:
If and then . If and then .
We say that a term is normalizable (respectively, strongly normalizable) if some (respectively, every), sequence of rewriting steps from the term terminates.
If then is strongly normalizable. If then and are strongly normalizable.
We say that a term is in normal form if it cannot be further simplified, and that a term is closed if no variable occurs freely in it. A closed normal type has to be a primitive type, i.e., of the form for some primitive constant (where the list of closed normal terms may be omitted if empty, for instance, as with ). In fact, we can explicitly describe all normal forms:
The terms in normal form can be described by the following syntax:
where represents a partial application of the defined function . In particular, a type in normal form is of the form or .
If is in normal form then the judgment is decidable. If and is in normal form then the judgment is decidable.
Logical consistency (of the system in \autorefsec:syntax-informally) follows immediately: if we had in the empty context, then by \autorefthm:conversion-preserves-typing,\autorefthm:strong-normalization, simplifies to a normal term . But by \autoreflem:normal-forms no such term exists.
The system in \autorefsec:syntax-informally is logically consistent.
Similarly, we have the canonicity property that if in the empty context, then simplifies to a normal term for some numeral .
The system in \autorefsec:syntax-informally has the canonicity property.
Finally, if are in normal form, it is decidable whether ; in other words, because type-checking amounts to verifying the correctness of a proof, this means we can always “recognize a correct proof when we see one.”
The property of being a proof in the system in \autorefsec:syntax-informally is decidable.
The above results do not apply to the extended system of homotopy type theory (i.e., the above system extended by \autorefsec:hott-features), since occurrences of the univalence axiom and constructors of higher inductive types never simplify, breaking \autoreflem:normal-forms. It is an open question whether one can simplify applications of these constants in order to restore canonicity. We also do not have a schema describing all permissible higher inductive types, nor are we certain how to correctly formulate their rules (e.g., whether the computation rules on higher constructors should be judgmental equalities).
The consistency of Martin-Löf type theory extended with univalence and higher inductive types could be shown by inventing an appropriate normalization procedure, but currently the only proofs that these systems are consistent are via semantic models—for univalence, a model in Kan complexes due to Voevodsky [klv:ssetmodel], and for higher inductive types, a model due to Lumsdaine and Shulman [ls:hits].
|Title||A.4 Basic metatheory|