5
$\begingroup$

This paper says: "In the presence of a unit type, $\eta$-reduction is not even locally confluent on well-typed terms [20]."

[20] is a reference to a 300-page book with no further details and I cannot find the relevant example there. So can you give an example of $\eta$-reduction not being locally confluent on well-typed terms?

$\endgroup$
1
  • $\begingroup$ Where did you find the book? I didn't find an online version. $\endgroup$
    – ice1000
    Jun 30 at 9:35
11
$\begingroup$

Yes, $\eta$ reduction for unit is terribly behaved. Suppose you are in a context $\Gamma \triangleq x:1, y:1$.

Then, the unit term $\Gamma \vdash \left\langle\right\rangle : 1$ has the following eta-reductions:

$$ \begin{array}{lcl} \left\langle\right\rangle & \leadsto_\eta & x \\ \left\langle\right\rangle & \leadsto_\eta & y \\ \end{array} $$

There are no further $\beta$ or $\eta$ reductions, so local confluence fails.

In practice (and in theory, actually), what you want to do instead is $\eta$-expansion. You have to do it in a typed way, but it is fantastically well-behaved.

$\endgroup$
3
  • $\begingroup$ Or stop using $\eta$-rules and use an extensionality rule instead. $\endgroup$ Jul 1 at 8:05
  • $\begingroup$ What do you mean by an extensionality rule? $\endgroup$ Jul 1 at 10:13
  • 3
    $\begingroup$ See Definition 3.22, for the unit type it is $$\frac{\vdash a : 1 \qquad \vdash b : 1}{\vdash a \equiv_1 b}$$ and examples are on the next page. $\endgroup$ Jul 1 at 10:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.