I am building a lambda applicator in Java, and I have uncovered a bit of misunderstanding. Either my question at the bottom is what I am asking, or something in the build-up below is wrong. Either way, I'd appreciate any insight.

So, NOT can be defined as

λb.b (λxy.y) (λuv.u)

If we allow

A1 = λb.b
B1 = (λxy.y)
C1 = (λuv.u)

Now NOT is (A1 B1 C1)

By order of operations, B1 will be applied before C1 So let Not1 = (A1 B1)

NOT can now be rewritten as (Not1 B1) or ((A1 B1) C1).

When we apply the expression

TRUE = (λdw.d)

to NOT, we have

((A1 B1) C1) TRUE

Which, because A1 is the identity function, is supposed to get us

((TRUE B1) C1)

... but why wouldn't we apply B1 to A1 first?


1 Answer 1


I believe you are misunderstanding what $\lambda$-abstraction represents and are not considering its scope. First; your definition of $NOT$ is correct and $NOT$ is in normal form.

It is not true that $\lambda b. b\ (\lambda x y. y)\ (\lambda u v. u)$ is the same as $(A_1\ B_1\ C_1)$ and I give here two reasons why:

  1. The body of $\lambda$-abstraction goes as far right as possible (after ".", until its enclosing brackets, in our case none) and therefore $\lambda b. b\ (\lambda x y. y)\ (\lambda u v. u)$ is a $\lambda$-abstraction with variable $b$ and body $b\ (\lambda x y. y)\ (\lambda u v. u)$. The string "$\lambda b. b$" in this case is not representing an identity expression, but is a part of the definition of $\lambda$-abstraction. Its $\lambda$ "belongs" to the whole $NOT$ expression. Written fully parenthesised, your expression for $NOT$ would be $$\biggl(\lambda b. \Bigl(\bigl(b\ (\lambda x y. y)\bigr)\ (\lambda u v. u)\Bigr)\biggr)$$
  2. If it were in fact the same as $(A_1\ B_1\ C_1)$, this could reduce to $(B_1\ C_1)$ which could then reduce to $\lambda y. y$ which is identity (which is not $NOT$) and $\lambda$-expressions have at most one normal form.

The $NOT$ operator, when applied to some expression $X$ should reduce like this: $$\bigl(\lambda b. b\ (\lambda x y. y)\ (\lambda u v. u)\bigr)\ X \rightarrow_\beta X\ (\lambda x y. y)\ (\lambda u v. u)$$

You can try your ideas and check existing examples with pLam to help you build a similar tool by yourself. Good luck!

  • $\begingroup$ Thank you for the explanation! I'm having a little trouble squaring that with this document, in which <expression> := <name>|<function>|<application>, and "we adopt the convention that function application associates from the left, that is, the expression $E_1E_2E_3...E_n$ is evaluated applying the expressions as follows: $(...((E_1E_2)E_3)...E_n)$". Is my source document simply incorrect? $\endgroup$
    – Ben I.
    Jan 22, 2019 at 18:18
  • $\begingroup$ Oh, I see that they've hinted that every expression there is an application. They don't clearly discuss the interplay between functions and applications, however. $\endgroup$
    – Ben I.
    Jan 22, 2019 at 18:20
  • $\begingroup$ The document looks correct. You can see that application is left associative in my answer also, where I fully parenthesised the body of $NOT$. In the document, “function” and “name” are what I and most other resources call “abstraction” and “variable”. Every lambda expression is either variable, abstraction or application. Does this clear your confusion? $\endgroup$ Jan 22, 2019 at 18:36
  • $\begingroup$ @SandroLovnički Is it safe to say, then, that an abstraction on the left side will pull in every expression to the right if not blocked by parenthesis? So ${\lambda}x.x (y) z (a) b (c) d (e)$ will become ${\lambda}x.(x (y) z (a) b (c) d (e))$? $\endgroup$
    – Ben I.
    Jan 22, 2019 at 22:15
  • $\begingroup$ @BenI. Yes, exactly :) $\endgroup$ Jan 22, 2019 at 22:36

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.