CODEWITHSUNDEEP
lambda-calculus
llamaro25
llamaro25

Reputation: 692

evaluate lambda calculus- OR FALSE TRUE

TRUE = λxy. x

FALSE = λxy. y

IF = λbtf. b t f

AND = λxy. IF x y FALSE

OR = λxy. IF x TRUE y

NOT = λx. IF x FALSE TRUE

How can I use lambda calculus to beta reduce the expression OR FALSE TRUE? I'm not sure where to start. My lecturer did not go through it. Here's my attempt

(\xy.IF x TRUE y)(\xy.y)(\xy.x)
= (\xy.IF x TRUE y)[x := (\xy.y))(\xy.x)
= (\y. IF (\xy.y) TRUE y)(\xy.x)
= (IF (\xy.y) TRUE y)[y := (\xy.x))
= IF (\xy.y) TRUE (\xy.x)

Upvotes: 0

Views: 527

Answers (1)

Théo Winterhalter
Théo Winterhalter

Reputation: 5108

When you are working with Church-encodings I think it is best to stay as abstract as possible, i.e., you should not unfold TRUE, FALSE, IF and NOT eagerly but only when needed.

Instead you first want to prove basic results about their behaviour, this will also make for a sanity check. For IF you want to check that IF TRUE t f = t and IF FALSE t f = f.

IF TRUE t f = TRUE t f   (IF returns its arguments directly)
            = t          (TRUE returns its first argument)

Same for IF FALSE.

Now

OR FALSE TRUE = IF FALSE TRUE TRUE

and by applying the identity you already proved you should be able to conclude.

Upvotes: 1

Related Questions