# What does all uppercase letters mean?

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?

• 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. Jan 31 '19 at 16:00
• So x is a part of M and N? Please explain with an example. I am absolute beginner Jan 31 '19 at 16:01
• 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. Jan 31 '19 at 16:27
• 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. Jan 31 '19 at 16:30
• Yep absolutely. M can be anything built up from the operators variables application and abstraction. Jan 31 '19 at 20:52

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})))$$