Can a totality checker be used to guarantee a proof on the calculus of constructions + inductive types is correct?

Question

If we extend the Calculus of Constructions with Fix, we gain a lot of expressivity for barely no added complexity. That includes being able to derive induction, perform large eliminations, prove 0 != 1 and so on. This system is, moreover, very user-friendly and comfortable to program in. Sadly, nothing of that because the resulting system becomes inconsistent. Making it consistent again requires, it seems, a lot of added complexity such as, for example, inductive types, or positive recursion checks + constructor-constrained recursive types + lift.

Suppose, though, that someone gives me a term T of type MyTheorem, programmed in that language (CoC + Fix), and that this term successfully pass through a totality checker. Wouldn't I be able to, then, trust, with absolute certainty, that MyTheorem holds? And, if that is true, doesn't that mean that, as long as that totality checker is used, one can just program on that comfortable language instead of dealing with the added complications of induction types and so on?

Answer 1

I'm going to assume that by $\mathrm{Fix}$ you mean a new type constructor

$$\frac{\Gamma\vdash F:*\rightarrow *}{\Gamma\vdash \mathrm{Fix}\ F:*} $$

Along with the conversion rule $\mathrm{Fix}\ F\simeq F\ (\mathrm{Fix}\ F)$. This is often referred to as equi-recursive types as opposed to iso-recursive types, where the conversion rule does not exist, and you need additional $\mathrm{fold}$ and $\mathrm{unfold}$ constructs to use $\mathrm{Fix}$.

I'll ignore the fact that the rule for $\mathrm{Fix}$ is non-terminating on it's own, since this isn't that harmful. You question about terms

$$\Gamma\vdash t:A$$ with $$\Gamma\vdash A:*$$

when are they sound proofs of the statement $A$?

You suggest using a "totality checker", to sidestep the need for messy rules such as positivity and various other restrictions when dealing with iso-recursive types.

The first remark is that simply checking termination of a term $t$ won't do: we can easily build a proof of $\forall n:\mathbb{N}. n = 0$ which has a normal form, but loops when applied to some natural number! So we really do need to check totality, which involves proving that $t$ will not lead to non-termination when placed in an arbitrary well-typed context.

Sadly, we don't really know how to do this, other than building back in all those nasty restrictions you want to avoid! For positivity for example, taking $\Lambda=\lambda X:*.X\rightarrow X$, then you can type $$\vdash \lambda x:\mathrm{Fix}\ \Lambda.x\ x:\mathrm{Fix}\ \Lambda $$

which smells like trouble: your totality checker had better reject that as a theorem.

The other restrictions will crop up pretty quickly.

As a side note, if you can prove something using some "reasonable" totality checker (provably correct in HOL) then you can actually "reverse engineer" a proof in CoC + $\forall n. S\ n\neq 0$, by internalizing the totality check. This technique is similar to realizability, where there is a correspondance between provably total functions and $\Pi^0_2$ theorems.

---

As a side note that came up in the comments, it seems to me that when restricting $\mathrm{Fix}$ to positive type constructors, i.e. type constructors $F$ for which (for each variable $f$) there exists a term $t_f$ such that

$${A:*,B:*,f:A\rightarrow B\vdash t_f:F\ A\rightarrow F\ B} $$

then there is no encoding of $\mathbb{N}$ such that induction over $\mathbb{N}$ holds.

The rough argument for this is to encode $\mathrm{Fix}\ F$ by $$\forall X, (F\ X\rightarrow X) \rightarrow X$$ which is the usual encoding for positive inductive types in system F, and show that every well typed term in the system with $\mathrm{Fix}$ can be well typed in the CoC without it. Then we can conclude by the fact that CoC doesn't have any inductive definitions of $\mathbb{N}$ itself.

The encoding is a little messy, though, I think. I'd be happy to have a reference for this.