[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Thanks, Sam! I think what you suggest here works. (You still have to prove the "key property" you mention separately, by that seems to go through by a relatively straightforward induction on typing derivations.) Gilles Barthe also pointed me to Herman Geuvers' LICS'92 paper (and also thesis), which proves the theorem I'm after in a more general setting (for the class of "functional, normalizing PTS's"): http://www.cs.ru.nl/~herman/PUBS/LICS92_CRbh.ps.gz http://www.cs.ru.nl/~herman/PUBS/Proefschrift.ps.gz (see Chapter 5, which contains an expanded/revised version of the proof in the LICS paper) FYI: According to Geuvers, the confluence counterexample I gave is due originally to Nederpelt (1973). Thanks, Derek On Fri, Aug 10, 2012 at 4:39 PM, Sam Lindley <[email protected]> wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > I think this is quite straightforward to show using the fact that > beta-eta-reduction is confluent on untyped terms. > > Write |M| for the type-erasure of the Church-style simply-typed term M. > > If M ~ N, then certainly |M| ~ |N|. Let M', N' be respectively the normal > forms of M and N. By confluence, |M'| = |N'|. The key property we need is > that given a Curry-style judgement, G |- P : A, where P is in normal form, > there is a unique Church-style term P* such that G |- P* : A and |P*| = P. > This means that M' = |M'|* = |N'|* = N'. > > Sam > > > On 10/08/12 12:34, Derek Dreyer wrote: >> >> [ 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 >> > > > -- > The University of Edinburgh is a charitable body, registered in > Scotland, with registration number SC005336. >
