Understanding a boolean expression in λ-calculus

(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 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?

• You have a typo in the last pair of expressions. Is there some reason you aren't parenthesizing the sub-expressions? Using usual conventions makes your expressions mean something that is very likely not what you meant which means what you actually mean is at least ambiguous. For the purposes of this problem, I would suggest fully parenthesizing the expressions to avoid notational ambiguity (even just for yourself). It's also possible that this will reveal part of the issue that is causing you a problem. – Derek Elkins Dec 5 '17 at 22:01
• You should use parentheses. – Andrej Bauer Dec 5 '17 at 22:01

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.
• Thinking about it now, why wouldn't you apply $\lambda x y . y$ to $\lambda b . b$ before applying $\lambda p q . p$? Don't we typically deal with what is inside of the parenthesis before taking other actions? – Ben I. Dec 23 '17 at 20:12
• An expression of the form $\lambda b . b C$ means $\lambda b . (b C)$ and not $(\lambda b . b) C$. You are misreading the syntax. In general, $\lambda$ always binds as much as it can. For instance, $\lambda x . x y z$ is the same as $\lambda x . ((x y) z))$, and not $((\lambda x . x) y) z$. – Andrej Bauer Dec 23 '17 at 21:25
• And another thing. In the expression $A \, B$ we say that "$A$ is applied to $B$", whereas you seem to be talking backwards, saying that "$B$ is applied to $A$". – Andrej Bauer Dec 23 '17 at 21:26