[Haskell] Re: ANN: Haskell98 termination analyzer (AProVE)

[Stephan Swiderski]

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