Search code examples
schemelambda-calculus

Y combinator in scheme blows up using Church numbers, but works on regular numbers


I've just read "A Tutorial Introduction to the Lambda Calculus1" by Raul Rojas. I put the lambda expressions into Scheme (TinyScheme) to try them out. Everything worked except the recursive function to calculate the sum of the Church numbers 0,1,...,N using the Y-combinator which runs out of memory. Bizarrely, the Y-combinator works if I calculate the sum using regular numbers.

Here is my Y-combinator,

(define myY
  (lambda (y) 
    ((lambda (x) (x x)) 
      (lambda (x) 
        (y (lambda (a) ((x x) a)))))))

Here is a recursive function to get the sum of N regular numbers,

(define sum1
  (lambda (r)
    (lambda (x)
      (cond
        ((zero? x) 0)
        (else (+ x (r (sub1 x))))))))

This works

> ((myY sum1) 10)
55

At the bottom of page 15 of the tutorial, the recursive function R=Lrx.Zx0(NS(r(PN))) is used to calculate the sum of N numbers (L=lambda). In this expression, r will be the recursive function, x will be a Church number, Z is the test for zero function, 0 is a zero as a Church number, N is a church number, S is the successor function, P is the predecessor function. I've translated this into Scheme as,

(define myR
  (lambda (r)
    (lambda (x)
      (((myZ x) my0) ((x myS) (r (myP x))))
     )))

However, even taking the sum of 0 number blows up.

> ((((myY myR) my0) add1) 0)
No memory!

In the above line, the ((myY myR) my0) should return the Church number zero. I just get the Church number to act on add1 in order to get a human-readable Church number.

Initially, I thought the Y-combinator was the problem, but, as I've shown, this works on recursive functions which use regular numbers. The Church numbers are defined as in the Tutorial and the Scheme versions of the lambda expressions work for arithmetic (addition, multiplication, inequalities).

Edit: The function myZ is the lambda expression Z=Lx.xF¬F where F=Lxy.y is False (True is T=Lxy.x) and ¬=Lx.xFT is NOT. The function Z implements a conditional test because Z0=T and ZN=F where 0 is the Church number for zero (0=Lxy.y) and N is a non-zero Church number (1=Lxy.xy, 2=Lxy.x(xy) etc.) The Scheme code myZ which implements Z is,

(define myZ
  (lambda (x)
    (((x myF) myNeg) myF)
    ))

Solution

  • The lambda calculus only works with normal order reduction (i.e. arguments are only evaluated when their values are needed), and Scheme uses applicative order reduction (arguments are evaluated first), except in "special forms".

    Your code works with regular numbers not because of the numbers, but because of cond, which will evaluate at most one of its clauses.

    If you replace the cond in your sum1 with a regular function, your computation will not terminate with regular numbers either.

    ; This does not work
    (define (conditional b t e)
      (if b t e))
    
    (define sum1
      (lambda (r)
        (lambda (x)
          (conditional
            (zero? x)
            0
            (+ x (r (sub1 x)))))))
    

    You can fix this by adding a level of indirection; suspending evaluation of the branches by wrapping them in functions:

    (define sum1
      (lambda (r)
        (lambda (x)
          ((conditional
            (zero? x)
            (lambda (y) 0)
            (lambda (y) (+ x (r (sub1 x)))))
           "some argument"))))
    

    and the corresponding transformation will work in your implementation.