Implementing Fibonacci sequence using pure lambda calculus and Church numerals in Racket

Question

I've been struggling with the Lambda Calculus for quite some time now. There are plenty of resources that explain how to reduce nested lambda expressions, but less so that guide me in writing my own lambda expressions.

I'm trying to write the a recursive Fibonacci solution in Racket using pure lambda calculus (i.e, single argument functions, Church numerals).

These are definitions for the Church Numerals I've been using:

(define zero  (λ (f) (λ (x) x)))
(define one   (λ (f) (λ (x) (f x))))
(define two   (λ (f) (λ (x) (f (f x)))))
(define three (λ (f) (λ (x) (f (f (f x))))))
(define four  (λ (f) (λ (x) (f (f (f (f x)))))))
(define five  (λ (f) (λ (x) (f (f (f (f (f x))))))))
(define six   (λ (f) (λ (x) (f (f (f (f (f (f x)))))))))
(define seven (λ (f) (λ (x) (f (f (f (f (f (f (f x))))))))))
(define eight (λ (f) (λ (x) (f (f (f (f (f (f (f (f x)))))))))))
(define nine  (λ (f) (λ (x) (f (f (f (f (f (f (f (f (f x))))))))))))

And these are the single-argument functions I've been attempting to incorporate:

(define succ   (λ (n) (λ (f) (λ (x) (f ((n f) x))))))
(define plus   (λ (n) (λ (m) ((m succ) n))))
(define mult   (λ (n) (λ (m) ((m (plus n)) zero))))
(define TRUE   (λ (t) (λ (f) t)))
(define FALSE  (λ (t) (λ (f) f)))
(define COND   (λ (c) (λ (x) (λ (y) ((c x) y)))))
(define iszero (λ (x) (x ((λ (y) FALSE) TRUE))))
(define pair   (λ (m) (λ (n) (λ (b) (((IF b) m) n)))))
(define fst    (λ (p) (p TRUE)))
(define snd    (λ (p) (p FALSE)))
(define pzero  ((pair zero) zero))
(define psucc  (λ (n) ((pair (snd n)) (succ (snd n)))))
(define pred   (λ (n) (λ (f) (λ (x) (((n (λ (g) (λ (h) (h (g f))))) (λ (u) x))(λ (u) u))))))
(define sub    (λ (m) (λ (n) ((n pred) m))))
(define leq    (λ (m) (λ (n) (iszero ((sub m) n))))) ;; less than or equal
(define Y      ((λ (f) (f f)) (λ (z) (λ (f) (f (λ (x) (((z z) f) x))))))) ;; Y combinator

I started by writing recursive Fibonacci in Racket:

(define (fib depth)
  (if (> depth 1)
    (+ (fib (- depth 1)) (fib (- depth 2)))
  depth))

But in my many tries, I've been unsuccessful to write it using pure lambda calculus. Even getting the beginning started has been a struggle.

(define fib
   (λ (x) ((leq x) one)))

Which I call with (for example):

(((fib three) add1) 0)

This at least works (correctly returns a Church zero or one), but adding anything beyond this breaks everything.

I'm very inexperienced with Racket, and the Lambda Calculus is quite a head scratcher as someone who's never picked it up until recently.

I would like to understand how to build this function out, and incorporate recursion with the Y combinator. I'd especially appreciate an explanation alongside any code. Getting it to work with fib(zero) up to fib(six) would be enough as I can worry about expanding the Church definitions at a later time.

---

EDIT:

My iszero function was a hidden saboteur in my implementation. Here is a proper version, with the updated Booleans from Alex's answer:

(define iszero (λ (x) ((x (λ (y) FALSE)) TRUE)))
(define TRUE   (λ (t) (λ (f) (t))))
(define FALSE  (λ (t) (λ (f) (f))))

With those changes, and incorporating the thunks, everything is working as it should!

Answer 1

Branching forms and short-circuiting

If you're in an eager (not lazy) language like Racket, you need to be careful about how you encode branching forms like your COND function.

Your existing definitions of booleans and conditionals are:

(define TRUE   (λ (t) (λ (f) t)))
(define FALSE  (λ (t) (λ (f) f)))
(define COND   (λ (c) (λ (x) (λ (y) ((c x) y)))))

And they work for simple cases like this:

> (((COND TRUE) "yes") "no")
"yes"
> (((COND FALSE) "yes") "no")
"no"

However, if the "branch not taken" would produce an error or an infinite loop, then a good branching form would "short-circuit" to avoid triggering it. A good branching form should only evaluate the branch it needs to take.

> (if #true "yes" (error "shouldn't get here"))
"yes"
> (if #false (error "shouldn't trigger this either") "no")
"no"

However your COND evaluates both branches, simply because Racket's function application evaluates all the arguments:

> (((COND TRUE) "yes") (error "shouldn't get here"))
;shouldn't get here
> (((COND FALSE) (error "shouldn't trigger this either")) "no")
;shouldn't trigger this either

Using extra lambdas to implement short-circuiting

The way I was taught to get around this in an eager language (without switching to #lang lazy for example) was to pass thunks to branching forms like this:

(((COND TRUE) (λ () "yes")) (λ () (error "doesn't get here")))

However, this requires some slight tweaks to the definition of what a boolean is. Before, a boolean took two values to choose from, and returned one. Now, a boolean would take in two thunks to choose from, and it would call one.

(define TRUE (λ (t) (λ (f) (t))))   ; note the extra parens in the body
(define FALSE (λ (t) (λ (f) (f))))  ; same extra parens

The COND form can be defined the same way as before, but you would have to use it differently. To translate (if c t e) where before you wrote:

(((COND c) t) e)

Now with the new definition of the booleans you would write:

(((COND c) (λ () t)) (λ () e))

I'm going to abbreviate (λ () expr) as {expr} so that I can write it as this instead:

(((COND c) {t}) {e})

Now what previously failed with an error, returns the correct result:

> (((COND TRUE) {"yes"}) {(error "shouldn't get here")})
"yes"

This allows you to write conditionals where one of the branches is a "base case" where it stops, and the other branch is a "recursive case" where it would keep going.

(Y (λ (fib)
     (λ (x)
       (((COND ((leq x) one))
         {x})
        {... (fib (sub x two)) ...}))))

Without those extra (λ () ....)'s and the new definition of booleans, this would loop forever because of Racket's eager (not lazy) argument-evaluation.