In this post, I propose a classification for expression transformations. This classification aims at generalness and generalness goes hand in hand with abstractness, so you shouldn't expect Coq tactics to be treated in too much depth here.
The bulk of expression transformations are based on evaluation. In this family of transformations, the fact that the value we end with is equivalent to the one we started from is obvious enough: evaluation preserves equality by definition.
There is an important distinction between reduction steps and more general evaluation-based expression transformations. Applying single reduction steps by hand is a rare occurrence — usually, people defer to automatic procedures which decide which reductions should be applied at which point in the term, in which order, as well as when to stop applying reductions.
In everyday talk, evaluation usually refers to total concrete evaluation: you start from a closed expression and you turn it into the value it stands for. The name is quite explicit — you keep applying reduction steps until you can't. In civilized rewriting systems, the order in which these reductions are applied doesn't matter, thanks to the confluence property.
Non-confluent rewriting systems are not strictly incompatible with total evaluation, however the equivalence relation can't just be equality, then. If you embrace nondeterminism, you can decide that your expression doesn't return a value, but the set of values compatible with the expression. However, whether this respects our definition of total concrete evaluation is at least questionable (we don't end up with a value). Alternatively, you can evaluate the expression down to one of the values it is compatible with, which is not the nicest equivalence property to work with but meets our criterion more manifestly.
As you will have guessed, total concrete evaluation is an evaluation procedure built out of concrete steps only.
However, the real world is a complex place where some expressions just can't be reduced down to values: 5 + 3 + 2 is 10, but what is 5 + 3 + a, when a is an abstract term? This expression can be reduced to 8 + a, but it can't be further simplified. This is not a value but it is a simpler expression, which is already interesting for many purposes. So evaluation-based expression transformations don't all have to be total.
Also, there are situations in which you want to evaluate only parts of your expression, be it because you need it to match a specific form for a proof you are writing, or because you want to control the reduction process to assure that you do not stumble into performance traps.
In the next two subsections, we will see what happens when we invert the constraints of concreteness and of totality, respectively.
A symbolic transformation is a transformation which can deal abstract expressions. It is not to be conflated with abstract interpretation, a technique mostly used in static analysis based on approximation. Symbolic evaluation is what you want to use when you handle open terms.
For instance, you may want to prove that 0 + n is equal to n for any value of n. The addition may be implemented as follows:
Then, a way of proving what you want would be to specialize this function with the argument 0 (note how n remains abstract at this point). Then, the code is equivalent to this:
As the comment points out, this is enough information to simplify the match:
At this point, the proof is trivial. Another example would be the following C program:
Compiling this program with basic optimizations should take about a minute and give us something equivalent to:
As the slow computation was pure, it could be done at compile time. The resulting program then runs nearly instantaneously! In fact, most compilations include optimization passes which basically amount to total symbolic evaluation.
Just like total concrete evaluation, total symbolic evaluation is an evaluation procedure. The main difference between the two is that total symbolic evaluation procedures can handle abstract terms, which contain unbound variables. Just what is meant by handling abstract terms vary a lot. Just as there are concrete evaluation steps, there are symbolic ones. Think about a - a: this is clearly enough equivalent to 0, but it takes some reasoning to show that this indeed constitutes a legal reduction step. Some rewriting system would include rules for doing e.g. arithmetic with opaque variables in their core, but not all do — for instance, in Coq, it takes some justification.
Another related example is given by the expression 4 + 1 + a + 2 + a. The procedure we described hitherto would turn this into 5 + a + 2 + a, which falls short of the better 7 + 2*a. Some procedures would always get this expression and related ones into a sort of normal form where the better 7 + 2*a. Some procedures would always get their input expression to some sort of normal form, with everything as reduced as possible, but some would be more limited.
In Coq, reduction steps are defined at a low-level compared to that of e.g. arithmetic expressions. Still, you have symbolic steps which can deal with abstract input, for instance for turning (fun x -> S x) a into S a. Some steps remain hopelessly concrete, for instance the one that picks the appropriate branch of a pattern match. You need the head matchee to be concrete, there is no way around that. Deeper parts of the matchee can be opaque though, no trouble there.
Up to this point, we mentioned evaluation procedures taking terms to some normal form — taking arithmetic expressions to integers, for instance. We are now going to zoom-in on the individual steps out of which these procedures were built. This is where partial evaluation enter the picture.
Sometimes, less is more. Strict impossibility is not the only reason why you may want not to fully reduce a term: you may need your expression to match a specific form for a proof you are writing, or it may be that not all ways of reducing your expression are equally fast, for example. In these situations, it pays to show some parsimony.
Assume we want to prove that if <x> then <y> else <z>. Now, you know that <x> evaluates to true, but you aren't done proving that just yet, and the term can't be reduced by evaluation. You notice that applying tactics takes more time than it should, and you wonder if the size of the object you are reasoning about plays a role in that. Additionally, you can see that the subterm <y> is very large, but shouldn't be that slow to compute. On the other hand, term <z> looks like it takes a lot of time to reduce but it also doesn't use that much memory. We want to get a smaller object as efficiently as possible. What we would like to do, then, is to reduce term <y> only. What we would like, in other words, is partial interpretation — being able to apply reductions steps at targeted points in the term. Note that in my definition partial evaluation is not limited to the total evaluation of subterms.
I mentioned concrete and symbolic steps earlier. For instance, turning 2 + 2 into 4 would be a concrete step, whereas turning 2 + a into a + 2 or a + a into 2*a would be symbolic steps (symbolic steps can handle symbols, concrete ones can't). It takes a symbolic step to take 2 + a + 2 to a + 2 + 2, and then a concrete one to then take this to a + 4.
Partial evaluation is not just about running steps in isolation. Procedures for automatically applying series of steps fall under this umbrella — in fact, total evaluation procedures can be viewed as a partial reduction procedure which just happens to always return fully reduced terms.
As we've seen, it is possible to devise rewriting systems even for impure languages. These rewriting systems can deal with the pure fragments of terms of such languages, but they are not limited to that, as we shall see. Of course, these rewriting systems get much more complex than their pure counterparts (in particular due to the need to keep track of state), and they are based on less elegant equivalence relations (some sort of compatibility rather than equality).
Consider the following function:
Simplifying its pure fragments leaves us with the following:
If our relation of choice is about compatibility, then the following transformation is surely legal, as we can imagine situations in which the second run of get_rand_int indeed yields 4:
However, this reduction step disallows other ones which would otherwise have been legal, such as the one leading to this term (take get_user_int to return 2):
Nevertheless, these (also reduction based) transformations are valid expression transformations worthy of a place in the classification.
The transformations that we considered up to this point were based on evaluation. That is, all of them took steps towards a normalized form for the expression (i.e., a fully evaluated form). However, this need not always be the case!
Expression transformations can move terms away from their normalized form (equality is symmetric, so any transformation can be undone!), or in fact, you can replace a term with one which may seem unrelated, but is still somehow equivalent to it.
In doing this, we stray away from the strict expression -> expression model of transformations. For instance, the following becomes a valid transformation: expression <e> -> <proof that a = b> -> <e where a is replaced with b> Note how arbitrary context elements can be used this way: maybe the proof that a = b comes from a Coq axiom or previously proven lemma! In fact, this prototype describes a common usecase of the rewrite tactic.
General transformation are an usual sight in theorem provers. You need to prove that your seemingly arbitrary transformation is legal, after all. Or do you? For instance, unrolling a loop in assembly is a form of general transformation. There is usually no proof of correctness of the implementation of this optimization pass, but that is to be expected of unverified systems. Another non-theorem prover related example of a general transformations is what happens when you jump from a language (intermediate representation or not) to an other in a compilation pipeline.
With general transformations, we stray away from reduction steps. Instead, we directly replace a whole term or subterms with something we assume — or prove — equivalent. In theorem prover, we usually have powerful building blocks (such as Coq's rewrite) for doing arbitrary replacements in exchange for some proof. These replacements usually are not limited to concrete terms or subterms (e.g. you can transform a - a into 0). Also, general transformations can be impure. For instance:
Can be rewritten into:
You could also choose to view reduction based expression transformations as special cases of general transformations. This is true and fine, but this does not mean that reduction based transformations are not special enough to deserve their own subcategory.
Reduction steps are expression transformations — usually very basic ones — that are local in nature, such as function definition unfolding or constant folding. They can be applied at a specified position in a given term, assuming the local context matches their prerequisites (i.e. don't try to apply definition unfolding on a constant).
The set of reduction steps available for the terms belonging to some language can be studied through the lens of rewriting systems. Transitions in a rewriting system usually directly correspond to the application of a reduction step.
Procedures for selecting which reduction steps to apply where and when (and also when to stop appling reduction steps) can be devised. For instance, it is often the case that sequentially picking reduction steps at random from the list of those compatible with the term at hand is guaranteed to lead to the same term, namely a normal form for the term in question. The rewriting system could then be said to be "confluent". A simple procedure for normalizing terms would then be to do just that. These procedures constitute evaluation-based expression transformations.
The order in which steps are taken sometimes matter. Even for confluent rewriting systems, where all paths are functionally equivalent, it may be that some order of evaluation drastically cuts down the complexity of the normalization. This is why being able to leave the user fine controls on how reductions are performed matters in some admittedly rare contexts, such as in proof assistants.
Not all expression transformations are related to reduction. In fact, at times, seemingly unrelated terms end up being equivalent, counterintuitively. It may be that term A is 1 + 7 and that term B is opaque, but that we somehow have a proof of B = 8 in our context (local hypothesis?). We should be able to replace A with B, yet our rewriting system probably won't let us as these things are usually geared towards reductions, not expansions or more radical transformations such as the proposed ones. The larger set of expression transformations which includes procedures for doing such transformations is that of general transformations. Reduction steps and evaluation-based expression transformations are special cases of general transformations.
It is always legal to replace a subterm of a term with something equivalent to it. Expression transformations can be applied at given positions. However, this does not mean that each practical implementation of an expression transformation let's you pick where you apply them. For instance, procedures for total evaluation almost always systematically apply to the head of the term.
Steps can be concrete or symbolic. Concrete steps may only deal with concrete inputs (i.e. do evaluation) and symbolic steps open the way to symbolic manipulations. This mostly depends on the language being treated. If the language supports symbolic variables, then the reduction steps are bound to be symbolic. For instance, in optimizing a function in some programming language, one has to deal as the future arguments can only be represented by abstract variables. It is not only steps which can be concrete or symbolic. This notion in fact extends to procedures. Procedures written for languages which have a notion of asbtract variables may be concrete when they content themselves with appling steps to concrete fragments of the term only. Otherwise, they are symbolic. The same goes for general expression transformations.
Impure expressions can also be transformed, but the side effects have to be preserved. Dealing with impure expressions forces contact with unpleasant equivalence relations.
In this section, I finally give my classification of expression transformations.
We are going to start from the set of all expression transformations and carve our classification in there.
Evaluation-based expression transformations form a subset of expression transformations. We give this category a lot of space, owing to its importance.
In many real-life occurrences of evaluation-based transformations, the evaluation process is carried out until the term is somehow normalized. These are total procedures. Evaluation-based transformations that are not total are partial. A special case of partial transformations are the transformations which correspond to the application of a single reduction step. In systems where these steps can be called applied directly by the user, the degree of control over the reduction process is maximal.
Some reductions are pure whereas others are impure. This is true in general and not just for evaluation-based transformations.
Similarly, some reductions are concrete whereas other handle symbolic inputs.
Let's populate our classification with some concrete examples to ground this all.
We are going to start by looking at examples of expression transformations from compilers. More specifically, we will analyze some common optimization passes. If not specified otherwise, assume that the passes are behave like those of C compilers.
Loops unrolling is an optimization pass with a quite explicit name: take any loop, for instance a for-based one, and copy and paste its body to reduce the numbers of jumps in machine code.
This pass is an impure transformation (as the body of the loop may include calls to effectful functions). It is not evaluation-based: it doesn't follow a natural evaluation step for C expressions.
Constant folding is about the evaluation of concrete subterms of programs. This pass lands firmly in the concrete, evaluation-based, pure subset of transformations. In particular, it is not total as it is not the whole program that is simplified.
In some languages such as Rust, access to containers is bound-checked.
Bounds-checking elimination is about removing such checks when they can be statically deduced to be useless. For instance, two checks are naively inserted when incrementing some integer in a fixed-size array: one to protect the read of its initial value and one to protect the write. The second one is extraneous and can be mechanically removed.
This is an example of a pure general transformation (in particular, the index can be abstract).
Tail-call elimination is a pass that helps with keeping the size of the call stack small ( more details).
Although it is quite different from the previous optimization pass we considered, it also falls in the pure general transformation category.
Evaluation strategies describe how function calls are evaluated. I wrote some posts on this topic, which you can can find here. You can expect all evaluation strategies to land in the impure subset of our classification, as the expressions they receive as arguments can be impure. The evaluation strategies either evaluate them or insert them in the function's body, as we shall see.
Different evaluation strategies can be used for different arguments of a function. You can assume that the arguments are dealt with one by one, and that each evaluation strategy also simplifies the expression as much after dealing with the argument — this oversimplification makes them total. Once all arguments have been dealt with, a concrete value is left.
Call-by-value: evaluate the arguments, and replace mentions of the arguments in the function's body with the appropriate resulting value.
Call-by-reference: same as previous, but this time the value is a handle to some external object. It still lands in the same category as call-by-value.
Lazy evaluation: only evaluate the argument if its value is actually required to evaluate the function. I didn't put it in the impure category as it is mostly found in pure languages (see why in here).
Call-by-name (ALGOL 60 style): this awful evaluation strategy is a glorified macro expansion. Surprisingly, it can actually pass expressions containing open variables!
More details here.
The classification only represents the "what" (functional criteria) and does not take into account the "how", although this information is often critical to performance. I will attempt to remedy that.
Non-strict evaluation strategies are marked with green. These strategies don't always evaluate the expressions they receive as arguments. This can lead to performance gains!
In my main post about evaluation strategies, I classified evaluation strategies according to their purity, however this criterion evidently doesn't match the one used here. In fact, the other criterion is about compatibility with pure languages. Here it is, marked in blue.
Unsurprisingly, Coq tactics constitute examples of expression transformations. We'll give them a more in-depth treatment in the next chapter, light spoilers warning.
simpl is about reducing the expression up to some point. Importantly, it does not fully reduce a term.
vm_compute is a strategy for total evaluation of terms. This transformation deals with symbolic terms, which makes it prone to explosions.
Not all Coq tactics are evaluation-based. A prime example of a general expression transformation is rewrite, a strategy which can replace a term with about anything that is provably equivalent.
lazy is yet another total evaluation-based transformation. Wait, isn't it redundant with vm_compute? Functionally, yes…
… But not as far as performance go: lazy is non-strict, just like its evaluation strategy counterpart.
Another family of expression transformations which I didn't even mention until now is the lambda calculus reductions.
α-conversion is about renaming variables to avoid name clashes. It is our first example of a single step reduction tactic. As you will see, it is not alone in this regards. edit: concrete?
β-conversion is about function application.
η-conversion is about the equivalence between functions and abstractions over functions.
We will go through a whirlwind tour of Coq's tactics and we will insert them into our classification.