Jim Apple wrote:
On 9/11/06, Neil Mitchell <ndmitchell@gmail.com> 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