In this recitation we will review the substitution model we have seen in last lecture, and we will give a few more examples. At the end on the lecture, 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.
Last time we have seen a few rules for evaluating. 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 first thing the evaluator does is try 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 statement is:
let x=v in e1 → e1{v/x}
And similarly to what happens for if statements, the first thing the evaluator does is try to reduce the value that will be assigned to x, so that if e → v, then:
let x=e in e1 → let x=v in e1
Here, we used the notation e1{v/x} whose idea is "replace all free occurrences of x in e1 by v. More precisely, this notation can be defined recursively by:
x{e/x} = e
x{e/y} = x
(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)
f(x) { fun y->e1 / f } = (fun y->e1)(x)
Finally, we want to be able to evaluate function applications. To do that, we first want to evaluate the argument, then replace the name of the argument by the value of that argument in the body of the function. The first rule involved here is the fact that if e → v, then:
(fun x -> e1) e → (fun x -> e1) vAnd the other rule describes the actual replacement:
(fun x -> e1) e → e1{v/x}
At that point, the only prob lem remaining was that we are not able to evaluate recursive functions. A way to understand this is that a recursive function is an infinite unfolding of the original definition. More precisely:
let rec f = fun x -> e in e' → e'{f'/f}
(with global binding f' = fun x -> e{f'/f}, f' fresh)
[Note to instructor:] Leave all these rules on the side of the board so that students can refer to them at all times when running through the examples.
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), 3)Here is the complete evaluation of that code:
f'((fun x->10), 3) (with f' = fun (g,n) ->
if n=1 then g(0)
else g(0) + f'((fun x->n), n-1))
→
(fun (g,n) ->
if n=1 then g(0)
else g(0) + f'((fun x->n), n-1)) ((fun x->10), 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,n) -> ...) ((fun x->3), 3-1)
→ 10 + (fun (g,n) -> ...) ((fun x->3), 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,n) -> ...)(fun x->2, 2-1)
→ 10 + 3 + (fun (g,n) -> ...)(fun x->2, 1)
→ 10 + 3 + if 1=1 then (fun x->2)(0) else ...
→ 10 + 3 + (fun x->2)(0)
→ 10 + 3 + 2
→ 10 + 5
→ 15
Last time we did not have time to completely and carefully go through the tricky example we had [Note to instructor: really go through this example, it is probably going to take 15 min or so but it is worth it]:
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:
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) → 2011Now, let us try by changing the last line to
evil(dummy, dummy, 2). Here is the evaluation:
evil(fun(x)->1000, fun(x)->1000, 2) → let f(x) = 10 + 2 in if 2 = 1 then f(0) + (fun(x)->1000)(0) + (fun(x)->1000)(0) else evil(f, (fun(x)->1000), 2-1) → evil(fun(x)->10+2, fun(x)->1000, 1) → let f(x) = 10 + 1 in if 1 = 1 then f(0) + (fun(x)->10+2)(0) + (fun(x)->1000)(0) else evil(f, (fun(x)->10+2), 1-1) → (fun(x)->10+1)(0) + (fun(x)->10+2)(0) + (fun(x)->1000)(0) → 1023Finally, the real case with
evil(dummy, dummy, 3)
evil(fun(x)->1000, fun(x)->1000, 3) → let f(x) = 10 + 3 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+3, fun(x)->1000, 2) → let f(x) = 10 + 2 in if 2 = 1 then f(0) + (fun(x)->10+3)(0) + (fun(x)->1000)(0) else evil(f, (fun(x)->10+3), 2-1) → evil(fun(x)->10+2, fun(x)->10+3, 1) → let f(x) = 10 + 1 in if 1 = 1 then f(0) + (fun(x)->10+2)(0) + (fun(x)->10+3)(0) else evil(f, (fun(x)->10+2), 1-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 thus far, variable names are
subsituted immediately throughout their scope
when a function is applied or a let is evaluated. This means that
whenever we see a variable, how that variable is bound is immediately clear:
the variable is bound at the closest enclosing binding occurrence that can be
seen in the program text. This rule is called lexical scoping.
To fully understand this, let us have a simple exemple:
let x=1 in let f(y)=y+x in let x=3 in f(1)In lexical scoping, the first declaration of
x (x=1) is used when evaluating f(1), because this is the one which was in scope when f was declared; thus the result is 2.
The most common alternative to lexical scoping is called dynamic scoping.
In dynamic scoping, a variable is bound to the most recently bound version of
the variable, and function values do not record how their variables such as
x are bound. In the language Perl, the equivalent
of the example code results in 4 because the second declaration of x (x=3)
is used when evaluating f(1). Dynamic scoping can be confusing
because the meaning of a function depends on the context where 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)