patternMinor
Lambda Calculus inductive substitution definition
Viewed 0 times
definitionsubstitutioncalculusinductivelambda
Problem
I'm reading Lambda-Calculus and Combinators: An Introduction, and there's the following definition of $\lambda$-substitution:
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 \equiv ([N/x]P)([N/x]Q)$
(d) $N/x \equiv (\lambda x.P)$
(e) $N/x \equiv P$ if $x \not \in FV(P)$.
(f) $N/x \equiv \lambda y. [N/x]P$ if $x \in FV(P)$ and $y \not \in FV(N)$.
(g) $N/x \equiv \lambda z. [N/x][z/y]P$ if $x \in FV(P)$ and $y \in FV(N)$.
I do understand that:
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 $$
- $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 \equiv ([N/x]P)([N/x]Q)$
(d) $N/x \equiv (\lambda x.P)$
(e) $N/x \equiv P$ if $x \not \in FV(P)$.
(f) $N/x \equiv \lambda y. [N/x]P$ if $x \in FV(P)$ and $y \not \in FV(N)$.
(g) $N/x \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 $$
Solution
"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)$
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)$
Context
StackExchange Computer Science Q#56755, answer score: 5
Revisions (0)
No revisions yet.