# lambda expressions, parenthesis, and order of application

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?

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!

• 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? – Ben I. Jan 22 at 18:18
• 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. – Ben I. Jan 22 at 18:20
• 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? – Sandro Lovnički Jan 22 at 18:36
• @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))$? – Ben I. Jan 22 at 22:15
• @BenI. Yes, exactly :) – Sandro Lovnički Jan 22 at 22:36