From cefc5c1a3fc59d086dc153af19f29c79135c1ba8 Mon Sep 17 00:00:00 2001 From: jim Date: Fri, 20 Feb 2015 15:35:24 -0500 Subject: [PATCH] tweak --- exercises/assignment4_hint.mdwn | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/exercises/assignment4_hint.mdwn b/exercises/assignment4_hint.mdwn index 339bb162..666b4603 100644 --- a/exercises/assignment4_hint.mdwn +++ b/exercises/assignment4_hint.mdwn @@ -67,6 +67,11 @@ 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 -- 2.11.0