Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] allowing non-structurally terminating functions ?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] allowing non-structurally terminating functions ?


chronological Thread 
  • From: frederic.blanqui AT loria.fr
  • To: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] allowing non-structurally terminating functions ?
  • Date: Sun, 15 Jun 2008 11:32:04 +0200 (CEST)
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
On Fri, 13 Jun 2008, Julien Forest wrote:

On Fri, 13 Jun 2008 11:32:12 +0200 (CEST)
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?

Hello Frederic,

If you do so, you will probably get a inconsistent environment for the
first function you will define without checking its termination (I
agree that for YOU it will probably not be for the first one).

I know that you -may- loose consistency for some non-terminating functions, although I don't think that non-termination -always- implies inconsistency.

But that's why I propose to use an option: a file compiled with this option won't be recognized as a completely safe coq proof. But the user is aware of this.

On the other side, you have now several method to define non structural
functions (Fix, Program Fixpoint and Function are all in the standard
distribution) which leads to reducible functions AND preserve the
consistency of the environment.

These methods are too restrictive. In particular, Function does not support mutually defined functions.

If those methods fails (because the terminaison proof is too hugly or you really don't want to make the proof, why not axiomatize your function with something like:

Axiom f x y z : t.
Axiom f_equation: foral x y z, f x y z = <body of f> ?

This is a good idea. But you cannot use compute in this case.



Archive powered by MhonArc 2.6.16.

Top of Page