Hi
1) The programmer has to detail in some form the proof that his program
terminates. Arguably, he ought to do so anyway but he doesn't need to
write his proof in a way that can be checked by a dumb computer. Take
for example
minimum = head . sort
minimum [1..] gives _|_ non-termination
miniumum [1,_|_,3] gives _|_ while head [1,_|_,3] doesn't.
Termination is all a bit more complex once you get to laziness.
Thanks
Neil
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
