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
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.
## Fixed-point Combinators Are a Bit Intoxicating ##
-[[tatto|/images/y-combinator-fixed.jpg]]
+[[tatto|/images/y-combinator-fixed.png]]
There's a tendency for people to say "Y-combinator" to refer to fixed-point combinators generally. We'll probably fall into that usage ourselves. Speaking correctly, though, the Y-combinator is only one of many fixed-point combinators.