Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Do C compilers disprove Fermat's Last Theorem?

blog.regehr.org

Post reply on HN
Print view View original

11–20 of 27 posts

Re: Do C compilers disprove Fermat's Last Theorem?

#11

Post by tetha »

barrkel wrote: post #9
tetha wrote: post #6

Earlier quoted context omitted.

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.

Compare to the reddit-thread and the other comments. I define boring as "without side effects", that is, without io-access, without access to volatile variables and such according to the C-Spec. Boring also is language dependant, of course, as different languages have different side effects.

And yes, as such, I define the theoretically interesting halting problem as practically boring, because I only care about the result my program computes and outputs. If there is no output, there is no output -- not even the possibility of output, no matter if my program runs in less than a second, an hour, a year or infinitely long.

Yes, technically they are differnt programs. Practically, I run the program, notice "What the... how is it so fast?", notice the missing printf in there, add it (while being happy about the change in semantics which saved me several minutes), see the result and do something useful.

Re: Do C compilers disprove Fermat's Last Theorem?

#12

Post by jfoutz »

barrkel wrote: post #9
tetha wrote: post #6

Earlier quoted context omitted.

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.

No, i think he's suggesting knowledge understanding and science as a whole depend on observable side effects. For example, i have a program that does in fact provide a counter example to fermat's last theorem. Unfortunately it does not print the result.

If you deny observable side effects as a requirement, you must accept that i do have a program that does that.

Most cs curriculums cover propositional logic. if you recall the truth table for implication, the false case always evaluates to true. my instructor used to call it the "who cares" case.

If you don't demand a witness for the proposition, the compiler is under no obligation to provide one.

Re: Do C compilers disprove Fermat's Last Theorem?

#13

Post by gojomo »

barrkel wrote: post #4
tetha wrote: post #2

Welcome 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.

The alternate behavior, while initially non-intuitive, seems more useful to me, in usual scenarios. And the grandparent post's taxonomy including the idea of "partial correctness" also seems useful. So you'll have to justify your "must" a bit more.

In particular: a programmer who wants an infinite loop can get one easily enough. Code that is complex, and has no side-effects other than affecting termination, and never terminates is likely to be a bug. As long as users of an optimizer know that it makes this choice -- that this particular pedantic kind of 'correctness' is waived in the face of otherwise side-effect-less code -- it seems an implementor's choice. And lots of competent implementors seem to have chosen the path you say they "must" not do.

Re: Do C compilers disprove Fermat's Last Theorem?

#14

Post by barrkel »

tetha wrote: post #11
barrkel wrote: post #9

Earlier quoted context omitted.

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.

Compare to the reddit-thread and the other comments. I define boring as "without side effects", that is, without io-access, without access to volatile variables and such according to the C-Spec. Boring also is language dependant, of course, as different languages have different side effects. And yes, as such, I define the theoretically interesting halting problem as practically boring, because I only care about the r…

The Halting problem is primarily practically useful in automated program analysis, of which the most common instance is compiler optimizers.

I'm loathe to reference Wikipedia as an authority, but it's even quoted there as part of a proof as to why compilers cannot optimize programs as much as might be possible:

http://en.wikipedia.org/wiki/Compiler_optimization

However, optimizing compilers are by no means perfect. There is no way that a compiler can guarantee that, for all program source code, the fastest (or smallest) possible equivalent compiled program is output; such a compiler is fundamentally impossible because it would solve the halting problem.

This may be proven by considering a call to a function, foo(). This function returns nothing and does not have side effects (no I/O, does not modify global variables and "live" data structures, etc.). The fastest possible equivalent program would be simply to eliminate the function call. However, if the function foo() in fact does not return, then the program with the call to foo() would be different from the program without the call; the optimizing compiler will then have to determine this by solving the halting problem.

Re: Do C compilers disprove Fermat's Last Theorem?

#15

Post by barrkel »

jfoutz wrote: post #12
barrkel wrote: post #9

Earlier quoted context omitted.

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.

No, i think he's suggesting knowledge understanding and science as a whole depend on observable side effects. For example, i have a program that does in fact provide a counter example to fermat's last theorem. Unfortunately it does not print the result. If you deny observable side effects as a requirement, you must accept that i do have a program that does that. Most cs curriculums cover propositional logic. if you r…

I find it somewhat difficult to believe we're having this conversation in any seriousness.

Consider this program fragment:

    for (;;)
        /* do nothing */;
    destroy_the_world(); /* has side-effects */
Would you say that a compiler that removed the loop changed the side-effects of the program?

Re: Do C compilers disprove Fermat's Last Theorem?

#16

Post by barrkel »

gojomo wrote: post #13
barrkel wrote: post #4

Earlier 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.

The alternate behavior, while initially non-intuitive, seems more useful to me, in usual scenarios. And the grandparent post's taxonomy including the idea of "partial correctness" also seems useful. So you'll have to justify your " must " a bit more. In particular: a programmer who wants an infinite loop can get one easily enough. Code that is complex, and has no side-effects other than affecting termination, and nev…

If you accept the grandparent's argument on face value, you should accept that a compiler should be able to remove other do-nothing infinite loops, like in the example I mentioned elsewhere:

    for (;;)
        /* do nothing */;
    destroy_the_world(); /* has side-effects */
Why should a compiler remove the loop in the OP's case, but not remove the loop above? Do you accept that removing the loop changes the side-effects of the program?

Re: Do C compilers disprove Fermat's Last Theorem?

#17

Post by neilc »

barrkel wrote: post #10
neilc wrote: post #8

Earlier quoted context omitted.

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 pa…

That an optimizer assumes without proof a solution to the halting problem for some sub-program would mean that it's an unreliable translator

The optimizer doesn't need to solve the halting problem for this example. It merely needs to prove that any iteration of the loop has no side effects; hence, an unbounded number of loop iterations also has no side effects, and the loop can be removed.

The real issue is whether termination is considered a side effect. The canon is the C spec; if you can point to some language in the spec that would prevent the optimization, I'd love to see it.

Update: on reflection, I think you're right. The point isn't that the loop has side-effects (it obviously doesn't); but by changing the termination behavior of the loop, the compiler is likely to induce additional side effects (when it runs the subsequent code).

Re: Do C compilers disprove Fermat's Last Theorem?

#18

Post by _delirium »

barrkel wrote: post #15
jfoutz wrote: post #12

Earlier quoted context omitted.

No, i think he's suggesting knowledge understanding and science as a whole depend on observable side effects. For example, i have a program that does in fact provide a counter example to fermat's last theorem. Unfortunately it does not print the result. If you deny observable side effects as a requirement, you must accept that i do have a program that does that. Most cs curriculums cover propositional logic. if you r…

I find it somewhat difficult to believe we're having this conversation in any seriousness. Consider this program fragment: for (;;) /* do nothing */; destroy_the_world(); /* has side-effects */ Would you say that a compiler that removed the loop changed the side-effects of the program?

Yes, but in what vaguely reasonable circumstances would you write dead code whose deadness depends on the fact that an infinite loop precedes it? The fact that the C standard doesn't consider changing termination properties from nonterminating to terminating to be an impermissible optimization seems reasonably practical.

The only thing I can guess at would be something in embedded-land that's using nonterminating loops as some sort of control-flow construct.

Re: Do C compilers disprove Fermat's Last Theorem?

#19

Post by barrkel »

_delirium wrote: post #18
barrkel wrote: post #15

Earlier quoted context omitted.

I find it somewhat difficult to believe we're having this conversation in any seriousness. Consider this program fragment: for (;;) /* do nothing */; destroy_the_world(); /* has side-effects */ Would you say that a compiler that removed the loop changed the side-effects of the program?

Yes, but in what vaguely reasonable circumstances would you write dead code whose deadness depends on the fact that an infinite loop precedes it? The fact that the C standard doesn't consider changing termination properties from nonterminating to terminating to be an impermissible optimization seems reasonably practical. The only thing I can guess at would be something in embedded-land that's using nonterminating loo…

Reasonable has nothing much to do with it, IMO; and I'm not really talking about C (it is only an example), but about compiler optimizers.

Re: Do C compilers disprove Fermat's Last Theorem?

#20

Post by barrkel »

neilc wrote: post #17
barrkel wrote: post #10

Earlier quoted context omitted.

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 pa…

That an optimizer assumes without proof a solution to the halting problem for some sub-program would mean that it's an unreliable translator The optimizer doesn't need to solve the halting problem for this example. It merely needs to prove that any iteration of the loop has no side effects; hence, an unbounded number of loop iterations also has no side effects, and the loop can be removed. The real issue is whether t…

But a loop that never exits will never continue on to the rest of the program, which will never have its side-effects.

This loop has no side-effects:

    for (;;)
        /* do nothing */;
So the compiler, according to the spec, can remove it, right?

    for (;;)
        /* do nothing */;
    destroy_the_world(); /* has side-effects */
So will the world be destroyed? Or is the following code dead? In which case, it's not OK for the compiler to remove loops that have no side-effects.
Post reply on HN