Recitation 6: More on the Substitution Model of Evaluation

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.

Review of the evaluation rules

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 e2e1
if false then e1 else e2e2
To 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 ev, then:
if e then e1 else e2   →  if v then e1 else e2

The rule for the let expression is:

let x = v in e1e1{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 ev, 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 ev, then
(fun x -> e1) e   →  (fun x -> e1) v
And the other rule describes the actual substitution:
(fun x -> e1) ve1{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.

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)

First example

Let us consider this difficult-to-understand code:
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:

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

The evil example

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
→  1023
Finally, 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
→  36
What about evil (dummy, dummy, 4)? evil (dummy, dummy, 5)? Can you guess? (Answer: 36 for any n > 2.)

Lexical vs. dynamic scoping

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)