index 339bb16..666b460 100644 (file)

where `X1` happens also to be the lambda term that is the head of `ξ1`; and `X2` happens also to be the lambda term that is the head of `ξ2`.

+*   Where we have `H` in `X1` (the head of `ξ1`), there we could just use the bound variable `u`, right? Similarly for `G` we could just use the bound variable `v`, right? And similarly for `X2` (the head of `ξ2`). So:
+
+        ξ1 ≡ (\u v. h (X1 u v) (X2 u v)) H G
+        ξ2 ≡ (\u v. g (X1 u v) (X2 u v)) H G
+
*   Can you solve it yet?

*   Don't bring in `Y` or any other already-familiar fixed point combinator; that's a false path. You don't need it.
@@ -79,8 +84,6 @@

*   `H` is `X1` and `G` is `X2`.

-*   Also, where we have `H` in `X1` (the head of `ξ1`), there we could just use the bound variable `u`, right? Similarly for `G` we could just use the bound variable `v`, right? And similarly for `X2` (the head of `ξ2`).
-
*   Now can you figure out how to get rid of the explicit self-referencing whereby `X1` contains the free variable `X1`, meant to refer to the lambda abstract that contains it? If `X1` is just `H`, also known inside the body of `X1` as `u`, we could just write `ξ1` like this, right:

ξ1 ≡ (\u v. h (u u v) (X2 u v)) H G