index f449ed4..cacb73f 100644 (file)
@@ -57,18 +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>

<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.
-
-Examples of expressions:
-
-       x
-       (y x)
-       (x x)
-       (\x y)
-       (\x x)
-       (\x (\y x))
-       (x (\x x))
-       ((\x (x x)) (\x (x x)))
+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.

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: