slippery substitutions

To: types@theory.LCS.MIT.EDU
Subject: slippery substitutions
From: jean@central.cis.upenn.edu
Date: Wed, 15 Mar 89 00:11:48 EST
Sender: meyer@theory.LCS.MIT.EDU
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