4
$\begingroup$

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

$\endgroup$
  • 1
    $\begingroup$ "(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$). $\endgroup$ – Anton Trunov Apr 29 '16 at 10:05
  • $\begingroup$ Thanks, that comment really cleared some of my doubts. I was reading (g) the wrong way. $\endgroup$ – Aristu Apr 29 '16 at 12:30
5
$\begingroup$

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

$\endgroup$
4
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.