evaluate lambda calculus- OR FALSE TRUE

Question

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)

Answer 1

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.