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,

will stand for expressions, *e*

for values, *v*

for patterns, and *p*

for variables.
*x,y,z*

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 thenTo 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 ife_{1}elsee_{2}→e_{1}if false thene_{1}elsee_{2}→e_{2}

*e*

→ *v*

, then:
ifethene_{1}elsee_{2}→ ifvthene_{1}elsee_{2}

The rule for the `let`

expression is:

letx=vine→_{1}e_{1}{v/x}

Similar to the `if`

expression, given a `let`

expression `let x = e in e`

, the evaluator first tries to reduce the expression _{1}`e`

to a value that will be bound to `x`

, so that if

→ *e*

, then:
*v*

letx=eine→ let_{1}x=vine_{1}

and now the `let`

rule can be applied.

The notation

means, "replace all free occurrences of *e{v/x}*`x`

in `e`

by `v`

." More precisely, this notation can be defined inductively by:

x {e/y} = x x {e/x} = e (fun y -> eTo evaluate a function application_{1}) {e/x} = fun y -> (e_{1}{e/x}) (fun x -> e_{1}) {e/x} = fun x -> e_{1}(let y = e_{2}in e_{1}) {e/x} = let y = e_{2}{e/x} in e_{1}{e/x} (let x = e_{2}in e_{1}) {e/x} = let x = e_{2}{e/x} in e_{1}(let rec y = e_{2}in e_{1}) {e/x} = let rec y = e_{2}{e/x} in e_{1}{e/x} (let rec x = e_{2}in e_{1}) {e/x} = let rec x = e_{2}in e_{1}(e_{1}e_{2}) {e_{3}/x} = (e_{1}{e_{3}/x}) (e_{2}{e_{3}/x})

`(e`_{1} e_{2})

, we first evaluate the left-hand expression `e`_{1}

, which should yield a function `fun x -> ...`

, then evaluate the argument `e`_{2}

, 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
(funAnd the other rule describes the actual substitution:x->e)_{1}e→ (funx->e)_{1}v

(funx->e)_{1}v→e_{1}{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)

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 → 2011Now, 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 1In 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)