1
$\begingroup$

I am trying to learn lambda calculus, and I am currently tackling a few boolean logic questions. I have gotten to one that I am stuck on, and I am looking for a little help proceding. I need to prove that:

or false (not true)

evaluates to false, using lazy evaluation. I am given the following, where '\' is a lambda:

or = \v.\w.(v w v)
false = \x.\y.(y)
not = \v.\w.\x.(v x w)
true = \x.\y.(x)

So far I have gotten:

or false (not true)
= \v.\w.(v w v) false (not true)
= \w.((false(not true)) (false(not true)) w)

From here I am lost, I think my next step should be along the lines of:

\w.((\a.\b.(b)(not true)) false(not true) w)

But I feel like it is completely wrong. Is anyone able to help out? What would be the next step. How do I go about solving this problem? Since it is lazy evaluation, should I have done something more like:

\w.(false(false(not true) true w))

The above seems certainly wrong.

Please help

Thanks,

cjd

$\endgroup$
1
$\begingroup$

So I was going horribly wrong even from the beginning. I have finally figured this out. Here is the solution.

or false (not true)
= \v.\w.(v v w) false (not true)
= \.w(false false w) (not true)
= false false (not true)
= \x.\y.(y) false (not true)
= \y.(y) (not true)
= (not true)
= \v.\w.\x.(v x w) true
= \w.\x.(true x w)
= \w.\x.(\a.\b.(a) x w)
= \w.\x.(\b.(x) w)
= \w.\x.(x)
= false
or is the same as \x.\y.(y) which is equal to false.
$\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.