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

[Derek Dreyer]

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 <Sam.Lindley at ed.ac.uk> 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.
>