index c9b52d1..c13fa7c 100644 (file)
@@ -62,6 +62,13 @@ Some authors reserve the term "term" for just variables and abstracts. We'll pro
Examples of expressions:

x
+       (y x)
+       (x x)
+       (\x y)
+       (\x x)
+       (\x (\y 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
@@ -596,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:
@@ -645,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)`.

+<!--
+