The Equiv chapter introduced constant folding as an example of a program transformation and proved that it preserves the meaning of programs. Constant folding operates on manifest constants such as ANum expressions. For example, it simplifies the command Y ::= 3 + 1 to the command Y ::= 4. However, it does not propagate known constants along data flow. For example, it does not simplify the sequence
X ::= 3;; Y ::= X + 1
to
X ::= 3;; Y ::= 4
because it forgets that X is 3 by the time it gets to Y.
We might naturally want to enhance constant folding so that it propagates known constants and uses them to simplify programs. Doing so constitutes a rudimentary form of partial evaluation. As we will see, partial evaluation is so called because it is like running a program, except only part of the program can be evaluated because only part of the input to the program is known. For example, we can only simplify the program
X ::= 3;; Y ::= (X + 1) - Y
to
X ::= 3;; Y ::= 4 - Y
without knowing the initial value of Y.
The starting point of partial evaluation is to represent our partial knowledge about the state. For example, between the two assignments above, the partial evaluator may know only that X is 3 and nothing about any other variable.
Conceptually speaking, we can think of such partial states as the type string -> option nat (as opposed to the type string -> nat of concrete, full states). However, in addition to looking up and updating the values of individual variables in a partial state, we may also want to compare two partial states to see if and where they differ, to handle conditional control flow. It is not possible to compare two arbitrary functions in this way, so we represent partial states in a more concrete format: as a list of string * nat pairs.
The idea is that a variable (of type string) appears in the list if and only if we know its current nat value. The pe_lookup function thus interprets this concrete representation. (If the same variable appears multiple times in the list, the first occurrence wins, but we will define our partial evaluator to never construct such a pe_state.)
For example, empty_pe_state represents complete ignorance about every variable -- the function that maps every identifier to None.
More generally, if the list representing a pe_state does not contain some identifier, then that pe_state must map that identifier to None. Before we prove this fact, we first define a useful tactic for reasoning with string equality. The tactic
compare V V'
means to reason by cases over eqb_string V V'. In the case where V = V', the tactic substitutes V for V' throughout.
In what follows, we will make heavy use of the In property from the standard library, also defined in Logic.v:
Besides the various lemmas about In that we've already come across, the following one (taken from the standard library) will also be useful:
If a type A has an operator eqb for testing equality of its elements, we can compute a boolean inb eqb a l for testing whether In a l holds or not.
It is easy to relate inb to In with the reflect property:
Partial evaluation of aexp is straightforward -- it is basically the same as constant folding, fold_constants_aexp, except that sometimes the partial state tells us the current value of a variable and we can replace it by a constant expression.
This partial evaluator folds constants but does not apply the associativity of addition.
Now, in what sense is pe_aexp correct? It is reasonable to define the correctness of pe_aexp as follows: whenever a full state st:state is consistent with a partial state pe_st:pe_state (in other words, every variable to which pe_st assigns a value is assigned the same value by st), evaluating a and evaluating pe_aexp pe_st a in st yields the same result. This statement is indeed true.
However, we will soon want our partial evaluator to remove assignments. For example, it will simplify
X ::= 3;; Y ::= X - Y;; X ::= 4
to just
Y ::= 3 - Y;; X ::= 4
by delaying the assignment to X until the end. To accomplish this simplification, we need the result of partial evaluating
pe_aexp (X,3) (X - Y)
to be equal to 3 - Y and not the original expression X - Y. After all, it would be incorrect, not just inefficient, to transform
X ::= 3;; Y ::= X - Y;; X ::= 4
to
Y ::= X - Y;; X ::= 4
even though the output expressions 3 - Y and X - Y both satisfy the correctness criterion that we just proved. Indeed, if we were to just define pe_aexp pe_st a = a then the theorem pe_aexp_correct_weak would already trivially hold.
Instead, we want to prove that the pe_aexp is correct in a stronger sense: evaluating the expression produced by partial evaluation (aeval st (pe_aexp pe_st a)) must not depend on those parts of the full state st that are already specified in the partial state pe_st. To be more precise, let us define a function pe_override, which updates st with the contents of pe_st. In other words, pe_override carries out the assignments listed in pe_st on top of st.
Although pe_update operates on a concrete list representing a pe_state, its behavior is defined entirely by the pe_lookup interpretation of the pe_state.
We can relate pe_consistent to pe_update in two ways. First, overriding a state with a partial state always gives a state that is consistent with the partial state. Second, if a state is already consistent with a partial state, then overriding the state with the partial state gives the same state.
Now we can state and prove that pe_aexp is correct in the stronger sense that will help us define the rest of the partial evaluator.
Intuitively, running a program using partial evaluation is a two-stage process. In the first, static stage, we partially evaluate the given program with respect to some partial state to get a residual program. In the second, dynamic stage, we evaluate the residual program with respect to the rest of the state. This dynamic state provides values for those variables that are unknown in the static (partial) state. Thus, the residual program should be equivalent to prepending the assignments listed in the partial state to the original program.
The partial evaluation of boolean expressions is similar. In fact, it is entirely analogous to the constant folding of boolean expressions, because our language has no boolean variables.
The correctness of pe_bexp is analogous to the correctness of pe_aexp above.
What about the partial evaluation of commands? The analogy between partial evaluation and full evaluation continues: Just as full evaluation of a command turns an initial state into a final state, partial evaluation of a command turns an initial partial state into a final partial state. The difference is that, because the state is partial, some parts of the command may not be executable at the static stage. Therefore, just as pe_aexp returns a residual aexp and pe_bexp returns a residual bexp above, partially evaluating a command yields a residual command.
Another way in which our partial evaluator is similar to a full
evaluator is that it does not terminate on all commands. It is
not hard to build a partial evaluator that terminates on all
commands; what is hard is building a partial evaluator that
terminates on all commands yet automatically performs desired
optimizations such as unrolling loops. Often a partial evaluator
can be coaxed into terminating more often and performing more
optimizations by writing the source program differently so that
the separation between static and dynamic information becomes more
apparent. Such coaxing is the art of binding-time improvement.
The binding time of a variable tells when its value is known --
either static
, or dynamic.
Anyway, for now we will just live with the fact that our partial evaluator is not a total function from the source command and the initial partial state to the residual command and the final partial state. To model this non-termination, just as with the full evaluation of commands, we use an inductively defined relation. We write
c1 / st \\ c1' / st'
to mean that partially evaluating the source command c1 in the initial partial state st yields the residual command c1' and the final partial state st'. For example, we want something like
/ (X ::= 3 ;; Y ::= Z * (X + X)) \\ (Y ::= Z * 6) / (X,3)
to hold. The assignment to X appears in the final partial state, not the residual command.
(Writing something like st =[ c1 ]=> c1' / st' would be closer to the notation used in Imp; perhaps this should be changed!)
Let's start by considering how to partially evaluate an assignment. The two assignments in the source program above needs to be treated differently. The first assignment X ::= 3, is static: its right-hand-side is a constant (more generally, simplifies to a constant), so we should update our partial state at X to 3 and produce no residual code. (Actually, we produce a residual SKIP.) The second assignment Y ::= Z * (X + X) is dynamic: its right-hand-side does not simplify to a constant, so we should leave it in the residual code and remove Y, if present, from our partial state. To implement these two cases, we define the functions pe_add and pe_remove. Like pe_update above, these functions operate on a concrete list representing a pe_state, but the theorems pe_add_correct and pe_remove_correct specify their behavior by the pe_lookup interpretation of the pe_state.
We will use the two theorems below to show that our partial evaluator correctly deals with dynamic assignments and static assignments, respectively.
Trickier than assignments to partially evaluate is the conditional, TEST b1 THEN c1 ELSE c2 FI. If b1 simplifies to BTrue or BFalse then it's easy: we know which branch will be taken, so just take that branch. If b1 does not simplify to a constant, then we need to take both branches, and the final partial state may differ between the two branches!
The following program illustrates the difficulty:
X ::= 3;; TEST Y <= 4 THEN Y ::= 4;; TEST X <= Y THEN Y ::= 999 ELSE SKIP FI ELSE SKIP FI
Suppose the initial partial state is empty. We don't know statically how Y compares to 4, so we must partially evaluate both branches of the (outer) conditional. On the THEN branch, we know that Y is set to 4 and can even use that knowledge to simplify the code somewhat. On the ELSE branch, we still don't know the exact value of Y at the end. What should the final partial state and residual program be?
One way to handle such a dynamic conditional is to take the intersection of the final partial states of the two branches. In this example, we take the intersection of (Y,4),(X,3) and (X,3), so the overall final partial state is (X,3). To compensate for forgetting that Y is 4, we need to add an assignment Y ::= 4 to the end of the THEN branch. So, the residual program will be something like
SKIP;; TEST Y <= 4 THEN SKIP;; SKIP;; Y ::= 4 ELSE SKIP FI
Programming this case in Coq calls for several auxiliary functions: we need to compute the intersection of two pe_states and turn their difference into sequences of assignments.
First, we show how to compute whether two pe_states to disagree at a given variable. In the theorem pe_disagree_domain, we prove that two pe_states can only disagree at variables that appear in at least one of them.
We define the pe_compare function to list the variables where two given pe_states disagree. This list is exact, according to the theorem pe_compare_correct: a variable appears on the list if and only if the two given pe_states disagree at that variable. Furthermore, we use the pe_unique function to eliminate duplicates from the list.
The intersection of two partial states is the result of removing from one of them all the variables where the two disagree. We define the function pe_removes, in terms of pe_remove above, to perform such a removal of a whole list of variables at once.
The theorem pe_compare_removes testifies that the pe_lookup interpretation of the result of this intersection operation is the same no matter which of the two partial states we remove the variables from. Because pe_update only depends on the pe_lookup interpretation of partial states, pe_update also does not care which of the two partial states we remove the variables from; that theorem pe_compare_update is used in the correctness proof shortly.
Finally, we define an assign function to turn the difference between two partial states into a sequence of assignment commands. More precisely, assign pe_st ids generates an assignment command for each variable listed in ids.
The command generated by assign always terminates, because it is just a sequence of assignments. The (total) function assigned below computes the effect of the command on the (dynamic state). The theorem assign_removes then confirms that the generated assignments perfectly compensate for removing the variables from the partial state.
At long last, we can define a partial evaluator for commands without loops, as an inductive relation! The inequality conditions in PE_AssDynamic and PE_If are just to keep the partial evaluator deterministic; they are not required for correctness.
Below are some examples of using the partial evaluator. To make the pe_com relation actually usable for automatic partial evaluation, we would need to define more automation tactics in Coq. That is not hard to do, but it is not needed here.
Finally let's prove that this partial evaluator is correct!
The main theorem. Thanks to David Menendez for this formulation!
It may seem straightforward at first glance to extend the partial evaluation relation pe_com above to loops. Indeed, many loops are easy to deal with. Considered this repeated-squaring loop, for example:
WHILE 1 <= X DO Y ::= Y * Y;; X ::= X - 1 END
If we know neither X nor Y statically, then the entire loop is dynamic and the residual command should be the same. If we know X but not Y, then the loop can be unrolled all the way and the residual command should be, for example,
Y ::= Y * Y;; Y ::= Y * Y;; Y ::= Y * Y
if X is initially 3 (and finally 0). In general, a loop is easy to partially evaluate if the final partial state of the loop body is equal to the initial state, or if its guard condition is static.
But there are other loops for which it is hard to express the residual program we want in Imp. For example, take this program for checking whether Y is even or odd:
X ::= 0;; WHILE 1 <= Y DO Y ::= Y - 1 ;; X ::= 1 - X END
The value of X alternates between 0 and 1 during the loop. Ideally, we would like to unroll this loop, not all the way but two-fold, into something like
WHILE 1 <= Y DO Y ::= Y - 1;; IF 1 <= Y THEN Y ::= Y - 1 ELSE X ::= 1;; EXIT FI END;; X ::= 0
Unfortunately, there is no EXIT command in Imp. Without extending the range of control structures available in our language, the best we can do is to repeat loop-guard tests or add flag variables. Neither option is terribly attractive.
Still, as a digression, below is an attempt at performing partial evaluation on Imp commands. We add one more command argument c'' to the pe_com relation, which keeps track of a loop to roll up.
Because this partial evaluator can unroll a loop n-fold where n is a (finite) integer greater than one, in order to show it correct we need to perform induction not structurally on dynamic evaluation but on the number of times dynamic evaluation enters a loop body.
Instead of partially evaluating WHILE loops directly, the standard approach to partially evaluating imperative programs is to convert them into flowcharts. In other words, it turns out that adding labels and jumps to our language makes it much easier to partially evaluate. The result of partially evaluating a flowchart is a residual flowchart. If we are lucky, the jumps in the residual flowchart can be converted back to WHILE loops, but that is not possible in general; we do not pursue it here.
A flowchart is made of basic blocks, which we represent with the inductive type block. A basic block is a sequence of assignments (the constructor Assign), concluding with a conditional jump (the constructor If) or an unconditional jump (the constructor Goto). The destinations of the jumps are specified by labels, which can be of any type. Therefore, we parameterize the block type by the type of labels.
We use the even or odd
program, expressed above in Imp, as our
running example. Converting this program into a flowchart turns
out to require 4 labels, so we define the following type.
The following block is the basic block found at the body label of the example program.
To evaluate a basic block, given an initial state, is to compute the final state and the label to jump to next. Because basic blocks do not contain loops or other control structures, evaluation of basic blocks is a total function -- we don't need to worry about non-termination.
A flowchart program is simply a lookup function that maps labels to basic blocks. Actually, some labels are halting states and do not map to any basic block. So, more precisely, a flowchart program whose labels are of type L is a function from L to option (block L).
Unlike a basic block, a program may not terminate, so we model the evaluation of programs by an inductive relation peval rather than a recursive function.
Partial evaluation changes the label type in a systematic way: if the label type used to be L, it becomes pe_state * L. So the same label in the original program may be unfolded, or blown up, into multiple labels by being paired with different partial states. For example, the label loop in the parity program will become two labels: ([(X,0)], loop) and ([(X,1)], loop). This change of label type is reflected in the types of pe_block and pe_program defined presently.