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

[Derek Dreyer]

Just to clarify, since several people e-mailed me and were confused
about my confluence counterexample:

The classic argument for showing decidability of convertibility
depends on a combination of Church-Rosser (confluence) and
normalization.  For the confluence part, the common approach I'm
familiar with involves proving

(a) If M ->* P and M ->* Q, then there exists T s.t. P ->* T and Q ->* T.

(b) If P ~ Q, then there exists T s.t. P ->* T and Q ->* T.

Part (b) follows by applying (a) to the "peaks" in the
reduction/expansion sequence converting P to Q (and then completing
the remaining diamonds till you arrive at T).  See for instance
Theorem 1B5 and Figure 1B5b on pages 5-6 of Hindley's "Basic Simple
Type Theory" book.  And part (b) is the one that's really important
for showing decidability of ~.

The problem in the setting I described (i.e. Church-style, with
beta-eta reduction) is that, even if P and Q are required to be
well-typed (at the same type), the definition of convertibility
permits the intermediate terms in the reduction/expansion sequence
between P and Q (and, in particular, the "peaks" M) to be ill-typed.
However, for ill-typed terms M, part (a) of the confluence property
does not hold when -> includes eta-reduction.

In particular, take the example I gave, with M = \x:A.(\y:B.y)x, P =
\x:A.x, Q = \y:B.y, and A distinct from B.  M, which is ill-typed,
reduces to both P and Q, but they are distinct normal forms.  I should
say, I got this specific example from Garrel Pottinger in the 1989
Types list thread:
http://www.seas.upenn.edu/~sweirich/types/archive/1989/msg00014.html

Now, for well-typed M, confluence *does* hold (see Theorem 5B8 on page
70 of Hindley).  So, if we instead define beta-eta convertibility to
require all terms M in the sequence connecting P and Q to be
well-typed, then the proof would work fine (I believe).

But I want to know if it is also provable without that requirement,
i.e. relying on the usual definition of beta-eta convertibility, which
says nothing about well-typedness even when it is defined on
Church-style explicitly-typed terms.

FWIW, Hindley follows Theorem 5B8 with a Warning: "No attempt is made
here to define a convertibility relation =beta or =beta/eta on typed
terms by expansions and contractions of redexes.  First, we shall not
need one.  Second, since the typed terms in this chapter correspond
exactly to TA\tau-deductions [Curry-style], any attempt to define such
a typed equality would meet the same type-variation problems as were
discussed for TA_\tau in 2C.  In fact, beta-expanding a typed term may
lead to an expression which is no longer a typed term (cf. 2C2.2-6)."

I'm not sure what to make of this warning.  In particular, if
beta-eta-convertibility is a property of interest (e.g. if it is used
to define equivalence of type constructors in F-omega), then what is
one supposed to do?

Thanks,
Derek


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