## 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.