4
and like all freedoms, it is not without consequences, but they are consequences90
you must inevitably reconcile on your own.
2. Programming language semantics
How do we know that a certain program computes a certain value? When
we present OCaml with the expression 3 + 4 * 5, how do we know that it will
calculate 23 as the result? This kind of question is the province of a programming 95
language semantics.1semantics
We’ll give the semantics of a language by defining a set of rules that provide a
schematic recipe for transforming one expression into another simpler expression.
Because the output of each rule is intended to be simpler than the input, the rules
are called reduction rules. The input expression to be transformed is the redex,reduction rules
redex
100
and the output its reduction.reduction
The idea is probably already familiar to you, as it is implicitly used as early as
grade school for providing the semantics of arithmetic expressions. For instance,
a sequence of reductions provides a value for the arithmetic expression 3 + 4 · 5:
3 + 4 · 5 −−→ 3 + 20 −−→ 23
Here, I’ve underlined each redex for clarity. The first redex is 4 · 5, for which we
substitute its value 20, implicitly appealing to a reduction rule
4 · 5 −−→ 20
resulting in an expression which is a redex in its entirety, 3 + 20; that redex further
reduces to 23 according to a reduction rule
3 + 20 −−→ 23 .
You may think these reduction rules seem awfully particular. We’d need an infinite
number of them, one for 1 + 1, one for 1 + 2, one for 2 + 1, and so forth. We will
shortly generalize them to more schematic rules.
The reduction approach applies to OCaml arithmetic expressions in exactly the 105
same manner, more or less undergoing a mere change of font.
3 + 4 * 5 −−→ 3 + 20 −−→ 23
2.1. Abstract and Concrete Syntax. In order to apply the reduction rules properly,
we need to have an understanding of the subparts of an expression. The following
is an improper application of the reduction rules, because the bit being substituted
for, the putative redex, is not a proper subpart of the expression: 110
3 + 4 * 5 −−→ 7 * 5 −−→ 35
1Syntax concerns the well-formed structures of a language, semantics the meaning of those structures.
Kally
Highlight
Kally
Highlight
Kally
Highlight
5
Expressions are notated as sequences of lexical items, the “words” that make up
the expressions – 3, +, 4, *, . . . . We call these elementary lexical units tokens. tokens
But expressions are really structured hierarchically as trees of subexpressions. We
distinguish between the abstract syntax of the language, the tree structures that abstract syntax
make up well-formed hierarchical expressions, and the concrete syntax of the concrete syntax115
language, the token sequences that notate those tree structures. Implicitly, the
concrete syntax 3 + 4 * 5 notates the abstract syntax that might be conveyed by
the following tree:
+
*
54
3
The alternative structure expressed in concrete syntax as (3 + 4) * 5would then120
be
*
5+
43
Notice how the abstract syntax has (and needs) no parentheses. Parentheses are
a notion of concrete syntax used to explicate the abstract syntax of an expression.
From here on, we will use the concrete syntax of OCaml to notate the abstract125
syntax where convenient, assuming that no confusion should result.
2.2. Implementing abstract syntax. For the purpose of writing an interpreter for
a language, it is useful to be able to specify the abstract syntax of an expression. An
appropriate abstract data type definition for the abstract syntax of an arithmetic
expression language might be given by the following:130
type expr =
| Num of int
| Unop of unop * expr
| Binop of binop * expr * expr ;;
The unop and binop types enumerate the operators that can be used to form
expressions:
type unop =
| Negate ;;
type binop =
| Plus
6
| Minus
| Times
| Equals
| LessThan ;;
This allows us to construct abstract syntax trees such as
# Binop (Plus, Num 3, Binop (Times, Num 4, Num 5)) ;;
– : expr = Binop (Plus, Num 3, Binop (Times, Num 4, Num 5))
(Section 6.3 discusses how a computer system like a compiler or interpreter con-
verts from concrete syntax to abstract syntax, a process known as parsing.) 135
Exercise 1. Draw the abstract syntax trees for the following concrete arithmetic expres-
sions.
(1) ~- 5 * 3
(2) 3 – 4 – 5
(3) 1 – 2 / 3 + 4 140
(4) (1 – 2) / (3 + 4)
(5) ((1 – 2) / (3 + 4))
(6) (1 – 2) / 3 + 4
�
Exercise 2. Write a function exp_to_string : expr -> string that converts an 145
abstract syntax tree of type expr to a concrete syntax string. �
2.3. Schematic reduction rules. Returning to the reduction semantics for OCaml
arithmetic expressions, the reduction rules governing integer arithmetic covering
a few binary and unary operators might be
m + n −−→ m + n
m * n −−→ m · n
m – n −−→ m − n
m / n −−→ bm/nc
~- n −−→ −n
and so forth. Here, we use the notation m for the OCaml numeral token that 150
encodes the number m. (The floor notation bxc might be unfamiliar to you. Itfloor
specifies the integer obtained by rounding a real number down, so b2.71828c = 2.)
These rules may look trivial, but they are not. The first rule specifies that the +
operator in OCaml when applied to two numerals has the property of generating
the numeral representing their sum. The language being specified might have 155
used the operator ♠ for integer addition, leading to the rule
m ♠ n −−→ m + n
7
making clear the distinction between the object language being defined and the
metalanguage being used to define it.
Similarly, the fourth rule specifies that the / operator in OCaml when applied
to two numerals specifies the integer portion of their ratio. It could have been160
otherwise.2 The language might have used a different operator for integer division,
m // n −−→ bm/nc
(as happens to be used in Python 3 for instance), or could have defined the result
differently, say
m / n −−→ dm/ne .
Nonetheless, there is not too much work being done by these rules, and if that
were all there were to defining a semantics, there would be little reason to go to the165
trouble. Things get more interesting, however, when additional constructs such as
function application are considered, which we turn to next.
3. Substitution semantics
Consider, for instance, the application of a function to an argument, which
would be expressed by a redex of the form (fun 〈var〉 -> 〈body〉) 〈arg〉. This170
allows programs like
(fun x -> x + x) (3 * 4)
The reduction rule for this construct might be something like
(fun x -> P) Q −−→ P[x 7→ Q]
where x stands for an arbitrary variable, and P and Q for arbitrary expressions,
and P[x 7→ Q] is the substitution of Q for x in P.3 Because of the central place of substitution
substitution in providing the semantics of the language, this approach to semantics175
is called substitution semantics. substitution semantics
Exercise 3. Give the expressions (in concrete syntax) specified by the following substitu-
tions:
(1) (x + x)[x 7→ 3]
(2) (x + x)[y 7→ 3]180
2What may be mind-boggling here is the role of the mathematical notation used on the right-hand side
of the rule. How is it that we can make use of notations like bm/nc in defining the semantics of the /
operator? Doesn’t appeal to that kind of mathematical notation beg the question? Or at least call for
its own semantics? Yes, it does, but since we have to write down the semantics of constructs somehow
or other, we use commonly accepted mathematical notation applied in the context of natural language
(in the case at hand, English). You may think that this merely postpones the problem of giving OCaml
semantics by reducing it to the problem of giving semantics for mathematical notation and English. You
would be right, and the problem is further exacerbated when the semantics makes use of mathematical
notation that is not so familiar, for instance, the substitution notation to be introduced shortly. But we
have to start somewhere.
3You may want to refer to the document “On notation” made available at the course website.
https://canvas.harvard.edu/files/3852169/download?download_frd=1
8
(3) (x * x)[x 7→ 3 + 4]
�
Let’s use this new rule to evaluate the example above:
(fun x -> x + x) (3 * 4)
−−→ 3 * 4 + 3 * 4
−−→ 12 + 3 * 4
−−→ 12 + 12
−−→ 24
Of course, there is an alternate derivation.
(fun x -> x + x) (3 * 4)
−−→ (fun x -> x + x) 12
−−→ 12 + 12
−−→ 24
In this case, it doesn’t matter which order we apply the rules, but later, it will 185
become important. We can mandate a particular order of reduction by introducing
a new concept, the value. An expression is a value if no further reduction rules ap-value
ply to it. Numerals, for instance, are values. We’ll also specify that fun expressions
are values; there aren’t any reduction rules that apply to a fun expression, and
we won’t apply any reduction rules within its body. We can restrict the function 190
application rule to apply only when its argument expression is a value, that is,
(fun x -> P) v −−→ P[x 7→ v]
(We use the schematic expression v to range only over values.) In that case, the
step
(fun x -> x + x) (3 * 4) −−→ 3 * 4 + 3 * 4
doesn’t hold because 3 * 4 is not a value. Instead, the second derivation is the
only one that applies. 195
What about OCaml’s local naming construct, the let … in … form? Once
we have function application in place, we can give a simple semantics to variable
definition by reducing it to function application as per this rewrite rule:
let x = v in P −−→ (fun x -> P) v
Exercise 4. Use the reduction rules developed so far to reduce the following expressions
to their values. 200
(1) let x = 3 * 4 in
x + x
(2) let f = fun x -> x in
f (f 5)
Kally
Highlight
Kally
Highlight
Kally
Highlight
9
�
Exercise 5. Show that the rule for the let construct could have been written instead as
let x = v in P −−→ P[x 7→ v]
From here on, we’ll use this rule instead of the previous rule for let. �
Let’s try a derivation using all these rules.
let double = fun x -> 2 * x in double (double 3)
−−→ (fun x -> 2 * x) ((fun x -> 2 * x) 3)
−−→ (fun x -> 2 * x) (2 * 3)
−−→ (fun x -> 2 * x) 6
−−→ 2 * 6
−−→ 12
Exercise 6. Carry out similar derivations for the following expressions:205
(1) let square = fun x -> x * x in
let y = 3 in
square y
(2) let id = fun x -> x in
let square = fun x -> x * x in
let y = 3 in
id square y
�
You may have noticed in Exercise 6 that some care must be taken when substi-
tuting. Consider the following case:
let x = 3 in let double = fun x -> x + x in double 4
If we’re not careful, we’ll get a derivation like this:
let x = 3 in let double = fun x -> x + x in double 4
−−→ let double = fun x -> 3 + 3 in double 4
−−→ (fun x -> 3 + 3) 4
−−→ 3 + 3
−−→ 6
or even worse210
let x = 3 in let double = fun x -> x + x in double 4
−−→ let double = fun 3 -> 3 + 3 in double 4
−−→ (fun 3 -> 3 + 3) 4
−−→ hunh?
It appears we must be very careful in how we define this substitution operation
P[x 7→ Q]. In particular, we don’t want to replace every occurrence of the token x in
Kally
Highlight
Kally
Highlight
Kally
Sticky Note
questions: is ocaml left associtive??
Kally
Highlight
10
P, only the free occurrences. A variable being introduced in a fun should definitely
not be replaced, nor should any occurrences of x within the body of a fun that also
introduces x. 215
More precisely, we can define the set of free variables in an expression P,free variables
notated FV(P) through the recursive definition in Figure 1. By way of example, the
definition says that the free variables in the expression fun y -> f (x + y) are
just f and x, as shown in the following derivation:
FV(fun y -> f (x + y)) = FV(f (x + y)) − {y}
= FV(f) ∪ FV(x + y) − {y}
= {f} ∪ FV(x) ∪ FV(y) − {y}
= {f} ∪ {x} ∪ {y} − {y}
= {f, x, y} − {y}
= {f, x}
Exercise 7. Use the definition of FV to derive the free variables in the expressions
(1) let x = 3 in let y = x in f x y
(2) let x = x in let y = x in f x y
(3) let x = y in let y = x in f x y
(4) let x = fun y -> x in x 220
�
Exercise 8. The definition of FV in Figure 1 is incomplete, in that it doesn’t specify the
free variables in a let rec expression. Add appropriate rules for this construct of the
language, being careful to note that in an expression like let rec x = fun y -> x in
x, the variable x is not free. (Compare with Exercise 7(4).) � 225
A good start to a definition of the substitution operation is given by the following
recursive definition, which replaces only free occurrences of variables:
m[x 7→ Q] = m
x[x 7→ Q] = Q
y[x 7→ Q] = y where x . y
(~- P)[x 7→ Q] = ~- P[x 7→ Q]
and similarly for other unary operators
(P + R)[x 7→ Q] = P[x 7→ Q] + R[x 7→ Q]
Kally
Highlight
Kally
Sticky Note
Kally
Highlight
Kally
Sticky Note
FV is f and x??
Kally
Highlight
Kally
Sticky Note
not sure either
Kally
Highlight
11
and similarly for other binary operators
(fun x -> P)[x 7→ Q] = fun x -> P
(fun y -> P)[x 7→ Q] = fun y -> P[x 7→ Q] where x . y
Exercise 9. Use the definition of the substitution operation above to verify your answers
to Exercise 3. �
3.1. More on capturing free variables. But there is still a problem in our definition
of substitution. Consider the following expression: let x = y in (fun y -> x).
Intuitively speaking, this expression seems ill-formed; it defines x to be an unbound230
variable y. But using the definitions that we have given so far, we would have the
following derivation:
let x = y in (fun y -> x)
−−→ (fun x -> (fun y -> x)) y
−−→ (fun y -> x)[x 7→ y]
= fun y -> (x[x 7→ y]) ⇐
= fun y -> y
The problem happens in the line marked⇐. We’re sneaking a y inside the scope
of the variable y bound by the fun. That’s not kosher. We need to change the
definition of substitution to make sure that such variable capture doesn’t occur. variable capture
The following rules work by replacing the bound variable y with a new freshly
minted variable, say z that doesn’t occur elsewhere, renaming all occurrences of y
accordingly.
(fun x -> P)[x 7→ Q] = fun x -> P
(fun y -> P)[x 7→ Q] = fun y -> P[x 7→ Q]
where x . y and y < FV(Q) (fun y -> P)[x 7→ Q] = fun z -> P[y 7→ z][x 7→ Q]
where x . y and y ∈ FV(Q) and z is a fresh variable
Exercise 10. Carry out the derivation for let x = y in (fun y -> x) as above but
with this updated definition of substitution. �
Exercise 11. What should the corresponding rule or rules defining substitution on let
…in … expressions be? That is, how should the following rule be completed? You’ll
want to think about how this construct reduces to function application in determining your
12
answer.
(let y = P in R)[x 7→ Q] = . . .
Try to work out your answer before checking it with the full definition of substitution in 235
Figure 1. �
Exercise 12. Use the definition of the substitution operation above to determine the results
of the following substitutions:
(1) (fun x -> x + x)[x 7→ 3]
(2) (fun x -> y + x)[x 7→ 3] 240
(3) (let x = y * y in x + x)[x 7→ 3]
(4) (let x = y * y in x + x)[y 7→ 3]
�
3.2. Substitution semantics of recursion. You may observe that the rule for eval-
uating let …in … expressions 245
let x = v in P −−→ P[x 7→ v]
doesn’t handle recursion properly. For instance, the Fibonacci example proceeds
as follows:
let f = fun n -> if n = 0 then 1 else n * f (n-1) in f 2
−−→ (f 2)[f 7→ (fun n -> if n = 0 then 1 else n * f (n-1))]
−−→ (fun n -> if n = 0 then 1 else n * f (n-1)) 2
−−→ if 2 = 0 then 1 else 2 * f (2-1)
which eventually leads to an attempt to apply the unbound f to its argument 1.
Occurrences of the definiendum in the body are properly replaced with the
definiens, but occurrences in the definiens itself are not. But what should those 250
recursive occurrences of f be replaced by? It doesn’t suffice simply to replace them
with the definiens, as that still has a free occurrence of the definiendum. Rather,
we’ll replace them with their own recursive let construction, thereby allowing
later occurrences to be handled as well. In particular, the rule for let rec, subtly
different from the let rule, can be as follows: 255
let rec x = v in P −−→ P[x 7→ v[x 7→ let rec x = v in x]]
For instance, in the factorial example above, we first replace occurrences of f in the
definiens with let rec f = fun n -> if n = 0 then 1 else n * f (n-1) in
f, forming
fun n -> if n = 0 then 1
else n * (let rec f = fun n -> if n = 0
then 1
else n * f (n-1) in f) (n-1)
https://en.wiktionary.org/wiki/definiendum
https://en.wiktionary.org/wiki/definiens
13
We use that as the expression to replace f with in the body (f 2), yielding
(fun n -> if n = 0 then 1
else n * (let rec f = fun n -> if n = 0
then 1
else n * f (n-1) in f) (n-1)) 2
Proceeding from there, we derive260
if 2 = 0 then 1
else 2 * (let rec f = fun n -> if n = 0
then 1
else n * f (n-1) in f) (2-1))
−−→
if false then 1
else 2 * (let rec f = fun n -> if n = 0
then 1
else n * f (n-1) in f) (2-1))
−−→
2 * (let rec f = fun n -> if n = 0
then 1
else n * f (n-1) in f) (2-1))
−−→
2 * (fun n -> if n = 0
then 1
else n * (let rec f = fun n -> if n = 0
then 1
else n * f (n-1) in f) (n-1)) (2-1))
−−→
2 * (fun n -> if n = 0
then 1
else n * (let rec f = fun n -> if n = 0
then 1
else n * f (n-1) in f) (n-1)) 1)
−−→
2 * (if 1 = 0
then 1
else 1 * (let rec f = fun n -> if n = 0
then 1
else n * f (n-1) in f) (1-1))
−−→
14
2 * (if false
then 1
else 1 * (let rec f = fun n -> if n = 0
then 1
else n * f (n-1) in f) (1-1))
Exercise 13. Thanklessly continue this derivation until it converges on the final result for
the factorial of 2, viz., 2. �
4. Implementing a substitution semantics forMiniML
You’ll start your implementation with a substitution semantics for MiniML, a
simple ML-like language. The abstract syntax of the language is given by the 265
following type definition:
type expr =
| Var of varid (* variables *)
| Num of int (* integers *)
| Bool of bool (* booleans *)
| Unop of unop * expr (* unary operators *)
| Binop of binop * expr * expr (* binary operators *)
| Conditional of expr * expr * expr (* if then else *)
| Fun of varid * expr (* function definitions *)
| Let of varid * expr * expr (* local naming *)
| Letrec of varid * expr * expr (* recursive local naming *)
| Raise (* exceptions *)
| Unassigned (* (temporarily) unassigned *)
| App of expr * expr (* function applications *)
and varid = string ;;
(The unop and binop enumerated types are as above.) These type definitions
can be found in the partially implemented Expr module in the files expr.ml and
expr.mli. You’ll notice that the module signature requires additional functionality
that hasn’t been implemented, including functions to find the free variables in an 270
expression, to generate a fresh variable name, and to substitute expressions for free
variables.
To get things started, we also provide a parser for the MiniML language, which
takes a string in a concrete syntax and returns a value of this type expr; you may
want to extend the parser in a later part of the project (Section 6.3). The compiled 275
parser and a read-eval-print loop for the language are available in the following
files:
15
evaluation.ml: The future home of anything needed to evaluate expressions
to values. Currently, provides a trivial “evaluator” that merely returns the
expression unchanged.280
miniml.ml: Runs a read-eval-print loop for MiniML, using the Evaluation
module that you will write.
miniml_lex.mll: A lexical analyzer for MiniML. (You should never need to
look at this unless you want to extend the parser.)
miniml_parse.mly: A parser for MiniML. (Ditto.)285
What’s left to implement is the Evaluationmodule in evaluation.ml.
Start by familiarizing yourself with the code. You should be able to compile
miniml.ml and get the following behavior.
# ocamlbuild miniml.byte
Finished, 13 targets (12 cached) in 00:00:00.290
# ./miniml.byte
Entering miniml.byte…
<== 3 ;;
Fatal error: exception Failure("exp_to_abstract_string not implemented")
Stage 1. Implement the function exp_to_abstract_string : expr -> string to295
convert abstract syntax trees to strings representing their structure and test it thoroughly.
If you did Exercise 2, the experience may be helpful here. �
Once you write the function exp_to_abstract_string, you should have a func-
tioning read-eval-print loop, except that the evaluation part is missing. It just prints
out the abstract syntax tree of the input concrete syntax:300
# ./miniml.byte
Entering miniml.byte…
<== 3 ;; ==> Num(3)
<== 3 4 ;;305 ==> App(Num(3), Num(4))
<== (((3) ;; xx> parse error
<== let f = fun x -> x in f f 3 ;;
==> Let(f, Fun(x, Var(x)), App(App(Var(f), Var(f)), Num(3)))310
<== let rec f = fun x -> if x = 0 then 1 else x * f (x – 1) in f 4 ;;
==> Letrec(f, Fun(x, Conditional(Binop(=, Var(x), Num(0)), Num(1),
Binop(*, Var(x), App(Var(f), Binop(-, Var(x), Num(1)))))),
App(Var(f), Num(4)))
<== Goodbye.315 16 To actually get evaluation going, you’ll need to implement a substitution se- mantics, which requires completing the functions in the Exprmodule. Stage 2. Start by writing the function free_vars in expr.ml, which takes an expression (expr) and returns a representation of the free variables in the expression, according to the definition in Figure 1. Test this function completely. � 320 Stage 3. Next, write the function subst that implements substitution as defined in Figure 1. In some cases, you’ll need the ability to define new fresh variables in the process of performing substitutions. Something like the gensym function that you wrote in lab might be useful for that. Once you’ve written subst make sure to test it completely. � You’re actually quite close to having your first working interpreter for MiniML. 325 All that is left is writing a function eval_s (the ‘s’ is for substitution semantics) that evaluates an expression using the substitution semantics rules. (Those rules were described informally in lecture 7. The lecture slides may be helpful to review.) The eval_s function walks an abstract syntax tree of type expr, evaluating subparts recursively where necessary and performing substitutions when appropriate. The 330 recursive traversal bottoms out when you get to primitive values like numbers or booleans or in applying primitive functions like the unary or binary operators to values. Stage 4. Implement the eval_s function in evaluation.ml. (You can ignore the signa- ture and implementation of the Env module for the time being. That comes into play in 335 later sections.) We recommend that you implement it in stages, from the simplest bits of the language to the most complex. You’ll want to test each stage thoroughly using unit tests as you complete it. Keep these unit tests around so that you can easily unit test the later versions of the evaluator that you’ll develop in future sections. � Using the substitution semantics, you should be able to handle evaluation of all 340 of the MiniML language. If you want to postpone handling of some parts while implementing the evaluator, you can always just raise the EvalError exception, which is intended just for this kind of thing, when a runtime error occurs. Another place EvalError will be useful is when a runtime type error occurs, for instance, for the expressions 3 + true or 3 4 or let x = true in y. 345 Now that you have implemented a function to evaluate expressions, you can make the REPL loop worthy of its name. Notice at the bottom of miniml.ml the definition of evaluate, which is the function that the REPL loop in miniml.ml calls. Replace the definition with the one calling eval_s and the REPL loop will evaluate the read expression before printing the result. It’s more pleasant to read 350 the output expression in concrete rather than abstract syntax, so you can replace 17 the exp_to_abstract_string call with a call to exp_to_string. You should end up with behavior like this: # miniml_soln.byte Entering miniml_soln.byte...355 <== 3 ;; ==> 3
<== 3 + 4 ;; ==> 7
<== 3 4 ;;360 xx> evaluation error: (3 4) bad redex
<== (((3) ;; xx> parse error
<== let f = fun x -> x in f f 3 ;;
==> 3365
<== let rec f = fun x -> if x = 0 then 1 else x * f (x – 1) in f 4 ;;
xx> evaluation error: not yet implemented: let rec
<== Goodbye. Some things to note about this example: • The parser that we provide will raise an exception Parsing.Parse_error370 if the input doesn’t parse as well-formed MiniML. The REPL handles the exception by printing an appropriate error message. • The evaluator can raise an exception Evaluation.EvalError at runtime if a (well-formed) MiniML expression runs into problems when being eval- uated.375 • You might also raise Evaluation.EvalError for parts of the evaluator that you haven’t (yet) implemented, like the tricky let rec construction in the example above. Stage 5. After you’ve changed evaluate to call eval_s, you’ll have a complete working implementation of MiniML. You should save a snapshot of this – using a git commit might380 be a good idea – so that if you have trouble down the line you can always roll back to this version to submit it. � 5. Implementing an environment semantics forMiniML The substitution semantics is sufficient for all of MiniML because it is a pure functional programming language. But binding constructs like let and let rec385 are awkward to implement, and extending the language to handle references, mutability, and imperative programming is impossible. For that, you’ll extend the language semantics to make use of an environment that stores a mapping environment Kally Highlight Kally Sticky Note how to add that? Kally Highlight 18 from variables to their values. You will want to be able to replace the values of variables dynamically – you’ll see why shortly – so that these variable values need 390 to be mutable. We’ve provided a type signature for environments. It stipulates types for environments and values, and functions to create an empty environment (which we’ve already implemented for you), to extend an environment with a new binding, that is, a mapping of a variable to its (mutable) value, and to look up thebinding value associated with a variable. 395 Stage 6. Implement the various functions involved in the Env module and test them thoroughly. � How will this be used? For atomic literals like numerals and truth values, they evaluate to themselves as usual, independently of the environment. But to evaluate a variable in an environment, we look up the value that the environment assigns 400 to it and return that value. A slightly more complex case involves function application, as in this example: (fun x -> x + x) 5
The abstract syntax for this expression is an application of one expression to an-
other.
To evaluate an application P Q in an environment ρ, 405
(1) Evaluate P in ρ to a value vP, which should be a function fun x -> B. If
vP is not a function, raise an evaluation error.
(2) Evaluate Q in the environment ρ to a value vQ.
(3) Evaluate B in the environment ρ extended with a binding of x to vQ.
In the example: (1) fun x -> x + x is already a function, so evaluates to itself. 410
(2) The argument 5 also evaluates to itself. (3) The body x + x is evaluated in an
environment that maps x to 5.
For let expressions, a similar evaluation process is used. Consider
let x = 3 * 4 in x + 1 ;;
The abstract syntax for this let expression has a variable name, a definition ex-
pression, and a body. To evaluate this expression in, say, the empty environment, 415
we first evaluate (recursively) the definition part in the same empty environment,
presumably getting the value 12 back. We then extend the environment to asso-
ciate that value with the variable x to form a new environment, and then evaluate
the body x + 1 in the new environment. In turn, evaluating x + 1 involves recur-
sively evaluating x and 1 in the new environment. The latter is straightforward. 420
The former involves just looking up the variable in the environment, retrieving the
previously stored value 12. The sum can then be computed and returned as the
value of the entire let expression.
19
For recursion, consider this expression, which makes use of an (uninteresting)
recursive function:425
let rec f = fun x -> if x = 0 then x else f (x – 1) in f 2 ;;
Again, the let rec expression has three parts: a variable name, a definition ex-
pression, and a body. To evaluate it, we ought to first evaluate the definition part,
but using what environment? If we use the incoming (empty) environment, then
what will we use for a value of f when we reach it? We should use the value
of the definition, but we don’t have it yet. In the interim, we’ll store a special430
value, Unassigned, which you’ll have noticed in the expr type but which is never
generated by the parser. We evaluate the definition in this extended environment,
hopefully generating a value. (The definition part better not ever evaluate the
variable name though, as it is unassigned; doing so should raise an EvalError. An
example of this problem might be let rec x = x in x.) The value returned for435
the definition can then replace the value for the variable name (thus the need for a
mutable environment) and that environment passed on to the body for evaluation.
In the example above, we augment the empty environment with a binding for f
to Unassigned and evaluate fun x -> if x = 0 then x else f (x – 1) in that
environment. Since this is a function, it is already a value, and the environment440
can be updated to have f have this function as a value. Finally, the body f 2 is
evaluated in this environment. The body, an application, evaluates f by looking
it up in this environment yielding fun x -> if x = 0 then x else f (x – 1)
and evaluates 2 to itself, then evaluates the body