Functional Evaluation/Substitution Model
After having reviewed the basics of writing functions and expressions in OCaml, you'll notice that if you try hard enough with even just the basics, you can produce some complicated, difficult to decipher expressions. Consider the following:
let ocaml = 15 in
let var1 = 15 in
let combination = ocaml + var1 in
let ocaml = var1 + combination in
let var1 = ocaml + ocaml in
let combination = ocaml + var1 in
combination + 1
;;
While this code would never be seen in the wild (and you could just have your compiler evaluate it), it is important for us as programmers to be able to evaluate expressions like these by ourselves (it evaluates to 136). This is for two reasons:
1.) Being able to reason about code in a consistent, logical manner makes us better programmers
2.) If we can determine the meaning of the source code, we can verify the correctness of the native code and program execution. This can help find errors in the compilation and execution process (gcc does have bugs^^).
So in order for us to understand the semantics of a program, we should develop some kind of conceptual framework or model for how OCaml should work.
1.) Being able to reason about code in a consistent, logical manner makes us better programmers
2.) If we can determine the meaning of the source code, we can verify the correctness of the native code and program execution. This can help find errors in the compilation and execution process (gcc does have bugs^^).
So in order for us to understand the semantics of a program, we should develop some kind of conceptual framework or model for how OCaml should work.
Our model will only briefly cover the core part of how OCaml works-the substitution process. There are alot of things we can do, but in order to be brief, we only cover them in broad strokes. I've linked to more resources from a variety of places that can cover these (and related) concepts in more depth.
Substitution
The first thing we cover is substituting values in for variables. In OCaml we can bind values (and expressions) to variables. For instance:
let var1 = 12;;
This let-expression binds the value 12 to our variable, var1. What happens when we use our now bound variable later on, for instance, in this new expression?
let var1 = 12 in
var1 + var1
;;
We can use the concept of substitution to substitute the value of the variable in the new expression and then perform the operation. Thus, our expression above can be evaluated as follows:
12 + 12;;
- : int = 24
And we can do this with multiple variables in our expression. For instance:
let var1 = 12 in
let var2 = 13 in
var1 + var2
;;
Substituting 12 in for var1 gives us
let var2 = 13 in
12 + var2
;;
Substituting 13 in for var2 gives us
12 + 13;;
- : int = 25
So as we can see, we replace the variables in our expressions with their values until we just have an expression consisting of values and expressions that we can evaluate. We can state this a bit more abstractly:
To evaluate a let-expression:
“let x = e1 in e2”
First, evaluate e1 to a value v.
Then substitute v for x in e2.
Evaluate the resulting expression.
Functions
In order to evaluate function calls such as "example_function input1;;", we evaluate the function until we get a function value (fun x -> e) input1, then substitute the input for x in the expression e. Let's see an example to make this more clear.
let double = fun x -> x * 2 in
double 12
;;
We substitute the definition of double in "double 12". This gives us
(fun x -> x * 2) 12;;
We then substitute 12 in for x. This gives us
12 * 2;;
- : int = 24
Great, let's see some more examples.
let add x y = x+y in
let inc = add 1 in
let dec = add -1 in
dec (inc 42)
;;
In order to make this more clear, recall from the unit on currying that add x y is a simplification of the following
let add = fun x -> (fun y -> x + y) in
let inc = add 1 in
let dec = add -1 in
dec (inc 42)
;;
Alright, now we can substitute in the value of add in for occurrences of add later on in the expression.
let inc = (fun x -> (fun y -> x + y)) 1 in
let dec = (fun x -> (fun y -> x + y)) -1 in
dec (inc 42)
;;
Now we can evaluate inc and dec as much as we can.
let inc = fun y -> 1 + y in
let dec = fun y -> -1 + y in
dec (inc 42)
;;
Now we can substitute in inc
let dec = fun y -> -1 + y in
dec ((fun y -> 1 + y) 42)
;;
And evaluate it as much as we can
let dec = fun y -> -1 + y in
dec (1 + 42)
;;
let dec = fun y -> -1 + y in
dec 43
;;
And substituting in dec
(fun y -> -1 + y) 43;;
-1 + 43;;
- : int = 24
Great. We've covered substitution, the important part of the substitution model. We've also seen how to deal with functions of 1 variable and multiple variables. Next we will examine some rules on when to substitute correctly.
Scope
Variable Names
When we write expressions, most of the time what we name our variables is of no consequence because eventually we will substitute in values for the variables and so the names are trivial aspects of the expression. For instance, the following two programs should evaluate to the same value
When we write expressions, most of the time what we name our variables is of no consequence because eventually we will substitute in values for the variables and so the names are trivial aspects of the expression. For instance, the following two programs should evaluate to the same value
let x = 1 in |
let val1 = 1 in |
When we go through the entire evaluation model, these two expressions should produce the same value. This concept, that this simple change in variable names should not change the behavior of the program or output of the expression reminds us of the fact that variables are abstract. However, we should be careful of a different form of variable renaming, having variable names overlap. Consider this variation of the previous expression:
let x = 1 in
let x = 2 in
x * x
;;
Certainly now that we have overlapping variable assignments, our program changes in behavior and our substitution model should account for this. If 2 is bound to x, this expression evaluates to 4. However, if 1 is bound to x, this expression evaluates to 1. How should our model of OCaml work under these circumstances?
Scope. This question of how to deal with overlapping variable assignments leads into our concept of scope. Statically scoped (lexically scoped) languages like OCaml have the simple rule that the "nearest" enclosing let definition of the variable defines the variable. So let's look at our confusing doubly defined x from above.
let x = 1 in
let x = 2 in
x * x
;;
In the second line, we do not need to substitute the x in "x = 2" because x is being defined. (Had we substituted the previous definition we would end up with "1 = 2" which makes no sense.) Additionally, because the second line redefines x, we can simply ignore the change in the first line. This gives us:
let x = 2 in
x * x
;;
This, based on the substitution rules from before, evaluates to 4.
Binding and Free Variables
We've worked with these concepts in the previous example, but let's be a little bit more formal about when we should or shouldn't substitute in previous variables. We should not substitute in variables when they are binding variables, but we should substitute in variables when they are free variables. Binding variables are ones that appear on the left side of a definition. Free variables are those that do not. As stated before, we substitute the "nearest" definition of a free variable. Let's take a look at this in action. I highlight the binding variables in red and the free variables in green
We've worked with these concepts in the previous example, but let's be a little bit more formal about when we should or shouldn't substitute in previous variables. We should not substitute in variables when they are binding variables, but we should substitute in variables when they are free variables. Binding variables are ones that appear on the left side of a definition. Free variables are those that do not. As stated before, we substitute the "nearest" definition of a free variable. Let's take a look at this in action. I highlight the binding variables in red and the free variables in green
let x = 4 in
let x = x + x in
let x = x + 1 in
let y = x in
y + x
;;
In order to evaluate this using our model, we need to replace all of the free variables with the nearest definition. As long as we do the correct series of bindings and substitutions, we will get the correct answer.
let x = 4 in
let x = x + x in
let x = x + 1 in
x + x
;;
let x = 4 in
let x = x + x in
x + 1 + x + 1
;;
let x = 4 in
x + x + 1 + x + x + 1
;;
4 + 4 + 1 + 4 + 4 + 1;;
- : int = 18
It is possible to use syntax trees to get a more visual picture of the substitution model as it has been described here. It is also possible to formalize this process in OCaml (which creates an interesting situation of formalizing a model in the language that we are trying to formally model, but whatever). We won't be covering that here, but I've included some links to resources that cover this and provide different perspectives on the substitution model and help add rules or give more details.
This simple substitution model that we've covered is important as a foundation for us to reason about simple and more complicated OCaml expressions. This sort of theory is important in designing programming languages of your own or ensuring the correctness of the native code after compilation. The theory of programming languages is a incredibly interesting subject with many, many branches and lots of promise.
This simple substitution model that we've covered is important as a foundation for us to reason about simple and more complicated OCaml expressions. This sort of theory is important in designing programming languages of your own or ensuring the correctness of the native code after compilation. The theory of programming languages is a incredibly interesting subject with many, many branches and lots of promise.
Previous:
|
Next:
|
Related:
http://www.cs.cornell.edu/courses/cs312/2008sp/lectures/lec05.html
http://www.cs.princeton.edu/~dpw/courses/cos326-12/lec/06-evaluation-model.pdf
http://www.cs.uml.edu/~dimock/courses/opl/Handouts/TheSubstitutionModel.pdf
http://www.cs.cornell.edu/courses/cs312/2008sp/lectures/lec05.html
http://www.cs.princeton.edu/~dpw/courses/cos326-12/lec/06-evaluation-model.pdf
http://www.cs.uml.edu/~dimock/courses/opl/Handouts/TheSubstitutionModel.pdf