coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] totality and consistency
- Date: Mon, 10 Feb 2014 19:01:42 +0100
Try
(it doesn't actually loop with [let '_ := …] but that's a technicality)Fixpoint f (x:nat) : nat := let y := f x in 0.
Eval compute in f 0.
Eval compute in f 0.
Arnaud
On 10 February 2014 15:28, Matthieu Sozeau <matthieu.sozeau AT gmail.com> wrote:
Hi all,
Termination is checked on a beta-let-hnf of the term (BTW, we don’t know it is normalizing yet…),
and the term in the kernel is this hnf (right?). So we’re not loosing SN in the kernel actually,
even though it looks like only cbn reduction is strongly normalizing due to this “feature” if
I’m not mistaken. For example:
For
and
Fixpoint f (x:nat) : nat := let '_ := f x in 0.
Fixpoint f (x:nat) : nat := match f x with _ => 0 end.
the hnf of the elaborated term is 0. While
Fixpoint f (x:nat) : nat := match f x with 0 => 0 | S n => 0 end.
is not accepted as the match is kept by the elaboration.
Best,
— Matthieu
On 10 févr. 2014, at 14:16, Kirill Taran <kirill.t256 AT gmail.com> wrote:
> Arnaud, Frederic,
>
> Thanks for elaborations.
>
> > Fixpoint f (x:nat) : nat := let '_ := f x in 0.
> Why it is allowed? Doesn't argument have to decrease on recursive call?
>
> Sincerely,
> Kirill Taran
>
>
> On Mon, Feb 10, 2014 at 2:45 PM, Arnaud Spiwack <aspiwack AT lix.polytechnique.fr> wrote:
> To elaborate on Frédéric's answer, termination is a technique to prove consistency. It goes like that:
> • If there is a closed proof of ⊥, then we can find a closed proof of ⊥ in normal form
> • Closed normal-form proofs start with an introduction rule
> • ⊥ has no introduction rule
> Note that we only need weak normalisation. In fact, we can settle with something weaker (like a semantic proof of cut elimination, which doesn't imply the existence of a set of terminating rewriting rules, I believe Olivier Hermant's PhD thesis was on the subject of such proofs). Strong normalisation, whereby every rewriting strategy terminates, is a much stronger result (at least in principle as there is a conjecture, originally by Klop I believe, that every weakly normalising PTS is strongly normalising, there are some thoughts on this conjecture in Denis Cousineau's PhD thesis). Proof theorists tend to favour strong normalisation result over consistency.
>
> This is what makes the fact that Coq accepts the following definition
>
> Fixpoint f (x:nat) : nat := let '_ := f x in 0.
>
> a (long standing) minor bug: it makes Coq only weakly normalising (which is a bug), but it doesn't threaten consistency (which prevents it from being a serious bug).
>
>
>
> On 10 February 2014 10:34, Frédéric Blanqui <frederic.blanqui AT inria.fr> wrote:
> Hi.
>
> I would answer that it depends. Guillaume provides an example of looping function in False. Then, of course, you can build a proof of False. But what if f is in nat? Then problems may arise if you can prove that 0=1. Define for instance f by f x = S (f x). So, I am not sure that non-termination always leads to inconsistency, especially if you restrict type dependencies to terminating terms (but it is not decidable...). See for instance the works of Constable et al on partial functions in constructive type theory, and the NuPRL proof assistant.
>
> Best regards,
>
> Frédéric.
>
> Le 08/02/2014 12:19, Guillaume Melquiond a écrit :
>
> On 08/02/2014 12:05, Kirill Taran wrote:
>
> Is it true that if we had possibility to write non-terminating programs
> (suppose we don't use non-terminating term in types, so type check
> terminates) then we would have possibility to prove everything?
>
> Fixpoint f (x : unit) : False := f x.
> Goal False. exact (f tt). Qed.
>
> Best regards,
>
> Guillaume
>
>
>
>
- [Coq-Club] totality and consistency, Kirill Taran, 02/08/2014
- Re: [Coq-Club] totality and consistency, Guillaume Melquiond, 02/08/2014
- Re: [Coq-Club] totality and consistency, Kirill Taran, 02/08/2014
- Re: [Coq-Club] totality and consistency, Frédéric Blanqui, 02/10/2014
- Re: [Coq-Club] totality and consistency, Arnaud Spiwack, 02/10/2014
- Re: [Coq-Club] totality and consistency, Kirill Taran, 02/10/2014
- Re: [Coq-Club] totality and consistency, Matthieu Sozeau, 02/10/2014
- Re: [Coq-Club] totality and consistency, Arnaud Spiwack, 02/10/2014
- Re: [Coq-Club] totality and consistency, Greg Morrisett, 02/10/2014
- Re: [Coq-Club] totality and consistency, Guillaume Melquiond, 02/10/2014
- Re: [Coq-Club] totality and consistency, Kirill Taran, 02/11/2014
- Re: [Coq-Club] totality and consistency, Greg Morrisett, 02/12/2014
- Re: [Coq-Club] totality and consistency, Mitchell Wand, 02/12/2014
- Re: [Coq-Club] totality and consistency, Greg Morrisett, 02/12/2014
- Re: [Coq-Club] totality and consistency, Arnaud Spiwack, 02/12/2014
- Re: [Coq-Club] totality and consistency, Matthieu Sozeau, 02/12/2014
- Re: [Coq-Club] totality and consistency, Bruno Barras, 02/12/2014
- Re: [Coq-Club] totality and consistency, Matthieu Sozeau, 02/12/2014
- Re: [Coq-Club] totality and consistency, Arnaud Spiwack, 02/10/2014
- Re: [Coq-Club] totality and consistency, Matthieu Sozeau, 02/10/2014
- Re: [Coq-Club] totality and consistency, Kirill Taran, 02/10/2014
- Re: [Coq-Club] totality and consistency, Arnaud Spiwack, 02/10/2014
- Re: [Coq-Club] totality and consistency, Guillaume Melquiond, 02/08/2014
Archive powered by MHonArc 2.6.18.