slight differences between non-termination and failure

From: Sebastian Fischer <sebf_at_informatik.uni-kiel.de>
Date: Wed, 02 Feb 2011 18:06:23 +0900

Hello,

I have defined three slightly different Curry functions, expected all of
them to be equivalent, found that two fail while one of them does not
terminate, and wonder why. Although non-termination and failure are usually
considered equivalent in Curry I am still interested in what causes the
different behavior. As both PAKCS and MCC behave in the same way, I may be
missing something and like to learn what.

Here are the functions:

foo [x] xs = x:y:ys
 where
  y:ys = foo [x] xs

bar [x] xs = extend (bar [x] xs)
 where
  extend (y:ys) = x:y:ys

baz [x] xs = extend (baz [x] xs)
 where
  extend ys = x:ys

While the goals

    foo [1] l =:= [1] where l free
    baz [1] l =:= [1] where l free

fail in finite time, the goal

    bar [1] l =:= [1] where l free

does not terminate. This is especially surprising because I thought that
'foo' is translated into something similar to 'bar' when eliminating local
pattern bindings.

Can somebody explain the difference?

Sebastian



_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Wed Feb 02 2011 - 11:42:22 CET

This archive was generated by hypermail 2.3.0 : Thu Sep 19 2019 - 07:15:08 CEST