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.
Indeed $\text{OR} \ \text{FALSE} \ \text{TRUE}$ $\beta$-reduces to $\text{TRUE}$, as expected. Let us see that in a step-by-step $\beta$-reduction.
\begin{align} \text{OR} \ \text{FALSE} \ \text{TRUE} &= (\lambda xy. \text{IF} \ x \ \text{TRUE} \ y) \ \text{FALSE} \ \text{TRUE} \\ &\to_\beta (\lambda y. \text{IF} \ \text{FALSE} \ \text{TRUE} \ y) \ \text{TRUE} \\ &\to_\beta \text{IF} \ \text{FALSE} \ \text{TRUE} \ \text{TRUE} \\ &= (\lambda btf. \, b\,t\,f) \ \text{FALSE} \ \text{TRUE} \ \text{TRUE} \\ &\to_\beta (\lambda tf. \text{FALSE} \ t\,f) \ \text{TRUE} \ \text{TRUE} \\ &\to_\beta (\lambda f. \text{FALSE} \ \text{TRUE} \ f) \ \text{TRUE} \\ &\to_\beta \text{FALSE} \ \text{TRUE} \ \text{TRUE} \\ &= (\lambda x y. y) \ \text{TRUE} \ \text{TRUE} \\ &\to_\beta (\lambda y. y) \ \text{TRUE} \\ &\to_\beta \text{TRUE} \end{align}
Your error in the first reduction you wrote is in the following step: \begin{equation} (\lambda xy. x (\lambda xy.x) y) (\lambda xy.y) (\lambda xy.x) \to_\beta (\lambda xy. x x) (\lambda xy.y) (\lambda xy.x) \end{equation} which is not correct. Indeed, you cannot reduce $(\lambda xy.x) y$ within $\lambda xy. x (\lambda xy.x) y$ because, as you said, application is left-associative, hence $\lambda xy. x (\lambda xy.x) y = \lambda xy. (x (\lambda xy.x)) y$. The correct step is: \begin{align} (\lambda xy. x (\lambda xy.x) y) (\lambda xy.y) (\lambda xy.x) &\to_\beta (\lambda y. (\lambda xy.y) (\lambda xy.x) y) (\lambda xy.x) \to_\beta \dots \end{align}