The evaluators we have seen so far (e.g., the ones for aexps, bexps, and commands) have been formulated in a "big-step" style -- they specify how a given expression can be evaluated to its final value (or a command plus a store to a final store) "all in one big step."

This style is simple and natural for many purposes, but it has some shortcomings. In particular, suppose we enriched the language of while programs with boolean variables in addition to the numeric ones. In this language, a command might fail to map a given starting state to any ending state for two quite different reasons: either because the execution gets into an infinite loop or because, at some point, the program tries to do an operation that makes no sense, such as taking the successor of a boolean variable, and none of the evaluation rules can be applied.

These two outcomes -- nontermination vs. getting stuck in an erroneous configuration -- need to be treated differently: we want to allow the first (permitting the possibility of infinite loops is the price we pay for the convenience of being able to program with general looping constructs like while) but prevent the second, for example by adding some form of typechecking to the language. (Indeed, this will be a major topic for the rest of the course.)

As a first step, it is useful to introduce a different way of defining how programs behave -- replacing the "big-step" eval relation with a "small-step" relation that specifies, for a given program, how just the FIRST atomic step of computation is to be performed.

A toy language

To save space in the discussion, let's work with an incredibly simple language containing just constants and addition.

Here is a standard big-step evaluator for this language, in exactly the same style as we've been using up to this point.

Here is a slight variation (still in "big-step" style) where the final result of evaluating a term is also a term.

Now, here is the small-step variant.

A few things to notice:

• We are defining just a single reduction step, in which one tm_plus node is replaced by its value.
  
  
• Each step finds the leftmost tm_plus node that is "ready to go" (both of its operands are constants) and reduces it. The first rule tells how to reduce this tm_plus node itself; the other two rules tell how to find it.
  
  
• A term that is just a constant cannot take a step.

A couple of examples of reasoning with the step relation...

If t1 can take a step to t1', then tm_plus t1 t2 steps to plus t1' t2:

Exercise: 2 stars (test_step_2)

Right-hand sides of sums can take a step only when the left-hand side is finished: if t2 can take a step to t2', then tm_plus (tm_const n) t2 steps to tm_plus (tm_const n) t2':

☐

One interesting property of the step relation is that, like the evaluation relation for our language of While programs, it is deterministic: for each t, there is at most one t' such that step t t' is provable. Formally, this is the same as saying that step is a partial function.

Proof sketch: We must show that if x steps to both y1 and y2 then y1 and y2 are equal. Consider the last rules used in the derivations of step x y1 and step x y2.

• If both are ST_PlusConstConst, the result is immediate.
  
  
• It cannot happen that one is ST_PlusConstConst and the other is ST_Plus1 or ST_Plus2, since this would imply that x has the form tm_plus t1 t2 where both t1 and t2 are constants (by ST_PlusConstConst) AND one of t1 or t2 has the form tm_plus ....
  
  
• Similarly, it cannot happen that one is ST_Plus1 and the other is ST_Plus2, since this would imply that x has the form tm_plus t1 t2 where t1 has both the form tm_plus t1 t2 and the form tm_const n.
  
  
• The cases when both derivations end with ST_Plus1 or ST_Plus2 follow by the induction hypothesis.

Values

Before we move on, let's take a moment to slightly generalize the way we state the definition of single-step reduction.

It is useful to think of the step relation as defining a sort of abstract machine for evaluating programs:

• At any moment, the state of the machine is a term.
  
  
• A step of the machine is an atomic unit of computation
  • - a single "add" operation, in the case of the present
  tiny programming language.
  
  
• The final states of the machine are ones where there is no more computation to be done.

We can then think about "executing" a term t as follows:

• Take t as the starting state of the machine.
  
  
• Repeatedly use the step relation to find a sequence of machine states such that each steps to the next.
  
  
• When no more reduction is possible, "read out" the final state of the machine as the result of execution.

Intuitively, it is clear that the final states of the machine are always terms of the form tm_const n for some n. We call such terms values.

Having introduced the idea of values, we can use it in the definition of the step relation to write ST_Plus2 rule in a slightly more intuitive way:

Exercise: 3 stars (redo_determinacy)

As a sanity check on this change, let's re-verify determinacy

Proof sketch: We must show that if x steps to both y1 and y2 then y1 and y2 are equal. Consider the final rules used in the derivations of step x y1 and step x y2.

• If both are ST_PlusConstConst, the result is immediate.
  
  
• It cannot happen that one is ST_PlusConstConst and the other is ST_Plus1 or ST_Plus2, since this would imply that x has the form tm_plus t1 t2 where both t1 and t2 are constants (by ST_PlusConstConst) AND one of t1 or t2 has the form tm_plus ....
  
  
• Similarly, it cannot happen that one is ST_Plus1 and the other is ST_Plus2, since this would imply that x has the form tm_plus t1 t2 where t1 both has the form tm_plus t1 t2 and is a value (hence has the form tm_const n).
  
  
• The cases when both derivations end with ST_Plus1 or ST_Plus2 follow by the induction hypothesis. ☐

Most of this proof is the same as the one above. But to get maximum benefit from the exercise you should try to write it from scratch and just use the earlier one if you get stuck.

☐

Normal forms

A fundamental property of this language is that every term is either a value or it can "make progress" by stepping to some other term. This property is called progress.

Proof sketch: By induction on t.

• If t is a constant, then it is a value.
  
  
• If t = tm_plus t1 t2, then by the IH t1 and t2 are either values or can take steps under step.
  
  
  • If t1 and t2 are both values, then t can take a step, by ST_PlusConstConst.
    
    
  • If t1 is a value and t2 can take a step, then so can t, by ST_Plus2.
    
    
  • If t1 can take a step, then so can t, by ST_Plus1.

☐

This property can be extended to tell us something very interesting about values: they are exactly the terms that cannot make progress in this sense. To state this fact, let's begin by giving a name to terms that cannot make progress: We'll call them normal forms.

We've actually defined what it is to be a normal form for an arbitrary relation R over an arbitrary set X, not just for the particular reduction relation over terms that we are interested in at the moment. We'll re-use the same terminology for talking about other relations later in the course.

We can use this terminology to generalize the observation we made in the progress theorem: normal forms and values are actually the same thing.

Note that we state and prove this result as two different lemmas, rather than using an if-and-only-if (<->). That's because it will be easier to apply the separate lemmas later on; as noted before, Coq's facilities for dealing "in-line" with <-> statements are a little awkward.

Proof sketch: This is a corollary of progress.

Why are these last two facts interesting? For two reasons:

• Because value is a syntactic concept -- it is a defined by looking at the form of a term -- while normal_form is a semantic one -- it is defined by looking at how the term steps. Is it not obvious that these concepts should coincide.
  
  
• Indeed, there are lots of languages in which the concepts of normal form and value do not coincide.

Let's examine how this can happen...

We might, for example, accidentally define value so that it includes some terms that are not finished reducing.

Exercise: 3 stars (value_not_same_as_normal_form)

☐

Alternatively, we might accidentally define step so that it permits something designated as a value to reduce further.

Exercise: 3 stars (value_not_same_as_normal_form)

☐

Finally, we might accidentally define value and step so that there is some term that is not a value but that cannot take a step in the step relation. Such terms are said to be stuck.

Note that ST_Plus2 is missing.

Exercise: 3 stars (value_not_same_as_normal_form')

☐

Exercises

Here is another very simple language whose terms, instead of being just plus and numbers, are just the booleans true and false and a conditional expression...

Exercise: 1 star (smallstep_bools)

Which of the following propositions are provable? (This is just a thought exercise, but for an extra challenge feel free to prove your answers in Coq.)

☐

Exercise: 3 stars (progress_bool)

Just as we proved a progress theorem for plus expressions, we can do so for boolean expressions, as well.

☐

Exercise: 2 stars, optional (step_deterministic)

☐

Exercise: 2 stars (smallstep_bool_shortcut)

Suppose we want to add a "short circuit" to the step relation for boolean expressions, so that it can recognize when the then and else branches of a conditional are the same value (either tm_true or tm_false) and reduce the whole conditional to this value in a single step, even if the guard has not yet been reduced to a value. For example, we would like this proposition to be provable:

Write an extra clause for the step relation that achieves this effect and prove bool_step_prop4.

☐

Exercise: 2 stars (bool_step_prop4_holds)

To check that your previous answer is correct, prove that the following step is now possible.

☐

Exercise: 3 stars (properties_of_altered_step)

It can be shown that the determinism and progress theorems for the step relation in the lecture notes also hold for the definition of step given above. After we add the clause ST_ShortCircuit...

• Does step_deterministic still hold? Write yes or no and briefly (1 sentence) explain your answer.
  
  Optional exercise: prove your answer correct in Coq.

• Does a progress theorem hold? Write yes or no and briefly (1 sentence) explain your answer.
  
  Optional exercise: prove your answer correct in Coq.

• In general, is there any way we could cause progress to fail if we took away one or more constructors from the original step relation? Write yes or no and briefly (1 sentence) explain your answer.

(* FILL IN HERE *)

☐

Multi-step reduction

Until now, we've been working with the single-step reduction relation step, which formalizes the individual steps of abstract machine for executing programs. It is also interesting to use this machine to reduce programs to completion, to find out what final result they yield. This can be formalized in two steps.

• First, we define a multi-step reduction relation stepmany, which relates terms t and t' if t can reach t' by any number (including 0) of single reduction steps.
  
  
• Then we can define a "result" of a term t as a normal form that t can reach by some number of reduction steps. Formally, we write normal_form_of t t' to mean that t' is a normal form reachable from t by many-step reduction.

Reflexive, Transitive Closure

To begin, let's review a bit of terminology from the basic theory of relations, which you probably saw at some point in a discrete math course.

The reflexive, transitive closure of a relation R is the smallest relation that contains R and that is both reflexive and transitive. Formally, it is defined like this in the Relations module of the Coq standard library:

For example, the reflexive and transitive closure of the next_nat relation coincides with the le relation.

The above definition of reflexive, transitive closure is natural -- it says, explicitly, that the reflexive and transitive closure of R is the least relation that includes R and that is closed under rules of reflexivity and transitivity. But it turns out that this definition is not very convenient for doing proofs -- the "nondeterminism" of the rt_trans rule can sometimes lead to tricky inductions.

Here is a more useful definition...

This new definition "bundles together" the rtc_R and rtc_trans rules into the single rule step. The left-hand premise of this step is a single use of R, leading to a much simpler induction principle.

Before we go on, we should check that the 2 definitions do indeed define the same relation...

First, we prove two lemmas showing that rsc mimics the behavior of the two "missing " rtc constructors.

Exercise: 2 stars (rsc_trans)

☐

Exercise: 3 stars (rtc_rsc_coincide)

☐

Multi-step reduction

Now we're ready to define the multi-step reduction relation.

(Note that we use Notation instead of Definition here. This means that stepmany will be automatically unfolded by Coq, which will simplify some of the proof automation later on.)

A few examples...

Here's another proof for the same example that uses eapply to avoid explicitly constructing all the intermediate terms.

Exercise: 1 star (test_stepmany_2)

☐

Exercise: 1 star (test_stepmany_3)

☐

Exercise: 2 stars (test_stepmany_4)

☐

Normal forms

Now we define normal forms and relate them to values.

If t steps to t' in zero or more steps and t' is a normal form, we say that "t' is a normal form of t."

We have already seen that single-step reduction is deterministic -- i.e., a given term can take a single step in at most one way. It follows from this that, if t can reach a normal form, then this normal form is unique -- i.e., normal_form_of is a partial function. In other words, we can actually pronounce normal_form t t' as "t' is the normal form of t."

Exercise: 3 stars, optional (test_stepmany_3)

☐

Indeed, something stronger is true for this language (though not for all programming languages!): the reduction of ANY term t will eventually reach a normal form -- i.e., normal_form_of is a total function. Formally, we say the step relation is normalizing.

To prove that step is normalizing, we need a few lemmas. First, we observe that, if t reduces to t' in many steps, then the same sequence of reduction steps is possible when t appears as the left-hand child of a tm_plus node, and similarly when t appears as the right-hand child of a tm_plus node whose left-hand child is a value.

Exercise: 2 stars

☐

Before proving it formally, let's sketch the proof that step is normalizing.

Theorem:

      forall t, exists t',
        stepmany t t' /\ normal_form step t'

Proof sketch: By induction on terms. There are two cases to consider:

• t = tm_const n for some n. Here t doesn't take a step, and we have t' = t. We can derive the left-hand side by reflexivity and the right-hand side by observing (a) that values are normal forms (by value_is_nf) and (b) that t is a value (by v_const).
  
  
• t = tm_plus t1 t2 for some t1 and t2. By the IH, both t1 and t2 normalize to normal forms t1' and t2', respectively. Recall that normal forms are values (by nf_is_value); we know that t1' = tm_const n1 and t2' = tm_const n2, for some n1 and n2. We can combine the stepmany derivations for t1 and t2 to prove that:
  
          stepmany (tm_plus t1 t2) (tm_const (plus n1 n2)).
  
  It is clear that our choice of t' = tm_const (plus n1 n2) is a value, which is in turn a normal form.

Equivalence of big-step and small-step reduction

Having defined the operational semantics of our tiny programming language in two different styles, it makes sense to ask whether these definitions actually define the same thing! They do, but it is not completely straightforward to show this, or even to see how to state it exactly, since one of the relations only goes a small step at a time while the other proceeds in large chunks.

Exercise: 3 stars (eval__stepmany)

You'll want to use the congruences and some properties of rsc.

☐

Exercise: 3 stars (eval__stepmany_inf)

Write an informal version of the proof of eval__stepmany. (* FILL IN HERE *)
☐

Exercise: 3 stars (step__eval)

☐

Bringing it all together into a crisp connection, we can simply say that the v is the normal form of t iff t evaluates to v.

Additional exercises

Exercise: 4 stars, optional (interp_tm)

Define a Fixpoint that evaluates tms. Prove that it is equivalent to the existing semantics.

Hint: we just proved that eval and stepmany are equivalent, so logically it doesn't matter which you choose. One will be easier than the other, though!

☐

Exercise: 4 stars, optional (combined_properties)

We've considered the arithmetic and conditional expressions separately. This exercise explores how the two interact.

Earlier, we separately proved for both plus- and if-expressions

• that the step relation was a partial function (i.e., it was deterministic), and
  
  
• a progress lemma, stating that every term is either a value or can take step.

Prove or disprove these for the combined langauge.

☐