[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Just to clarify, since several people e-mailed me and were confused about my confluence counterexample: The classic argument for showing decidability of convertibility depends on a combination of Church-Rosser (confluence) and normalization. For the confluence part, the common approach I'm familiar with involves proving (a) If M ->* P and M ->* Q, then there exists T s.t. P ->* T and Q ->* T. (b) If P ~ Q, then there exists T s.t. P ->* T and Q ->* T. Part (b) follows by applying (a) to the "peaks" in the reduction/expansion sequence converting P to Q (and then completing the remaining diamonds till you arrive at T). See for instance Theorem 1B5 and Figure 1B5b on pages 5-6 of Hindley's "Basic Simple Type Theory" book. And part (b) is the one that's really important for showing decidability of ~. The problem in the setting I described (i.e. Church-style, with beta-eta reduction) is that, even if P and Q are required to be well-typed (at the same type), the definition of convertibility permits the intermediate terms in the reduction/expansion sequence between P and Q (and, in particular, the "peaks" M) to be ill-typed. However, for ill-typed terms M, part (a) of the confluence property does not hold when -> includes eta-reduction. In particular, take the example I gave, with M = \x:A.(\y:B.y)x, P = \x:A.x, Q = \y:B.y, and A distinct from B. M, which is ill-typed, reduces to both P and Q, but they are distinct normal forms. I should say, I got this specific example from Garrel Pottinger in the 1989 Types list thread: http://www.seas.upenn.edu/~sweirich/types/archive/1989/msg00014.html Now, for well-typed M, confluence *does* hold (see Theorem 5B8 on page 70 of Hindley). So, if we instead define beta-eta convertibility to require all terms M in the sequence connecting P and Q to be well-typed, then the proof would work fine (I believe). But I want to know if it is also provable without that requirement, i.e. relying on the usual definition of beta-eta convertibility, which says nothing about well-typedness even when it is defined on Church-style explicitly-typed terms. FWIW, Hindley follows Theorem 5B8 with a Warning: "No attempt is made here to define a convertibility relation =beta or =beta/eta on typed terms by expansions and contractions of redexes. First, we shall not need one. Second, since the typed terms in this chapter correspond exactly to TA\tau-deductions [Curry-style], any attempt to define such a typed equality would meet the same type-variation problems as were discussed for TA_\tau in 2C. In fact, beta-expanding a typed term may lead to an expression which is no longer a typed term (cf. 2C2.2-6)." I'm not sure what to make of this warning. In particular, if beta-eta-convertibility is a property of interest (e.g. if it is used to define equivalence of type constructors in F-omega), then what is one supposed to do? Thanks, Derek On Fri, Aug 10, 2012 at 1:34 PM, Derek Dreyer <[email protected]> wrote: > 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
