From: Jesse
Subject: Correction of [Summary of Church Numeral]
Date: Sat, 15 Aug 1992 09:33:56 +0000
Message-ID: <cyen.713871236@ponder>

Days ago I said when m=zero the mult and expt functions will go wrong.
Maybe because of the evaluation order of ML , these functions cannot be
tested right.

The lambda expression of these two functions are absolutely right.

mult=\m.\n.\f.\x. m (n f) x
expt=\m.\n.\f.\x. m n f x

Besides the substraction function of two Church Numerals is:

sub=\m.\n.n pre m

whereas pre=\n.\f.\x.snd (n (prefn f) (pair x x))
        prefn=\f.\p.pair (f (fst p))(fst p)
        pair=\x.\y.\f.f x y
        fst=\p.p true
        snd=\p.p false
        true=\x.\y.x
        false=\x.\y.y

Sorry for the mistake I made in the last post, please post if you know
any interesting stuff on Church Numeral.

Jesse