2
$\begingroup$

How do you prove $\mathsf{xor} \, \mathsf{True}\, \mathsf{True}$ is false in lambda calculus using call-by-value reduction.

This is the approach I tried but it is not working:

$$\mathsf{xor} \equiv \lambda xy.x(y F T) y$$

$$\mathsf{xor} \, T T \equiv (\lambda xy.x(y F T)y) T T$$

$$\mathsf{xor}\, T T \equiv (\lambda xy.x(y (\lambda x y.y) (\lambda x y.x))y) T T$$

Then by beta reduction of leftmost inner

$$\mathsf{xor}\, T T \equiv (\lambda xy.x(y (\lambda y.y) )y) T T$$

But I feel there is a mistake somewhere as the steps above did not lead me to the expected answer.

$\endgroup$
1
  • 1
    $\begingroup$ this question most likely belongs in the computer science theory forum, where you will most likely get more traction on it anyway. $\endgroup$ Commented Mar 19, 2022 at 23:31

1 Answer 1

Reset to default
2
$\begingroup$

You are mistaken. The subterm $yFT$ does not contain any $\beta$-redex. Indeed, every term of the form $MNL$ must be read as $(MN)L$, and not as $M(NL)$ (technically, the application is said to be left-associative). This means that $yFT = (yF)T = (y (\lambda xy.y))\lambda xy.x$ and so there is no $\beta$-redex to fire.

Therefore, in the term $\mathsf{xor}\, T T = (\lambda xy.x(y (\lambda x y.y) (\lambda x y.x))y) T T$ there is only one $\beta$-redex, made up of the subterm from the first occurrence of $\lambda x$ to the first occurrence of $T$. You can easily see that the leftmost-innermost reduction from $\mathsf{xor}\, T T $ yields $F$, as expected.

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