ANN: Haskell98 termination analyzer (AProVE)
Dear all, we are pleased to announce the integration of an automatic Haskell98 termination analyzer in the termination tool AProVE [1]. Our tool accepts full Haskell as specified in the Haskell 98 Report and is available through our web interface [2]. USE Our tool checks termination of given start terms w.r.t. a Haskell program. A start term is a Haskell term accepted by the command line of Haskell interpreters like GHCi or Hugs. Moreover, start terms may contain free variables representing arbitrary terminating terms. EXAMPLE For example the start term "take x (repeat y)" can be proved terminating (where "take" and "repeat" are defined in the Haskell prelude). On the other hand, the start term "repeat y" does not terminate, because the function "repeat" generates the infinite list of "y"s. For more details on our approach see [3]. EXPERIMENTS We evaluated our tool on standard libraries (Prelude, List, ...) of the Hugs implementation. In this setting we could show the termination of almost 80 percent of 1281 start terms resulting from these libraries. More details on the evaluation can be found in [4]. FEEDBACK We would be grateful for comments and suggestions on our tool or on our approach. Please send them to: aprove@i2.informatik.rwth-aachen.de Stephan Swiderski, Jürgen Giesl, Peter Schneider-Kamp, René Thiemann [1] AProVE home page: http://aprove.informatik.rwth-aachen.de [2] web interface: http://aprove.informatik.rwth-aachen.de/index.asp?subform=termination_proofs... [3] RTA06 paper: http://aprove.informatik.rwth-aachen.de/eval/Haskell/RTA06-distribute.ps [4] experimental evaluation: http://aprove.informatik.rwth-aachen.de/eval/Haskell/
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@informatik.rwth-aachen.de LuFG Informatik II http://www-i2.informatik.rwth-aachen.de/~nowonder RWTH Aachen phone: ++49 241 80-21211
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
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. Jim
participants (7)
-
Ashley Yakeley -
Bill Wood -
Jim Apple -
Neil Mitchell -
Peter Schneider-Kamp -
Stephan Swiderski -
Taral