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.
- $\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)
- $\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?
