guile-user
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: A bit further toward the flamewar


From: Ludovic Courtès
Subject: Re: A bit further toward the flamewar
Date: Fri, 14 Oct 2011 11:28:34 +0200
User-agent: Gnus/5.110018 (No Gnus v0.18) Emacs/24.0.90 (gnu/linux)

Hans Aberg <address@hidden> skribis:

> On 13 Oct 2011, at 23:14, Ludovic Courtès wrote:
>
>> Did you know that Coq would only compile a function when it can prove
>> that it terminates?  That’s another kind of compiler-supported proof one
>> quickly gets used to.
>
> Termination is a non-deducable property. They look at a intuitionistic subset 
> of programs.

Sorry, I’m not sure what you mean.

What I had in mind is what they call “well-founded recursion” [0] and
the idea that a recursive function must have a “decreasing argument” [1].

Thanks,
Ludo’.

[0] http://coq.inria.fr/refman/Reference-Manual005.html#htoc79
[1] http://coq.inria.fr/refman/Reference-Manual003.html#Fixpoint



reply via email to

[Prev in Thread] Current Thread [Next in Thread]