# Substitution Model Today we will study the semantics given in yesterday's lecture notes on [a core sub-language of OCaml](core-ocaml.html). These rules extend the rules you've seen in lecture to support pairs, simple variants, and anonymous functions. ## Evaluation Here is an example of evaluating an expression:  7+5*2 --> (step * operation) 7+10 --> (step + operation) 17  There are two steps in that example, and we've annotated each step with a parenthetical comment to hint at which evaluation rule we've used. We stopped evaluating when we reached a value. We could write that evaluation more tersely as 7+5*2 --> 7+10 --> 17, or even more tersely as 7+5*2 -->* 17, but each of those provides progressively less detail about the evaluation. ##### Exercise: simple expressions [&#10029;] Evaluate the following expressions using the small-step substitution model. Use the "long form" of evaluation that we demonstrated above, in which you provide a hint as to which rule is applied at each step. - (3 + 5) * 2 (2 steps) - if 2 + 3 < 4 then 1 + 1 else 2 + 2 (4 steps) &square; Here is an example of evaluating a let expression:  let x = 2 in x+x --> (step let expression) (x+x){2/x} = 2+2 --> (step + operation) 4  Here we've first taken one step, which results in a substitution. We put parentheses around the x+x to be clear that the substitution operation {2/x} applies to both of the x's: if we had instead written x+x{2/x} it might be ambiguous as to whether we wanted to apply the substitution to the x on the left-hand side. We then applied the substitution. That was not a step of evaluation, because it was not a use of a --> rule. So we wrote it on the same line. Then we took a second step. ##### Exercise: substitution [&#10029;&#10029;] Evaluate these expressions, again using the "long form" we just demonstrated. Be very careful to correctly use the definition of substitution that is provided in the notes. Double check your answers against utop. - let x = 2 + 2 in x + x (3 steps) - let x = 5 in ((let x = 6 in x) + x) (3 steps) - let x = 1 in (let x = x + x in x + x) (4 steps) &square; ## Pairs In OCaml, a pair of values (v1,v2) is a value. OCaml does not specify whether pairs of expressions are evaluated from left to right or from right to left. The evaluation rules we gave in our core OCaml semantics evaluates from left to right. It turns out this is actually different from what the current implementation of OCaml does. ##### Exercise: pairs [&#10029;&#10029;] Evaluate these: - (3 + 5, 2 + 4) (2 steps) - (fst (3,4), snd (3,4)) (2 steps) - ((if fst (true, 3) then snd (1,2) else 3), (if snd (3,false) then snd (1,2) else 3)) (5 steps) &square; ## Variants A variant value is either the constructor Left or Right applied to a value. ##### Exercise: variants [&#10029;&#10029;] Evaluate these: - Left (1+2) (1 step) - match Left 42 with Left x -> x+1 | Right y -> y-1 (2 steps) - (4 steps)  match Right (Left (1+2)) with Left a -> 1+a | Right a -> match a with Left b -> 2+b | Right b -> 3+b  &square; ## Functions Function evaluation in the substitution model is very similar to the evaluation of let expressions. Recall that anonymous functions are values, and do not evaluate any further. To evaluate a function application, we first evaluate the function being applied, then we evaluate the argument, then we substitute the argument into the body of the function. Like with pairs, OCaml does not specify whether the function being applied is evaluated before or after the argument to which it is being applied. Our core semantics does specify that the function being applied is evaluated first. ##### Exercise: application [&#10029;&#10029;] Evaluate these: - (fun x -> 3 + x) 2 (2 steps) - let f = (fun x -> x + x) in (f 3) + (f 3) (6 steps) - let f = fun x -> x + x in let x = 1 in let g = fun y -> x + f y in g 3 (7 steps) - let f = (fun x -> fun y -> x + y) in let g = f 3 in (g 1) + (f 2 3) (9 steps) &square; ## Lists In lecture, we claimed that Left and Right were sufficient to code up more complicated variants. Let's give an example of that now by coding up lists. Suppose we treat list expressions like syntactic sugar in the following way: * [] is syntactic sugar for Left 0. * e1::e2 is syntactic sugar for Right (e1,e2). ##### Exercise: desugar list [&#10029;] What is the core OCaml expression to which [1;2;3] desugars? &square; ##### Exercise: list not empty [&#10029;&#10029;] Write a core OCaml function not_empty that returns 1 if a list is non-empty and 0 if the list is empty. Use the substitution model to check that your function behaves properly on these test cases: - not_empty [] - not_empty [1] &square; ## Additional exercise: pattern matching [&#10029;&#10029;&#10029;] In core OCaml, there are only two patterns: Left x and Right x, where x is a variable name. But in full OCaml, patterns are far more general. Let's see how far we can generalize patterns in core OCaml. **Step 1:** Here is a BNF grammar for patterns, and slightly revised BNF grammar for expressions:  p ::= i | (p1,p2) | Left p | Right p | x | _ e ::= ... | match e with | p1 -> e1 | p2 -> e2 | ... | pn -> en  In the revised syntax for match, only the very first | on the line, immediately before the keyword match, is meta-syntax. The remaining four | on the line are syntax. Note that we require | before the first pattern. **Step 2:** A value v matches a pattern p if by substituting any variables or wildcards in p with values, we can obtain exactly v. For example: * 2 matches x because x{2/x} is 2. * Right(0,Left 0) matches Right(x,_) because Right(x,_){0/x}{Left 0/_} is Right(0,Left 0). Let's define a new ternary judgement called matches, guided by those examples:  v =~ p // s  Pronounce this judgement as "v matches p producing substitutions s. Here, s is a sequence of substitutions, such as {0/x}{Left 3/y}{(1,2)/z}. There is just a single rule for this judgement:  v =~ p // s if v = p s  For example,  2 =~ x // {2/x} because 2 = x{2/x}  **Step 3:** To evaluate a match expression: * Evaluate the expression being matched to a value. * If that expression matches the first pattern, evaluate the expression corresponding to that pattern. * Otherwise, match against the second pattern, the third, etc. * If none of the patterns matches, evaluation is *stuck*: it cannot take any more steps. Using those insights, complete the following evaluation rules by filling in the places marked with ???:  (* This rule should implement evaluation of e. *) match e with | p1 -> e1 | p2 -> e2 | ... | pn -> en --> ??? if ??? (* This rule implements moving past p1 to the next pattern. *) match v with | p1 -> e1 | p2 -> e2 | ... | pn -> en --> match v with | p2 -> e2 | ... | pn -> en if there does not exist an s such that ??? (* This rule implements matching v with p1 then proceeding to evaluate e1. *) match v with | p1 -> e1 | p2 -> e2 | ... | pn -> en --> ??? (* something involving e1 *) if ???  Note that we don't need to write the following rule explicitly:  match v with | -/->  Evaluation will get stuck at that point because none of the three other rules above will apply. **Step 4:** Double check your rules by evaluating the following expression: - match (1 + 2, 3) with | (1,0) -> 4 | (1,x) -> x | (x,y) -> x + y ## Additional exercise: let rec [&#10029;&#10029;&#10029;] One of the evaluation rules for let is  let x=v in e --> e{v/x}  This rule doesn't work properly for let rec expressions. Explain what happens when you try to use it on the following expression:  let rec fact = fun x -> if x <= 1 then 1 else x * (fact (x - 1)) in fact 3  When evaluating let rec expressions in the substitution model, you need to perform two substitutions: when evaluating let rec f = e1 in e2, you need to first "unfold" f in the body of e1 by substituting the entire let rec expression in for f. Then you can substitute this unfolded f into e2. Formally:  let rec f = v in e --> e{(v{(let rec f = v in f) / f}) / f}  Use that rule to evaluate the following expression (16 steps, we think, though it does get pretty tedious!). You may want to simplify your life by writing "F" in place of (let rec fact = fun x -> if x <= 1 then 1 else x * (fact (x-1)) in fact)  let rec fact = fun x -> if x <= 1 then 1 else x * (fact (x - 1)) in fact 3