## The substitution model
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.
## Syntax
Here is a 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 v
This 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.
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.
## Dynamic semantics
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:
* A function `fun x -> e` binds `x` in the body `e`.
* A match expression `match e with Left x -> e1 | Right y -> e2` binds
`x` in `e1` and binds `y` in `e2`.
* A let expression `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})
if y is not free in e
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}
if y and z are not free in e
(match e' with Left x -> e1 | Right z -> e2){e/x}
= match e'{e/x} with Left x -> e1 | Right z -> e2{e/x}
if z is not free in e
(match e' with Left y -> e1 | Right x -> e2){e/x}
= match e'{e/x} with Left y -> e1{e/x} | Right x -> e2
if y is not free in e
(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){e/x} = let x = e1{e/x} in e2
(let y = e1 in e2){e/x} = let y = e1{e/x} in e2{e/x}
if y is not free in e
This kind of substitution is called *capture-avoiding substitution*, because
it avoids "capturing" any occurrences of a variable underneath a binding expression.
## Examples in the substitution model
### Example 1:
(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
--> 3110
Hence `(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](http://caml.inria.fr/pub/docs/manual-ocaml-4.02/expr.html#sec116)
to read more about precedence and associativity.
### Example 2:
let x=2 in x+1
--> (x+1){2/x} = x{2/x} + 1{2/x} = 2+1
--> 3
and
(fun x -> x+1) 2
--> (x+1){2/x} = x{2/x} + 1{2/x} = 2+1
--> 3
Note 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.
### Example 3:
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} = 1
Note how substitution stops when it reaches a binding of the same
name: we don't continue substituting inside the body of the `let`.
### Example 4:
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
--> 1
and
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
--> 1
Note that the inner binding of `x` *shadows* the outer binding, but only
temporarily. So `let` is **not** the same as assignment from other languages.