From: jim <jim@web>
Date: Sun, 22 Feb 2015 21:37:50 +0000 (-0500)
Subject: add explanatory paragraph
X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=e7c61d01fb015af60f2f8e266f7a5931283945fc

add explanatory paragraph
---

diff --git a/topics/week4_fixed_point_combinators.mdwn b/topics/week4_fixed_point_combinators.mdwn
index ed22cfff..ca9ab649 100644
--- a/topics/week4_fixed_point_combinators.mdwn
+++ b/topics/week4_fixed_point_combinators.mdwn
@@ -281,7 +281,7 @@ saying that we are looking for a fixed point for `h`:
 
     h LENGTH <~~> LENGTH
 
-Replacing `h` with its definition, we have
+Replacing `h` with its definition, we have:
 
     (\xs. (empty? xs) 0 (succ (LENGTH (tail xs)))) <~~> LENGTH
 
@@ -289,7 +289,17 @@ If we can find a value for `LENGTH` that satisfies this constraint, we'll
 have a function we can use to compute the length of an arbitrary list.
 All we have to do is find a fixed point for `h`.
 
-The strategy we will present will turn out to be a general way of
+Let's reinforce this. The left-hand side has the form:
+
+    (\body. Φ[...body...]) LENGTH
+
+which beta-reduces to:
+
+    Φ[...LENGTH...]
+
+where that whole formula is convertible with the term LENGTH itself. In other words, the term `Φ[...LENGTH...]` contains (a term that convertible with) itself --- despite being only finitely long. (If it had to contain a term *syntactically identical to* itself, this could not be achieved.)
+
+The key to achieving all this is finding a fixed point for `h`. The strategy we will present will turn out to be a general way of
 finding a fixed point for any lambda term.