1
$\begingroup$

I am reading https://www.irif.fr/~mellies/mpri/mpri-ens/biblio/Selinger-Lambda-Calculus-Notes.pdf and would like to know, what the following statement means:

Lambda terms: M,N ::= x | (M N) | (λx.M).

It is from page 11.

What does for example mean? Is x a type of M and N?

Improve this question
$\endgroup$
6
  • $\begingroup$ They are metavariables (variables in the language of math). They stand for arbitrary lambda terms. This is distinct from x which is an object variable and part of the syntax of the language we're defining. $\endgroup$
    – daniel gratzer
    Commented Jan 31, 2019 at 16:00
  • $\begingroup$ So x is a part of M and N? Please explain with an example. I am absolute beginner $\endgroup$
    – zero_coding
    Commented Jan 31, 2019 at 16:01
  • 1
    $\begingroup$ M stands for a chunk of syntax. Any chunk of syntax that we can build up with these operators. x is a particular piece of syntax so M could stand for x certainly. It could stand for (x x) x as well. Or \x. x x. $\endgroup$
    – daniel gratzer
    Commented Jan 31, 2019 at 16:27
  • 1
    $\begingroup$ The important thing is that x is the syntax for variables in the language we're defining. M is a variable that ranges over a piece of syntax. $\endgroup$
    – daniel gratzer
    Commented Jan 31, 2019 at 16:30
  • 1
    $\begingroup$ Yep absolutely. M can be anything built up from the operators variables application and abstraction. $\endgroup$
    – daniel gratzer
    Commented Jan 31, 2019 at 20:52

1 Answer 1

Reset to default
5
$\begingroup$

As it's explained in the comments, $M$ and $N$ are know as metavariables. More importantly, this kind of definition is known as an inductive definition, that is, you start with very basic elements (symbols belonging to the set $\mathcal{V}$) and build up more complex things from there.

For instance, let $\mathcal{V} = \{v_0, v_1, \ldots, v_{1001}, \ldots\}$. In the BNF definition:

$$ M,N ::= x \mid (M N) \mid (\lambda x.M) $$

  • $x$ can be any of the $\{v_0, v_1, v_2, \ldots \}$. That means any symbol from $\mathcal{V}$ can be considered a $\lambda$-term, a most basic of rules.
  • $M$, $N$ are structures already known to be $\lambda$-terms, so from the previous example we can build expressions like $(v_0 ~ v_1)$, $(v_{100} ~ (v_{0} ~ v_{1}))$, $((v_{100} ~ (v_{0} ~ v_{1})) ~ v_2) $ and so on.
  • With the previous two rules you can now build more complex expressions like $(\lambda v_{100}. (v_0 ~ v_1))$, since all previous terms made by combining the two previous rules are known to be $\lambda$-terms.
  • Now you can mix all three rules, like in $(v_0 ~ (\lambda v_9.(v_9 ~ v_{999})))$
Improve this answer
$\endgroup$

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.