When writing a program in OCaml (resp. when writing a compiler for OCaml programs), one is tempted to simplify one’s program (resp. source programs). The goal of the following series of exercises is to reflect on which simplifications are valid and which are not. To this end, we introduce the following notion of equivalence: two expressions are observationally equivalent if evaluating them carries out the same computation.
Each OCaml program is inductively assembled using the syntax constructors enumerated in the BNF of OCaml:
Each of these syntactic constructions was introduced by describing:
For example,
given a test expression, e1, a consequent expression, e2, and an alternative expression, e3, the corresponding conditional expression is written as if e1 then e2 else e3;
in any type environment G, the expression if e1 then e2 else e3 has type t whenever in that environment, e1 (the test) has type bool and each of e2 (the consequent) and e3 (the alternative) has type t:
| IF | G |- e1 : bool | G |- e2 : t | G |- e3 : t | |
| G |- if e1 then e2 else e3 : t | ||||
The Food for thought in Week 05 recapitulates how each expression is evaluated in OCaml:
Either way, evaluation may have side effects: data may be read or written (e.g., to trace the computation), files may be open or closed, etc.
Evaluating an expression might not terminate (or again: might “diverge”):
For example, consider the following recursive OCaml function:
let rec diverge_silently () =
diverge_silently ();;
The only thing it does is to tail-call itself.
So calling this function does not terminate:
# diverge_silently ();;
C-c C-cInterrupted.
#
Food for thought: what is the type of diverge_silently and why does this type makes sense?
For another example, consider the following recursive OCaml function:
let diverge_noisily () =
let rec loop n =
let () = Printf.printf "%d bottles of beer on the wall\n" n in
loop (n + 1)
in let () = Printf.printf "1 bottle of beer on the wall\n" in
loop 2;;
When called, this function emits a message and calls loop, which emits another message and then tail-calls itself.
So calling this function does not terminate:
# diverge_noisily ();;
1 bottle of beer on the wall
2 bottles of beer on the wall
3 bottles of beer on the wall
4 bottles of beer on the wall
5 bottles of beer on the wall
6 bottles of beer on the wall
7 bottles of beer on the wall
...
Food for thought: what is the type of diverge_noisily and why does this type makes sense?
Evaluating an expression might raise an error.
If the expression contains an explicit assertion that fails, then evaluating this expression raises an error.
For example, consider the following OCaml function:
let zero_or_one n =
let () = assert (0 <= n && n <= 1) in
if n = 0
then "zero"
else "one";;
When this function is called on an integer which is not 0 or 1, its assertion fails and an error is raised:
# zero_or_one 2 = "zero";;
Exception: Assert_failure ("//toplevel//", 1969, -55).
#
Evaluating zero_or_one 2 does not complete, nor does evaluating zero_or_one 2 = "zero".
If the expression contains an implicit assertion that fails, then evaluating this expression also raises an error:
# String.get "" 0;;
Exception: Invalid_argument "index out of bounds".
#
If the expression contains a division by 0, then evaluating this expression raises an error:
# (1 / 0) = 0;;
Exception: Division_by_zero.
#
Evaluating 1 / 0 does not complete, nor does evaluating (1 / 0) = 0.
The implementation of OCaml dedicates a memory area, the “runtime stack”, to manage nested function calls. Too many nested calls (typically recursive calls) can make this memory area overflow.
For example, consider the following recursive OCaml function:
let rec overflow_silently () =
not (overflow_silently ());;
Applying this function induces unboundedly many non-tail calls, which makes the runtime stack overflow:
# overflow_silently ();; Stack overflow during evaluation (looping recursion?). #Evaluating the expression overflow_silently () does not complete, nor does evaluating not (overflow_silently ()).
For another example, consider the following recursive OCaml function:
let rec overflow_noisily () =
let () = Printf.printf "Thanks for calling.\n" in
not (overflow_noisily ());;
Applying this function induces unboundedly many non-tail calls, which makes the runtime stack overflow:
# overflow_noisily ();; Thanks for calling. Thanks for calling. Thanks for calling. ... Stack overflow during evaluation (looping recursion?). #Evaluating the expression overflow_noisily () does not complete, nor does evaluating not (overflow_noisily ()).
Evaluating an expression might terminate and yield a value, possibly with side effects, e.g., emitting traces for calls and returns:
# twice_v1 3;;
- : int = 6
# traced_twice_v1 3;;
twice_v1 3 ->
visit 3 ->
visit 2 ->
visit 1 ->
visit 0 ->
visit 0 <- 0
visit 1 <- 2
visit 2 <- 4
visit 3 <- 6
twice_v1 3 <- 6
- : int = 6
#
Evaluating twice_v1 3 and traced_twice_v1 3 both complete, but the latter evaluation can be observed to emit a trace of its recursive calls and returns.
The present section is a reprise of the section with the same name in the mini-project about the underlying determinism of OCaml.
Just like an OCaml expression is a combination of its parts, evaluating an OCaml expression is a combination of evaluating its parts:
As a corollary, evaluating a pure expression always silently completes, i.e., (1) always yields a value, and (2) performs no observable side effects such as tracing.
Two expressions are observationally equivalent when evaluating them carries out the same computation, whether this computation diverges, raises an error, or yields a value, with or without observable side effects.
For example (see Exercise 08 below),
using an_int, the tracing identity function over integers from the mini-project about the underlying determinism of OCaml:
let an_int n =
let () = Printf.printf "processing %d...\n" n in
n;;
the two expressions an_int 1 + an_int 10 and an_int 10 + an_int 1 are not observationally equivalent because while evaluating them yields the same result, we observe that their traces (i.e., what is printed out in the course of evaluation) are not emitted in the same order:
# an_int 1 + an_int 10;;
processing 10...
processing 1...
- : int = 11
# an_int 10 + an_int 1;;
processing 1...
processing 10...
- : int = 11
#
the two expressions 1 + 10 and 10 + 1 are observationally equivalent because evaluating them silently yields the same result.
The exercises below invite us to ponder whether some OCaml expressions are equivalent. To answer this question, one should enumerate each of the possibilities, namely:
To prove that two expressions are not observationally equivalent, one example is enough.
For any OCaml name b of type bool, are the following expressions observationally equivalent?
Justify your answer.
For any OCaml expression e of type bool, are the following expressions observationally equivalent?
Justify your answer.
First of all, we note that the 3 expressions are pure.
Evaluating b, a name of type bool, yields its value in the current environment. This value is either true or false, a Boolean.
To evaluate if b then true else false, we first evaluate b. Evaluating b, a name of type bool, yields its value in the current environment, a Boolean. If this value is true, evaluating if b then true else false reduces to evaluating true, which yields true. If this value is false, evaluating if b then true else false reduces to evaluating false, which yields false.
To evaluate b = true, we first evaluate true, which yields true. We then evaluate b, a name of type bool, which yields its value in the current environment, a Boolean. If this value is true, evaluating b = true reduces to applying the equality predicate to true and true, which yields true. If this value is false, evaluating b = true reduces to applying the equality predicate to false and true, which yields false.
To sum up, if b denotes true in the current environment, then evaluating each of the 3 expressions yields true, and if b denotes false in the current environment, then evaluating each of the 3 expressions yields false.
Therefore, evaluating the 3 expressions always yield the same value, and since each of them is pure, they are observationally equivalent.
Generalizing, and by the same argument, we observe that for any value v of type bool, the expressions v, if v then true else false, and v = true are equivalent.
First of all, we note that the 3 expressions are pure if e is pure, and are impure if e is impure.
We also note that evaluating each of the 3 expressions requires one to evaluate e first. So if evaluating e induces side effects, these side effects will take place in the same order.
Evaluating e either diverges, or raises an error, or yields a value, possibly performing side effects in passing. This value is either true or false, a Boolean.
So in all cases, evaluating the 3 expressions gives rise to the same computation: these 3 expressions are observationally equivalent.
For any OCaml name b2 of type bool, are the following expressions observationally equivalent?
Justify your answer.
For any OCaml expression e of type bool, are the following expressions observationally equivalent?
Justify your answer.
First of all, we note that the two expressions are pure.
Evaluating b2, a name of type bool, yields its value in the current environment. This value is either true or false, a Boolean.
To evaluate b2 || not b2, we first evaluate b2. Evaluating b2, a name of type bool, yields its value in the current environment, a Boolean.
So in both cases, evaluating b2 || not b2 yields true.
As for the second expression, evaluating true yields true.
Therefore, evaluating either expression always yields the same value, and since each of these expressions is pure, they are observationally equivalent.
Generalizing, and by the same argument, we observe that for any value v of type bool, the expressions v || not v and true are observationally equivalent.
First of all, we note that the first expression is pure if e is pure and is impure if e is impure, and that the second expression is pure.
Therefore the two expressions are not observationally equivalent, which we can illustrate with a tracing version of the identity function:
let a_bool b =
let () = Printf.printf "processing %B...\n" b in
b;;
Here are two examples:
e is a_bool true:
# a_bool true || not (a_bool true);;
processing true...
- : bool = true
#
which illustrates short-circuit evaluation in passing, and
e is a_bool false:
# a_bool false || not (a_bool false);;
processing false...
processing false...
- : bool = true
#
In each of these two examples, evaluating e gives rise to a trace. In contrast, evaluating true gives rise to no traces:
# true;;
- : bool = true
#
So the expressions e || not e and true are not observationally equivalent.
For any OCaml expression e, are the following expressions observationally equivalent?
Justify your answer.
For any OCaml expression e, are the following expressions observationally equivalent?
Justify your answer.
For any OCaml expression e, are the following expressions observationally equivalent?
Justify your answer.
For any OCaml expressions e1, e2, and e3, are the following expressions observationally equivalent?
Justify your answer.
First of all, we note that evaluating each of the two expressions requires e to be evaluated first. So if evaluating e induces side effects, these side effects will take place in the same order.
So evaluating let x = e in x requires one to first evaluate e. If this evaluation yields a value, then evaluating let x = e in x reduces to evaluating x in an environment where x denotes this value.
So in both cases, the evaluation proceeds in the same way and yields the same result: the two expressions are observationally equivalent.
Evaluating let x2 = (let x1 = e1 in e2) in e3 in an environment G requires one to first evaluate let x1 = e1 in e2 in G, which requires one to first evaluate e1 in G. Assuming that evaluating e1 yields a value v1, e2 is then evaluated in an extension of G that binds x1 to v1 (let us name it G1). Assuming that evaluating e2 yields a value v2, e3 is then evaluated in an extension of G that binds x2 to v2.
Evaluating let x1 = e1 in let x2 = e2 in e3 in the same environment G requires one to first evaluate e1 in G. Assuming that evaluating e1 yields a value v1 (which can only be the same value as above, due to the determinism of OCaml’s evaluation), let x2 = e2 in e3 is then evaluated in an extension of G that binds x1 to v1 (let us name it G1 too). Evaluating let x2 = e2 in e3 in G1 requires one to first evaluate e2 in G1. Assuming that evaluating e2 yields a value v2 (which again can only be the same value as above, due to the determinism of OCaml’s evaluation), e3 is then evaluated in an extension of G1 that binds x2 to v2.
Therefore in the first case, e3 is evaluated in an extension of G that binds x2 to v2 and in the second case, e3 is evaluated in G1 that binds x2 to v2. So if e3 contains x1 and x1 is evaluated in the course of evaluating e3, the result of evaluation will differ: these two expressions are not observationally equivalent.
To wit, let x1 denote 100 in the global environment, let e1 be 0, e2 be x1 + 10, and e3 be x1 + x2:
# let x1 = 100;;
val x1 : int = 100
# let x2 = (let x1 = 0 in x1 + 10) in x1 + x2;;
- : int = 110
# let x1 = 0 in let x2 = x1 + 10 in x1 + x2;;
- : int = 10
#
If x1 does not occur in e3 or if x1 occurs in e3 but is not evaluated in the course of evaluating e3, the two expressions are observationally equivalent.
For any OCaml expression e, are the following expressions observationally equivalent?
Justify your answer.
For any OCaml expressions e1, e2, and e3, are the following expressions observationally equivalent?
Justify your answer.
For any OCaml expressions e1, e2, e3, e4, and e5, are the following expressions observationally equivalent?
Justify your answer.
Pablito (out of breath, having ran all the way from the Mechanical solution for Exercise 09): I can do this, I can do this. First, the generic description of how conditional expressions are evaluated:
Pablito (thinking aloud): Lucky me, the names are the same in the description and in the first expression. Now for instantiating this description with the second expression: e1 is not e1, e2 is e3, and e3 is e2. Easy peasy:
Pablito (vocalizing his train of thoughts): The generic description of how applications are evaluated, trimming it to the fact that we are applying a predefined function:
Pablito (celeritous): Now for instantiating this description: e0 is not and e1 is e1. Again, easy peasy:
Pablito (continuing): So, splicing this instantiated description of applications in the previous instantiation of conditional expressions:
Pablito (reasoning): So all in all, in both cases, e1 is evaluated, and
Pablito (concluding): So the two expressions are observationally equivalent.
Anton (who sedately arrived in the meanwhile): Yup. Awesome.
Pablito (beaming): Yes.
Anton: To solve Part c. of this exercise, however, the names in the abstract description are really clashing with the names in the concrete expressions.
Pablito (radical): Let me capitalize them:
Anton: That lifts the confusion indeed.
Peter Landin: It does, doesn’t it?
Mimer: Prof. Landin! Thank you so much for coming by! Er, would you mind autographing my copy of “The Mechanical Evaluation of Expressions”? Do forgive its worn-out appearance, it’s all the well thumbing.
Peter Landin: Sure. I’m not the Beatles, though.
Olin Shivers: Mine too?
Simplify the following OCaml expression (and justify your simplification):
if (if b || not b then true else false) then true else false
where b is an OCaml name.
Simplify the following OCaml expression (and justify your simplification):
if b then b else b
where b is an OCaml name.
Simplify the following OCaml expression (and justify your simplification):
if e then e else e
where e is an OCaml expression.
Are the following two expressions observationally equivalent?
where e1 and e2 are OCaml expressions.
Given any OCaml expressions e1, e2, and e3, are the following two expressions observationally equivalent?
The question is whether + is associative in OCaml.
Reminders:
for any expressions e0 and e1, evaluating e0 e1 requires first evaluating e1;
if evaluating e1 completes, it yields a value v1 (let us say of type t1, for some t1),
then evaluating e0 e1 requires evaluating e0;
if evaluating e0 completes, it yields a value v0, which is a function (let us say of type t1 -> t2, for some t2), due to the typing constraints of OCaml;
evaluating e0 e1 then reduces to applying v0 to v1;
if this application completes, it yields a value v2 of type t2, due to the typing constraints of OCaml;
for any expressions e1 and e2, e1 + e2 is syntactic sugar for Int.add e1 e2, or more precisely for (Int.add e1) e2 since application associates to the left;
So evaluating e1 + e2 takes the same steps as evaluating (Int.add e1) e2:
evaluating (Int.add e1) e2 requires first evaluating e2;
if evaluating e2 completes, it yields a value v2, which is of type int due to the typing constraints of OCaml
then evaluating (Int.add e1) e2 requires evaluating Int.add e1;
evaluating Int.add e1 requires first evaluating e1;
if evaluating e1 completes, it yields a value v1, which is of type int due to the typing constraints of OCaml;
then evaluating Int.add e1 requires evaluating Int.add;
evaluating Int.add yields the value this name denotes in the current environment; this value is a function of type int -> int -> int due to the typing constraints of OCaml;
evaluating Int.add e1 then reduces to applying this function to v1; the result is a function of type int -> int, due to the typing constraints of OCaml;
evaluating (Int.add e1) e2 then reduces to applying this function to v2; the result is a value of type int, due to the typing constraints of OCaml; more precisely, this value is the result of adding v1 to v2, because the function denoted by Int.add implements the addition function.
Here is a simplified version:
evaluating e1 + e2 requires first evaluating e2;
if evaluating e2 completes, it yields a value v2, which is of type int, due to the typing constraints of OCaml;
then evaluating e1 + e2 requires evaluating e1;
if evaluating e1 completes, it yields a value v1, which is of type int, due to the typing constraints of OCaml;
evaluating e1 + e2 then reduces to adding v1 to v2; the result is a value of type int, due to the typing constraints of OCaml.
Let us use this simplified version to answer the question:
To sum up, in both cases,
in that order. So if computational effects take place (from tracing to raising an error to diverging), they do in the same order. If the three evaluations complete, they give rise to the values v1, v2, v3. Evaluating the first expression gives rise to the addition (v1 + v2) + v3, and evaluating the first expression gives rise to the addition v1 + (v2 + v3), which yield the same result because addition is associative.
Therefore yes, the two expressions are observationally equivalent: + is associative in OCaml.
Given any OCaml expressions e1 and e2, are the following two expressions observationally equivalent?
The question is whether + is commutative in OCaml.
The following answer is based on the reminders listed in Solution for Exercise 07:
To sum up,
So if computational effects take place (from tracing to raising an error to diverging), they do in a different order.
Therefore no, the two expressions are not observationally equivalent: + is not commutative in OCaml over arbitrary expressions. For a simple example that uses an_int, the tracing identity function over integers:
# an_int 1 + an_int 10;;
processing 10...
processing 1...
- : int = 11
# an_int 10 + an_int 1;;
processing 1...
processing 10...
- : int = 11
#
The two traces are not the same.
That said, if e1 and e2 are pure expressions, then it does not matter in which order they are evaluated, and the two expressions are observationally equivalent: + is commutative in OCaml over pure expressions.
Given an OCaml expression e and a pure OCaml expression pe, are the following two expressions observationally equivalent?
Anton: Mechanical now.
Alfrothul: I am tempted to think so.
Anton: Pray elaborate.
Dana: May I, Alfrothul?
Alfrothul: By all means.
Dana: The lecture notes so far have a common thread, namely abstracting concepts and instantiating them. Concepts are abstracted by parameterizing them, and then they are instantiated by supplying concrete arguments for these parameters.
Alfrothul: For example, functions are parameterized expressions.
Dana: And structurally recursive functions are abstracted into fold or parafold functions.
Anton: OK.
Dana: But it’s not just that. For example, in a grammar, non-terminals are instantiated to construct an abstract-syntax tree, and likewise, proof trees are constructed by instantiating proof rules.
Alfrothul: In the same vein, the characteristic equations of the S-m-n theorem are instantiated to account for specific situations, e.g., to specialize an interpreter.
Anton: All right, all right, I get it. Now what is generic here that you want to instantiate to solve Exercise 09 mechanically?
Dana: The evaluation of OCaml expressions.
Anton: Now what.
Alfrothul: Look at the beginning of the Solution for Exercise 08. It reminds us of the process of evaluating an addition in OCaml.
Anton: OK, I see that:
Dana: This description is parameterized by e1 and e2.
Alfrothul: All that we need to do is to instantiate it with e and pe, and then with pe and e.
Dana: Then we can simplify the instantiations.
Alfrothul: And then we can compare the result of the simplifications.
Anton: Interesting. Let me try for e and pe:
Wow, this specific description of how e + pe is evaluated can indeed be simplified. For example, pe is pure, so evaluating it always completes and makes no side effects. Let’s see:
Pablito: The same goes for pe and e:
OK, similar simplifications can take place:
Alfrothul: So in both cases, e is evaluated, which can be observed if it is impure. Otherwise, pe is evaluated, which cannot be observed since it is pure. And addition takes place, a pure operation that cannot be observed.
Dana: The only difference is that in one case, n2 and n1 are added, and in the other, n1 and n2 are added. Since addition is commutative, the result is the same.
Anton: So observably, the evaluations proceed in the same way and the result is the same.
Dana: Yes. The two expressions are observationally equivalent.
Alfrothul: And the argument was mechanical.
Pablito (leaving on a run): That was awesome. Thanks, guys!
Anton: Where is he going?
Dana (smiling): To Exercise 05.
Changed the non-terminal for pure expressions to be pe and expanded Exercise 06 [04 Mar 2023]
Created [10 Jan 2023]