In this recitation we will review the substitution model introduced in lecture and give a few more examples. We will also spend some time on lexical and dynamic scoping. In the following, e will stand for expressions, v for values, p for patterns, and x,y,z for variables.
One important fact about the substitution model that may not have been clear from the previous lecture is that each substitution rule takes in an expression and outputs a simplified expression. This means that the expression listed at each step must be valid, and must evaluate to the same value as any other expression throughout the substitution. In other words, you should be able to plug in each line of an evaluation by substitution into the OCaml toplevel, and each line should evaluate to the same answer. Thus, be sure that each line is a well-formed OCaml expression, which will be the case if you follow the below rules precisely.
Last time we saw a few rules for evaluating expressions. In these rules, the arrow → just means "reduces to" and is completely different from the arrows in the function types.
The two main rules for the if statements:
if true then e1 else e2 → e1 if false then e1 else e2 → e2To get an expression of the above form, the evaluator first tries to reduce the conditional expression to a boolean value, either true or false; so if
e → v, then:
if e then e1 else e2 → if v then e1 else e2
The rule for the let expression is:
let x = v in e1 → e1{v/x}
Similar to the if expression, given a let expression let x = e in e1, the evaluator first tries to reduce the expression e to a value that will be bound to x, so that if e → v, then:
let x = e in e1 → let x = v in e1
and now the let rule can be applied.
The notation e{v/x} means, "replace all free occurrences of x in e by v." More precisely, this notation can be defined inductively by:
x {e/y} = x
x {e/x} = e
(fun y -> e1) {e/x} = fun y -> (e1{e/x})
(fun x -> e1) {e/x} = fun x -> e1
(let y = e2 in e1) {e/x} = let y = e2{e/x} in e1{e/x}
(let x = e2 in e1) {e/x} = let x = e2{e/x} in e1
(let rec y = e2 in e1) {e/x} = let rec y = e2{e/x} in e1{e/x}
(let rec x = e2 in e1) {e/x} = let rec x = e2 in e1
(e1 e2) {e3/x} = (e1{e3/x}) (e2{e3/x})
To evaluate a function application (e1 e2), we first evaluate the left-hand expression e1, which should yield a function fun x -> ..., then evaluate the argument e2, then substitute the resulting value for the function parameter x in the body of the function, then evaluate the body. The first rule involved here is that if e → v, then
(fun x -> e1) e → (fun x -> e1) vAnd the other rule describes the actual substitution:
(fun x -> e1) v → e1{v/x}
Note that the latter rule may only be applied if the right-hand expression is a value, i.e. has already been evaluated.
Match statements are evaluated by first reducing the expression being matched to a value, much like the
condition of an if statement. Thus, if e → v, then:
match e with p1 -> ... | p2 -> ... → match v with p1 -> ... | p2 -> ...At this point, we can apply the
match rule. To do this, we determine which pi matches v, insert
let statements to make the bindings created in the pattern, and finish with the result of that pattern match. This is
perhaps best illustrated with an example:
match [1; 2; 3] with [] -> 0 hd::tl -> hd + (addList tl) → let hd = 1 and tl = [2; 3] in hd + (addList tl)
The only issue remaining is how to evaluate recursive functions. One way to understand this is that a recursive function is like an infinite unfolding of the original definition. More precisely:
let rec f = fun x -> e in e'
→
e'{f'/f} (with f' = fun x -> e{f'/f}, f' fresh)
let rec f g n = if n = 1 then g 0 else g 0 + f (fun x -> n) (n - 1) in f (fun x -> 10) 3Here is the complete evaluation of that code:
We introduce a fresh symbol f' for the recursive function bound in the let rec expression, along with the reduction rule
f' → fun g -> fun n ->
if n = 1 then g 0
else g 0 + f' (fun x -> n) (n - 1)
then evaluate
let f = f' in f (fun x -> 10) 3
The evaluation then proceeds as follows.
let f = f' in f (fun x -> 10) 3
→ f' (fun x -> 10) 3
→ (fun g -> fun n ->
if n = 1 then g 0
else g 0 + f' (fun x -> n) (n - 1)) (fun x -> 10) 3
→ (fun n ->
if n = 1 then (fun x -> 10) 0
else (fun x -> 10) 0 + f' (fun x -> n) (n - 1)) 3
→ if 3 = 1 then (fun x -> 10) 0
else (fun x -> 10) 0 + f' (fun x -> 3) (3 - 1)
→ if false then (fun x -> 10) 0
else (fun x -> 10) 0 + f' (fun x -> 3) (3 - 1)
→ (fun x -> 10) 0 + f' (fun x -> 3) (3 - 1)
→ 10 + f' (fun x -> 3) (3 - 1)
→ 10 + (fun g -> fun n -> ...) (fun x -> 3) (3 - 1)
→ 10 + (fun n -> ...) 2
→ 10 + if 2 = 1 then (fun x -> 3) 0
else (fun x -> 3) 0 + f' (fun x -> 2) (2 - 1)
→ 10 + if false then (fun x -> 3) 0
else (fun x -> 3) 0 + f' (fun x -> 2) (2 - 1)
→ 10 + (fun x -> 3) 0 + f' (fun x -> 2) (2 - 1)
→ 10 + 3 + f' (fun x -> 2) (2 - 1)
→ 10 + 3 + (fun g -> fun n -> ...) (fun x -> 2) (2 - 1)
→ 10 + 3 + (fun n -> ...) 1
→ 10 + 3 + if 1 = 1 then (fun x -> 2) 0 else ...
→ 10 + 3 + if true then (fun x -> 2) 0 else ...
→ 10 + 3 + (fun x -> 2) 0
→ 10 + 3 + 2
→ 15
Last time we did not have time to completely and carefully go through the tricky example we had.
let rec evil (f1, f2, n) =
let f x = 10 + n in
if n = 1 then f 0 + f1 0 + f2 0
else evil (f, f1, n-1)
and dummy x = 1000
in evil (dummy, dummy, 3)
Let us first try by changing the last line to evil (dummy, dummy, 1). The evaluation goes as follows. We introduce a fresh variable evil' denoting the recursive function bound to evil along with the reduction rule
evil' → fun (f1, f2, n) ->
let f x = 10 + n in
if n = 1 then f 0 + f1 0 + f2 0
else evil' (f, f1, n-1)
and the tricky example can be rewritten
let evil = evil' and dummy = fun x -> 1000 in evil (dummy, dummy, 1)
Now evaluating this expression by substitution,
let evil = evil'
and dummy = fun x -> 1000
in evil (dummy, dummy, 1)
→ evil' ((fun x -> 1000), (fun x -> 1000), 1)
→ let f x = 10 + 1 in
if 1 = 1 then f 0 + (fun x -> 1000) 0 + (fun x -> 1000) 0
else evil' (f, (fun x -> 1000), 1 - 1)
→ (fun x -> 10 + 1) 0 + (fun x -> 1000) 0 + (fun x -> 1000) 0
→ 2011
Now, let us try by changing the last line to evil (dummy, dummy, 2). Here is the evaluation:
let evil = evil' and dummy = fun x -> 1000 in evil (dummy, dummy, 2) → evil' ((fun x -> 1000), (fun x -> 1000), 2) → evil' ((fun x -> 10 + 2), (fun x -> 1000), 1) → (fun x -> 10 + 1) 0 + (fun x -> 10 + 2) 0 + (fun x -> 1000) 0 → 1023Finally, the real case with
evil (dummy, dummy, 3):
let evil = evil' and dummy = fun x -> 1000 in evil (dummy, dummy, 3) → evil' ((fun x -> 1000), (fun x -> 1000), 3) → evil' ((fun x -> 10 + 3), (fun x -> 1000), 2) → evil' ((fun x -> 10 + 2), (fun x -> 10 + 3), 1) → (fun x -> 10 + 1) 0 + (fun x -> 10 + 2) 0 + (fun x -> 10 + 3) 0 → 36What about
evil (dummy, dummy, 4)? evil (dummy, dummy, 5)? Can you guess? (Answer: 36 for any n > 2.)
In the substitution model we have seen so far, variable names are substituted immediately throughout their scope
when a function is applied or a let is evaluated. This means that
whenever we see an occurrence of a variable, how that variable is bound is immediately clear from the program text: the variable is bound to the innermost binding occurrence in whose scope it occurs. This rule is called lexical scoping.
To fully understand this, let us look at a simple example:
let x = 1 in
let f y = y + x in
let x = 3 in
f 1
In lexical scoping, the first declaration of x, namely x = 1, is used for the value of x in the body of f when evaluating f 1, because this is the one that was in scope when f was declared; thus the result is 2.
The most common alternative to lexical scoping is dynamic scoping.
In dynamic scoping, a variable's value is determined by its most recent binding. In the languages Perl and Lisp, which are dynamically scoped, the equivalent
of the example above results in 4 because the second declaration of x, namely x = 3, is used for the value of x in the body of f when evaluating f 1. Dynamic scoping can be confusing because the meaning of a function depends on the context in which it is used. Most modern languages use lexical scoping.
Let us apply this to the tricky example from earlier.The key question
is what the variable n means within the
functions f, f1, f2. In lexical scoping, even though these
variables are all bound to the function f, they are bound to
versions of the function f that occurred in three different
scopes, where the variable n was bound to 1, 2, and 3 respectively.
For example, on the first entry to evil, the value 3 is substituted for
the variable n within the function f (which
ultimately becomes f2 on the third application on evil).
In dynamic scoping on the other hand, it
would print 33 rather than 36, because the most recently
bound value for the variable n is 1. Here is the complete evaluation, where
we do not replace the n because of the dynamic scoping nature of our evaluation:
evil ((fun x -> 1000), (fun x -> 1000), 3) → let f x = 10 + n in if 3 = 1 then f 0 + (fun x -> 1000) 0 + (fun x -> 1000) 0 else evil (f, (fun x -> 1000), 3 - 1) → evil ((fun x -> 10 + n), (fun x -> 1000), 2) → let f x = 10 + n in if 2 = 1 then f 0 + (fun x -> 10 + n) 0 + (fun x -> 1000) 0 else evil (f, (fun x -> 10 + n), 2 - 1) → evil ((fun x -> 10 + n), (fun x -> 10 + n), 1) → let f x = 10 + n in if 1 = 1 then f 0 + (fun x -> 10 + n) 0 + (fun x -> 10 + n) 0 else evil (f, (fun x -> 10 + 2), 1 - 1) → (fun x -> 10 + n) 0 + (fun x -> 10 + n) 0 + (fun x -> 10 + n) 0 → 33 (because n is bound to 1 at that point)