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: Hans Aberg
Subject: Re: A bit further toward the flamewar
Date: Fri, 14 Oct 2011 12:53:51 +0200

On 14 Oct 2011, at 11:28, 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.

If one adds non-termination to the set of all programs, it is not possible to 
make an algorithm that tells exactly which programs that avoid it, though it 
may be possible to prove it for some of them.

> 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].

I was looking at the normalization property*).

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

This is essentially mathematical induction. More general, one might use 
ordinals (I wrote some Haskell code.)

Hans


*)
http://en.wikipedia.org/wiki/Coq
http://en.wikipedia.org/wiki/Calculus_of_inductive_constructions
http://en.wikipedia.org/wiki/Calculus_of_constructions
http://en.wikipedia.org/wiki/Normalization_property_(lambda-calculus)






reply via email to

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