0
$\begingroup$

I am making my first steps in lambda calculus, so please bear with me.
I want to create a lambda function, that given two boolean expressions (either $F$ or $T$ - defined below), simulates the formula $\neg p\vee q$ where the $p$ is its first argument and $q$ is the second.

Here is my attempt and how it fails:
The definitions are:
$T=\lambda xy.x$
$F=\lambda xy.y$
$\bigvee_{or}=\lambda xy.xTy$
$\neg_{negaion}=\lambda x.xFT$

Considering the above definitions, I tried:

$$\overbrace{\lambda st. \underbrace{(\lambda x.xFT)s}_\text{negates first arg}Tt}^{\text{represents }\neg p\vee q}$$

using $\beta$ reductions, I get:

$\lambda st.(\lambda x.xFT)sTt=_{\beta}\lambda st.sFTTt=_{\beta}\lambda st.sTt$

The problem is, as you probably notice - I get the logical $\bigvee_{or}$ again... which obviously does not produce the truth table I want.
What am I doing wrong?

$\endgroup$
1
$\begingroup$

Your erros is that

$$f = \lambda st.\ sFTTt=\lambda st.\ (((sF)T)T)t\neq_{\beta}\lambda st.\ sTt$$

hence

$$f\ T =_\beta \lambda t.\ FTt =_\beta \lambda t.\ t$$

and

$$f\ F =_\beta \lambda t.\ TTt =_\beta \lambda t.\ T$$

I hope this helps $\ddot\smile$

$\endgroup$
  • $\begingroup$ Ohh! Is that because function application is left associative? $\endgroup$ – so.very.tired Dec 5 '14 at 22:39

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.