index 75f0cc1..c13fa7c 100644 (file)
@@ -57,7 +57,7 @@ We'll tend to write <code>(&lambda;a M)</code> as just `(\a M)`, so we don't hav
<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 for expressions of any of these three forms.
+Some authors reserve the term "term" for just variables and abstracts. We'll probably just say "term" and "expression" indiscriminately for expressions of any of these three forms.

Examples of expressions:

@@ -68,13 +68,13 @@ Examples of expressions:
(\x x)
(\x (\y x))
(x (\x x))
-       ((\x (x x)) (\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:

-       ((\a M) N)
+       ((\ a M) N)

that is, an application of an abstract to some other expression. This compound form is called a **redex**, meaning it's a "beta-reducible expression." `(\a M)` is called the **head** of the redex; `N` is called the **argument**, and `M` is called the **body**.

@@ -603,7 +603,6 @@ Here's how it looks to say the same thing in various of these languages.

It's easy to be lulled into thinking this is a kind of imperative construction. *But it's not!* It's really just a shorthand for the compound "let"-expressions we've already been looking at, taking the maximum syntactically permissible scope. (Compare the "dot" convention in the lambda calculus, discussed above.)

-
9.     Some shorthand

OCaml permits you to abbreviate:
@@ -652,6 +651,8 @@ Here's how it looks to say the same thing in various of these languages.

or in other words, interpret the rest of the file or interactive session with `bar` assigned the function `(lambda (x) B)`.

+<!--
+