When are two expressions equal? Two possible answers are:
When they are syntatically identical.
When they are semantically equivalent: they produce the same value.
For example, are
41+1 equal? The syntactic answer
would say they are not, because they involve different tokens.
The semantic answer would say they are: they both produce the value
What about functions: are
fun x -> x and
fun y -> y equal? Syntactically
they are different. But semantically, they both produce a value that is the
identity function: when they are applied to an input, they will both produce
the same output. That is,
(fun x -> x) z = z, and
(fun y -> y) z = z. If
it is the case that for all inputs two functions produce the same output,
we will consider the functions to be equal:
if (forall x, f x = g x), then f = g.
That definition of equality for functions is known as the Axiom of Extensionality in some branches of mathematics; henceforth we'll refer to it simply as "extensionality".
Here we will adopt the semantic approach. If
e2 evaluate to the same
v, then we write
e1 = e2. We are using
= here in a mathematical
sense of equality, not as the OCaml polymorphic equality operator. For example,
(fun x -> x) = (fun y -> y), even though OCaml's operator would raise
an exception and refuse to compare functions.
We're also going to restrict ourselves to expressions that are well typed, pure (meaning they have no side effects), and total (meaning they don't have exceptions or infinite loops).