week1: tweaks
[lambda.git] / week1.mdwn
index a5e697a..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>
 
-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: