1
$\begingroup$

I am recently learning the theory behind Coq and learnt that positivity condition guarantees termination of the program. But my question is, what would you think of the following definition?

Inductive t : Set := b : t | c : ((t -> unit) -> unit) -> t.

Sure it won't compile in Coq, but would it jeopardize termination guarantee? More precisely, in this definition, t is in a positive position as well, isn't it? So can I say theoretically speaking this should have also been a valid definition? Otherwise do you have any counter example?

My thought is, (t -> unit) -> unit should be isomorphic to t according to Yoneda lemma so it should be pretty safe, isn't it?

$\endgroup$
  • 1
    $\begingroup$ Uh, the Yoneda lemma does not say that. In fact, ((t -> unit) -> unit) is isomorphic to unit. So t will be quite safe. $\endgroup$ – Derek Elkins Sep 24 '17 at 23:23
  • $\begingroup$ @DerekElkins I don't think so. Yoneda lemma says $Nat(Hom(a, -), F) \equiv Fa$, letting $F$ be identity functor, it says $Nat(Hom(a, -), Id) \equiv a$, which means $\forall b, (a \to b) \to b \equiv a$. $\endgroup$ – Jason Hu Sep 24 '17 at 23:41
  • 1
    $\begingroup$ The set of natural transformations is what is isomorphic to $a$. That is, you have something more like $(\forall b.(a\to b)\to b))\equiv a$, not $\forall b.\left((a\to b)\to b \equiv a\right)$. You can also verify my statement. It's a very easy theorem in Coq to prove that a -> unit is isomorphic to unit for any a whatsoever. $\endgroup$ – Derek Elkins Sep 24 '17 at 23:48
  • 2
    $\begingroup$ Actually, I'm not sure if you can completely prove the isomorphism in Coq since it doesn't (didn't?) have the eta-conversions rules for unit types that you'd need for showing $\forall f: A\to\mathtt{unit}.f = \lambda x\!:\!A.\mathtt{tt}$. (Maybe I just don't know how to convince it.) You can prove a weaker statement, like these are extensionally equal, though (and from there prove that they are equal if you have function extensionality). In Agda, these are definitionally equal if unit is defined with record. $\endgroup$ – Derek Elkins Sep 25 '17 at 1:35
  • 3
    $\begingroup$ @DerekElkins: nope, can't prove that in pure Coq. You need to assume function extensionality. $\endgroup$ – Andrej Bauer Sep 25 '17 at 8:08
5
$\begingroup$

The positivity condition is not there just so that "programs terminate", as you put it (what programs?), but to make sure the type is well defined in the first place. The inductive definitions define the smallest type satisfying an equation. That is, we put into the type only those things which are prescribed by the clauses of the definition, and no arbitrary garbage. (Non-normalizing terms count as garbage, and I think that's what you meant when you spoke of terminating programs.)

Let us take a step back and think where the inductive definitions come from. They are solutions to type equations. Here is a type equation: $$N = \mathtt{unit} + N.$$ What could $N$ be? We might be thinking that it must be the natural numbers, since every element of $N$ is either $\mathtt{inl}(\mathtt{tt})$, which is a fancy way to say "zero", or it is of the form $\mathtt{inr}(n)$ for some $n : N$. But this need not be the case! For example, $N$ could also contain a special element $\infty$ satisfying $\infty = \mathtt{inr}(\infty)$. It could also contain an extra "fake zero" $\mathtt{Z}$, together with its successors $\mathtt{inr}(\mathtt{Z})$, $\mathtt{inr}(\mathtt{inr}(\mathtt{Z}))$, ... There are many solutions to the above equation.

The smallest solution is called the inductive type, and the largest one the coinductive type. I am skipping technicalities about what "smallest" and "largest" mean precisely (they are the "initial algebra" and "final coalgebra", respectively), but I hope you get the point.

In order for us to say that we have a well-defined inductive type, we need to know that the smallest solution to the type equation actually exists. In fact, it does not always exist, sometimes there can be several incomparable solutions, or none at all. The positivity condition in Coq and CIC ensures that a smallest solution exists. It's not the only possible condition one could come up with, and there are variants, but for the purposes of a proof assistant we need something that makes sense computationally, and can actually be verified by a type checker (for instance, it wouldn't do to say that an inductive definition is valid if it defines a $\kappa$-accessible functor for some cardinal $\kappa$, and have the proof checker look for $\kappa$ – hmm, that's an interesting thought).

If we now look at your proposed definition

Inductive t : Type := b : t | c : ((t -> unit) -> unit) -> t.

the question to be asked is: how do you know that the smallest solution exists? Somebody proved that the strict positivity requirement ensures the existence, but your definition falls outside that criterion. You need to provide evidence that there is such a type. The evidence must be a well argued explanation of what the terms of t are that they do not break strong normalization of CIC. You might as well succeed, and there is such a type. The next question then is how do you propose to incorporate your argument into a type checker as a useful algorithm. It's probably not worth the trouble.

Just to show you how problematic these things are, how about the type

Inductive t : Type := c : ((t -> bool) -> bool) -> t.

Is it still totally obvious that there is a smallest solution? We're trying to solve the type equation $$T = (T \to 2) \to 2.$$ It has no solution in set theory.

$\endgroup$
  • $\begingroup$ I am confused. wouldn't unit denote 1 instead? I'd imagine Empty_set denotes 0. Regarding the last equation, is it the right understanding that $T \to 2$ generate the power set of $T$, and $(T \to 2) \to 2$ is another layer of power set, such that there's provably no isomorphism between them and $T$? $\endgroup$ – Jason Hu Sep 25 '17 at 9:57
  • $\begingroup$ Why did you say "provably"? $\endgroup$ – Andrej Bauer Sep 25 '17 at 12:22
  • $\begingroup$ Cuz Cantor proved it. $\endgroup$ – Jason Hu Sep 25 '17 at 12:23
  • 1
    $\begingroup$ yes it was clear. last bit, what type $T$ can be isomorphic to $T \to 2$? I would expect this won't work also for infinite types. $\endgroup$ – Jason Hu Sep 25 '17 at 12:44
  • 1
    $\begingroup$ I don't think any type $T$ can be isomorphic to $T \to 2$ by Cantor's diagonal argument (which is implementable in Haskell). But $T$ may be isomorphic to $(T \to 2) \to 2$, see my blog post math.andrej.com/2009/10/12/constructive-gem-double-exponentials where I implement an isomorphism betwween $\mathbb{N}$ and $(\mathbb{N} \to 2) \to 2$ in Haskell. $\endgroup$ – Andrej Bauer Sep 27 '17 at 9:01

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.