exercises/assignment4_hint.mdwn

   1 ## Hint/solution for Y1, Y2 ##
   2
   3 (Perhaps you might read a few bullet points to get some momentum, then stop reading and see how much further you can get on your own.)
   4
   5 *   First, the thought exercise about `T T T`. Recall that `h` was of the form `\body. ...body...`, and we created one fixed point `ξ` like this:
   6
   7         H ≡ \u. h (u u)
   8         ξ ≡ H H
   9
  10     Now we want to create another fixed point `ξ′` that works like this:
  11
  12         T  ≡ \u v. h ...
  13         ξ′ ≡ T T T
  14            ≡ (\u v. h ...) T T
  15         <~~> h (T T T)
  16
  17     The last line is justified because we know that `ξ′ ≡ T T T` is supposed to be a fixed point of `h`. How could you fill in the `...` so that the next to last line reduced to the last line?
  18
  19 *   We're going to give the answer now, so try to solve it without looking...
  20
  21 *   Answer: `T ≡ (\u v. h (u u v))`. (Really it could be three occurrences of any mix of `u`s or `v`s. You could also use, for example `(\u v. h (v u v)`.) You'll see that when `u` is bound to `T` and so is `v`, then `(u u v) <~~> T T T`.
  22
  23 *   Ok, now let's tackle `Y1` and `Y2`. Begin by trying to specify `ξ1` and `ξ2` directly, then worry about making operators `Y1` and `Y2` such that:
  24
  25         ξ1 ≡ Y1 h g
  26         ξ2 ≡ Y2 h g
  27
  28     later. Remember how `ξ1` and `ξ2` need to work:
  29
  30         ξ1 <~~> h ξ1 ξ2 and
  31         ξ2 <~~> g ξ1 ξ2
  32
  33 *   First hint: `ξ1` is going to have the form `X1 H G`, for three terms `X1`, `H`, and `G`. Don't worry yet about what the terms `H` and `G` are.
  34
  35 *   Second hint: `ξ2` is going to have the form `X2 H G`.
  36
  37 *   So evidently, `X1` will be an abstract that accepts (at least) two arguments, and so too `X2`. We can write them schematically like this:
  38
  39         X1 ≡ \u v. ...
  40         X2 ≡ \u v. ...
  41
  42     (What fills in the `...` in the two cases will presumably be different.) And thus:
  43
  44         ξ1 ≡ (\u v. ...) H G
  45         ξ2 ≡ (\u v. ...) H G
  46
  47 *   Can you solve it now?
  48
  49 *   Another hint. `h` is going to be a function like `even?` that needs to refer to `odd?`, and possibly also to itself. (In the particular case of `even?` it doesn't need to refer to itself, but in general a mutually recursive function might.) So we can imagine `h` to have the form `\h g. ...`, and similarly, we can imagine `g` to have the form `\h g. ...`. For `g`, the `...` will presumably be different than it is for `h`. (We adopt the convention of always having the `\h` come first and the `\g` come second in *both* `h` and `g`, just because that makes some of the patterns that will emerge easier to see. You could do it differently if you wanted. Then your answer would be different than the one we're developing here.)
  50
  51 *   What `h` should be using for its `\h` variable is the fixed point `ξ1`; and for its `\g` variable is the fixed point `ξ2`. Same for `g`.
  52
  53 *   So `X1` will have the form:
  54
  55         X1 ≡ \u v. h ξ1 ξ2
  56            ≡ \u v. h (X1 H G) (X2 H G)
  57
  58     And `X2` will have the form:
  59
  60         X2 ≡ \u v. g ξ1 ξ2
  61            ≡ \u v. g (X1 H G) (X2 H G)
  62
  63     Thus:
  64
  65         ξ1 ≡ (\u v. h (X1 H G) (X2 H G)) H G
  66         ξ2 ≡ (\u v. g (X1 H G) (X2 H G)) H G
  67
  68     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`.
  69
  70 *   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:
  71
  72         ξ1 ≡ (\u v. h (X1 u v) (X2 u v)) H G
  73         ξ2 ≡ (\u v. g (X1 u v) (X2 u v)) H G
  74
  75 *   Can you solve it yet?
  76
  77 *   Don't bring in `Y` or any other already-familiar fixed point combinator; that's a false path. You don't need it.
  78
  79 *   The question you should be focusing on is: what are `H` and `G`? What are their relations to `X1` and `X2`? These might not be four distinct lambda terms. How many lambda terms do you think those four labels collectively designate?
  80
  81 *   They designate only two lambda terms.
  82
  83 *   Can you figure out what they are?
  84
  85 *   `H` is `X1` and `G` is `X2`.
  86
  87 *   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:
  88
  89         ξ1 ≡ (\u v. h (u u v) (X2 u v)) H G
  90
  91     And similarly, if `X2` is just `G`, also known inside the body of `X1` as `v`, we could just write `ξ1` like this, right:
  92
  93         ξ1 ≡ (\u v. h (u u v) (v u v)) H G
  94
  95     The lambda abstract that is the head of `ξ1` is just an ordinary, non-self-referring lambda term, and it is what we've been calling `X1` and `H`.
  96
  97 *   Now can you write `ξ2`?
  98
  99 *   Answer:
 100
 101         ξ2 ≡ (\u v. g (u u v) (v u v)) H G
 102
 103 *   So in short, `ξ1 ≡ H H G` and `ξ2 ≡ G H G`, where `H` and `G` are the terms `(\u v. h (u u v) (v u v))` and `(\u v. g (u u v) (v u v))`, respectively. If you do the substitutions, you will see that these definitions do indeed satisfy our constraint that:
 104
 105         ξ1 <~~> h ξ1 ξ2 and
 106         ξ2 <~~> g ξ1 ξ2
 107
 108 *   Ok, so that provides a `ξ1` and a `ξ2` for our specific choice of the functions `h` and `g`. Now can you generalize this, so that
 109
 110         ξ1 ≡ Y1 h g
 111         ξ2 ≡ Y2 h g
 112
 113 *   We're going to give the answer. Do you want to try again to solve it yourself? By this point you should be able to do it.
 114
 115 *   If you're confused, read this all through again until you understand it.
 116
 117 *   Ready for the answer?
 118
 119 *   Ok, here it is:
 120
 121         Y1 ≡ \h g. (\H G. H H G) (\u v. h (u u v) (v u v)) (\u v. g (u u v) (v u v))
 122         Y2 ≡ \h g. (\H G. G H G) (\u v. h (u u v) (v u v)) (\u v. g (u u v) (v u v))
 123
 124     You can reduce those a bit further, but it makes the pattern harder to see.
 125