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
[email protected]
http://www.haskell.org/mailman/listinfo/haskell
