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?