Can anybody give me a simple explanation why the second definition of a palindrome checker does not terminate, although the first one does? pal :: Eq a => [a] -> Bool pal s = b where (b,r) = eqrev s r [] eqrev :: Eq a => [a] -> [a] -> [a] -> (Bool,[a]) eqrev (x:s1) ~(y:s2) acc = (x==y&&b,r) where (b,r) = eqrev s1 s2 (x:acc) eqrev _ _ acc = (True,acc) pal :: Eq a => [a] -> Bool pal s = b where (b,r) = eqrev' s r eqrev' :: Eq a => [a] -> [a] -> (Bool,[a]) eqrev' (x:s1) ~(y:s2) = (x==y&&b,r++[y]) where (b,r) = eqrev' s1 s2 eqrev' _ _ = (True,[]) Peter
On Wed, 6 Feb 2008, Peter Padawitz wrote:
Can anybody give me a simple explanation why the second definition of a palindrome checker does not terminate, although the first one does?
Just another question, what about x == reverse x ? - You can still optimize for avoiding duplicate equality tests.
On 6 Feb 2008, at 16:32, Peter Padawitz wrote:
Can anybody give me a simple explanation why the second definition of a palindrome checker does not terminate, although the first one does?
pal :: Eq a => [a] -> Bool pal s = b where (b,r) = eqrev s r []
eqrev :: Eq a => [a] -> [a] -> [a] -> (Bool,[a]) eqrev (x:s1) ~(y:s2) acc = (x==y&&b,r) where (b,r) = eqrev s1 s2 (x:acc) eqrev _ _ acc = (True,acc)
I. eqrev "" (_|_) acc = (True, acc) II.a. eqrev "1" (_|_) "" = ('1' == (_|_) && b, r) where (b,r) = eqrev "" (_|_) "1" By (I), (b,r) = (True, "1"), so eqrev "1" (_|_) "" = ((_|_),"1") II.b. eqrev "1" "1" "" = ('1' == '1' && b, r) where (b,r) = eqrev "" "" "1" (b,r) = (True,"1"), so eqrev "1" "1" "" = (True,"1") Therefore, the least fixed point of \r -> eqrev "1" r "" is "1" and the answer is True.
pal :: Eq a => [a] -> Bool pal s = b where (b,r) = eqrev' s r
eqrev' :: Eq a => [a] -> [a] -> (Bool,[a]) eqrev' (x:s1) ~(y:s2) = (x==y&&b,r++[y]) where (b,r) = eqrev' s1 s2 eqrev' _ _ = (True,[])
I. eqrev' "" (_|_) = (True,[]) II.a. eqrev' "1" (_|_) = ('1' == (_|_) && b, r ++ [(_|_)]) where (b,r) = eqrev' "" (_|_) By (I), (b,r) = (True,[]), so eqrev' "1" (_|_) = ((_|_),[(_|_)]) II.b. eqrev' "1" [(_|_)] = ('1' == (_|_) && b, r ++ [(_|_)]) where (b,r) = eqrev' "" [] (b,r) = (True,[]), so eqrev' "1" [(_|_)] = ((_|_),[(_|_)]) Therefore, the least fixed point of \r -> eqrev' "1" r is [(_|_)] and the answer is (_|_). No wonder it hangs.
On Feb 6, 2008 3:06 PM, Miguel Mitrofanov
On 6 Feb 2008, at 16:32, Peter Padawitz wrote:
Can anybody give me a simple explanation why the second definition of a palindrome checker does not terminate, although the first one does?
pal :: Eq a => [a] -> Bool pal s = b where (b,r) = eqrev s r []
eqrev :: Eq a => [a] -> [a] -> [a] -> (Bool,[a]) eqrev (x:s1) ~(y:s2) acc = (x==y&&b,r) where (b,r) = eqrev s1 s2 (x:acc) eqrev _ _ acc = (True,acc)
I. eqrev "" (_|_) acc = (True, acc) II.a. eqrev "1" (_|_) "" = ('1' == (_|_) && b, r) where (b,r) = eqrev "" (_|_) "1" By (I), (b,r) = (True, "1"), so eqrev "1" (_|_) "" = ((_|_),"1") II.b. eqrev "1" "1" "" = ('1' == '1' && b, r) where (b,r) = eqrev "" "" "1" (b,r) = (True,"1"), so eqrev "1" "1" "" = (True,"1")
Therefore, the least fixed point of \r -> eqrev "1" r "" is "1" and the answer is True.
pal :: Eq a => [a] -> Bool pal s = b where (b,r) = eqrev' s r
eqrev' :: Eq a => [a] -> [a] -> (Bool,[a]) eqrev' (x:s1) ~(y:s2) = (x==y&&b,r++[y]) where (b,r) = eqrev' s1 s2 eqrev' _ _ = (True,[])
I. eqrev' "" (_|_) = (True,[]) II.a. eqrev' "1" (_|_) = ('1' == (_|_) && b, r ++ [(_|_)]) where (b,r) = eqrev' "" (_|_) By (I), (b,r) = (True,[]), so eqrev' "1" (_|_) = ((_|_),[(_|_)]) II.b. eqrev' "1" [(_|_)] = ('1' == (_|_) && b, r ++ [(_|_)]) where (b,r) = eqrev' "" [] (b,r) = (True,[]), so eqrev' "1" [(_|_)] = ((_|_),[(_|_)]) Therefore, the least fixed point of \r -> eqrev' "1" r is [(_|_)] and the answer is (_|_). No wonder it hangs.
This proof also shows us where the problem lies and how to fix it. It turns out to be really easy: change 'r++[y]' to 'r++[x]' and the program works. Cheers, Josef
@ Miguel: Thanks for carrying out the fixpoint computation I was too lazy to do! I see: lazy evaluation programmers must not be lazy ;-) @ Josef: Oh yes, I mixed up x and y! In fact, I was confused about the semantical difference between eqrev and eqrev', although eqrev is just an iterative version of eqrev' -- if x and y were not mixed up. Peter Peter Padawitz wrote:
Can anybody give me a simple explanation why the second definition of a palindrome checker does not terminate, although the first one does?
pal :: Eq a => [a] -> Bool pal s = b where (b,r) = eqrev s r []
eqrev :: Eq a => [a] -> [a] -> [a] -> (Bool,[a]) eqrev (x:s1) ~(y:s2) acc = (x==y&&b,r) where (b,r) = eqrev s1 s2 (x:acc) eqrev _ _ acc = (True,acc)
pal :: Eq a => [a] -> Bool pal s = b where (b,r) = eqrev' s r
eqrev' :: Eq a => [a] -> [a] -> (Bool,[a]) eqrev' (x:s1) ~(y:s2) = (x==y&&b,r++[y]) where (b,r) = eqrev' s1 s2 eqrev' _ _ = (True,[])
participants (4)
-
Henning Thielemann -
Josef Svenningsson -
Miguel Mitrofanov -
Peter Padawitz