1
$\begingroup$

how to define lambda calculus encoding for boolean implication(⇒). (Recall that in boolean logic, x ⇒ y iff ¬x ∨ y.) You may use true, false and cond by name in your definitions if you want.

true := λx. λy. x

false := λx. λy. y

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

I currently have got "not" := λx.x false true "or" := λx.λy.x true y What should I do next ?

$\endgroup$
  • $\begingroup$ Comments are not for extended discussion; this conversation has been moved to chat. $\endgroup$ – Aloizio Macedo Nov 23 '18 at 19:28
1
$\begingroup$

Let me go through how you might come up with the formula for or, and then let you do something similar for impl.

The key observation here is: if $x$ is true, then $x \vee y$ is always true. Whereas if $x$ is false, then $x \vee y$ is equal to $y$. Therefore, $x \vee y = cond ~ x ~ true ~ y.$ In other words, $$\vee = \lambda x . \lambda y . (\mathbf{if}~ x~ \mathbf{then}~ true ~ \mathbf{else}~ y) = \lambda x . \lambda y . cond ~ x ~ true ~ y = \lambda x . \lambda y . x ~ true ~ y.$$ (And if you like, you can then make this a bit shorter using the $\eta$ rule: it is equivalent to $\lambda x . x ~ true$.)

Now, for impl, we can start off with a similar analysis: if $x$ is true, then $x \rightarrow y$ is equal to $y$; whereas if $x$ is false, then $x \rightarrow y$ is always true. I'll leave it to you to take the construction of impl as a lambda expression from here.

$\endgroup$
  • $\begingroup$ Thanks, I have figured that out. $\endgroup$ – Student Feb 15 '18 at 1:06

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.