# Any notions of operations in basic postulates of lambda calculus

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 ?

• I'm not sure I understand the last sentence. – Martin Berger Feb 20 '17 at 13:34

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.
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.
• @AgniveshSingh No, abstraction constructs a function, application uses it. E.g. $\lambda x. x x$ is an abstraction, if you apply it to $M$ you get $(\lambda x. x x) M$ which according to the beta rule reduces to $MM$. – chi Feb 27 '17 at 22:32