week4 tweaking

Signed-off-by: Jim Pryor <profjim@jimpryor.net>

diff --git a/advanced_lambda.mdwn b/advanced_lambda.mdwn
index 6760ae7..d23245c 100644 (file)
--- a/advanced_lambda.mdwn
+++ b/advanced_lambda.mdwn
@@ -3,31 +3,7 @@
 
 #Version 4 lists: Efficiently extracting tails#
 
 
 #Version 4 lists: Efficiently extracting tails#
 

-An advantage of the v3 lists and v3 (aka "Church") numerals is that they
-have a recursive capacity built into their skeleton. So for many natural
-operations on them, you won't need to use a fixed point combinator. Why is
-that an advantage? Well, if you use a fixed point combinator, then the terms
-you get
-won't be strongly normalizing: whether their reduction stops at a normal form
-will depend on what evaluation order you use. Our online [[lambda evaluator]]
-uses normal-order reduction, so it finds a normal form if there's one to be
-had. But if you want to build lambda terms in, say, Scheme, and you wanted to
-roll your own recursion as we've been doing, rather than relying on Scheme's
-native `let rec` or `define`, then you can't use the fixed-point combinators
-`Y` or <code>&Theta;</code>. Expressions using them will have non-terminating
-reductions, with Scheme's eager/call-by-value strategy. There are other
-fixed-point combinators you can use with Scheme (in the [week 3 notes](/week3/#index7h2) they
-were <code>Y&prime;</code> and <code>&Theta;&prime;</code>. But even with
-them, evaluation order still matters: for some (admittedly unusual)
-evaluation strategies, expressions using them will also be non-terminating.
-
-The fixed-point combinators may be the conceptual stars. They are cool and
-mathematically elegant. But for efficiency and implementation elegance, it's
-best to know how to do as much as you can without them. (Also, that knowledge
-could carry over to settings where the fixed point combinators are in
-principle unavailable.)
-
-This is why the v3 lists and numbers are so lovely. However, one disadvantage
+Version 3 lists and Church numerals are lovely, because they have their recursive capacity built into their very bones. However, one disadvantage

 to them is that it's relatively inefficient to extract a list's tail, or get a
 number's predecessor. To get the tail of the list `[a;b;c;d;e]`, one will
 basically be performing some operation that builds up the tail afresh: at
 to them is that it's relatively inefficient to extract a list's tail, or get a
 number's predecessor. To get the tail of the list `[a;b;c;d;e]`, one will
 basically be performing some operation that builds up the tail afresh: at

diff --git a/week4.mdwn b/week4.mdwn
index bc154ae..150e883 100644 (file)
--- a/week4.mdwn
+++ b/week4.mdwn
@@ -276,6 +276,35 @@ can just deliver that answer, and not branch into any further recursion. If
 you've got the right evaluation strategy in place, everything will work out
 fine.
 
 you've got the right evaluation strategy in place, everything will work out
 fine.
 

+--
+An advantage of the v3 lists and v3 (aka "Church") numerals is that they
+have a recursive capacity built into their skeleton. So for many natural
+operations on them, you won't need to use a fixed point combinator. Why is
+that an advantage? Well, if you use a fixed point combinator, then the terms
+you get
+won't be strongly normalizing: whether their reduction stops at a normal form
+will depend on what evaluation order you use. Our online [[lambda evaluator]]
+uses normal-order reduction, so it finds a normal form if there's one to be
+had. But if you want to build lambda terms in, say, Scheme, and you wanted to
+roll your own recursion as we've been doing, rather than relying on Scheme's
+native `let rec` or `define`, then you can't use the fixed-point combinators
+`Y` or <code>&Theta;</code>. Expressions using them will have non-terminating
+reductions, with Scheme's eager/call-by-value strategy. There are other
+fixed-point combinators you can use with Scheme (in the [week 3 notes](/week3/#index7h2) they
+were <code>Y&prime;</code> and <code>&Theta;&prime;</code>. But even with
+them, evaluation order still matters: for some (admittedly unusual)
+evaluation strategies, expressions using them will also be non-terminating.
+
+The fixed-point combinators may be the conceptual stars. They are cool and
+mathematically elegant. But for efficiency and implementation elegance, it's
+best to know how to do as much as you can without them. (Also, that knowledge
+could carry over to settings where the fixed point combinators are in
+principle unavailable.)
+
+This is why the v3 lists and numbers are so lovely..
+
+--
+

 But what if you're using v3 lists? What options would you have then for
 aborting a search?
 
 But what if you're using v3 lists? What options would you have then for
 aborting a search?
 

diff --git a/week5.mdwn b/week5.mdwn
index a13c55e..3eed60e 100644 (file)
--- a/week5.mdwn
+++ b/week5.mdwn
@@ -2,7 +2,7 @@
 
 ##The simply-typed lambda calculus##
 
 
 ##The simply-typed lambda calculus##
 

-The uptyped lambda calculus is pure computation.  It is much more
+The untyped lambda calculus is pure computation.  It is much more

 common, however, for practical programming languages to be typed.
 Likewise, systems used to investigate philosophical or linguistic
 issues are almost always typed.  Types will help us reason about our
 common, however, for practical programming languages to be typed.
 Likewise, systems used to investigate philosophical or linguistic
 issues are almost always typed.  Types will help us reason about our