It's possible to enhance the lambda calculus so that functions do get identified when they map all the same inputs to the same outputs. This is called making the calculus **extensional**. Church called languages which didn't do this **intensional**. If you try to understand that kind of "intensionality" in terms of functions from worlds to extensions (an idea also associated with Church), you may hurt yourself. So too if you try to understand it in terms of mental stereotypes, another notion sometimes designated by "intension."
It's often said that dynamic systems are distinguished because they are the ones in which **order matters**. However, there are many ways in which order can matter. If we have a trivalent boolean system, for example---easily had in a purely functional calculus---we might choose to give a truth-table like this for "and":
+
+ true and true = true
+ true and true = true
+ true and * = *
+ true and false = false
+ * and true = *
+ * and * = *
+ * and false = *
+ false and true = false
+ false and * = false
+ false and false = false
+
+And then we'd notice that `* and false` has a different intepretation than `false and *`. (The same phenomenon is already present with the material conditional in bivalent logics; but seeing that a non-symmetric semantics for `and` is available even for functional languages is instructive.)
+
+Another way in which order can matter that's present even in functional languages is that the interpretation of some complex expressions can depend on the order in which sub-expressions are evaluated. Evaluated in one order, the computations might never terminate (and so semantically we interpret them as having "the bottom value"---we'll discuss this). Evaluated in another order, they might have a perfectly mundane value. Here's an example, though we'll reserve discussion of it until later:
+
+ (\x. y) ((\x. x x) (\x. x x))
+
+Again, these facts are all part of the metatheory of purely functional languages. But *there is* a different sense of "order matters" such that it's only in imperatival languages that order so matters.
+
+ x := 2
+ x := x + 1
+ x == 3
+
+Here the comparison in the last line will evaluate to true.
+
+ x := x + 1
+ x := 2
+ x == 3
+
+Here the comparison in the last line will evaluate to false.
+
+One of our goals for this course is to get you to understand *what is* that new
+sense such that only so matters in imperatival languages.
+
+Finally, you'll see the term **dynamic** used in a variety of ways in the literature for this course:
+
+* dynamic versus static typing
+
+* dynamic versus lexical scoping
+
+* dynamic versus static control operators
+
+* finally, we're used ourselves to talking about dynamic versus static semantics
+
+For the most part, these uses are only loosely connected to each other. We'll tend to use "imperatival" to describe the kinds of semantic properties made available in dynamic semantics, languages which have robust notions of sequencing changes, and so on.
+
+Map
+===
+
+<table>
+<tr>
+<td width=30%>Scheme (functional part)</td>
+<td width=30%>OCaml (functional part)</td>
+<td width=30%>C, Java, Pasval<br>
+Scheme (imperative part)<br>
+OCaml (imperative part)</td>
+<tr>
+<td width=30%>lambda calculus<br>
+combinatorial logic</td>
+<tr>
+<td colspan=3 align=center>--------------------------------------------------- Turing complete ---------------------------------------------------</td>
+<tr>
+<td width=30%>
+<td width=30%>more advanced type systems, such as polymorphic types
+<td width=30%>
+<tr>
+<td width=30%>
+<td width=30%>simply-typed lambda calculus (what linguists mostly use)
+<td width=30%>
+</table>
+
+Rosetta Stone
+=============
+
+Here's how it looks to say the same thing in various of these languages.
+
+1. Binding suitable values to the variables `three` and `two`, and adding them.
+
+ In Scheme:
+
+ (let* ((three 3))
+ (let ((two 2))
+ (+ three two)))
+
+ In OCaml:
+
+ let three = 3 in
+ let two = 2 in
+ three + two
+
+ Notice OCaml lets you write the `+` in between the `three` and `two`, as you're accustomed to. However most functions need to come leftmost, even if they're binary. And you can do this with `+` too, if you enclose it in parentheses so that the OCaml parser doesn't get confused by your syntax:
+
+ let three = 3 in
+ let two = 2 in
+ ( + ) three two
+
+ In the lambda calculus: here we're on our own, we don't have predefined constants like `+` and `3` and `2` to work with. We've got to build up everything from scratch. We'll be seeing how to do that over the next weeks.
+
+ But supposing you had constructed appropriate values for `+` and `3` and `2`, you'd place them in the ellided positions in:
+
+ (((\three (\two ((... three) two))) ...) ...)
+
+ In an ordinary imperatival language like C:
+
+ int three = 3;
+ int two = 2;
+ three + two;
+
+2. Mutation
+
+ In C this looks almost the same as what we had before:
+
+ int x = 3;
+ x = 2;
+
+ Here we first initialize `x` to hold the value 3; then we mutate `x` to hold a new value.
+
+ In (the imperatival part of) Scheme, this could be done as:
+
+ (let ((x (box 3)))
+ (set-box! x 2))
+
+ In general, mutating operations in Scheme are named with a trailing `!`. There are other imperatival constructions, though, like `(print ...)`, that don't follow that convention.
+
+ In (the imperatival part of) OCaml, this could be done as:
+
+ let x = ref 3 in
+ x := 2
+
+ Of course you don't need to remember any of this syntax. We're just illustrating it so that you see that in Scheme and OCaml it looks somewhat different than we had above. The difference is much more obvious than it is in C.
+
+ In the lambda calculus: sorry, you can't do mutation. At least, not natively. Later in the term we'll be learning how in fact, really, you can embed mutation inside the lambda calculus even though the lambda calculus has no primitive facilities for mutation.
+
+