Magritte (wisely): This is not a pipe.Mimer (curious): This what is not a pipe?Magritte: I mean that source arithmetic expressions are not arithmetic expressions.Mimer: Right. They are syntactic representations of arithmetic expressions.Magritte: Yup.
The goal of this chapter is to revisit the source arithmetic expressions from Chapter Arithmetic expressions with names and to determine which properties of arithmetic expressions are satisfied by these source arithmetic expressions.
When a programming language is defined through the implementation of an interpreter, this interpreter can be used to characterize properties of programs written in this programming language.
Here, we revisit the source arithmetic expressions from Chapter Arithmetic expressions with names and two interpreters for them: one implemented by the left-to-right evaluation function – evaluate_ltr, and the other implemented by the right-to-left evaluation function – evaluate_rtl.
Based on these two interpreters, we can investigate which properties of arithmetic expressions hold for source arithmetic expressions.
These properties are typically stated as follows:
Property ... :
forall evaluate : arithmetic_expression -> environment nat -> expressible_value,
specification_of_evaluate evaluate ->
forall (ae1 ae2 : arithmetic_expression)
(e : environment nat),
evaluate ae1 e = evaluate ae2 e.
When evaluating ae1 in an environment e and when evaluating ae2 in the same environment give the same result, ae1 and ae2 are said to be observationally equivalent to convey that evaluating them in the same environment yields the same result with the same computational effects, if there are any. (For example, the first evaluation could yield an error message, and for observational equivalence to hold, the second evaluation should yield the same error message.)
This notion of equivalence is similar to the extensional equivalence of functions and of programs and is due to Jim Morris. Two expressions are observationally equivalent if evaluating one is indistinguishable from evaluating the other: Either both of their evaluations do not terminate, or they yield the same error, or they yield the same result, and if any side effects occur in the course of their evaluation, these side effects are the same and they occur in the same order.
Halcyon: But isn’t 0 neutral for addition in arithmetic expressions?Bong-sun: They are not arithmetic expressions...Dana: ...they are syntactic representation of arithmetic expressions.Pablito: You mean like Magritte’s pipe?Bong-sun and Dana: Yes.Halcyon (lost): But he said that it was not a pipe?
Exercise 07 is solved in the accompanying .v file documenting the live-proving session at the lecture. The proof is by cases, depending on the result of evaluating the second argument of Plus.
Note how the proofs do not start by eagerly naming each leaf in the binary tree of conjunctions that represents the specification. Instead, this naming is delayed to each case, and in each case, only the necessary leaves are named. This delaying strategy minimizes the number of assumptions in the *goals* window.
It would be wise to use this delaying strategy in the term project.
Exercise 11.a is solved in the accompanying .v file that documents the live-proving session at the lecture.
The proof for Exercise 11.a is a proof by cases, depending on the result of evaluating each of ae1, ae2, and ae3. Reflecting that Exercise 11.a is about left-to-right evaluation, this proof starts as follows:
intros evaluate S_evaluate ae1 ae2 ae3 e.
case (evaluate ae1 e) as [n1 | m1] eqn:E_ae1.
- case (evaluate ae2 e) as [n2 | m2] eqn:E_ae2.
+ case (evaluate ae3 e) as [n3 | m3] eqn:E_ae3.
* ...
The proof for Exercise 11.b is also a proof by cases, depending on the result of evaluating each of ae1, ae2, and ae3. Reflecting that Exercise 11.b is about right-to-left evaluation, however, this proof starts as follows:
intros evaluate S_evaluate ae1 ae2 ae3 e.
case (evaluate ae3 e) as [n3 | m3] eqn:E_ae3.
- case (evaluate ae2 e) as [n2 | m2] eqn:E_ae2.
+ case (evaluate ae1 e) as [n1 | m1] eqn:E_ae1.
* ...
Here is the complete skeleton of this proof:
intros evaluate S_evaluate ae1 ae2 ae3 e.
case (evaluate ae3 e) as [n3 | m3] eqn:E_ae3.
- case (evaluate ae2 e) as [n2 | m2] eqn:E_ae2.
+ case (evaluate ae1 e) as [n1 | m1] eqn:E_ae1.
* ...
* ...
+ ...
- ...
See how there are four (4) subcases?
One might be tempted to be smart and to use ; to flatten the proof. Here is the skeleton of that proof:
intros evaluate S_evaluate ae1 ae2 ae3 e.
case (evaluate ae3 e) as [n3 | m3] eqn:E_ae3;
case (evaluate ae2 e) as [n2 | m2] eqn:E_ae2;
case (evaluate ae1 e) as [n1 | m1] eqn:E_ae1.
- admit.
- admit.
- admit.
- admit.
- admit.
- admit.
- admit.
- admit.
See how there are eight (8) subcases? Why is that? What are these four more subcases and how are they proved?
As usual, the proof is by cases, depending on the result of evaluating the second argument of Times. Proving the second case, however, fails, indicating that Literal 0 is not an absorbing element for Times on the left. (See the accompanying .v file documenting the live-proving session at the lecture.)
If all of the properties from Exercise 07 to Exercise 18 hold unconditionally, you can skip this exercise.
Otherwise, can you state a conditional version for each property that does not hold? In other words, if you have proved that for all arithmetic expressions ae, a property does not hold, try to prove that for all arithmetic expressions ae such that something or other holds about ae, this property actually does hold. Seek generality.
Assuming that Literal 0 is not neutral for Plus on the left for left-to-right evaluation, here is one example for such a conditional observational equivalence:
Proposition sufficient_conditions_for_Literal_0_to_be_neutral_for_Plus_on_the_left_ltr :
forall evaluate : arithmetic_expression -> environment nat -> expressible_value,
specification_of_evaluate_ltr evaluate ->
forall (ae : arithmetic_expression)
(e : environment nat),
...properties of the evaluation of ae in e... ->
evaluate (Plus (Literal 0) ae) e = evaluate ae e.
Proposition necessary_conditions_for_Literal_0_to_be_neutral_for_Plus_on_the_left_ltr :
forall evaluate : arithmetic_expression -> environment nat -> expressible_value,
specification_of_evaluate_ltr evaluate ->
forall (ae : arithmetic_expression)
(e : environment nat),
evaluate (Plus (Literal 0) ae) e = evaluate ae e ->
...properties of the evaluation of ae in e... .
Proposition Literal_0_is_conditionally_neutral_for_Plus_on_the_left_ltr :
forall evaluate : arithmetic_expression -> environment nat -> expressible_value,
specification_of_evaluate_ltr evaluate ->
forall (ae : arithmetic_expression)
(e : environment nat),
...properties of the evaluation of ae in e...
<->
evaluate (Plus (Literal 0) ae) e = evaluate ae e.
Here, since Literal 0 is a neutral element for Plus on the left for left-to-right evaluation, (witness the Solution for Exercise 07), ...properties of the evaluation of ae in e... is True, the neutral element of logical disjunction.)
The Solution for Exercise 13.a showed that when evaluation proceeds from left to right, Literal 0 is not an absorbing element for Times on the left, and therefore the observational equivalence does not hold.
The accompanying .v file documenting the live-proving session at the lecture contains a conditional observational equivalence for Literal 0 to be an absorbing element for Times on the left when evaluation proceeds from left to right.
In the light of observational equivalence, revisit Exercise 05 in Chapter Arithmetic expressions with names.
Bong-sun: This chapter has implications well outside LPP.
Pablito: How so?
Dana: Well, the arithmetic expressions we write, e.g., in C, are not arithmetic expressions.
Halcyon (sententious): Indeed they are not. They are syntactic representations of arithmetic expressions.
Bong-sun: Right. And so we can’t massage them as we would massage arithmetic expressions in mathematics.
Pablito: OK, I get that. For example, given an arbitrary C expression e, I can’t just simplify e * 0 into 0.
Halcyon (judicious): And 0 * e into 0.
Pablito: Right. This simplification is incorrect when evaluating e has an effect. For example, it could contain x++ or a division by 0.
Dana: So we should not perform this simplification... and neither should the optimization phase in the compiler.
Anton (sinister): Otherwise there would be a bug in the compiler.
Bong-sun: On the other hand, if we can determine that evaluating e has no effect – i.e., that e is “pure” – then the simplification is valid.
Alfrothul: So we need to know the semantics of our programming language in other to write programs. For example, multiplication left-distributes over addition if evaluation proceeds from left to right but not if evaluation proceeds from right to left.
Loki (ironic): You mean programming is not just coding?
The Greek chorus: UN ANGE PASSE.
Bong-sun: Associativity is OK, though.
Dana: Yes, since it does not change the order in which the sub-expressions are evaluated.
Pablito (shyly): Actually, I meant to ask – what is the big deal about associativity anyway?
Dana: Another good question, Pablito. The associativity rule says that two nested binary operations can be re-associated to the left or to the right.
Pablito: Thank you. And I get that it does. Re-associate, I mean. To the left or to the right. Our choice.
Dana: Now suppose you have an expression with many additions and you fully reassociate it.
Pablito: To the left or to the right?
Dana: Your choice. How would characterize the result?
Pablito: Well, I would say that doing that to a bushy expression has the effect of flattening it?
Dana: Yes it does. For example, (1 + 2) + (3 + 4) is either flattened into ((1 + 2) + 3) + 4 if it is fully reassociated to the left, or it is flattened into 1 + (2 + (3 + 4)) if it is fully reassociated to the right.
Bong-sun: And if the expression is already flat, fully re-associating it has either no effect because it was already flat, or it flattens it in the other direction.
Dana: So when a compiler “flattens the code”...
Bong-sun: ...it actually re-associates binary operations.
Alfrothul: Which only works if these binary operations are associative.
Loki: So when we want to justify the correctness of a program transformation...
Mimer: ...we argue semantics.
Anton: That sounds complicated.
Mimer: Not necessarily. Did you find the observational-equivalence exercises complicated?
Anton: They were doable. We just reasoned based on the specification of the interpreter.
Mimer: Which provides the meaning – the semantics – of arithmetic expressions. So literally, you were arguing semantics. Formally, even.
Anton: I guess we did.
Dana: The heart of the matter, though, is that Plus is associative because + is associative and because of the deterministic way the interpreter processes error cases.
Alfrothul: Another case in point – + is commutative but Plus is not commutative because of the deterministic way the interpreter processes error cases.
Bong-sun: So the properties of these syntactic arithmetic expressions are inherited from the semantic properties of arithmetic expressions in Gallina, modulo the deterministic way the interpreter processes error cases.
Mimer: Yup.
Extracted the beginning of this chapter to create Chapter Arithmetic expressions with names [21 May 2025]
Fixed a typo, thanks to Kakkad Shreya Ketan’s eagle eye [12 Apr 2025]
Properly spelled “indistinguishable”, thanks to Lei Jianwen’s eagle eye [12 Apr 2025]
Tuned the narrative and added the postlude [12 Apr 2025]
Added One solution among many for Exercise 19 [12 Apr 2025]
Added a Solution for Exercise 07, some Food for thought about solving Exercise 07, a Solution for Exercise 11.a, and some Food for thought about solving Exercise 11 [11 Apr 2025]
Added the live-proving session that took place at the lecture [11 Apr 2025]
Created [11 Apr 2025]