Any notions of operations in basic postulates of lambda calculus

Question

I am learning Lambda Calculus from the book by Hindley and Seldin . They start the formal postulation of lambda calculus as follow :

(a) all variables and atomic constants are λ-terms (called atoms);

(b) if M and N are any λ-terms, then (MN) is a λ-term (called an application);

(c) if M is any λ-term and x is any variable, then (λx.M) is aλ-term (called an abstraction).

In the second postulate $MN$ has been termed as a $\lambda$ term . How to define $MN$ , what does it mean ? Is it an operation? Is there any scope of defining operations in lambda calculus which are associative and/or distributive ?

Answer 1

You can think of application $MN$ as an algebraic operation, where the operator has been elided for convenience. Instead of $MN$ some people write $M @ N$, or even $$ apply(M, N) $$ So $apply(\cdot, \cdot)$ is a binary operation, and, as @chi points out, $apply(\cdot, \cdot)$ is is neither associative nor commutative. The precise nature of what $apply(\cdot, \cdot)$ does depends on exactly what $\lambda$-calculus you have in mind.

Answer 2

The application $MN$ is just syntax. On its own it does not mean anything.

There is, however, an intuition behind its semantics: $M$ is to be regarded as a function, and $N$ as its argument. Evaluating an application $MN$ simply corresponds to evaluating function $M$ at point $N$. This is formally defined through the $\beta$ reduction law.

Note that application is not associative or commutative. $MN$ is in general different from $NM$, and $MNO$ is an alternative notation for $(MN)O$, which is different from $M(NO)$.

This is not terribly different from any other programming language. Think about f(x) and x(f), or f(x)(y) and f(x(y)) in JavaScript, for instance.