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, 2021 at 9:35

1 Answer 1

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, 2021 at 8:05
  • $\begingroup$ What do you mean by an extensionality rule? $\endgroup$ Jul 1, 2021 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, 2021 at 10:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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