<p>I'm going to assume that by <span class="math-container">$\mathrm{Fix}$</span> you mean a new type constructor</p>

<p><span class="math-container">$$\frac{\Gamma\vdash F:*\rightarrow *}{\Gamma\vdash \mathrm{Fix}\ F:*} $$</span></p>

<p>Along with the conversion rule <span class="math-container">$\mathrm{Fix}\ F\simeq F\ (\mathrm{Fix}\ F)$</span>. This is often referred to as <em>equi-recursive types</em> as opposed to <em>iso-recursive types</em>, where the conversion rule does not exist, and you need additional <span class="math-container">$\mathrm{fold}$</span> and <span class="math-container">$\mathrm{unfold}$</span> constructs to use <span class="math-container">$\mathrm{Fix}$</span>.</p>

<p>I'll ignore the fact that the rule for <span class="math-container">$\mathrm{Fix}$</span> is non-terminating on it's own, since this isn't that harmful. You question about terms</p>

<p><span class="math-container">$$\Gamma\vdash t:A$$</span>
with
<span class="math-container">$$\Gamma\vdash A:*$$</span></p>

<p>when are they sound proofs of the statement <span class="math-container">$A$</span>?</p>

<p>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.</p>

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

<p>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 <span class="math-container">$\Lambda=\lambda X:*.X\rightarrow X$</span>, then you can type
<span class="math-container">$$\vdash \lambda x:\mathrm{Fix}\ \Lambda.x\ x:\mathrm{Fix}\ \Lambda $$</span></p>

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

<p>The other restrictions will crop up pretty quickly.</p>

<p>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 + <span class="math-container">$\forall n. S\ n\neq 0$</span>, by internalizing the totality check. This technique is similar to realizability, where there is a correspondance between provably total functions and <span class="math-container">$\Pi^0_2$</span> theorems.</p>

<hr>

<p>As a side note that came up in the comments, it seems to me that when restricting <span class="math-container">$\mathrm{Fix}$</span> to <em>positive type constructors</em>, i.e. type constructors <span class="math-container">$F$</span> for which (for each variable <span class="math-container">$f$</span>) there exists a term <span class="math-container">$t_f$</span> such that</p>

<p><span class="math-container">$${A:*,B:*,f:A\rightarrow B\vdash t_f:F\ A\rightarrow F\ B} $$</span></p>

<p>then there is no encoding of <span class="math-container">$\mathbb{N}$</span> such that induction over <span class="math-container">$\mathbb{N}$</span> holds.</p>

<p>The rough argument for this is to encode <span class="math-container">$\mathrm{Fix}\ F$</span> by 
<span class="math-container">$$\forall X, (F\ X\rightarrow X) \rightarrow X$$</span>
which is the usual encoding for positive inductive types in system F, and show that every well typed term in the system with <span class="math-container">$\mathrm{Fix}$</span> 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 <span class="math-container">$\mathbb{N}$</span> itself.</p>

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

CC BY-SA 4.0
2017-05-19T13:25:16.253Z
2018-12-10T18:39:50.943Z
2018-12-10T18:39:50.943Z
cody
<p>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 <code>0 != 1</code> 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 <a href="http://homepage.cs.uiowa.edu/~astump/papers/cedille-draft.pdf" rel="noreferrer">positive recursion checks + constructor-constrained recursive types + lift</a>.</p>

<p>Suppose, though, that someone gives me a term <code>T</code> of type <code>MyTheorem</code>, programmed in that language (<code>CoC + Fix</code>), and that this term successfully pass through a totality checker. Wouldn't I be able to, then, trust, with absolute certainty, that <code>MyTheorem</code> 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?</p>

CC BY-SA 3.0
2017-05-19T12:02:25.353Z
Doesn't Agda do what you're proposing, more or less?
Andrej Bauer
CC BY-SA 3.0
2017-05-19T12:03:00.197Z
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?
Andrej Bauer
CC BY-SA 3.0
2017-05-19T12:44:46.297Z
What is the type of `Fix`? How do you propose to prove $0\neq 1$ in `CoC + Fix`?
cody
CC BY-SA 3.0
2017-05-19T14:14:50.657Z
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?
gallais
CC BY-SA 3.0
2017-05-19T16:57:56.887Z
@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...)
MaiaVictor
CC BY-SA 3.0
2017-05-20T15:16:20.677Z
@MaiaVictor if you have arbitrary `Fix`, you can prove anything, but if you restrict `Fix` to "positive" types ($F$s that are "functorial") then I'm not actually sure! I think you're out of luck, but I need to think for a minute about why...
cody
<type-theory><lambda-calculus>
Can a totality checker be used to guarantee a proof on the calculus of constructions + inductive types is correct?
MaiaVictor
# Can a totality checker be used to guarantee a proof on the calculus of constructions + inductive types is correct?

(Asked by: username_0 on 2017-05-19)

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](http://homepage.cs.uiowa.edu/~astump/papers/cedille-draft.pdf).

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?

**Tags:** type-theory, lambda-calculus
> **Comments:**
> **username_1**: Doesn't Agda do what you're proposing, more or less?  
> **username_1**: 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?  
> **username_2**: What is the type of `Fix`? How do you propose to prove $0\neq 1$ in `CoC + Fix`?  
> **username_3**: 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?  
> **username_0**: @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...)  
> **username_2**: @MaiaVictor if you have arbitrary `Fix`, you can prove anything, but if you restrict `Fix` to "positive" types ($F$s that are "functorial") then I'm not actually sure! I think you're out of luck, but I need to think for a minute about why...  

---

## 1 answers

### Answer by username_2 on 2017-05-19. Score: 10 | Accepted answer

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.


---

