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 Answer 1

Reset to default
3
$\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$

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.