# Lambda Calculus inductive substitution definition

I'm reading Lambda-Calculus and Combinators: An Introduction, and there's the following definition of $$\lambda$$-substitution:

• $$FV(P)$$ stands for the set containing all free-variables from $$P$$.

Definition 1.12 (Substitution) For any $$M, N, x$$, define $$[N/x]M$$ to be the result of substituting $$N$$ for every free occurrence of $$x$$ in $$M$$, and changing bound variables to avoid clashes. The precise definition is by induction on $$M$$, as follows (after [CF58, p.94]).

(a) $$[N/x]x \equiv N$$

(b) $$[N/x]a \equiv a$$ for all atoms $$a \not \equiv x$$

(c) $$[N/x](PQ) \equiv ([N/x]P)([N/x]Q)$$

(d) $$[N/x](\lambda x.P) \equiv (\lambda x.P)$$

(e) $$[N/x](\lambda y.P) \equiv P$$ if $$x \not \in FV(P)$$.

(f) $$[N/x](\lambda y.P) \equiv \lambda y. [N/x]P$$ if $$x \in FV(P)$$ and $$y \not \in FV(N)$$.

(g) $$[N/x](\lambda y.P) \equiv \lambda z. [N/x][z/y]P$$ if $$x \in FV(P)$$ and $$y \in FV(N)$$.

I do understand that:

• $$(a), (b)$$ are the base cases for this induction.
• $$(d)$$ exists per definition, as one is not allowed to substitute bound variables.
• $$(g)$$ prevents a bound variable from changing to a free one. It does this by first substituting a bound variable.

My question is: If one deletes $$(d)$$ and allows bound variables to be substituted, is $$(g)$$ strong enough to handle it without messing up everything?

I'm asking this because $$(d)$$ seems to prevent the following $$\alpha$$-equivalent substitutions.

$$[y/x] ~~ \lambda x. x \equiv \lambda y.y$$

• "(g) prevents a bound variable from changing to a free one" - It's the other way around: (g) prevents capturing of a free $y$ (it's free in $N$). Commented Apr 29, 2016 at 10:05
• Thanks, that comment really cleared some of my doubts. I was reading (g) the wrong way. Commented Apr 29, 2016 at 12:30

"If one deletes $(\mathrm{d})$ and allows bound variables to be substituted..."

The problem here is that substitution of a bound variable makes little sense, since one substitutes a variable (let's forget for a moment it should be free) with a term, which may very well be an abstraction or application, but not a variable.

Let me illustrate this by example. What if we are trying to substitute a bound variable with a term, which is not a variable? Like this: $$[(y\; y)\ / \ x]\ \lambda x. x.$$ What should we do?

• Produce $\lambda (y\; y). (y\; y)$? It is not a well-formed term, so the answer is no.

• Another choice would be to leave the binding instance intact and make $\lambda x. (y\; y)$ a result. Let's not take into account if it makes sense, at least it is syntactically correct. This variant causes us major troubles too: it will mess up scopes and render $\beta$-reduction useless. And our end goal is to define $\beta$-reduction via substitution.

$(\mathrm{g})$ prevents a bound variable from changing to a free one. It does this by first substituting a bound variable.

It does not use substitution, it uses renaming, which is a different notion.

"...is $(\mathrm{g})$ strong enough to handle it without messing up everything?"

$(\mathrm{g})$ does not tell us anything about substitution of bound variables, since it has the condition $x \in \mathrm{FV}(P)$

First of all, you can't always define a substitution for bound variables. Having $[x/y](\lambda y.\ y) = \lambda x.\ x$ may look appealing, but there's no real way to replace the bound variable in $[(xx)/y](\lambda y.\ y)$ since $\lambda$ wants a variable, not a term. (As Anton Trunov points out above)

It is true however that the $\lambda$ rules in the definition of substitution $(d,e,f,g)$ consider a lot of cases, which could be combined at the cost of a few more $\alpha$-conversions. For instance, we could replace all the $\lambda$ rules with this one: $$\qquad [N/x](\lambda y.\ P) = (\lambda z.\ [N/x][z/y]P) \qquad \mbox{where z is the first variable not free in x N (\lambda y.\ P)}$$ This rule always renames bound variables to fresh ones, even when it is not necessary to do so. Moreover, it always distributes the substitution inside the lambda, even when $x \notin FV(P)$ and the substitution has no effect.

The result of the rule above is the same of what you get using rules $(d,e,f,g)$ up to $\alpha$-conversion. Hence, it only differs from the rules in the book by performing more renamings.

Rules $(d,e,f,g)$ can be seen as a "smarter" way of performing substitution, stopping as soon as there is no more $x$ around, and renaming variables only as needed.