I'm given the following where:
TRUE = λxy.x FALSE = λxy.y IF = λbtf. b t f OR = λxy. IF x TRUE y
and I'm trying to evaluate:
OR FALSE TRUE
using Beta reduction. Since beta reduction is left associative, i started from the left but I'm having difficulties with the OR where there contains IF and TRUE inside it's expression. So i tried:
OR FALSE TRUE (λxy. IF x TRUE y) (λxy.y) (λxy.x) (λxy. (λbtf. b t f) x (λxy.x) y) (λxy.y) (λxy.x) #i substituted btf with x here but I'm not fully sure if it's valid (λxy. x (λxy.x) y) (λxy.y) (λxy.x) (λxy. x x) (λxy.y) (λxy.x) (λxy.y) (λxy.y) (λxy.x) (y) (λxy.x)
But I'm pretty sure I messed up somewhere along way as evaluating the OR was confusing enough. I'm not certain if I beta reduced correctly so I would appreciate some help on this.
I gave it another go so here's what I did:
OR FALSE TRUE (λxy. IF x TRUE y) FALSE TRUE IF FALSE TRUE FALSE TRUE (λbtf. btf) FALSE TRUE FALSE TRUE FALSE TRUE FALSE TRUE (λxy.y) TRUE FALSE TRUE (λx.TRUE) FALSE TRUE TRUE TRUE (λxy.x) TRUE λy.TRUE
Again I'm still uncertain if it's correct this way too. Some help needed.