3
$\begingroup$

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

Improve this question
$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$
    – Derek Elkins left SE
    Commented Dec 5, 2017 at 22:01
  • $\begingroup$ You should use parentheses. $\endgroup$
    – Andrej Bauer
    Commented Dec 5, 2017 at 22:01

1 Answer 1

Reset to default
4
$\begingroup$

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.

Improve this answer
$\endgroup$
3
  • $\begingroup$ 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? $\endgroup$
    – Ben I.
    Commented Dec 23, 2017 at 20:12
  • $\begingroup$ 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$. $\endgroup$
    – Andrej Bauer
    Commented Dec 23, 2017 at 21:25
  • $\begingroup$ 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$". $\endgroup$
    – Andrej Bauer
    Commented Dec 23, 2017 at 21:26

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.