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 e2   →  e1
if false then e1 else e2  →  e2
```
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 `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) v`
And 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.

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)
```