1
$\begingroup$

In Wikipedia I found out that the formal grammar of $\lambda$-calculus is the following:

<λexp> ::= <var>
  | λ<var> . <λexp>
  | ( <λexp> <λexp> )

Then, a few lines later they say that this is a valid $\lambda$-expression:

$$\lambda x.x^{2}+2$$

How does one matches with the other? Where is the "+" operator in the formal grammar? Where is the integer 2?

Improve this question
$\endgroup$
5
  • $\begingroup$ The definition you are giving is of "pure" lambda calculus, but we can add constants like $2, +$ and infix and postfix notation for convenience, and call it "applied" lambda calculus. $\endgroup$
    – Natalie Clarius
    Commented Jan 26, 2023 at 14:18
  • $\begingroup$ How far I can do in making the text after the dot "convenient"? And another question: what's the point of calling the grammar "formal" if we go around the formality? $\endgroup$
    – yegor256
    Commented Jan 26, 2023 at 15:13
  • $\begingroup$ As far as you can still formalize it if you want to. You can define the syntactic transformation from e.g. $+(a,b)$ to $a + b$ pretty straightforwardly. The point is to make the system more usable for real-life applications while knowing that you can do it formally and prove a lot of interesting things about that formal system that is behind your syntactic sugar if you need to. $\endgroup$
    – Natalie Clarius
    Commented Jan 26, 2023 at 16:06
  • $\begingroup$ @lemontree: $a+b$ is syntactic sugar for $((+ a) b)$. The transformation is still straightforward. $\endgroup$
    – rici
    Commented Jan 26, 2023 at 16:35
  • $\begingroup$ Right, $+(a,b)$ is syntactic sugar in itself. Thanks for pointing it out. $\endgroup$
    – Natalie Clarius
    Commented Jan 26, 2023 at 19:33

1 Answer 1

Reset to default
1
$\begingroup$

From the Wikipedia article:

An abstraction $\lambda x.t$ denotes an anonymous function that takes a single input $x$ and returns $t$. For example, $\lambda x.x^{2}+2$ is an abstraction for the function $f(x)=x^{2}+2$ using the term $x^{2}+2$ for $t$.

It doesn't claim $\lambda x. x^2 + 2$ is a $\lambda$-expression. Rather, it is an example of a general concept of abstraction.

In other words, a syntax rule for a lambda expression λ<var> . <λexp> is an abstraction, but not every abstraction is a lambda expression.

Similarly, application is a syntax rule for a lambda expression but this concept is used for other formalities, such as combinatorial calculus.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Long story short, without arithmetic operators and numbers, lambda calculus is just a funny collection of good looking letters :) $\endgroup$
    – yegor256
    Commented Feb 23, 2023 at 8:02

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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