Re: Response to Karen and to Willem on recursive proofs

From: Richard Heathfield (invalid_at_address.co.uk.invalid)
Date: 01/23/04 

Date: Fri, 23 Jan 2004 22:51:18 +0000

Willem wrote:

> Richard wrote:
> ) Willem wrote:
> )
> )> If I wanted to be exact, I would have been a lot more rigorous.
> )> Besides, proving termination is usually quite easy for loops.
> )
> ) Usually, yes. But...
> )
> ) #include "halting.h"
> )
> ) int main(void)
> ) {
> ) if(program_terminates())
> ) {
> ) for(;;)
> ) {
> ) continue;
> ) }
> ) }
> ) return 0;
> ) }
> )
> ) ...there are exceptions. :-)
>
> I think you meant 'while (program_terminates()) { }',

Nope. Sorry for not being clear; I thought it would be self-evident that I
was describing the Halting Problem: program_terminates() reads a program
from stdin and decides whether it halts. The idea is to feed the program to
itself, of course.

> otherwise I can simply prove that the loop doesn't terminate.

In which case, the input program halts, in which case the program above
doesn't halt. But they're the same program!

> What I wanted to say, of course, is that it's usually quite easy to prove
> that a loop terminates if it's designed to terminate. Or whatever sounds
> roughly like what I just said but is actually correct. :-)

I think you actually said it correctly the first time - after all, you
included the weasel-word "usually", which made it all okay. I was just
shooting the moon. 

-- 
Richard Heathfield : binary@eton.powernet.co.uk
"Usenet is a strange place." - Dennis M Ritchie, 29 July 1999.
C FAQ: http://www.eskimo.com/~scs/C-faq/top.html
K&R answers, C books, etc: http://users.powernet.co.uk/eton