the natural numbers using lambda calculus

On Wednesday, November 2, 2011, Jim Snavely wrote:

Ok, this paper sort of blew my mind a little. I knew a little about
lambda calculus before this...but not really, I realized.

As usual, the only way I understand anything is by writing working
code. The following is the logical operations section translated into
Haskell. (note the backslash is Haskell syntax for a lambda
_expression_)

true = \x y -> x
false = \x y -> y

toBool f = f 1 2 == 1

land = \x y -> x y (\u v -> v)
lor = \x y -> x (\u v -> u) y

lnegate = \x -> x (\u v -> v) (\a b -> a)

main = print $ toBool $ lnegate false

or try:

main = print $ toBool $ true `land` false

contrast with:

main = print $ toBool $ true `lor` false

--Jim

On Wed, Nov 2, 2011 at 12:15 AM, Dan Mead <d.w.mead@gmail.com> wrote:
> the other longer paper gives alot of good definitions that this one kind of
> just skips over. I'll bring printouts.
>
> Dan
>
> On Tue, Nov 1, 2011 at 2:42 PM, Lalish-Menagh, Trevor <trev@trevmex.com>
> wrote:
>>
>> Hi all,
>>
>> Don't forget that tomorrow night at 6:30pm is Functional Fall 5 at the
>> Comcast Center (Room 45P). We will be
>> reading "A Tutorial Introduction to the Lambda Calculus."
>> (http://www.utdallas.edu/~gupta/courses/apl/lambda.pdf)
>>
>> As always there will be pizza and cola provided, and beer afterwards.
>>
>> Don't forget to RSVP at http://www.doodle.com/dvd85t6iw8hs8vqp
>>
>> I hope to see you there!
>>
>> Yours,
>> Trevor
>> --
>> Trevor Lalish-Menagh
>> trev@trevmex.com
>> 484.868.6150 (mobile)
>> trevmex (AIM)
>
>

--
--Jim

data Natural = Nat Natural | Zero deriving Show suc = \n -> Nat n prd (Nat n) = n one = suc Zero add :: Natural -> Natural -> Natural add a Zero = a add a b = add (suc a) (prd b) natToInt Zero = 0 natToInt (Nat n) = 1 + natToInt n two = add one one three = add one two main = print $ natToInt $ add two three