[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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
