Lambda calculus: How to define a function that simulates $\neg p\vee q$?

313 Views Asked by At

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?

1

There are 1 best solutions below

1
On BEST ANSWER

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$