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

[Derek Dreyer]

Hi, Thorsten.  Yes, I'm well aware that the theorem (and proof) I was
asking for are not very robust in the sense of being scalable to
richer type systems, and using beta-eta normalization to implement
equivalence is not very practical algorithmically.

But in the particular case of Church-style STLC, I thought the proof
of confluence of beta-eta normalization was a standard (old?) result.
However, the only reference I can find is the Geuvers paper from 1992,
which presents a much more involved proof for the more general class
of PTS's.  I'd be glad if anyone can point me to an older reference
containing the simple proof that Sam suggested.

Thanks,
Derek

On Tue, Aug 14, 2012 at 11:13 AM, Altenkirch Thorsten
<psztxa at exmail.nottingham.ac.uk> wrote:
> I don't think the classical approach of showing decidability via strong
> normalisation and confluence of small step reduction is such a good
> choice. Indeed it ceases to work for systems with dependnet types and
> eta-reductions. Another issue is that it is hardly the way we would
> implement a decision procedure.
>
> An alternative are semantic methods, I.e. normalisation by evaluation.
> There is a weak version for combinatory logic which can be used to only
> implement beta reduction (but not xi or eta rules) or a strong one which
> does give you full beta eta equality. However, to extend strong NBE for
> more complex systems can be quite tricky too. I don't think I have seen a
> straightforward extension of the strong version to dependent types (I am
> saying this expecting somebody to scream :-).
>
> Another idea which James Chapman and I have investigated is to directly
> prove that the natural implementation of a decision procedure using big
> step semantics is correct. This also has the advantage that you actually
> prove the correctness of the implementation. This has been written up in
> James PhD and there is also a journal paper - see
> http://www.cs.nott.ac.uk/~txa/publ/jtait07.pdf
>
> Cheers,
> Thorsten
>
> On 11/08/2012 13:13, "Derek Dreyer" <dreyer at mpi-sws.org> wrote:
>
>>[ The Types Forum,
>>http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>>
>>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.
>>>>
>
> This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it.   Please do not use, copy or disclose the information contained in this message or in any attachment.  Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.
>
> This message has been checked for viruses but the contents of an attachment
> may still contain software viruses which could damage your computer system:
> you are advised to perform your own checks. Email communications with the
> University of Nottingham may be monitored as permitted by UK legislation.