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
Well 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, Ive 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. Wed 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? Doesnt 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]
Lets 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 doesnt 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. Well also specify that fun expressions
are values; there arent any reduction rules that apply to a fun expression, and
we wont 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
doesnt hold because 3 * 4 is not a value. Instead, the second derivation is the
only one that applies. 195
What about OCamls 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, well use this rule instead of the previous rule for let.
Lets 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 were not careful, well 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 dont 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 doesnt 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. Were sneaking a y inside the scope
of the variable y bound by the fun. Thats not kosher. We need to change the
definition of substitution to make sure that such variable capture doesnt occur. variable capture
The following rules work by replacing the bound variable y with a new freshly
minted variable, say z that doesnt 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? Youll
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]
doesnt 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 doesnt suffice simply to replace them
with the definiens, as that still has a free occurrence of the definiendum. Rather,
well 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
Youll 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. Youll notice that the module signature requires additional functionality
that hasnt 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
Whats 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.31516To actually get evaluation going, youll 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 thedefinition in Figure 1. Test this function completely. 320Stage 3. Next, write the function subst that implements substitution as defined inFigure 1. In some cases, youll need the ability to define new fresh variables in the processof performing substitutions. Something like the gensym function that you wrote in labmight be useful for that. Once youve written subst make sure to test it completely. Youre actually quite close to having your first working interpreter for MiniML. 325All that is left is writing a function eval_s (the s is for substitution semantics) thatevaluates an expression using the substitution semantics rules. (Those rules weredescribed informally in lecture 7. The lecture slides may be helpful to review.) Theeval_s function walks an abstract syntax tree of type expr, evaluating subpartsrecursively where necessary and performing substitutions when appropriate. The 330recursive traversal bottoms out when you get to primitive values like numbers orbooleans or in applying primitive functions like the unary or binary operators tovalues.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 335later sections.) We recommend that you implement it in stages, from the simplest bits ofthe language to the most complex. Youll want to test each stage thoroughly using unittests as you complete it. Keep these unit tests around so that you can easily unit test thelater versions of the evaluator that youll develop in future sections. Using the substitution semantics, you should be able to handle evaluation of all 340of the MiniML language. If you want to postpone handling of some parts whileimplementing the evaluator, you can always just raise the EvalError exception,which is intended just for this kind of thing, when a runtime error occurs. Anotherplace 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. 345Now that you have implemented a function to evaluate expressions, you canmake the REPL loop worthy of its name. Notice at the bottom of miniml.ml thedefinition of evaluate, which is the function that the REPL loop in miniml.mlcalls. Replace the definition with the one calling eval_s and the REPL loop willevaluate the read expression before printing the result. Its more pleasant to read 350the output expression in concrete rather than abstract syntax, so you can replace17the exp_to_abstract_string call with a call to exp_to_string. You should endup with behavior like this:# miniml_soln.byteEntering miniml_soln.byte…355<== 3 ;;==> 3
<== 3 + 4 ;;==> 7
<== 3 4 ;;360xx> 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_error370if the input doesnt parse as well-formed MiniML. The REPL handles theexception by printing an appropriate error message. The evaluator can raise an exception Evaluation.EvalError at runtime ifa (well-formed) MiniML expression runs into problems when being eval-uated.375 You might also raise Evaluation.EvalError for parts of the evaluator thatyou havent (yet) implemented, like the tricky let rec construction in theexample above.Stage 5. After youve changed evaluate to call eval_s, youll have a complete workingimplementation of MiniML. You should save a snapshot of this using a git commit might380be a good idea so that if you have trouble down the line you can always roll back to thisversion to submit it. 5. Implementing an environment semantics forMiniMLThe substitution semantics is sufficient for all of MiniML because it is a purefunctional programming language. But binding constructs like let and let rec385are awkward to implement, and extending the language to handle references,mutability, and imperative programming is impossible. For that, youll extendthe language semantics to make use of an environment that stores a mapping environmentKallyHighlightKallySticky Notehow to add that?KallyHighlight18from variables to their values. You will want to be able to replace the values ofvariables dynamically youll see why shortly so that these variable values need 390to be mutable. Weve provided a type signature for environments. It stipulatestypes for environments and values, and functions to create an empty environment(which weve already implemented for you), to extend an environment with a newbinding, that is, a mapping of a variable to its (mutable) value, and to look up thebindingvalue associated with a variable. 395Stage 6. Implement the various functions involved in the Env module and test themthoroughly. How will this be used? For atomic literals like numerals and truth values, theyevaluate to themselves as usual, independently of the environment. But to evaluatea variable in an environment, we look up the value that the environment assigns 400to 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 dont have it yet. In the interim, well store a special430
value, Unassigned, which youll 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
Reviews
There are no reviews yet.