coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [Coq-Club] allowing non-structurally terminating functions ?, frederic . blanqui
- Re: [Coq-Club] allowing non-structurally terminating functions ?, Johannes Waldmann
- Re: [Coq-Club] allowing non-structurally terminating functions ?, Julien Forest
- Re: [Coq-Club] allowing non-structurally terminating functions ?, frederic . blanqui
- [Coq-Club] Re: allowing non-structurally terminating functions ?,
frederic . blanqui
- Re: [Coq-Club] Re: allowing non-structurally terminating functions ?,
Matthieu Sozeau
- Re: [Coq-Club] Re: allowing non-structurally terminating functions ?, Arnaud Spiwack
- Re: [Coq-Club] Re: allowing non-structurally terminating functions ?, Pierre Letouzey
- Re: [Coq-Club] Re: allowing non-structurally terminating functions ?,
Matthieu Sozeau
Archive powered by MhonArc 2.6.16.