None, due to the midterm project.
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 variable.
Simplify the following OCaml expression (and justify your simplification):
if b then b else b
where b is an OCaml variable.
Are the following two expressions observationally equivalent?
where e1 and e2 are OCaml expressions.
Are the following two expressions observationally equivalent?
where e1, e2, and e3 are OCaml expressions.
Are the following two expressions observationally equivalent?
where e1, e2, and e3 are OCaml expressions.
Reminders:
thanks to its static type system, there are no type errors in OCaml;
all expressions are evaluated in the current environment;
evaluating a variable yields the value this variable denotes in the current environment;
for any expressions e1, e2, and e3, evaluating the conditional expression if e1 then e2 else e3 requires first evaluating its test, i.e., e1;
if evaluating e1 completes, it yields a value v1 of type bool, due to the typing constraints of OCaml;
if v1 is true, then evaluating if e1 then e2 else e3 reduces to evaluating its consequent, i.e., e2;
if v1 is false, then evaluating if e1 then e2 else e3 reduces to evaluating its alternative, i.e., e3.
for any expressions e1 and e2, evaluating the let-expression let x1 = e1 in e2 requires first evaluating its definiens, i.e., e1;
if evaluating e1 completes, it yields a value v1 (let us say of type t1, for some t1);
evaluating let x1 = e1 in e2 then reduces to evaluating e2 in an environment that extends the current environment with the binding of x1 to v1.
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 (+) e1 e2, or more precisely for ((+) e1) e2 since application associates to the left;
So evaluating e1 + e2 takes the same steps as evaluating ((+) e1) e2:
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;
evaluating (+) 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 (+) e1 requires evaluating (+);
evaluating (+), which is a variable, yields the value this variable denotes in the current environment; this value is a function of type int -> int -> int, due to the typing constraints of OCaml;
evaluating (+) 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 ((+) 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 (+) 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 the Solution for Exercise 18:
To sum up, in the first case cases,
in that order. 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:
# let an_int n = let () = Printf.printf "processing %d...\n" n in n;;
val an_int : int -> int = <fun>
# 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, e.g., values, then it does not matter in which order they are evaluated, and the two expressions are observationally equivalent: + is not commutative in OCaml over pure expressions.