[Top][All Lists]
[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)
- Re: A bit further toward the flamewar, (continued)
- Re: A bit further toward the flamewar, Hans Aberg, 2011/10/13
- Re: A bit further toward the flamewar, Panicz Maciej Godek, 2011/10/14
- Re: A bit further toward the flamewar, Ludovic Courtès, 2011/10/13
- Re: A bit further toward the flamewar, rixed, 2011/10/13
- Re: A bit further toward the flamewar, Ludovic Courtès, 2011/10/13
- Re: A bit further toward the flamewar, Hans Aberg, 2011/10/13
- Re: A bit further toward the flamewar, Ludovic Courtès, 2011/10/14
- Re: A bit further toward the flamewar,
Hans Aberg <=
- Re: A bit further toward the flamewar, rixed, 2011/10/14
- Re: A bit further toward the flamewar, Ludovic Courtès, 2011/10/14
Re: Why is guile still so slow?, Andy Wingo, 2011/10/12
Re: Why is guile still so slow?, John Lewis, 2011/10/12