Picking up from where we left off in lecture, we defined the rules of the
substitution model and looked at some simple examples. Now lets look at a
slightly more realistic example:
let
val x = 5
in
let
val y = x + 3
in
(fn u => x + y * u) 7
end
end
To save space, we write the entire expression onto one line:
eval(let val x = 5 in let val y = x+3 in (fn u => x + y * u) 7 end end) | | E8.0. eval_decl(val x = 5) | | | | D1.0. eval(5) | | | | | | E1. eval(5) = 5 | | | | | |eval(5) = 5 | | | | D1.1. S = [(x, 5)] | | | | eval_decl(val x = 5) = [(x, 5)] | | E8.1. substitute([(x, 5)], let val y = x + 3 in (fn u => x + y * u) 7 end) | = let val y = 5 + 3 in (fn u => 5 + y * u) 7 end | | E8.2. eval(let val y = 5 + 3 in (fn u => 5 + y * u) 7 end) | | | | E8.0. eval_decl(val y = 5 + 3) = ... = [(y, 8)] | | | | E8.1. substitute([(y, 8)], (fn u => 5 + y * u) 7) | | = (fn u => 5 + 8 * u) 7 | | | | E8.2. eval((fn u => 5 + 8 * u) 7) | | | | | | E3.0. eval(fn u => 5 + 8 * u) | | | | | | | | E2. eval(fn u => 5 + 8 * u) = (fn u => 5 + 8 * u) | | | | | | | |eval(fn u => 5 + 8 * u) = (fn u => 5 + 8 * u) | | | | | | E3.1 eval(7) | | | | | | | | E1. eval(7) = 7 | | | | | | | |eval(7) = 7 | | | | | | E3.2. substitute([(u, 7)], 5 + 8 * u)) | | | = 5 + 8 * 7 | | | | | | E3.3. eval(5 + 8 * 7) = ... = 61 | | | | | |eval((fn u => 5 + 8 * u) 7) = 61 | | | |eval(let val y = 5 + 3 in (fn u => 5 + y * u) 7 end) = 61 | |eval(let val x = 5 in let val y = x + 3 in (fn u => x + y * u) 7 end end) = 61
As you will note, we have skipped some steps. It is clear that fully worked out applications of the substitution model are tedious to write and time-consuming. In our applications of the substitution model we will focus on the important steps only to keep the size of the resulting writeup somewhat manageable.
The derivation above emphasizes the recursive structure of the rules, and it provides the rule number and step number wherever applicable.
We have not yet considered the evaluation rules for recursive functions, which as we noted in lecture are different from the rules for anonymous functions, because the expression body of a recursive function must be able to reference itself.
Rule #D2[fun declarations]: to evaluate a function declaration fun f(x:t):t' =e, return the substitution that maps f to the function expression fun f(x:t):t'=e. (We omit the types below for simplicity, because they are simply copied along).
eval_decl(fun f(x) = e) = [(f,fun f(x)=e)]
Rule #E8 [fun expressions]: to evaluate a recursive function expression (fun f(x:t):t' = e), we "unroll" the function once. In other words, we return the anonymous function (fn (x:t) => e') where e' is the result of substituting (fun f(x:t):t' = e) for the identifier f within the body e.
eval(fun f(x) = e) = (fn (x) => e') where
substitute([f,(fun f(x) = e)],e) = e'.
Note that this substitution is necessary so that the body of the function can
refer to f itself. This allows for recursive functions, in contrast with
anonymous functions which cannot be recursive (and do not have an analogous
substitution).eval(let fun fact(z:int):int = if (z = 1) then z else z * fact (z – 1) in fact(3) end)
By E7 ̃
eval((fun fact(z:int):int = if (z = 1) then z else z * fact (z – 1)) (3))
By E8 ̃
eval((fn (z:int):int =>
if (z = 1) then z else z * (fun fact(z:int):int =
if (z = 1) then z else z * fact (z – 1)) (z – 1)) (3))
By E3 ̃
eval(if (3 = 1) then 3 else 3 * (fun fact(z:int):int =
if (z = 1) then z else z * fact (z – 1)) (3 - 1)))
By E6 ̃
eval(3*(fun fact(z:int):int = if (z = 1) then z else z * fact (z – 1)) (2))
As we can see, the evaluation model is not as trivial as we thought it was. Note
that there end up being deferred evaluations here; we can’t multiply 3 * fact(2)
until we know what fact(2) is.
Now, try to use this new evaluation rule with other recursive funtions, like repeated.
fun repeated(f:func,n:int):func = if (n=0) then(fn(x:base) => x) else compose (f, repeated(f,n-1))
This set of rules gives us a precise model for understanding the functional subset of SML that we have been using so far this semester. We will use these rules, although the are sometime tedious, to work through some relatively simple examples by hand to improve our understanding. A bit later in the semester, once we have built some degree of comfort with the substitution model, we will then see how to use these rules as part of inductive proofs of the correctness of recursive functional programs, that is proving that a program computes a particular value.