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

[Sam Lindley]

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.