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

[Derek Dreyer]

A quick follow-up:

The proof in Geuvers' LICS'92 paper is in fact a generalization of
Sam's argument to a broader class of PTS's.  If one instantiates
Geuvers' proof to STLC, it degenerates precisely to Sam's proof, with
the "key property" Sam mentioned being an instance of Lemma 3.12 in
Geuvers' paper.

Derek

On Fri, Aug 10, 2012 at 5:48 PM, Derek Dreyer <dreyer at mpi-sws.org> wrote:
> 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.
>>