For example, you'll encounter the claim that declarative languages are distinguished by their **referential transparency.** What's meant by this is not always exactly the same, and as a cluster, it's related to but not the same as this means for philosophers and linguists.
-The notion of "function" that we'll be working with will be one that, by default, sometimes counts as non-identical functions that map all their inputs to the very same outputs. For example, two functions from jumbled decks of cards to sorted decks of cards may use different algorithms and hence be different functions.
+The notion of **function** that we'll be working with will be one that, by default, sometimes counts as non-identical functions that map all their inputs to the very same outputs. For example, two functions from jumbled decks of cards to sorted decks of cards may use different algorithms and hence be different functions.
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 this in terms of functions from worlds to extensions (an idea also associated with Church), you will hurt yourself. So too if you try to understand it in terms of mental stereotypes, another notion sometimes designated by "intension."
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 static typing
- * dynamic versus lexical scoping
+* dynamic versus lexical scoping
- * dynamic versus static control operators
+* dynamic versus static control operators
- * finally, we're used ourselves to talking about dynamic versus static semantics
+* 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.
Here is its syntax:
- Variables: x, y, z, ...
+<blockquote>
+<strong>Variables</strong>: <code>x</code>, <code>y</code>, <code>z</code>...
+</blockquote>
Each variable is an expression. For any expressions M and N and variable a, the following are also expressions:
-<blockquote><code>
- Abstract: ( λa M )
+<blockquote>
+<strong>Abstract</strong>: <code>(λa M)</code>
+</blockquote>
- Application: ( M N )
-</code></blockquote>
+We'll tend to write <code>(λa M)</code> as just `(\a M)`, so we don't have to write out the markup code for the <code>λ</code>. You can yourself write <code>(λa M)</code> or `(\a M)` or `(lambda a M)`.
-We'll tend to write <code>( λa M )</code> as just `( \a M )`.
+<blockquote>
+<strong>Application</strong>: <code>(M N)</code>
+</blockquote>
-Some authors reserve the term "term" for just variables and abstracts. We won't participate in that convention; we'll probably just say "term" and "expression" indiscriminately.
+Some authors reserve the term "term" for just variables and abstracts. We won't participate in that convention; we'll probably just say "term" and "expression" indiscriminately for expressions of any of these three forms.
Examples of expressions:
(x (\x x))
((\x (x x)) (\x (x x)))
-The lambda calculus has an associated proof theory. For now, we can regard the proof theory as having just one rule, called the rule of "beta-reduction" or "beta-contraction". Suppose you have some expression of the form:
+The lambda calculus has an associated proof theory. For now, we can regard the proof theory as having just one rule, called the rule of **beta-reduction** or "beta-contraction". Suppose you have some expression of the form:
((\a M) N)
The rule of beta-reduction permits a transition from that expression to the following:
- M {a:=N}
+ M [a:=N]
What this means is just `M`, with any *free occurrences* inside `M` of the variable `a` replaced with the term `N`.