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?
Order of argument application in lambda calculus
lambda calculus
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).