A concrete definition of scope in lambda calculus that can be applied to determine which variables are bound and which are free

I would like to write a summary of scoping, free and bound variables, and substitution in lambda calculus. Ideally, I would first give a simple, easy to apply definition of scope and then go through a bunch of interesting examples that just apply the definition to determine which variables are free, which are bound, which are rebound, etc. Having built up some intuition, I would then introduce substitution[1].

So far I have the just a short introduction and want to put it out there to get thoughts on it. I would welcome any suggestions for improvement. E.g., if I am misusing terminology, I would like to know. What I have so far:

The expression $\lambda x. M$ is a lambda abstraction. It defines a variable $x$, a binding of $x$, a scope within which that binding applies, in this case term $M$, and within which $x$ is bound.

To give a concrete example, take the expression:

$$\lambda x.\lambda y.xyz$$

It defines two variables, $x$ and $y$, their corresponding binding, and their corresponding scope. More explicitly,

$$\lambda x.\overbrace{\lambda y.\underbrace{xyz}_{\text{scope of > }\lambda y}}^{\text{scope of }\lambda x}$$

Since $x$ appears within a scope of $\lambda x$, x is bound, that is, $x$ is a bound variable. Similarly, $y$ is a bound variable. Since $z$ does not appear within any scope of $\lambda z$ (in fact, there is no $\lambda z$), $z$ is not bound, that is, it is free, a free variable.

In particular, I have the following questions:

The expression $\lambda x. M$ is a lambda abstraction. It defines a variable $x$, a binding of $x$, a scope within which that binding applies, in this case term $M$, and within which $x$ is bound.

I try really hard to use terminology consistently. If there are two terminologies which are interchangeable, I prefer picking one and using it exclusively. And if two terminologies are similar, but different, I want to know how they differ, so that I don't use them interchangeably. I do these things to avoid confusing the reader (which might be myself in the future). In light of this, how do the terminologies "lambda expression" and "lambda term" differ? They are different, right?

It defines a variable 𝑥, a binding of 𝑥, a scope within which that binding applies, in this case 𝑀, and within which 𝑥 is bound.

I want to give a concrete definition of scope and binding as I think that would help ground any later discussion, but the above sounds confusing and perhaps not concrete enough. I have the notion that $\lambda x$ defines a new context or scope within which $x$ is bound, so I would like to convey that, but haven't found the right wording yet. It would also be useful for a definition to allow for the possibility of nested scopes, some of which may rebind outer scope variables. Ideally, a discussion of scope, would first give a simple, easy to apply definition of scope and then go through a bunch of interesting examples that just apply the definition to determine which variables are free, which are bound, which are rebound, etc. Here are two examples of nested scopes. The second example has a rebinding.

1. $\lambda x.x \lambda y. xy$ in which we have an outer $\lambda x$ scope and within that we have an inner $\lambda y$ scope (no rebinding)
2. $\lambda x.x \lambda x.x$ in which we have an outer $\lambda x$ scope and within that we have an inner $\lambda x$ scope (rebinding)

The definition of scope should also allow for the possibility that a variable may occur as bounded and free within the same expression as the following examples show:

• $x\lambda x.x$
• $(\lambda x.x)x$ (ofc, this one evaluates to the free variable $x$ if we perform $\beta$-reduction, but before $\beta$ we have a bounded $x$ and a free $x$.

And speaking of $(\lambda x.x)x$, what if instead we had $(\lambda x.x)M$ where $M$ is a term. Would we say $M$ is free? This doesn't make sense, right?

Rather than write a long response for all of your questions, I am going to suggest you look at the Barendregt book and also this short introduction by Barendregt and Barendsen. I think many of your notions are a little bit confused (just a little!), and it would be quicker for you to read the Barendregt thing to un-confuse them. For example, you use the phrase “defines a variable” but it's not clear what you mean by “define”; why does the term $𝜆𝑥.𝜆𝑦.𝑥𝑦𝑧$ “define” variables $x$ and $y$ but not $z$? And you say

Since $𝑧$ does not appear within any scope of $𝜆𝑧$, $𝑧$ is … a free variable

but this is misleading, since $z$ could be a free variable of a term in which it does appear bound: $z$ is free in the term $\lambda y.(z\ \lambda z.z)$ for example. You probably need to observe that while a particular name might appear in a term both free and bound, each occurrence of the name is one or the other.

Anyway the only point of yours I wanted to address specifically was

what if instead we had $(𝜆𝑥.𝑥)\ 𝑀$ where $𝑀$ is a term. Would we say $𝑀$ is free?

If you really meant what you said

$𝑀$ is a term. Would we say $𝑀$ is free?

then the answer is “you can't ask if terms are free, you can only ask if variables are free, and only in the context of a particular term.” But I think what you meant to ask is

The letter $𝑀$ stands for a term. Would we say that the variable $𝑀$ is free?

If this is what you meant, you are confusing two kinds of things. The lambda-calculus defines a family of “terms”, which are sequences of symbols. The symbols include parentheses, dots, spaces, $\mathtt{\lambda}$, and also some “variable” symbols which we typically take to be $\mathtt x, \mathtt y, \mathtt z$, and so on. The symbols do not include $M$. Here $M$ is not part of the syntax of the lambda-calculus. It's what we call metalanguage, part of the language, along with English, that we are using to talk about the lambda-calculus. When we say something like

Consider the lambda-term $(\lambda\mathtt{x}.\mathtt x)\ M$…

this is a shorthand. What we really mean is

Suppose $M$ represents some lambda-term. Now consider the lambda term formed by concatenating the term $(\lambda\mathtt{x}.\mathtt x)$ with the term represented by $M$.

The letter “M” is not part of the language of lambda-calculus, so it does not make sense to ask if it is free or bound.

Sorry if all this is excessively abstruse. These kinds of object-lanaguge metalanguage issues are hard to talk about clearly.