With some programming languages and computation models, you could even say that optimizing programs is the same as running them — just with a subset of computation rules. Then, if you allow enough optimizations to happen, it is clear that optimization faces the same non-termination problems as running programs.
Let me elaborate on my claim by providing a concrete example of a made-up language and its computational semantics.
Consider the following source code of a very primitive imperative language .
i := 0;;
IF (i == 0) do:
WHILE true do:
i := i + (1 + 1) ;;
i := i + 3
I hope the language grammar becomes clear from the above sample. It supports statements such as assignments
variable name := ..., if conditions
IF ... do:, while loops
WHILE ... do:), and concatenated statements
... ;; .... Moreoever, it allows scalar expressions such as boolean conditions
... == ...,
false, and simple arithmetic like
... + 3 within some of the previous statements.
Evaluation by Rules
Let us now invent a computational semantics for running such programs. Concretely, we will do so in terms of small-step semantics, i.e. a binary evaluation relation between contextual statements: we write
p,Γ ⤳ p',Γ' if program
p with variable states
Γ transitions (computes, evaluates) to program
p' with variable states
Then, the interpreter for our language works as follows: upon a program
p, it picks the default start state for variables
Γ_ini and tries reducing it as long as possible:
p,Γ_ini ⤳ p',Γ' ⤳ p'',Γ'' ⤳ ... ⤳ RET
Hopefully, this ends with a special program
RET denoting termination. But it may very well happen that running does not terminate at all. For instance, our sample program invokes such non-terminating behavior — at least with the (intuitive) semantics we give next.
We give the following rules on statements, where
T are meta variables for statements,
E' are meta variables for expressions, and
Γ a meta variable for contexts, and all of them are implicitly all-quantified.
S,Γ ⤳ S',Γ', then
(S ;; T),Γ ⤳ (S' ;; T),Γ'
(SKIP ;; S),Γ ⤳ S,Γ
E,Γ ⇝ E', then
(X := E),Γ ⤳ (X := E'),Γ
E,Γ ⇝ E', then
(IF E do S),Γ ⤳ (IF E' do: S),Γ
(IF true do: S),Γ ⤳ S,Γ
(IF false do: S),Γ ⤳ SKIP,Γ
(WHILE E do: S),Γ ⤳ (IF E do: S ;; WHILE E do: S),Γ
where ⇝ is a similar small-step relation on expressions that I omit here. There,
E,Γ ⇝ E' means that expression
E in context
Γ transitions to expression
E'. Note that since expressins cannot change variable state in our language, we omit the context
Γ on the right-hand side of ⇝.
Optimization by Restricted Evaluation
How can we now formulate optimization rules for our language? For instance, our intuition demands that in the program above the statement
IF (i == 0) do: SKIP optimize to nothing.
It turns out we can achieve this with the very same tool of small-step semantics. For our purposes, we give the following set of optimization rules for the optimization relation ⤅:
S,Γ ⤅ S',Γ', then
(S ;; T),Γ ⤳ (S' ;; T),Γ'
- if forall Δ,
T,Δ ⤅ T',Δ, then
(S ;; T),Γ ⤳ (S ;; T'),Γ (optimization does not need to be sequential as evaluation was)
(IF E do: SKIP),Γ ⤅ SKIP,Γ
(SKIP ;; E),Γ ⤅ E,Γ
With them, we see that our program above indeed first optimizes to
i := 0 ;; (SKIP ;; WHILE true do: ...) (where I annotated parentheses explicitly) and then to
i := 0 ;; (WHILE true do: ...) as desired.
Note that in contrast to the evaluation rules, here the exhaustive application of the optimization rules above does terminate — at least I hope this can be proven via induction. But this is just a consequence of our yet naive way of optimization. If we optimized many things further, we would also run into possibly non-terminating territory.
Correctness of Optimization
Importantly, optimization rules need to be derivable from the evaluation rules for sane programs, i.e. be a subset in some sense. Otherwise, our optimizations would be wrong. Regarding sanity, for instance our third optimization rule can only be derived if we assume that for
E occurring in the if condition, we always have either
E,Γ ⇝ ... ⇝ true or
E,Γ ⇝ ... ⇝ false.
Moreover, our second rule is only derivable if we assume that the
S contained therein never gets stuck. In richer languages,
S may even throw an exception.
However, both previous assumptions do usually hold if our language is typed, our type theory ensures soundness ("well-typed programs never get stuck/throw exceptions"), and the input program for optimization is actually well-typed.
Indeed, the definitions of sanity of many programming language optimizers usually include well-typedness as a necessary condition.
The C language is a prime example for a case where sanity of programs encompasses much more than well-typedness alone: namely, many optimizations by compilers are only correct if the input programs do not exhibit undefined behavior.
: the language and its semantics are heavily inspired from the language Imp presented in the Software Foundations series, Volume 1: Logical Foundations by Pierce, de Amorim, Casinghino, Gaboardi, Greenberg, Hriţcu, Sjöberg, Yorgey et al.