0
$\begingroup$

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.

$\endgroup$
1
$\begingroup$

$\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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.