In lambda calculus, application is left associative. That is, if M, N, and P are expressions, then we parse MNP1 as (MN)P. But if we want the "alternative" parsing, we can get it using parentheses/grouping: M(NP).
Conversely, abstraction is right associative. That is, if x and y are variables, then we parse λx.λy.M2 as λx.(λy.M). Is there an "alternative" parsing to λx.λy.M? Does (λx.λy).M makes sense? If not, can you give an example of a valid "alternative" parsing of chained abstractions where parenthesis would have to be used to the get the "alternative" parsing?
1 My understanding is that when we see two expressions next to each other as in MN there is an implied application operator between them which says "apply M to N" or more verbosely "feed N as input to M". Is this correct? If so, a phrase like "M something N" is desirable so we can read lambda expressions left to right. Maybe "M consumes N"?
2 In this case it looks like the dot (.) is acting as the abstraction operator. Is there a way to verbalize λx.M left to right? Something like "function (λ) taking x outputing (.) M"?
Best Answer
No. A term in the lambda calculus is either:
So concretely, a term is represented by a tree where leaves are always variables, binary nodes are applications, and unary nodes (indexed by an identifier) are lambda abstractions. For example: $$\texttt{Lam}(x,\texttt{Lam}(y,M))$$ where $M$ may depend on $x,y$, or $$\texttt{Lam}(y,\texttt{App}(\texttt{Lam}(x,\texttt{Var}(x)),\texttt{Var}(y))).$$
This means that $\lambda x. t$ is just a way of writing $\texttt{Lam}(x,t)$, and the dot has no semantic value.
But now let's consider an alternative way of representing terms. A term is now either:
The key difference now is that a lambda abstraction is given by a lambda abstraction $ x\mapsto M$ in the meta-language, so we might as well write $x . M$ and the examples above are now:
$$\texttt{Lam}(x . \texttt{Lam}(y . M))$$ and $$\texttt{Lam}(y.\texttt{App}(\texttt{Lam}(x . \texttt{Var}(x)), \texttt{Var}(y))).$$ So now, $\lambda x . t$ could be parsed $\lambda (x . t)$, where $x . t$ is a function $x \mapsto t$ in the meta language.
Furthermore, if $f$ is a function producing a term, it would also be valid to write $\lambda f$, which in turn is equivalent to $\lambda (x\mapsto (f x))$, which we may write $\lambda(x.(f x))$ or $\lambda x. (f x)$.