[plt-scheme] Y Combinator Exercise

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