The goal of this chapter is to study several specifications of an evaluation function for arithmetic expressions with names.
A source arithmetic expression is either a literal, a name, an addition, or a multiplication:
Definition name : Type :=
string.
Inductive arithmetic_expression : Type :=
Literal : nat -> arithmetic_expression
| Name : name -> arithmetic_expression
| Plus : arithmetic_expression -> arithmetic_expression -> arithmetic_expression
| Times : arithmetic_expression -> arithmetic_expression -> arithmetic_expression.
An environment is an abstract data type that binds names to denotations:
Definition environment (denotable : Type) : Type :=
...
Names are looked up in an environment using a lookup function:
Definition lookup (denotable : Type) (x : name) (e : environment denotable) : option denotable :=
...
Looking up for a name in an environment that does not bind this name yields None. Looking up for a name in an environment that binds this name to a denotable d yields Some d.
In the accompanying .v file, an environment is defined as a list of pairs.
Arithmetic expressions are evaluated in an environment. This evaluation either yields a number or an error message:
Inductive msg : Type :=
Undeclared_name : name -> msg.
Inductive expressible_value : Type :=
Expressible_nat : nat -> expressible_value
| Expressible_msg : msg -> expressible_value.
In this informal specification,
given a literal and given an environment,
evaluating this literal in this environment yields the number represented by this literal;
given a name and given an environment that binds this name to a denotation,
evaluating this name in this environment yields this denotation;
given a name and given an environment that does not bind this name to a denotation,
evaluating this name in this environment yields an error message;
given two arithmetic expressions and given an environment,
if evaluating each of these arithmetic expressions in this environment yields a number
then evaluating the syntactic addition of these two arithmetic expressions in this environment yields the semantic addition of these two numbers;
given two arithmetic expressions and given an environment,
if evaluating either arithmetic expression in this environment yields an error
then evaluating the syntactic addition of these two arithmetic expressions in this environment yields this error;
and likewise for multiplications (replace “addition” with “multiplication”).
This specification is ambiguous because given two arithmetic expressions whose evaluation yields two distinct errors, which of these two errors should be yielded by the evaluation of the syntactic addition or multiplication of these two arithmetic expressions?
We formalize the specification as a parameterized conjunction, with one conjunct for each syntax constructor:
Definition specification_of_evaluate (evaluate : arithmetic_expression -> environment nat -> expressible_value) :=
...conjunct for Literal...
/\
...conjunct for Name...
/\
...conjunct for Plus...
/\
...conjunct for Times...
For literals, the informal specification reads:
given a literal and given an environment,
evaluating this literal in this environment yields the number represented by this literal;
Formally:
forall (n : nat)
(e : environment nat),
evaluate (Literal n) e = Expressible_nat n
For names, the informal specification reads:
given a name and given an environment that binds this name to a denotation,
evaluating this name in this environment yields this denotation;
given a name and given an environment that does not bind this name to a denotation,
evaluating this name in this environment yields an error message;
Formally:
(forall (x : string)
(e : environment nat)
(n : nat),
lookup nat x e = Some n ->
evaluate (Name x) e = Expressible_nat n)
/\
(forall (x : string)
(e : environment nat),
lookup nat x e = None ->
evaluate (Name x) e = Expressible_msg (Undeclared_name x))
For additions, the informal specification reads:
given two arithmetic expressions and given an environment,
if evaluating each of these arithmetic expressions in this environment yields a number
then evaluating the syntactic addition of these two arithmetic expressions in this environment yields the semantic addition of these two numbers;
given two arithmetic expressions and given an environment,
if evaluating either arithmetic expression in this environment yields an error
then evaluating the syntactic addition of these two arithmetic expressions in this environment yields this error;
Formally:
(forall (ae1 ae2 : arithmetic_expression)
(e : environment nat)
(n1 n2 : nat),
evaluate ae1 e = Expressible_nat n1 ->
evaluate ae2 e = Expressible_nat n2 ->
evaluate (Plus ae1 ae2) e = Expressible_nat (n1 + n2))
/\
(forall (ae1 ae2 : arithmetic_expression)
(e : environment nat)
(m1 : msg),
evaluate ae1 e = Expressible_msg m1 ->
evaluate (Plus ae1 ae2) e = Expressible_msg m1)
/\
(forall (ae1 ae2 : arithmetic_expression)
(e : environment nat)
(m2 : msg),
evaluate ae2 e = Expressible_msg m2 ->
evaluate (Plus ae1 ae2) e = Expressible_msg m2)
For multiplications, the informal specification and the formal specification read likewise (replacing “addition” with “multiplication”, Plus with Times, and + with *).
The following theorem captures the ambiguity of this specification:
Theorem specification_of_evaluate_is_ambiguous :
forall evaluate : arithmetic_expression -> environment nat -> expressible_value,
specification_of_evaluate evaluate ->
exists (ae : arithmetic_expression)
(e : environment nat),
evaluate ae e <> evaluate ae e.
The accompanying .v file contains a proof of this theorem where Plus (Name "x") (Name "y") is the witness arithmetic expression and the empty environment is the witness environment. And indeed evaluating (Name "x") in the empty environment yields one error message and evaluating (Name "y") in the empty environment yields another error message, and so
Since these two error messages are distinct, specification_of_evaluate is ambiguous.
In this left-to-right specification,
given a literal and given an environment,
evaluating this literal in this environment yields the number represented by this literal;
given a name and given an environment that binds this name to a denotation,
evaluating this name in this environment yields this denotation;
given a name and given an environment that does not bind this name to a denotation,
evaluating this name in this environment yields an error message;
given two arithmetic expressions and given an environment,
if evaluating the first arithmetic expression in this environment yields a number and then if evaluating the second arithmetic expression in this environment yields another number
then evaluating the syntactic addition of these two arithmetic expressions in this environment yields the semantic addition of these two numbers;
given two arithmetic expressions and given an environment,
if evaluating the first arithmetic expression in this environment yields a number and then if evaluating the second arithmetic expression in this environment yields an error
then evaluating the syntactic addition of these two arithmetic expressions in this environment yields this error;
given two arithmetic expressions and given an environment,
if evaluating the first arithmetic expression in this environment yields an error
then evaluating the syntactic addition of these two arithmetic expressions yields this error;
and likewise for multiplications (replace “addition” by “multiplication”).
Whereas the ambiguous specification said “either” in the second-to-last clause, this specification says “the first”: Evaluation proceeds from left to right.
We formalize the specification as a parameterized conjunction, with one conjunct for each syntax constructor:
Definition specification_of_evaluate_ltr (evaluate : arithmetic_expression -> environment nat -> expressible_value) :=
...conjunct for Literal...
/\
...conjunct for Name...
/\
...conjunct for Plus...
/\
...conjunct for Times...
For literals, the informal specification reads:
given a literal and given an environment,
evaluating this literal in this environment yields the number represented by this literal;
Formally:
forall (n : nat)
(e : environment nat),
evaluate (Literal n) e = Expressible_nat n
For names, the informal specification reads:
given a name and given an environment that binds this name to a denotation,
evaluating this name in this environment yields this denotation;
given a name and given an environment that does not bind this name to a denotation,
evaluating this name in this environment yields an error message;
Formally:
(forall (x : string)
(e : environment nat)
(n : nat),
lookup nat x e = Some n ->
evaluate (Name x) e = Expressible_nat n)
/\
(forall (x : string)
(e : environment nat),
lookup nat x e = None ->
evaluate (Name x) e = Expressible_msg (Undeclared_name x))
For additions, the informal specification reads:
given two arithmetic expressions and given an environment,
if evaluating the first arithmetic expression in this environment yields a number and then if evaluating the second arithmetic expression in this environment yields another number
then evaluating the syntactic addition of these two arithmetic expressions in this environment yields the semantic addition of these two numbers;
given two arithmetic expressions and given an environment,
if evaluating the first arithmetic expression in this environment yields a number and then if evaluating the second arithmetic expression in this environment yields an error
then evaluating the syntactic addition of these two arithmetic expressions in this environment yields this error;
given two arithmetic expressions and given an environment,
if evaluating the first arithmetic expression in this environment yields an error
then evaluating the syntactic addition of these two arithmetic expressions yields this error;
Formally:
(forall (ae1 ae2 : arithmetic_expression)
(e : environment nat)
(n1 n2 : nat),
evaluate ae1 e = Expressible_nat n1 ->
evaluate ae2 e = Expressible_nat n2 ->
evaluate (Plus ae1 ae2) e = Expressible_nat (n1 + n2))
/\
(forall (ae1 ae2 : arithmetic_expression)
(e : environment nat)
(n1 : nat)
(m2 : msg),
evaluate ae1 e = Expressible_nat n1 ->
evaluate ae2 e = Expressible_msg m2 ->
evaluate (Plus ae1 ae2) e = Expressible_msg m2)
/\
(forall (ae1 ae2 : arithmetic_expression)
(e : environment nat)
(m1 : msg),
evaluate ae1 e = Expressible_msg m1 ->
evaluate (Plus ae1 ae2) e = Expressible_msg m1)
For multiplications, the informal specification and the formal specification read likewise (replacing “addition” with “multiplication”, Plus with Times, and + with *).
Prove that at most one function satisfies the left-to-right specification.
Prove that at least one function satisfies the left-to-right specification.
In this right-to-left specification,
given a literal and given an environment,
evaluating this literal in this environment yields the number represented by this literal;
given a name and given an environment that binds this name to a denotation,
evaluating this name in this environment yields this denotation;
given a name and given an environment that does not bind this name to a denotation,
evaluating this name in this environment yields an error message;
given two arithmetic expressions and given an environment,
if evaluating the second arithmetic expression in this environment yields a number and then if evaluating the first arithmetic expression in this environment yields another number
then evaluating the syntactic addition of these two arithmetic expressions in this environment yields the semantic addition of these two numbers;
given two arithmetic expressions and given an environment,
if evaluating the second arithmetic expression in this environment yields a number and then if evaluating the first arithmetic expression in this environment yields an error
then evaluating the syntactic addition of these two arithmetic expressions in this environment yields this error;
given two arithmetic expressions and given an environment,
if evaluating the second arithmetic expression in this environment yields an error
then evaluating the syntactic addition of these two arithmetic expressions yields this error;
and likewise for multiplications (replace “addition” by “multiplication”).
Whereas the ambiguous specification said “either” in the second-to-last clause, this specification says “the second”: Evaluation proceeds from right to left.
We formalize the specification as a parameterized conjunction, with one conjunct for each syntax constructor:
Definition specification_of_evaluate_rtl (evaluate : arithmetic_expression -> environment nat -> expressible_value) :=
...conjunct for Literal...
/\
...conjunct for Name...
/\
...conjunct for Plus...
/\
...conjunct for Times...
For literals, the informal specification reads:
given a literal and given an environment,
evaluating this literal in this environment yields the number represented by this literal;
Formally:
forall (n : nat)
(e : environment nat),
evaluate (Literal n) e = Expressible_nat n
For names, the informal specification reads:
given a name and given an environment that binds this name to a denotation,
evaluating this name in this environment yields this denotation;
given a name and given an environment that does not bind this name to a denotation,
evaluating this name in this environment yields an error message;
Formally:
(forall (x : string)
(e : environment nat)
(n : nat),
lookup nat x e = Some n ->
evaluate (Name x) e = Expressible_nat n)
/\
(forall (x : string)
(e : environment nat),
lookup nat x e = None ->
evaluate (Name x) e = Expressible_msg (Undeclared_name x))
For additions, the informal specification reads:
given two arithmetic expressions and given an environment,
if evaluating the second arithmetic expression in this environment yields a number and then if evaluating the first arithmetic expression in this environment yields another number
then evaluating the syntactic addition of these two arithmetic expressions in this environment yields the semantic addition of these two numbers;
given two arithmetic expressions and given an environment,
if evaluating the second arithmetic expression in this environment yields a number and then if evaluating the first arithmetic expression in this environment yields an error
then evaluating the syntactic addition of these two arithmetic expressions in this environment yields this error;
given two arithmetic expressions and given an environment,
if evaluating the second arithmetic expression in this environment yields an error
then evaluating the syntactic addition of these two arithmetic expressions yields this error;
Formally:
(forall (ae1 ae2 : arithmetic_expression)
(e : environment nat)
(n2 n1 : nat),
evaluate ae2 e = Expressible_nat n2 ->
evaluate ae1 e = Expressible_nat n1 ->
evaluate (Plus ae1 ae2) e = Expressible_nat (n1 + n2))
/\
(forall (ae1 ae2 : arithmetic_expression)
(e : environment nat)
(n2 : nat)
(m1 : msg),
evaluate ae2 e = Expressible_nat n2 ->
evaluate ae1 e = Expressible_msg m1 ->
evaluate (Plus ae1 ae2) e = Expressible_msg m1)
/\
(forall (ae1 ae2 : arithmetic_expression)
(e : environment nat)
(m2 : msg),
evaluate ae2 e = Expressible_msg m2 ->
evaluate (Plus ae1 ae2) e = Expressible_msg m2)
For multiplications, the informal specification and the formal specification read likewise (replacing “addition” with “multiplication”, Plus with Times, and + with *).
Prove that at most one function satisfies the right-to-left specification.
Prove that at least one function satisfies the right-to-left specification.
Write the specification of an evaluation function where additions are evaluated from left to right and multiplications are evaluated from right to left. What do you make of this specification?
Alfrothul: So...
Dana: Yes?
Alfrothul: In the definition of evaluate_ltr, left-to-right evaluation is implemented by first evaluating the first argument of additions and multiplications, and then only evaluating the second argument if evaluating the first did not yield an error.
Dana: Yes. And vice versa in evaluate_rtl.
Alfrothul: Right. But what if we left this order implicit?
Dana: Ah, you mean that both arguments are evaluated, and then we pattern match on the results of these evaluations?
Alfrothul: Yes. The salient point is the clause for Plus, look:
Fixpoint evaluate_implicit (ae : arithmetic_expression) (e : environment nat) : expressible_value :=
match ae with
Literal n =>
...
| Name x =>
...
| Plus ae1 ae2 =>
match (evaluate_implicit ae1 e, evaluate_implicit ae2 e) with
(Expressible_nat n1, Expressible_nat n2) =>
Expressible_nat (n1 + n2)
| (Expressible_msg m1, _) =>
Expressible_msg m1
| (_, Expressible_msg m2) =>
Expressible_msg m2
end
| Times ae1 ae2 =>
...
end.
Alfrothul (continuing): See how this evaluation function does not specify in which order ae1 and ae2 are evaluated?
Dana: True, but then you test first whether the result of evaluating ae1 is an error.
Alfrothul: Yes, and then I test whether the result of evaluating ae2 is an error.
Dana: So your implicit evaluation function operates from left to right. Indulge me:
Fixpoint evaluate_ltr2 (ae : arithmetic_expression) (e : environment nat) : expressible_value :=
match ae with
Literal n =>
Expressible_nat n
| Name x =>
match lookup nat x e with
Some n =>
Expressible_nat n
| None =>
Expressible_msg (Undeclared_name x)
end
| Plus ae1 ae2 =>
match (evaluate_ltr2 ae1 e, evaluate_ltr2 ae2 e) with
(Expressible_nat n1, Expressible_nat n2) =>
Expressible_nat (n1 + n2)
| (Expressible_msg m1, _) =>
Expressible_msg m1
| (_, Expressible_msg m2) =>
Expressible_msg m2
end
| Times ae1 ae2 =>
match (evaluate_ltr2 ae1 e, evaluate_ltr2 ae2 e) with
(Expressible_nat n1, Expressible_nat n2) =>
Expressible_nat (n1 * n2)
| (Expressible_msg m1, _) =>
Expressible_msg m1
| (_, Expressible_msg m2) =>
Expressible_msg m2
end
end.
Alfrothul: Yes, this definition is what I had in mind.
Dana: And now we can check that evaluate_ltr2 satisfies specification_of_evaluate_ltr.
Alfrothul: Sure, let’s give it a shot:
Theorem evaluate_ltr2_satisfies_the_specification_of_evaluate_ltr :
specification_of_evaluate_ltr evaluate_ltr2.
Halcyon: The proof goes through!
The Greek chorus: SEE THE ACCOMPANYING .V FILE.
Anton: So logically, swapping the two clauses for errors should give right-to-left evaluation. Look:
Fixpoint evaluate_rtl2 (ae : arithmetic_expression) (e : environment nat) : expressible_value :=
match ae with
Literal n =>
Expressible_nat n
| Name x =>
match lookup nat x e with
Some n =>
Expressible_nat n
| None =>
Expressible_msg (Undeclared_name x)
end
| Plus ae1 ae2 =>
match (evaluate_rtl2 ae1 e, evaluate_rtl2 ae2 e) with
(Expressible_nat n1, Expressible_nat n2) =>
Expressible_nat (n1 + n2)
| (_, Expressible_msg m2) =>
Expressible_msg m2
| (Expressible_msg m1, _) =>
Expressible_msg m1
end
| Times ae1 ae2 =>
match (evaluate_rtl2 ae1 e, evaluate_rtl2 ae2 e) with
(Expressible_nat n1, Expressible_nat n2) =>
Expressible_nat (n1 * n2)
| (_, Expressible_msg m2) =>
Expressible_msg m2
| (Expressible_msg m1, _) =>
Expressible_msg m1
end
end.
Dana: Right. Testing first whether evaluating the second argument yields an error should give right-to-left evaluation.
Bong-sun: Let me try:
Theorem evaluate_rtl2_satisfies_the_specification_of_evaluate_rtl :
specification_of_evaluate_rtl evaluate_rtl2.
Halcyon: The proof goes through!
The Greek chorus: SEE THE ACCOMPANYING .V FILE.
Pablito: So how should we implement our evaluation function? As in evaluate_ltr or as in evaluate_ltr2?
Bong-sun: Well, if we think operationally in call by value, we should implement our evaluation function as in evaluate_ltr, since if ae1 evaluates to an error, ae2 is not evaluated.
Anton: And if we think declaratively in call by name, it does not matter since in both cases, ae2 is only evaluated when ae1 does not evaluate to an error.
Halcyon: Welcome to the wonderful world of referential transparency!
Dana: Hmm...
Bong-sun: Yes, Dana?
Dana: The definitions that use a pair contain syntactic sugar.
Anton: Probably. And so what?
Dana: This syntactic sugar is blinding us. Look at the actual definition of evaluate_ltr2:
Print evaluate_ltr2.
Pablito (helpful): The *response* window reads:
evaluate_ltr2 =
fix evaluate_ltr2 (ae : arithmetic_expression) (e : environment nat) {struct ae} : expressible_value :=
match ae with
| Literal n => Expressible_nat n
| Name x =>
match lookup nat x e with
| Some n => Expressible_nat n
| None => Expressible_msg (Undeclared_name x)
end
| Plus ae1 ae2 =>
let (e0, e1) := (evaluate_ltr2 ae1 e, evaluate_ltr2 ae2 e) in
match e0 with
| Expressible_nat n1 =>
match e1 with
| Expressible_nat n2 => Expressible_nat (n1 + n2)
| Expressible_msg m2 => Expressible_msg m2
end
| Expressible_msg m1 => Expressible_msg m1
end
| Times ae1 ae2 =>
let (e0, e1) := (evaluate_ltr2 ae1 e, evaluate_ltr2 ae2 e) in
match e0 with
| Expressible_nat n1 =>
match e1 with
| Expressible_nat n2 => Expressible_nat (n1 * n2)
| Expressible_msg m2 => Expressible_msg m2
end
| Expressible_msg m1 => Expressible_msg m1
end
end
: arithmetic_expression -> environment nat -> expressible_value
Dana: Thanks, Pablito. See how the pairing is implemented? Look at the Plus clause, for example:
| Plus ae1 ae2 =>
match (evaluate_ltr2 ae1 e, evaluate_ltr2 ae2 e) with
(Expressible_nat n1, Expressible_nat n2) =>
Expressible_nat (n1 + n2)
| (Expressible_msg m1, _) =>
Expressible_msg m1
| (_, Expressible_msg m2) =>
Expressible_msg m2
end
Anton: I see that it is desugared as:
| Plus ae1 ae2 =>
let (e0, e1) := (evaluate_ltr2 ae1 e, evaluate_ltr2 ae2 e) in
match e0 with
| Expressible_nat n1 =>
match e1 with
| Expressible_nat n2 => Expressible_nat (n1 + n2)
| Expressible_msg m2 => Expressible_msg m2
end
| Expressible_msg m1 => Expressible_msg m1
end
Dana: Right. And what happens if we unfold the let-expression?
Anton: Harrumph. We get the Plus clause of evaluate_ltr.
Halcyon (dreamily): The wonders of referential transparency...
Consider the following two evaluation functions, where the two components of the pairs, in the Plus and in the Times clauses, are switched:
Fixpoint evaluate_ltr2_switched (ae : arithmetic_expression) (e : environment nat) : expressible_value :=
match ae with
Literal n =>
Expressible_nat n
| Name x =>
match lookup nat x e with
Some n =>
Expressible_nat n
| None =>
Expressible_msg (Undeclared_name x)
end
| Plus ae1 ae2 =>
match (evaluate_ltr2_switched ae2 e, evaluate_ltr2_switched ae1 e) with
(Expressible_nat n2, Expressible_nat n1) =>
Expressible_nat (n1 + n2)
| (Expressible_msg m2, _) =>
Expressible_msg m2
| (_, Expressible_msg m1) =>
Expressible_msg m1
end
| Times ae1 ae2 =>
match (evaluate_ltr2_switched ae2 e, evaluate_ltr2_switched ae1 e) with
(Expressible_nat n2, Expressible_nat n1) =>
Expressible_nat (n1 * n2)
| (Expressible_msg m2, _) =>
Expressible_msg m2
| (_, Expressible_msg m1) =>
Expressible_msg m1
end
end.
Fixpoint evaluate_rtl2_switched (ae : arithmetic_expression) (e : environment nat) : expressible_value :=
match ae with
Literal n =>
Expressible_nat n
| Name x =>
match lookup nat x e with
Some n =>
Expressible_nat n
| None =>
Expressible_msg (Undeclared_name x)
end
| Plus ae1 ae2 =>
match (evaluate_rtl2_switched ae2 e, evaluate_rtl2_switched ae1 e) with
(Expressible_nat n2, Expressible_nat n1) =>
Expressible_nat (n1 + n2)
| (_, Expressible_msg m1) =>
Expressible_msg m1
| (Expressible_msg m2, _) =>
Expressible_msg m2
end
| Times ae1 ae2 =>
match (evaluate_rtl2_switched ae2 e, evaluate_rtl2_switched ae1 e) with
(Expressible_nat n2, Expressible_nat n1) =>
Expressible_nat (n1 * n2)
| (_, Expressible_msg m1) =>
Expressible_msg m1
| (Expressible_msg m2, _) =>
Expressible_msg m2
end
end.
Do these evaluation functions operate from left to right or from right to left?
Created [21 May 2025]