## 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 | n | b | e1 + e2 | (e1,e2) | fst e1 | snd e2 | Left e | Right e | match e with Left x -> e1 | Right y -> e2 | if e1 then e2 else e3 | let x = e1 in e2 v ::= fun x -> e | n | b | (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. Although we include just one operator, written +, that operator could in fact be any primitive binary operation, such as addition, multiplication, equality, or less than. 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. One caution in reading the BNF above: the occurrence of | in the match expression just before the Right constructor denotes syntax, not meta-syntax. 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} if e1 then e2 else e3 --> if e1' then e2 else e3 if e1 --> e1' if true then e2 else e3 --> e2 if false then e2 else e3 --> e3 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'. In lecture we've been writing e{v/x} to hint that the expression being substituted for x is in fact a value, but it turns out the notion of substitution works even when we have an e' that is not a value. 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}) n{e/x} = n b{e/x} = b (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 (if e1 then e2 else e3){e/x} = if e1{e/x} then e2{e/x} else e3{e/x} (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! ## 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.