Do C compilers disprove Fermat's Last Theorem?
blog.regehr.org
Do C compilers disprove Fermat's Last Theorem?
1–10 of 27 posts
Re: Do C compilers disprove Fermat's Last Theorem?
#2Welcome to the world of compiler optimization. A compiler optimization has to preserve all side effects of a program. This is pretty similar to partial correctness.
Partial correctness means: This code computes the right thing whenever it terminates. It is a subset of total correctness, which states: This code terminates given the precondition and also computes the right then whenever it terminates.
In his case, the first loop had a simple side effect: None. Thus it was a correct optimization to replace the code with nothing. Fixes would include adding volatile to a variable, returning the variables as he did, printing something, ...
Re: Do C compilers disprove Fermat's Last Theorem?
#3Proggit had a lively discussion on this earlier today: http://www.reddit.com/r/programming/comments/byilp/c_compile...
Re: Do C compilers disprove Fermat's Last Theorem?
#4Welcome to the world of compiler optimization. A compiler optimization has to preserve all side effects of a program. This is pretty similar to partial correctness. Partial correctness means: This code computes the right thing whenever it terminates. It is a subset of total correctness, which states: This code terminates given the precondition and also computes the right then whenever it terminates. In his case, the…
Termination is an observable side-effect of a program. It is not a correct compiler optimization to turn a non-terminating program into a terminating one. Turing completeness is the black box beyond which a compiler's optimizer cannot see past, and it must, for correctness' sake, must give up when it cannot prove termination.
Re: Do C compilers disprove Fermat's Last Theorem?
#5I can't say I've tried it, but shouldn't this be enough to avoid the optimization?
volatile int i=1;
while (i) { }Re: Do C compilers disprove Fermat's Last Theorem?
#6Welcome to the world of compiler optimization. A compiler optimization has to preserve all side effects of a program. This is pretty similar to partial correctness. Partial correctness means: This code computes the right thing whenever it terminates. It is a subset of total correctness, which states: This code terminates given the precondition and also computes the right then whenever it terminates. In his case, the…
Termination is an observable side-effect of a program. It is not a correct compiler optimization to turn a non-terminating program into a terminating one. Turing completeness is the black box beyond which a compiler's optimizer cannot see past, and it must , for correctness' sake, must give up when it cannot prove termination.
That is correct. However, in reality, a program whose only side effect is to terminate (or not terminate) is boring enough to be considered an edge case and changed.
Re: Do C compilers disprove Fermat's Last Theorem?
#7I can't say I've tried it, but shouldn't this be enough to avoid the optimization? volatile int i=1; while (i) { }
Being volatile, i can change in ways which cannot be deduced from the program code.
Thus, the loop loops until something which cannot be deduced from the program code happens.
Thus, yes.
Re: Do C compilers disprove Fermat's Last Theorem?
#8Welcome to the world of compiler optimization. A compiler optimization has to preserve all side effects of a program. This is pretty similar to partial correctness. Partial correctness means: This code computes the right thing whenever it terminates. It is a subset of total correctness, which states: This code terminates given the precondition and also computes the right then whenever it terminates. In his case, the…
Termination is an observable side-effect of a program. It is not a correct compiler optimization to turn a non-terminating program into a terminating one. Turing completeness is the black box beyond which a compiler's optimizer cannot see past, and it must , for correctness' sake, must give up when it cannot prove termination.
Termination is an observable side-effect of a program
Not per the C99 spec, at least (5.1.2.3: "Accessing a volatile object, modifying an object, modifying a file, or calling a function that does any of those operations are all side effects, which are changes in the state of the execution environment.")
Termination is "observable", but so is runtime, memory consumption, code size, and myriad other properties that a compiler is at liberty to manipulate.
Turing completeness is the black box beyond which a compiler's optimizer cannot see past, and it must, for correctness' sake, must give up when it cannot prove termination.
Correctness according to what standard?
Re: Do C compilers disprove Fermat's Last Theorem?
#9Earlier quoted context omitted.
Termination is an observable side-effect of a program. It is not a correct compiler optimization to turn a non-terminating program into a terminating one. Turing completeness is the black box beyond which a compiler's optimizer cannot see past, and it must , for correctness' sake, must give up when it cannot prove termination.
That is correct. However, in reality, a program whose only side effect is to terminate (or not terminate) is boring enough to be considered an edge case and changed.
I don't think "boring" is the right technical term; are you suggesting that the halting problem itself is boring, since it explicitly only relates to whether programs terminate or not?
The compiler is not privileged enough to state what is boring and what isn't. The example program calculates something meaningful - if it terminated, it would mean that there was a solution found, contrary to Fermat's theorem.
Re: Do C compilers disprove Fermat's Last Theorem?
#10Earlier quoted context omitted.
Termination is an observable side-effect of a program. It is not a correct compiler optimization to turn a non-terminating program into a terminating one. Turing completeness is the black box beyond which a compiler's optimizer cannot see past, and it must , for correctness' sake, must give up when it cannot prove termination.
Termination is an observable side-effect of a program Not per the C99 spec, at least (5.1.2.3: "Accessing a volatile object, modifying an object, modifying a file, or calling a function that does any of those operations are all side effects, which are changes in the state of the execution environment.") Termination is "observable", but so is runtime, memory consumption, code size, and myriad other properties that a c…
Re C99 - the existence of an execution environment is certainly observable (it'll disappear with respect to the program when the program terminates), unless you try to argue that exit(0) has no observable side-effects according to the C standard, and thus we should expect code following exit(0) to also be executed, where I think we would be entering absurdity.
Re correctness: That the compiler optimizer cannot see past the halting problem is a general fact about compiler analysis, which you should be familiar with from most introductions to compiler theory. That an optimizer assumes without proof a solution to the halting problem for some sub-program would mean that it's an unreliable translator, because it is making unsound assumptions.
Of course, if your define your language such that it's OK to make unsound assumptions, that's another matter.