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

[Peter Schneider-Kamp]

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:psk at informatik.rwth-aachen.de
LuFG Informatik II     http://www-i2.informatik.rwth-aachen.de/~nowonder
RWTH Aachen            phone: ++49 241 80-21211