# Lambda calculus: Simplifying booleans with beta reductions

I have been doing a homework assignment wherein I have been trying to determine the result of ((or true) false) using beta reduction. I began by writing the entire expression using lambda notation and performed the following steps:

((λx.λy.((x (λa.λb.a)) y) (λa.λb.a)) (λa.λb.b))
((λx.(x (λa.λb.a)) (λa.λb.a) ) (λa.λb.b))
(((λa.λb.a) (λa.λb.a))) (λa.λb.b))
((true true) false)


I don't understand how to go about simplifying this further, however. Can someone explain whether this is the final result, or what further steps I can take? I'm just learning lambda calculus, and haven't quite gotten a feel for it yet.

$\def\OR{\mathtt{OR\ }}\def\IF{\mathtt{IF\ }}\def\TRUE{\mathtt{TRUE\ }}\def\FALSE{\mathtt{FALSE\ }}$ I think it's easiest to leave values unexpanded as long as possible, until you need to reduce them. So while you can write $\OR$ as $(\lambda a b . (a (\lambda x y. x) b))$ it's easier to leave it as $\lambda a b.(a\ \TRUE b)$ until the moment that you have to apply that middle $\TRUE$ to an argument.
Then to calculate $\OR\TRUE\FALSE$ we would proceed like this:
\begin{align} \OR\TRUE\FALSE & \Rightarrow (\lambda a b.(a\ \TRUE b)) \TRUE\FALSE &\text{(replacing \OR with its definition)}\\ & \Rightarrow (\lambda b.(\TRUE\TRUE b))\FALSE\\& \Rightarrow \TRUE\TRUE\FALSE \\ & \Rightarrow (\lambda a b.a)\TRUE\FALSE &(\star) \ \text{(replacing \TRUE with its definition)}\\ & \Rightarrow (\lambda b.\TRUE)\ \FALSE \\ & \Rightarrow\TRUE \end{align}
This is a lot simpler than writing a dozen $(\lambda ab.b)$s everywhere.
In particular, notice that your next-to-last line, $(((λa.λb.a) (λa.λb.a))) (λa.λb.b))$, is equal to the line above that I marked with a $(\star)$, and that further reductions are possible at that point.