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)
