The substitution model is a way of thinking about how OCaml programs evaluate. It uses a small-step semantics that describes how an expression is re-written or reduced into a new expression. Evaluation finishes when a value is reached. Values are a syntactic subset of expressions.
For today, let's consider this core sublanguage of OCaml:
e ::= x | e1 e2 | fun x -> e -- i.e., the lambda calculus
| n | e1 + e2 -- i.e., ints and binops on them
| (e1,e2) | fst e1 | snd e2 -- i.e., pairs and projections
| Left e | Right e -- i.e., constructors and pattern match
| match e with Left x -> e1 | Right y -> e2
| let x = e1 in e2 -- i.e., non-recursive let expressions
v ::= fun x -> e | i | (v1,v2) | Left v | Right vThis core language is untyped. We could add types at the cost of making our model more complicated, but at the benefit of ruling out non-sensical expressions, such as (1,2)+3.
We have only one primitive type in this core model, which is int.
The + operator could be any primitive binary operation of type int -> int -> int.
To keep tuples simple in this core model, we represent them with only two components (i.e., they are pairs). A longer tuple could be coded up with nested pairs. For example, (1,2,3) in OCaml could be (1,(2,3)) in this core language.
Also to keep datatypes simple in this core model, we represent them with only two constructors, which we name Left and Right. A datatype with more constructors could be coded up with nested applications of those two constructors. Since we have only two constructors, match expressions need only two branches. For more complicated datatypes and match expressions, we could instead use the syntax and semantics from Lecture 2.
We don't actually need if expressions in the core model, because they can be coded up with match expressions: imagine that Left represents true and Right represents false, and that the data they carry is ignored.
We omitted recursive functions from this core language. They can certainly be added, but we'll leave them out for simplicity.
In the substitution model semantics, an expression e steps to a simpler expression e', and we denote that as e --> e'. We write that only if e can take exactly one step---no more, no less. The reflexive, transitive closure of -->, written -->*, means 0 or more single steps.
Here's the substitution model semantics for the core sublanguage:
e1 + e2 --> e1' + e2
if e1 --> e1'
v1 + e2 --> v1 + e2'
if e2 --> e2'
n1 + n2 --> n3
where n3 is the result of applying primitive operation +
to n1 and n2
(e1, e2) --> (e1', e2)
if e1 --> e1'
(v1, e2) --> (v1, e2')
if e2 --> e2'
fst (v1,v2) --> v1
snd (v1,v2) --> v2
Left e --> Left e'
if e --> e'
Right e --> Right e'
if e --> e'
match e with Left x -> e1 | Right y -> e2
--> match e' with Left x -> e1 | Right y -> e2
if e --> e'
match Left v with Left x -> e1 | Right y -> e2
--> e1{v/x}
match Right v with Left x -> e1 | Right y -> e2
--> e2{v/y}
let x = e1 in e2 --> let x = e1' in e2
if e1 --> e1'
let x = v in e2 --> e2{v/x}
e1 e2 --> e1' e2
if e1 --> e1'
v e2 --> v e2'
if e2 --> e2'
(fun x -> e) v2 --> e{v2/x}The substitution model, as its name suggests, uses a substitution operator written e{e'/x}, which means the expression e but with all free occurrences of variable x replaced by expression e'. A variable is free if it is not bound by an expression that "creates" new variables:
fun x -> e binds x in the body e.match e with Left x -> e1 | Right y -> e2 binds x in e1 and binds y in e2.let x=e1 in e2 binds x in e2.Here's how to define substitution:
x{e/x} = e
y{e/x} = y
(e1 e2){e/x} = e1{e/x} e2{e/x}
(fun x -> e'){e/x} = (fun x -> e')
(fun y -> e'){e/x} = (fun y -> e'{e/x})
n{e/x} = n
(e1 + e2) {e/x} = e1{e/x} + e2{e/x}
(e1,e2){e/x} = (e1{e/x}, e2{e/x})
(fst e'){e/x} = fst e'{e/x}
(snd e'){e/x} = snd e'{e/x}
(Left e'){e/x} = Left e'{e/x}
(Right e'){e/x} = Right e'{e/x}
(match e' with Left y -> e1 | Right z -> e2){e/x}
= match e'{e/x} with Left y -> e1{e/x} | Right z -> e2{e/x}
(match e' with Left x -> e1 | Right z -> e2){e/x}
= match e'{e/x} with Left x -> e1 | Right z -> e2{e/x}
(match e' with Left y -> e1 | Right x -> e2){e/x}
= match e'{e/x} with Left y -> e1{e/x} | Right x -> e2
(match e' with Left x -> e1 | Right x -> e2){e/x}
= match e'{e/x} with Left x -> e1 | Right x -> e2
(let x = e1 in e2){v/x} = let x = e1{v/x} in e2
(let y = e1 in e2){v/x} = let y = e1{v/x} in e2{v/x}This kind of substitution is called capture-avoiding substitution, because it avoids "capturing" any occurrences of a variable underneath a binding expression. It took mathematicians a couple centuries to get the definition of capture-avoiding substitution right!
(3*1000) + ((1*100) + ((1*10) + 0))
--> 3000 + ((1*100) + ((1*10) + 0))
--> 3000 + (100 + ((1*10) + 0))
--> 3000 + (100 + (10 + 0))
--> 3000 + (100 + 10)
--> 3000 + 110
--> 3110Hence (3*1000) + ((1*100) + ((1*10) + 0)) -->* 3110.
Note that in OCaml, the * and + operators are left associative, and * has higher precedence than +, so 3*1000 + 1*100 + 1*10 + 0 would actually be (((3*1000) + (1*100)) + (1*10)) + 0 if fully parenthesized. As a simple exercise, try evaluating that expression with the substitution model.
Scroll up from this link in the OCaml language manual to read more about precedence and associativity.
let x=2 in x+1
--> (x+1){2/x} = x{2/x} + 1{2/x} = 2+1
--> 3and
(fun x -> x+1) 2
--> (x+1){2/x} = x{2/x} + 1{2/x} = 2+1
--> 3Note how we "pause" evaluation when we reach a substitution to complete the substitution operation.
Also note how the two expressions evaluate in exactly the same way. In fact, we do not really need let in our language: every occurrence of let x=e1 in e2 could be replaced by (fun x -> e2) e1. So let is really just syntactic sugar for function application.
let x = 0 in (let x = 1 in x)
--> (let x = 1 in x){0/x} = (let x = 1{0/x} in x) = (let x = 1 in x)
--> x{1/x} = 1Note how substitution stops when it reaches a binding of the same name: we don't continue substituting inside the body of the let.
let x = 0 in x + (let x = 1 in x)
--> (x + (let x = 1 in x)){0/x} = x{0/x} + (let x = 1 in x){0/x}
= 0 + (let x = 1{0/x} in x)
= 0 + (let x = 1 in x)
--> 0 + x{1/x} = 0 + 1
--> 1and
let x = 0 in (let x = 1 in x) + x
--> ((let x = 1 in x) + x){0/x} = (let x = 1 in x){0/x} + x{0/x}
= (let x = 1{0/x} in x) + 0
= (let x = 1 in x) + 0
--> x{1/x} + 0 = 1 + 0
--> 1Note that the inner binding of x shadows the outer binding, but only temporarily. So let is not the same as assignment from other languages.
The environment model is a different way of thinking about how OCaml programs evaluate. It uses a big-step semantics that describes how an expression evaluates all the way down to a value. None of the intermediate expressions produced by the small-step semantics (i.e., the substitution model) are represented. It also uses an environment, which is a data structure mapping variable names to values.
In the environment model semantics, an expression e reduces to a value v in an environment env, and we denote that as env :: e || v. The double bar || is meant to evoke the image of a double downward arrow (missing the arrowhead) while still being easy to type.
We want it to be a theorem that {} :: e || v iff e -->* v for our core language. That theorem does hold for the environment model we present below. So the substitution model and environment model always agree! They're just different ways of mentally imagining how OCaml evaluation works. The substitution model is a little simpler, but the environment model is much closer to the way the OCaml implementation (i.e., compiler and runtime) actually works. The theorem becomes a little more complicated for the environment model with closures (which we'll discuss next time).
Here's the environment model semantics for most of the core sublanguage:
env :: n || n
env :: e1 + e2 || n
if env :: e1 || n1 and env :: e2 || n2
and n is the result of applying primitive operation +
to n1 and n2
env :: (e1, e2) || (v1, v2)
if env :: e1 || v1 and env :: e2 || v2
env :: fst e || v1
if env :: e || (v1,v2)
env :: snd e || v2
if env :: e || (v1,v2)
env :: Left e || Left v
if env :: e || v
env :: Right e || Right v
if env :: e || v
env :: match e with Left x -> e1 | Right y -> e2 || v1
if env :: e || Left v
and env+{x=v} :: e1 || v1
env :: match e with Left x -> e1 | Right y -> e2 || v1
if env :: e || Right v
and env+{y=v} :: e2 || v2
env :: let x = e1 in e2 || v2
if env :: e1 || v1
and env+{x=v1} :: e2 || v2
env :: x || v
if env(x) = vFor now, we omit the evaluation rules for functions and function application. They require closures, which we'll discuss in the next lecture.
{} :: (3*1000) + ((1*100) + ((1*10) + 0)) || 3110In some sense, there are no intermediate steps to show, because the big-step semantics reduces the entire expression directly down to a value. But there are a lot of intermediate facts that justify that reduction: {} :: 1*10 || 10 is one of them. For brevity, let's leave out the empty environment everywhere, and just write 1*10 || 10. We could arrange those facts into a kind of outline or tree:
(3*1000) + ((1*100) + ((1*10) + 0)) || 3110
because 3*1000 || 3000
because 3 || 3
and because 1000 || 1000
and because 3*1000 = 3000
and because (1*100) + ((1*10) + 0) || 110
because 1*100 || 100
because 1 || 1
and because 100 || 100
and because 1*100 = 100
and because (1*10) + 0 || 10
because 1*10 || 10
because 1 || 1
and because 10 || 10
and because 1*10 = 10
and because 0 || 0
and because 10 + 0 = 10
and because 100 + 10 = 110
and because 3000 + 110 = 3110Note how the tree involves many applications of the evaluation rule for +. At each application, we justify it by explaining why the side conditions (the if... following the first line of the rule) of the + rule hold. The only rules we don't have to justify are the rules without side conditions, such as env :: n || n.
Again, 3*1000 + 1*100 + 1*10 + 0 would actually be (((3*1000) + (1*100)) + (1*10)) + 0 if fully parenthesized. As a simple exercise, try evaluating that expression with the environment model, showing the justification as above.
{} :: let x=2 in x+1 || 3
because {} :: 2 || 2
and because {}+{x=2} :: x+1 || 3
-- note {}+{x=2} = {x=2}
because {x=2} :: x || 2
because {x=2}(x) = 2
and because {x=2} :: 1 || 1
and because 2+1 = 3Note how evaluation does not need to "pause" for substitution. Instead, the environment records all the substitutions that need to be made, and they are lazily made as variable names are encountered.
{} :: let x = 0 in (let x = 1 in x) || 1
because {} :: 0 || 0
and because {}+{x=0} :: let x = 1 in x || 1
because {x=0} :: 1 || 1
and because {x=0}+{x=1} :: x || 1
-- note {x=0}+{x=1} = {x=1}
because {x=1}(x) = 1Note how the environment is updated: when {x=0} is updated to record that now x is bound to 1, the environment becomes {x=1}. So environment update is kind of like assignment from imperative languages you know.
{} :: let x = 0 in x + (let x = 1 in x) || 1
because {} :: 0 || 0
and because {} + {x=0} :: x + (let x = 1 in x) || 1
-- note {}+{x=0} = {x=0}
because {x=0} :: x || 0
because {x=0}(x) = 0
and because {x=0} :: let x = 1 in x || 1
because {x=0} :: 1 || 1
and because {x=0}+{x=1} :: x || 1
-- note {x=0}+{x=1} = {x=1}
because {x=1}(x) = 1
and because 0+1 = 1and
{} :: let x = 0 in (let x = 1 in x) + x || 1
because {} :: 0 || 0
and because {} + {x=0} :: (let x = 1 in x) + x || 1
-- note {} + {x=0} = {x=0}
because {x=0} :: let x = 1 in x || 1
because {x=0} :: 1 || 1
and because {x=0}+{x=1} :: x || 1
-- note {x=0}+{x=1} = {x=1}
because {x=1}(x) = 1
and because {x=0} :: x || 0
because {x=0}(x) = 0
and because 0+1 = 1Note that after we get to the second level of indentation, the justifications are the same for the two examples, just in a different order. In both cases, the innermost environment is updated to bind x to 1, while x remains bound to 0 in the outer environment. They are different environments, so updating one does not cause a change in the other. In that sense, environment update is kind of unlike assignment from imperative languages you know. The key idea is that the environment is not shared among all the applications of the evaluation rule; instead, copies of it are made then updated.