X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week1.mdwn;h=6391bb5a177fc8a6411f9387c5ecc73e4c4e28dd;hp=af079edf543c975f90a646c8d4ea6a8625cd6454;hb=830bceeb7d4175430140587be3a80747a6a69314;hpb=2b49dd93ee877d3a9f868933c9113fbbda94df88
diff --git a/week1.mdwn b/week1.mdwn
index af079edf..6391bb5a 100644
--- a/week1.mdwn
+++ b/week1.mdwn
@@ -57,11 +57,22 @@ We'll tend to write (λa M)
as just `(\a M)`, so we don't hav
Application: (M N)
-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.
-Samples of expressions
+Examples of expressions:
-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:
+ 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
+"beta-contraction". Suppose you have some expression of the form:
((\a M) N)
@@ -143,47 +154,53 @@ Shorthand
The grammar we gave for the lambda calculus leads to some verbosity. There are several informal conventions in widespread use, which enable the language to be written more compactly. (If you like, you could instead articulate a formal grammar which incorporates these additional conventions. Instead of showing it to you, we'll leave it as an exercise for those so inclined.)
-**Dot notation** Dot means "put a left paren here, and put the right
-paren as far the right as possible without creating unbalanced
-parentheses". So:
+**Parentheses** Outermost parentheses around applications can be dropped. Moreover, applications will associate to the left, so `M N P` will be understood as `((M N) P)`. Finally, you can drop parentheses around abstracts, but not when they're part of an application. So you can abbreviate:
- (\x (\y (x y)))
+ (\x (x y))
-can be abbreviated as:
+as:
+
+ \x (x y)
+
+but you should include the parentheses in:
- (\x (\y. x y))
+ (\x (x y)) z
and:
- (\x (\y. (z y) z))
+ z (\x (x y))
+
+
+**Dot notation** Dot means "put a left paren here, and put the right
+paren as far the right as possible without creating unbalanced
+parentheses". So:
-would abbreviate:
+ \x (\y (x y))
- (\x (\y ((z y) z)))
+can be abbreviated as:
-This on the other hand:
+ \x (\y. x y)
- (\x (\y. z y) z)
+and that as:
-would abbreviate:
+ \x. \y. x y
- (\x (\y (z y)) z)
+This:
-**Parentheses** Outermost parentheses around applications can be dropped. Moreover, applications will associate to the left, so `M N P` will be understood as `((M N) P)`. Finally, you can drop parentheses around abstracts, but not when they're part of an application. So you can abbreviate:
+ \x. \y. (x y) x
- (\x. x y)
+abbreviates:
-as:
+ \x (\y ((x y) x))
- \x. x y
+This on the other hand:
-but you should include the parentheses in:
+ (\x. \y. (x y)) x
- (\x. x y) z
+abbreviates:
-and:
+ ((\x (\y (x y))) x)
- z (\x. x y)
**Merging lambdas** An expression of the form `(\x (\y M))`, or equivalently, `(\x. \y. M)`, can be abbreviated as:
@@ -249,7 +266,7 @@ computer](/how_to_get_the_programming_languages_running_on_your_computer), and
proposed answers to the assignment.
-
+There's also a (slow, bare-bones, but perfectly adequate) version of Scheme available for online use at
- ∀x. (F x or ∀x (not (F x)))
-
+ ∀x. (F x or ∀x (not (F x)))
+
When a previously-bound variable is rebound in the way we see here, that's called **shadowing**: the outer binding is shadowed during the scope of the inner binding.
@@ -739,7 +754,7 @@ Or even:
(define foo B)
(foo 2)
-don't involve any changes or sequencing in the sense we're trying to identify. As we said, these programs are just syntactic variants of (single) compound syntactic structures involving "let"s and "lambda"s.
+don't involve any changes or sequencing in the sense we're trying to identify. As we said, these programs are just syntactic variants of (single) compound syntactic structures involving `let`s and `lambda`s.
Since Scheme and OCaml also do permit imperatival constructions, they do have syntax for genuine sequencing. In Scheme it looks like this:
@@ -778,18 +793,5 @@ contributes no more to a larger context in which it's embedded than C does. This
We'll discuss this more as the seminar proceeds.
-1. Declarative vs imperatival models of computation.
-2. Variety of ways in which "order can matter."
-3. Variety of meanings for "dynamic."
-4. Schoenfinkel, Curry, Church: a brief history
-5. Functions as "first-class values"
-6. "Curried" functions
-
-1. Beta reduction
-1. Encoding pairs (and triples and ...)
-1. Encoding booleans
-
-
-