[plt-scheme] Y Combinator Exercise

Thanks all for the tips and suggestions on the Y combinator.
I'll be giving some references to my students a couple of exercises.

Thanks once again,

Paulo Matos

On 16/11/05, Matthias Felleisen <matthias at ccs.neu.edu> wrote:
>
> On Nov 16, 2005, at 6:20 PM, John Clements wrote:
>
> >
> > On Nov 16, 2005, at 12:59 PM, Matthias Felleisen wrote:
> >
> >> In the monograph on reduction semantics [Felleisen & Flatt], we had
> >> some sample calculations using the Y combinator along the lines of
> >> what John points out. Use reductions to show ((Y mk-!) 2) is 2. Then
> >> show them that the fixpoint equation helps. Reprove the first one and
> >> wow it all gets easier. Then show them that you need a calculus (=)
> >> and that reductions (->) are no longer enough for this. Puzzle: can
> >> you design a cbv Y-like combinator that doesn't use 'backwards'
> >> reductions. -- Matthias
> >
> > <humility>
> > Okay, now I'm confused.  Isn't cbv Y _itself_ a Y-like combinator that
> > doesn't use 'backwards' reductions?
> > </humility>
>
> Watch below. Y doesn't show up anymore after you start reducing. The
> terms get bigger and bigger.
>
> More succicently:
>
>   \-v |- Y (\f\.xM) = ((\f.\x.M) (Y (\f\.xM)))
>
> but not
>
>   \-v |- Y (\f\.xM) ->* ((\f.\x.M) (Y (\f\.xM)))
>
> Of course all of the below is easier to calculate out if you use the
> unrolling/fixpoint equation. See monograph -- Matthias
>
>
> (define -> '->)
>
> (define Y
>    (lambda (f)
>      ((lambda (g) (f (lambda (x) ((g g) x))))
>       (lambda (g) (f (lambda (x) ((g g) x)))))))
>
> (define !!
>    (lambda (!)
>      (lambda (n)
>        (if (zero? n) 1 (* n (! (- n 1)))))))
>
> ((Y !!) 0)
> ->
> (((lambda (f)
>      ((lambda (g) (f (lambda (x) ((g g) x))))
>       (lambda (g) (f (lambda (x) ((g g) x))))))
>    (lambda (!)
>      (lambda (n)
>        (if (zero? n) 1 (* n (! (- n 1)))))))
>   0)
> ->
> (((lambda (g) ((lambda (!)
>                   (lambda (n)
>                     (if (zero? n) 1 (* n (! (- n 1))))))
>                 (lambda (x) ((g g) x))))
>    (lambda (g) ((lambda (!)
>                   (lambda (n)
>                     (if (zero? n) 1 (* n (! (- n 1))))))
>                 (lambda (x) ((g g) x)))))
>   0)
> ->
> ((lambda (n)
>     (if (zero? n)
>         1
>         (* n ((lambda (x)
>                 (((lambda (g) ((lambda (!)
>                                  (lambda (n)
>                                    (if (zero? n) 1 (* n (! (- n 1))))))
>                                (lambda (x) ((g g) x))))
>                   (lambda (g) ((lambda (!)
>                                  (lambda (n)
>                                    (if (zero? n) 1 (* n (! (- n 1))))))
>                                (lambda (x) ((g g) x)))))
>                  x))
>               (- n 1)))))
>   0)
> ->
> (if (zero? 0)
>      1
>      (* 0 ((lambda (x)
>              (((lambda (g) ((lambda (!)
>                               (lambda (n)
>                                 (if (zero? n) 1 (* n (! (- n 1))))))
>                             (lambda (x) ((g g) x))))
>                (lambda (g) ((lambda (!)
>                               (lambda (n)
>                                 (if (zero? n) 1 (* n (! (- n 1))))))
>                             (lambda (x) ((g g) x)))))
>               x))
>            (- 0 1))))
> ->
> ->
> 1
>
>


--
Paulo Jorge Matos - pocm at sat inesc-id pt
Web: http://sat.inesc-id.pt/~pocm
Computer and Software Engineering
INESC-ID - SAT Group