6
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ Doesn't Agda do what you're proposing, more or less? $\endgroup$ – Andrej Bauer May 19 '17 at 12:02
  • $\begingroup$ In order for your question to be a bit more focus, could you please explicitly write what you mean by "totality checker"? For instance, Agda has a built-in totality checker. It works well in most cases, but sometimes people dance a little magic dance around it, or just turn it off. Are you thinking of a built-in checker? How powerful would it be? $\endgroup$ – Andrej Bauer May 19 '17 at 12:03
  • 2
    $\begingroup$ What is the type of Fix? How do you propose to prove $0\neq 1$ in CoC + Fix? $\endgroup$ – cody May 19 '17 at 12:44
  • $\begingroup$ Why is representing first order data as first order data "added complications" as opposed to representing first order data using a higher order encoding and self-referential types? $\endgroup$ – gallais May 19 '17 at 14:14
  • $\begingroup$ @cody sorry for the delay. You already answered before I had a chance to reply this comment. I guess, though, you're right, Fix isn't sufficient to encode that (we could do that with * : *, right? But that's yet another "bad" extension...) $\endgroup$ – MaiaVictor May 19 '17 at 16:57
10
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.