24 Jun
2007
24 Jun
'07
7:36 a.m.
Neil Mitchell wrote:
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.
Oops, the example was not meant for termination but for the invariants. I wanted to say that the code of minimum is likely to be shorter than a computer-checkable proof that shows that its result is indeed the smallest element from the list. Regards, apfelmus