Subject: Lambda Calculus Proof for Review

From: Shlomi Fish <[email-masked]>
Date: Fri, 19 Dec 2003 23:05:48 +0200 (IST)

Hi!

Someone sent me an E-mail recently saying that he read my lecture about
Lambda Calculus, and asked me to prove that the two versions of the
addition function of church numerals are equivalent:

<<<
(define add
    (lambda (n)
        (lambda (m)
            ((n succ) m)
        )
    )
)

And

<<<
(define add
    (lambda (m)
        (lambda (n)
            (lambda (f)
                (lambda (x)
                    ((m f)
                        ((n f) x)
                    )
                )
            )
        )
    )
)

So I set out to prove it and in a few hours came with this proof that I'm
including below. However, I'm not sure it is correct, so if any more
professional LCer can review it that would be nice.

If you need some background, you can refer here:

http://vipe.technion.ac.il/~shlomif/lecture/Lambda-Calculus/

(or any other resource that teaches Lambda Calculus)

Thanks in advance,

	Shlomi Fish

<<<
add ==  (lambda (n) (lambda (m) ((n succ) m)))

succ == (lambda (n) (lambda (f) (lambda (x) (f ((n f) x)))))

; Proof by Induction. Let's prove it for n == lc_zero
; Step 1 : Base
add == (lambda (n)
         (lambda (m)
            ((n succ) m)
         )
       )

; n == lc_zero so:
n == (lambda (f) (lambda (x) x))

add == (lambda (n) (lambda (m) m))

add == (lambda (n) (lambda (m) (lambda (f) (lambda (x) ((m f) x)))))

; Since ((n f) x) is:

((n f) x) == ((lc_zero f) x) == x

; It means that also:

add = (lambda (n) (lambda (m) (lambda (f) (lambda (x) ((n f) (m f) x)))))

; Step 2 : Induction step
; Let's assume it holds for n and prove it for n* = (succ n)

add == (lambda (n*)
         (lambda (m)
           ((n* succ) m)
         )
       )

add == (lambda (n*)
         (lambda (m)
           (((succ n) succ) m)))

; Substituting succ once
add == (lambda (n*)
         (lambda (m)
           (((
            (lambda (t)
              (lambda (f)
                (lambda (x)
                  (f ((t f) x))
                  )))
            n) succ) m)))

; Evalutating

add == (lambda (n*)
         (lambda (m)
           (succ ((n succ) m))
           )
         )

; Substituting succ again.

add == (lambda (n*)
         (lambda (m)
           ((lambda (t)
              (lambda (f)
                (lambda (x)
                  (f ((t f) x))
                  )))
           ((n succ) m)
           )
           )
         )

add == (lambda (n*)
         (lambda (m)
           (lambda (f)
             (lambda (x)
               (f (((n succ) m) f) x)
               )
             )
           )
         )

; ((((n succ) m) f) x) is ((n f) ((m f) x)) according to the induction hypothesis

add == (lambda (n*)
         (lambda (m)
           (lambda (f)
             (lambda (x)
               (f ((n f) ((m f) x)))
               )
             )
           )
         )

; Since (succ n) ==  (f ((n f) x)))
; It means we can substitute (f ((n f) [Expr])) with (((succ n) f) [Expr])

add == (lambda (n*)
         (lambda (m)
           (lambda (f)
             (lambda (x)
               (((succ n) f) ((m f) x))
               )
             )
           )
         )

; n* == (succ n)

add == (lambda (n*)
         (lambda (m)
           (lambda (f)
             (lambda (x)
               ((n* f) ((m f) x))
               )
             )
           )
         )

; Q.E.D.

----------------------------------------------------------------------
Shlomi Fish        [email-masked]
Home Page:         http://t2.technion.ac.il/~shlomif/

An apple a day will keep a doctor away. Two apples a day will keep two
doctors away.

	Falk Fish