patternMinor
Understanding a boolean expression in λ-calculus
Viewed 0 times
expressionunderstandingbooleancalculus
Problem
(NOTE: This is not a homework question at at all. Rather, this was something that I thought that I understood (at least on the surface), but now appear to have no clue about, and am not currently finding any resources helpful. I know that we typically like to see what people have tried, but I am honestly discombobulated enough at this moment that I am truly unsure about where to even begin. If this turns out to be a duplicate that I haven't found, I would also be perfectly happy. I just want to understand.)
Anyway, on to the question itself:
So, if $\lambda xy.x$ represents true, and $\lambda xy.y$ represents false, then I have been told that $(\lambda b.b \ \ \lambda xy.y \ \ \lambda xy.x)$ is a
$(\lambda b.b \ \ \lambda xy.y \ \ \lambda xy.x) \ \lambda xy.x$ results in $\lambda xy.y$,
and the expression
$(\lambda b.b \ \ \lambda xy.y \ \ \lambda xy.x) \ \lambda xy.x$ results in $\lambda xy.x$.
Where I am stuck is that I don't see how to apply $\beta$-reductions here. There are three expressions inside the parenthesis. How is one of them chosen by applying the outer expression?
Anyway, on to the question itself:
So, if $\lambda xy.x$ represents true, and $\lambda xy.y$ represents false, then I have been told that $(\lambda b.b \ \ \lambda xy.y \ \ \lambda xy.x)$ is a
not function, because the expression $(\lambda b.b \ \ \lambda xy.y \ \ \lambda xy.x) \ \lambda xy.x$ results in $\lambda xy.y$,
and the expression
$(\lambda b.b \ \ \lambda xy.y \ \ \lambda xy.x) \ \lambda xy.x$ results in $\lambda xy.x$.
Where I am stuck is that I don't see how to apply $\beta$-reductions here. There are three expressions inside the parenthesis. How is one of them chosen by applying the outer expression?
Solution
It's a very bad idea to omit parentheses. Correct is:
$$\lambda b . b (\lambda x y . y) (\lambda x y . x)$$
Next, it is confusing to reuse bound variables, so let me rename them:
$$\lambda b . b (\lambda x y . y) (\lambda u v . u)$$
And now we can apply this to $\lambda p q . p$ (which is just "true" with bound vraiables renamed yet again):
\begin{align*}
(\lambda b . b (\lambda x y . y) (\lambda u v . u)) (\lambda p q . p)
&=_\beta (\lambda p q . p) (\lambda x y . y) (\lambda u v . u) \\
&=_\beta (\lambda q . (\lambda x y . y)) (\lambda u v . u) \\
&=_\beta (\lambda x y . y).
\end{align*}
So we did get false. In every step there was exactly one $\beta$-redex. By the way, writing $A B C$ in $\lambda$-calculus means $(A B) C$ by convention.
I will leave the other one as exercise.
$$\lambda b . b (\lambda x y . y) (\lambda x y . x)$$
Next, it is confusing to reuse bound variables, so let me rename them:
$$\lambda b . b (\lambda x y . y) (\lambda u v . u)$$
And now we can apply this to $\lambda p q . p$ (which is just "true" with bound vraiables renamed yet again):
\begin{align*}
(\lambda b . b (\lambda x y . y) (\lambda u v . u)) (\lambda p q . p)
&=_\beta (\lambda p q . p) (\lambda x y . y) (\lambda u v . u) \\
&=_\beta (\lambda q . (\lambda x y . y)) (\lambda u v . u) \\
&=_\beta (\lambda x y . y).
\end{align*}
So we did get false. In every step there was exactly one $\beta$-redex. By the way, writing $A B C$ in $\lambda$-calculus means $(A B) C$ by convention.
I will leave the other one as exercise.
Context
StackExchange Computer Science Q#84989, answer score: 4
Revisions (0)
No revisions yet.