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: Julien Forest <forest AT ensiie.fr>
  • To: frederic.blanqui AT loria.fr
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] allowing non-structurally terminating functions ?
  • Date: Fri, 13 Jun 2008 19:20:02 +0200
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=date:from:to:cc:subject:message-id:in-reply-to:references :organization:x-mailer:mime-version:content-type :content-transfer-encoding:sender; b=oV8dv3A60+NDg3YwzjgWU9rCCG0/+9qmLvxoKtNYZ7F1P9TUU+SbjQR6K87xx1ipZJ cj9tEDBGojcQ3u9u8E9MQklorbYN2B5GeQbXZZASq4BFX4+f+6Er2BOrLHT61C6O3t30 fa9PsUtKEE3/VFyKzskXAcGmpawQwdEackMQY=
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
  • Organization: CNAM
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?
> 
> --------------------------------------------------------
> 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
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). 

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. 

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> ?

Julien.



Archive powered by MhonArc 2.6.16.

Top of Page