Comment
Comment by a1369209993
Do you mean `x = slow_function_no_side_effects( x );`?
Because if slow_function_no_side_effects really doesn't have side effects, then your version is equivalent to:
That said, I suppose it might be reasonable to explicitly note that a optimiser is allowed to make a program or subroutine complete in less time than it otherwise would, even that reduces the execution time from infinite to finite. That doesn't imply inferring any new facts about the program - either loop termination or otherwise - though. On the other hand it might be better to not allow that; you could make a case that the optimisation you describe is a algorithmic change, and if the programmer wants better performance, they need to write:
, just the same as if they wanted their sorting algorithm to complete in linear time on already-sorted inputs.