0
$\begingroup$

The encoding of booleans in pure lambda calculus:

true := λx.λy.x

false := λx.λy.y

cond := λb.λx.λy.b x y

So if "cond" re-defined as cond := λx.x and assume "true" and "false" are keep same as before, does this result in a valid encoding of booleans?

$\endgroup$

1 Answer 1

1
$\begingroup$

Yes, you are correct. The two definitions of cond are extensionally equal. But using the short version would make the definition even more mysterious, and it is very mysterious already.

You could also use $\lambda xy.xy$ or $\lambda abcd.abcd$ and it would work the same.

Some presentations omit cond completely and just say that the boolean value is itself the test.

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