Order of argument application in lambda calculus

Question

I encountered the following exercise in a textbook about logic:

$\lambda x \lambda Y(Y(x))(j)(M)$

It seems that the expected result from the textbook should be $M(j)$, since there were some type specifications on the variables. However, if I substitute $M$ for $x$, and $j$ for $Y$, then the result would become $j(M)$, which would be erroneous in terms of type.

I've seen elsewhere expressions such as:

(λa.λb.λs.λz. a s (b s z)) x y →
(λb.λs.λz. x s (b s z)) y →
λs.λz. x s (y s z)

which seems to have the same application order of arguments as the one desired by this exercise.

It actually seems to make sense if I think of function application in Haskell, but I still find it weird since I expect the rightmost argument to be substituted first for the leftmost lambda term.

Therefore, does the notation $\lambda x \lambda Y(Y(x))(j)(M)$ implicitly entail $\lambda x (\lambda Y(Y(x))(j)(M))$, which would yield the desired result? Is such implicit omission of brackets a normal convention in lambda calculus, and thus every such expression should be treated as such? Or did I misunderstand the order of argument application in lambda calculus after all?

Answer 1

It seems that your book uses the notation $$ \lambda x_1 \ldots \lambda x_n (M_1 \ldots M_k) $$ instead of the more commonly found (in my experience) $$ (\lambda x_1 \ldots \lambda x_n. M_1 \ldots M_k) $$ Both notations are used for logical quantifiers by different authors, so it's not completely surprising. E.g., compare $$ \exists x (P(x) \land Q(x)) \qquad {\rm vs} \qquad (\exists x. P(x) \land Q(x)) $$

In the second style, the scope of binders ($\lambda x$, $\exists x$) extends as far to the right as possible.

---

About application order: the notation of your book $$ \lambda x_1 \lambda x_2 \lambda x_3 (M) N_1 N_2 N_3 $$ stands for $$ (((\lambda x_1 (\lambda x_2 (\lambda x_3 (M)))) N_1) N_2) N_3 $$ It is correct that the outermost application is of $N_3$ but this does not get bound to $x_1$. To see where $M_3$ goes, one first needs to reduce the function $$ ((\lambda x_1 (\lambda x_2 (\lambda x_3 (M)))) N_1) N_2 $$ to a lambda, and this involves applying $N_2$ first. That will require applying $M_1$ first, in turn.

The net effect is that $N_i$ gets bound to $x_i$.

Since you mentioned the Haskell notation, it is basically the same thing, even if Haskell uses the other notation (binders extend to the right as possible).