- h := \xy.x
- H := \f.h(ff) == \f.(\xy.x)(ff) ~~> \fy.ff
- H H := (\fy.ff)(\fy.ff) ~~> \y.(\fy.ff)(\fy.ff)
-
-Ok, it doesn't have a normal form. But let's check that it is in fact
-a fixed point:
-
- K(H H) == (\xy.x)((\fy.ff)(\fy.ff)
+Before we begin, we can reason a bit about what the fixed point must
+be like. We're looking for a fixed point for `K`, i.e., `\xy.x`. `K`
+ignores its second argument. That means that no matter what we give
+`K` as its first argument, the result will ignore the next argument
+(that is, `KX` ignores its first argument, no matter what `X` is). So
+if `KX <~~> X`, `X` had also better ignore its first argument. But we
+also have `KX ≡ (\xy.x)X ~~> \y.X`. This means that if `X` ignores
+its first argument, then `\y.X` will ignore its first two arguments.
+So once again, if `KX <~~> X`, `X` also had better ignore at least its
+first two arguments. Repeating this reasoning, we realize that `X`
+must be a function that ignores an infinite series of arguments.
+Our expectation, then, is that our recipe for finding fixed points
+will build us a function that somehow manages to ignore an infinite
+series of arguments.
+
+ h ≡ \xy.x
+ H ≡ \f.h(ff) ≡ \f.(\xy.x)(ff) ~~> \fy.ff
+ H H ≡ (\fy.ff)(\fy.ff) ~~> \y.(\fy.ff)(\fy.ff)
+
+Let's check that it is in fact a fixed point:
+
+ K(H H) ≡ (\xy.x)((\fy.ff)(\fy.ff)