Re: [Haskell] Re: ANN: Haskell98 termination analyzer (AProVE)
Jim Apple wrote: On 9/11/06, Neil Mitchell [EMAIL PROTECTED] wrote: Can you give any examples of terminating Haskell programs that a human can analyse (perhaps with a bit of thought), but that your system can't? (I couldn't find any in your paper) Euclid's algorithm is mentioned on the web page, if I remember correctly. Unfortunately, we are unable to show the termination of the gcd function as definied in the Hugs Prelude. But we could show the termination of this slightly modified version: igcd :: Int - Int - Int igcd x y = igcd' (abs x) (abs y) igcd' :: Int - Int - Int igcd' 0 x = x igcd' y 0 = y igcd' (x+1) (y+1) | x y = igcd' (x-y) (y+1) | otherwise = igcd' (y-x) (x+1) So not only the algorithm itself is important; also the way it is written is sometimes essential for proving termination. Best regards, Stephan ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Re: ANN: Haskell98 termination analyzer (AProVE)
Ashley Yakeley wrote: Cool! So are there an infinite number of twin primes or not? Good one. Wish I knew ;-) Any (correct) termination analyzer is, of course, incomplete as the halting problem is undecidable. Our goal is to handle as many typical/practical/easy programs as possible. One should certainly not expect automatic tools to solve open problems from mathematics that can be encoded as termination problems. By the way, if you want to make automatic termination analyzers fail, then you should also try the most famous open termination problem: syra :: Int - Int syra x | x = 1 = x | True = if even x then syra (div x 2) else syra (3 * x + 1) Best regards, Peter -- Peter Schneider-Kamp mailto:[EMAIL PROTECTED] LuFG Informatik II http://www-i2.informatik.rwth-aachen.de/~nowonder RWTH Aachenphone: ++49 241 80-21211 ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Re: ANN: Haskell98 termination analyzer (AProVE)
Hi Peter, Any (correct) termination analyzer is, of course, incomplete as the halting problem is undecidable. Our goal is to handle as many typical/practical/easy programs as possible. Can you give any examples of terminating Haskell programs that a human can analyse (perhaps with a bit of thought), but that your system can't? (I couldn't find any in your paper) Thanks Neil ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Re: ANN: Haskell98 termination analyzer (AProVE)
On 9/11/06, Neil Mitchell [EMAIL PROTECTED] wrote: Can you give any examples of terminating Haskell programs that a human can analyse (perhaps with a bit of thought), but that your system can't? (I couldn't find any in your paper) Euclid's algorithm is mentioned on the web page, if I remember correctly. Jim ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Re: ANN: Haskell98 termination analyzer (AProVE)
Stephan Swiderski wrote: Dear all, we are pleased to announce the integration of an automatic Haskell98 termination analyzer Cool! So are there an infinite number of twin primes or not? -- Ashley Yakeley Seattle, WA ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Re: ANN: Haskell98 termination analyzer (AProVE)
On Fri, 2006-09-08 at 17:03 -0700, Ashley Yakeley wrote: . . . Cool! So are there an infinite number of twin primes or not? We await the response with bated breath. On second thought, maybe that's not a good idea ... -- Bill Wood ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Re: ANN: Haskell98 termination analyzer (AProVE)
On 9/8/06, Bill Wood [EMAIL PROTECTED] wrote: We await the response with bated breath. Don't hold your breath. -- Taral [EMAIL PROTECTED] You can't prove anything. -- Gödel's Incompetence Theorem ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
