tweaks

[lambda.git] / topics / week4_more_about_fixed_point_combinators.mdwn

diff --git a/topics/week4_more_about_fixed_point_combinators.mdwn b/topics/week4_more_about_fixed_point_combinators.mdwn
index 11754dd..763c18b 100644 (file)
--- a/topics/week4_more_about_fixed_point_combinators.mdwn
+++ b/topics/week4_more_about_fixed_point_combinators.mdwn
@@ -60,15 +60,15 @@ Used in a context in which *this sentence meaning* refers to the meaning express
 or `\m y n. m n y`, which is the `C` combinator.  So in such a
 context, (2) might denote
 
 or `\m y n. m n y`, which is the `C` combinator.  So in such a
 context, (2) might denote
 

-     Y C
-     (\h. (\u. h (u u)) (\u. h (u u))) C
-     (\u. C (u u)) (\u. C (u u)))
-     C ((\u. C (u u)) (\u. C (u u)))
-     C (C ((\u. C (u u)) (\u. C (u u))))
-     C (C (C ((\u. C (u u)) (\u. C (u u)))))
+     Y C ≡
+     (\h. (\u. h (u u)) (\u. h (u u))) C ~~>
+     (\u. C (u u)) (\u. C (u u))) ~~>
+     C ((\u. C (u u)) (\u. C (u u))) ~~>
+     C (C ((\u. C (u u)) (\u. C (u u)))) ~~>
+     C (C (C ((\u. C (u u)) (\u. C (u u))))) ~~>

      ...
 
      ...
 

-And infinite sequence of `C`s, each one negating the remainder of the
+An infinite sequence of `C`s, each one negating the remainder of the

 sequence.  Yep, that feels like a reasonable representation of the
 liar paradox.
 
 sequence.  Yep, that feels like a reasonable representation of the
 liar paradox.
 


@@ -161,13 +161,13 @@ of `N`, by the reasoning in the previous answer.
 
 A: Right:
 
 
 A: Right:
 

-    let Y = \N. (\u. N (u u)) (\u. N (u u)) in
-    Y Y
-    ≡   \N. (\u. N (u u)) (\u. N (u u)) Y
-    ~~>     (\u. Y (u u)) (\u. Y (u u))
-    ~~>          Y ((\u. Y (u u)) (\u. Y (u u)))
-    ~~>          Y (     Y ((\u. Y (u u)) (\u. Y (u u))))
-    ~~> Y (Y (Y (...(Y (Y Y))...)))
+    let Y = \h. (\u. h (u u)) (\u. h (u u)) in
+    Y Y ≡
+    \h. (\u. h (u u)) (\u. h (u u)) Y ~~>
+        (\u. Y (u u)) (\u. Y (u u)) ~~>
+             Y ((\u. Y (u u)) (\u. Y (u u))) ~~>
+             Y (     Y ((\u. Y (u u)) (\u. Y (u u)))) <~~>
+             Y (     Y (     Y (...(Y (Y Y))...)))

 
 
 
 
 
 


@@ -176,8 +176,8 @@ A: Right:
 A: Is that a question?
 
 Let's come at it from the direction of arithmetic.  Recall that we
 A: Is that a question?
 
 Let's come at it from the direction of arithmetic.  Recall that we

-claimed that even `succ`---the function that added one to any
-number---had a fixed point.  How could there be an `ξ` such that `ξ <~~> succ ξ`?
+claimed that even `succ` --- the function that added one to any
+number --- had a fixed point.  How could there be an `ξ` such that `ξ <~~> succ ξ`?

 That would imply that
 
     ξ <~~> succ ξ <~~> succ (succ ξ) <~~> succ (succ (succ ξ)) <~~> succ (...(succ ξ)...)
 That would imply that
 
     ξ <~~> succ ξ <~~> succ (succ ξ) <~~> succ (succ (succ ξ)) <~~> succ (...(succ ξ)...)


@@ -294,19 +294,19 @@ So for instance:
 
 `A 1 x` is to `A 0 x` as addition is to the successor function;
 `A 2 x` is to `A 1 x` as multiplication is to addition;
 
 `A 1 x` is to `A 0 x` as addition is to the successor function;
 `A 2 x` is to `A 1 x` as multiplication is to addition;

-`A 3 x` is to `A 2 x` as exponentiation is to multiplication---
+`A 3 x` is to `A 2 x` as exponentiation is to multiplication ---

 so `A 4 x` is to `A 3 x` as hyper-exponentiation is to exponentiation...
 
 ## Q: What other questions should I be asking? ##
 
 so `A 4 x` is to `A 3 x` as hyper-exponentiation is to exponentiation...
 
 ## Q: What other questions should I be asking? ##
 

-*    What is it about the variant fixed-point combinators that makes
-     them compatible with a call-by-value evaluation strategy?
+*    What is it about the "primed" fixed-point combinators `Θ′` and `Y′` that
+     makes them compatible with a call-by-value evaluation strategy?
+
+*    What *exactly* is primitive recursion?

 
 *    How do you know that the Ackermann function can't be computed
      using primitive recursion techniques?
 
 
 *    How do you know that the Ackermann function can't be computed
      using primitive recursion techniques?
 

-*    What *exactly* is primitive recursion?
-

 *    I hear that `Y` delivers the/a *least* fixed point.  Least
      according to what ordering?  How do you know it's least?
      Is leastness important?
 *    I hear that `Y` delivers the/a *least* fixed point.  Least
      according to what ordering?  How do you know it's least?
      Is leastness important?