1
$\begingroup$

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 ?

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

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.

$\endgroup$
3
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Evaluating the value of a function at a given point , we do it in an abstraction right ? So , in essence , as per your answers , application and abstraction perform the same thing ? $\endgroup$ – Agnivesh Singh Feb 27 '17 at 22:15
  • $\begingroup$ @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$. $\endgroup$ – chi Feb 27 '17 at 22:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.