Normalization, eta-conversion and Church-Rosser

[Blaisorblade]

We use η-expansion in PTS. Is this safe? Apparently, there are some strange issues with η-reduction in PTSs.

Hindley's and Seldin's "Lambda-Calculus and Combinators: an Introduction" discusses some problems with η-reduction in PTSs — apparently, it breaks Church-Rosser, though in a strange way (in the given example, it looks as if the two distinct normal forms should still be definitionally equal).

Warning 13.63 (βη-conversion) In simply typed λ-calculus it was easy to add a rule for η-conversion, as in Definition 10.16. But in a PTS the syntax of terms is more complex, and if η-reductions were allowed, the Church–Rosser theorem would fail. This is shown by the following example, due to Nederpelt [NGdV94, Chapter C.3, Section 7]. Let x, y, and z be distinct variables, and consider the term λx : y . (λx : z . x)x. We would have
λx:y.(λx:z.x)x →β λx:y.x
by contracting the β-redex (λx:z . x)x, and we would also have
λx:y.(λx:z.x)x →η λx:z.x
by contracting the η-redex λx:y . (λx:z . x)x. But λx:y . x and λx:z . x are both irreducible, and they are distinct normal forms.

What the remark doesn't point out (though the source might) is that the term can only typecheck (AFAICS) in a context where y = z (which isn't possible, since y and z are variables — the PTS syntax for contexts can't contain equalities, especially used "extensionally" as here). Otherwise, the original term is not well-typed. Moreover, the remark should be discussing typed reduction (I thought), since it appears after discussing of Church-style typing (where pseudo-/pre-terms are only terms if they typecheck).

[Blaisorblade]

Sorry, editing.

[Toxaris]

We don't use eta-reduction. We don't use eta-expansion literally, but the following pieces relate to eta-expansion:

1. equiv (Function ...) (Function ...)
2. equiv (PiType ...) (PiType ...)
3. reify (Function ...)
4. reify (PiType ...)

These functions are only called on values, which are only produced from well-typed terms. So we never eta-expand an ill-typed term.

If we want to understand what's going on in more detail, maybe we should formalize (as a derivation system on paper) what our PTS typechecker is doing.

[Blaisorblade]

So we never eta-expand an ill-typed term.

Looking at the example, it seems that should be enough — but the discussion I quoted do isn't quite clear.

If we want to understand what's going on in more detail, maybe we should formalize (as a derivation system on paper) what our PTS typechecker is doing.

That would fit well with/for the paper we've been discussing — that's the (implicit) reason I started creating such issues (like #139).

[Blaisorblade]

These functions are only called on values, which are only produced from well-typed terms. So we never eta-expand an ill-typed term.

I found a clearer discussion of the issue (with the same example) when browsing some other paper — indeed, eta-expansion is only unsafe on terms with type errors.

[Toxaris]

Cool. Can you add a link or reference to the "some other paper"?

[Blaisorblade]

Can you add a link or reference to the "some other paper"?

Found it again! This fact is in the beginning of Sec. 3 of On the Church-Rosser property for expressive type systems and its consequences for their metatheoretic study (warning: the link is gzipped Postscript):

\beta\eta-reduction is not confluent on [pseudoterms]

followed by the same example. The rest of the paper uses confluence for eta, discussing where it is available — for most non-normalizing PTSs it was an open problem at the time. In particular, they show that a fixpoint combinator (not a looping combinator) would break confluence for eta.

Lesson: should we ever add recursive types, we better restrict to positive type constructors by default (à la Agda), though we might not always need that restriction (we shouldn't need it for LF).