[Prev][Next][Index][Thread]
slippery substitutions
Posted-Date: Tue, 14 Mar 89 19:18:16 -0500
Date: Tue, 14 Mar 89 19:18:16 -0500
It is well known that substitutions are tricky. Here is
another illustration of this fact.
In proofs of strong normalization for the simply-typed
lambda calculus (or higher-order typed lambda calculi),
the following step takes place:
(For simplicity, I will assume that we are dealing with the
simply-typed case)
We are proving by induction on the length of a proof
of typing judgment D -> M: sigma,
that for EVERY substitution [N1/x1,...,Nk/xk], if
N1, ..., Nk are terms with Ni in [[sigma_i]]
(with x1,...,xk the free variables in M, and D -> xi: sigma_i),
then M[N1/x1,...,Nk/xk] is in [[sigma]].
(Here [N1/x1,...,Nk/xk] denotes the simultaneous substitution
of Ni for xi.)
The proof proceeds by cases, depending on the last inference.
The interesting case is the case where M is a
lambda abstraction, say \x: sigma. Q.
In this case, the induction hypothesis applies to the proof of
D, x: sigma -> Q: tau,
where the set of free variables in Q is
{x1,...,xk,x}. We fix any N in [[sigma]],
and apply the induction hypothesis to the substitution
[N1/x1,...,Nk/xk,N/x]. Thus, we have that
Q[N1/x1,...,Nk/xk,N/x] is in [[tau]].
>From this, we note that
(*) Q[N1/x1,...,Nk/xk,N/x] = (Q[N1/x1,...,Nk/xk])[N/x],
and that
(**) (\x: sigma. Q)[N1/x1,...,Nk/xk] = \x: sigma. Q[N1/x1,...,Nk/xk],
and then use a lemma (or a property of the candidates) that says that whenever
Q[N/x] in [[tau]], then (\x: sigma. Q)N in [[tau]],
to conclude that
((\x: sigma. Q)[N1/x1,...,Nk/xk])[N/x] in [[tau]].
Since this holds for every N in [[sigma]], we have shown that
(\x: sigma. Q)[N1/x1,...,Nk/xk] in [[sigma -> tau]], which is
what we want.
Now, for the slippery steps!
Both (*) and (**) are FALSE if x is free in any of the N1,...,Nk!
One could say that in (**) some automatic renaming of bound
variables is performed, so that capture does not take place.
But in (*), x is free in Q, and it MUST be chosen so that it
DOES NOT occur free in any of the N1,...,Nk!
The point is that alpha-conversion, usually ignored,
must be used. In fact, we are working with
equivalence classes of terms modulo alpha-conversion, and
we can choose a representative \y: sigma. Q such
that y is not free in N1,...,Nk.
If one wanted to formalize the above proof, say in Coquand/Huet's
theory of constructions, it would be necessary to prove
(*) Q[N1/x1,...,Nk/xk,N/x] = (Q[N1/x1,...,Nk/xk])[N/x],
and this requires the assumption that x is not free in any of the
Ni. The careful choice of x is crucial.
I admit, this is not such a big deal.
However, I have rarely seen this point mentioned
in the proofs I have seen, and my own proof
(in a paper mentioned a few weeks ago) lacked precision on
this point.
Jean