The Coq mailing list

[Benjamin Werner <benjamin.werner AT inria.fr>]

Actually I think I wrote to hastily here and the seg fault
thing is probably to true.

In general however, it is true one should not expect too much
logically from the system with general fix-point. But I agree it is
certainly something one sometimes want for experimentations.

Benjamin

which is indee
Le 20 juin 08 à 18:31, Benjamin Werner a écrit :

> Hi,
>
> Obviously, having unguarded fixpoints yields paradoxes.
>
> It could also be worse, since with a fixpoint we can build
> a type A such that   A is convertible to A->A.
>
> We then can type any term. If we use this and have
> a case analysis over (say) a type with n constructors and
> apply it to an object of a type with n+1 constructors, we could
> end up with a segmentation fault (for the compiled version
> of reduction).
>
> Whether this can really be done boils down to the fact whether
> one can really use the fix-point to have the system "understand"
> that A and A->A are convertible, without entering a loop first; as
> hinted by Pierre below.
>
> But I  would say this is not too important, if one agrees that the
> "no-check" option is really unsafe and for experimentation.
> Whether this option should be offered and documented in
> the standard Coq is however a question I would not decide
> alone.
>
>
> Best,
>
> Benjamin
>
>
>
> Le 20 juin 08 à 18:15, Pierre Letouzey a écrit :
>
> > On Sun, Jun 15, 2008 at 01:06:46PM +0200, Matthieu Sozeau wrote:
> > > Hello,
> > >
> > > Le 15 juin 08 à 12:00, 
> > > frederic.blanqui AT loria.fr
> > >  a écrit :
> > >
> > > > On Fri, 13 Jun 2008, 
> > > > frederic.blanqui AT loria.fr
> > > >  wrote:
> > > >
> > > > > Hello. As it is well known, many function definitions are rejected
> > > > > by Coq since they do not pass Coq termination checker which  
> > > > > accepts
> > > > > only structurally terminating functions. Would it be possible to
> > > > > add a new command line option to coqc that would disable the
> > > > > termination checker?
> > > >
> > > > Instead of a command line option, it would be better to have a
> > > > command like "Unsafe Fixpoint" to disable the termination check
> > > > locally and keep a trace of this in the file itself.
> > >
> > > Actually, one would still need to tell on which argument to recurse,
> > > as the reduction functions need this to decide when to unfold. So I
> > > think a { general x } annotation would be the right way to do it.  
> > > I'm
> > > willing to make the change (I have a patch somewhere doing that
> > > already), but maybe there are some arguments against it?
> >
> >
> > Humm...
> >
> > It would be nice to have the opinion of "(in)coherence experts"
> > concerning this, but in the meantime I happened to had last Monday a
> > discussing with Colin Riba on that topic. He provided me an example
> > that strongly suggests that Bad Things May Happen very quickly with
> > the above ideas.
> >
> > More precisely:
> >
> > * It is common knowledge that having unguarded fixpoints of
> > unrestricted type kills not only the termination, but also the
> > coherence: take for instance ((fix bug (n:nat) : False := bug n) O).
> >
> > * Now, the example mentionned to me by Colin shows that even ungarded
> > fixpoints of "friendly types" such as bool->bool can hurt a lot.
> > Take:
> >
> > Fixpoint bug (b : bool) : bool := negb (bug b).
> >
> > Then, morally, (bug true) is equal to (negb (bug true)) by unfold of
> > the left occurrence of bug, whereas it's very easy to prove that
> > (forall b:bool, b <> negb b), hence you have your contradiction.
> >
> > I say "morally" above since I've actually tried to do it in Coq and
> > only almost succeeded (i.e. failed). First, killing the check of
> > fixpoints is really straightforward: for those would want to try, you
> > just have to bypass function check_fix in kernel/inductive.ml and  
> > make
> > sure this function always returns () immediately.
> >
> > Then the following script becomes possible:
> >
> > -----------------------------------------------------------------------
> > Fixpoint bug (b : bool) : bool := negb (bug b).
> >
> > Lemma bug_eqn : forall b, b = true -> bug b = negb (bug b).
> > Proof.
> > intros.
> > pattern b at 1; rewrite H.
> > (* Note that you're now in a true minefield.
> >  All your favorite tactics diverge : unfold, rewrite, change, ...
> >  We need to go low-level *)
> > lazy delta [bug].
> > lazy iota.
> > lazy beta.
> > remember true as b'. (* don't know why this work and not rewrite *)
> > rewrite H.
> > reflexivity.
> > Show Proof.
> > (* Qed.  *)(* Proof is actually finished for good ... but Qed  
> > diverges *)
> > Admitted.
> >
> > Lemma negb_neq : forall b, b = negb b -> False.
> > Proof.
> > destruct b; discriminate.
> > Qed.
> >
> > Lemma Bug : False.
> > Proof.
> > apply negb_neq with (bug true).
> > apply bug_eqn.
> > reflexivity.
> > Qed.
> > ---------------------------------------------------------------------
> >
> >
> > As you can see, I haven't obtain rigorously a proof of False, but  
> > this
> > is only because Coq has diverged first. This isn't particularly
> > comfortable: maybe someone more clever could achieve this proof or
> > maybe benign changes in Coq could lead to acceptance of the above
> > script. Or maybe not.
> >
> > Anyway, this example is far from solving all questions:
> >
> > * first, is it safe to add this way a truly terminating (but not
> > structural) fixpoint this way ? I suppose yes, but even that is
> > not clear, at least for me.
> >
> > * Second, is it safe to add a non-terminating fixpoint that doesn't
> > provide immediate contradiction in its equation as above ? For
> > instance, what about (fix f (n:nat) : nat := f n) or
> > (fix g (n:nat) := g (S n)) ?
> > I would be tempted to think that something wrong is still going on,
> > since you would have nat objects around that neither compute to O or
> > (S _). But since they have no normal form, maybe we're only
> > loosing termination.
> >
> > With this kind of questions around, with the risk of ending on a
> > diverging Coq (see the comments in the script above), and with the
> > high probability of loosing coherence as well, I really don't think
> > it's a good idea to provide such an Unsafe Fixpoint feature by
> > default.
> >
> > Best,
> > Pierre Letouzey
> >
> > --------------------------------------------------------
> > Bug reports: http://logical.futurs.inria.fr/coq-bugs
> > Archives: http://pauillac.inria.fr/pipermail/coq-club
> >         http://pauillac.inria.fr/bin/wilma/coq-club
> > Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>         http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club