[TYPES] decidability/confluence of beta-eta convertibility in Church-style STLC

[Derek Dreyer]

Hi, all.  I'm having a hard time finding a (canonical) source for what
I thought would be a very simple question.

Consider the simply-typed lambda calculus (STLC), Church-style (with
type annotations on variable binders), and beta-eta reduction.
Beta-eta convertibility, which I'll write as M ~ N, means that M is
convertible to N by some sequence of beta/eta reductions/expansions,
which may very well go through ill-typed intermediate terms even if M
and N are themselves well-typed.

I want to show the following:

If G |- M : A and G |- N : A, and M ~ N, then M and N have the same
beta-eta (short) normal form.

It is well known that well-typed terms in STLC are strongly
normalizing wrt beta-eta reduction.  But to prove the above, one also
needs confluence.  The problem is that the intermediate terms in the
beta-eta conversion of M and N may be ill-typed, and
beta-eta-reduction is not confluent in this setting for ill-typed
terms.  In particular,

(\x:A.(\y:B.y)x)

can eta-convert to

\y:B.y

or beta-convert to

\x:A.x

which are only equal if A = B.

One strategy would be to prove that beta-eta-convertibility --
*between terms of the same type* -- going through ill-typed terms is
equivalent to beta-eta convertibility restricted to going only through
well-typed terms.  Intuitively, this seems like it should be true, but
it is not at all clear to me how to show it.  In particular, the
*between terms of the same type* part seems critical in order to
outlaw the confluence counterexample given above.

I found some discussion of some related questions in a thread on the
Types list from 1989:

http://article.gmane.org/gmane.comp.science.types/266  (and subsequent posts)

But it doesn't seem to contain a direct answer to my question.

Thanks!
Derek