<p>For typed calculi, if you consider the negative types ($1$, $\times$, $\to$), you can turn the eta rules on or off basically at will without affecting confluence. </p>

<p>For positive types (sums, and pairs with the pattern-matching elimination), the situation is much messier. Basically, the question is whether the term has a closed-scope elimination form, which let contexts interact in complicated ways with eta-expansions. For example, if $e$ has type $A \times B$, then its eta-expansion is $\mathsf{let}\;(a,b) = e \;\mathsf{in}\; (a,b)$. But to get the equational theory a category theorist would expect, you need to consider contexts $\mathbb{C}[-]$, and generalize the equation to be $\mathbb{C}[e] \equiv \mathsf{let}\;(a,b) = e\;\mathsf{in}\;\mathbb{C}[(a,b)]$ (with the expected scoping restrictions). </p>

<p>I think that you can still prove a confluence result if you don't allow the commuting conversions. But this is hearsay -- I've never tried it myself, nor looked at papers documenting it. </p>

<p>I don't really know anything about untyped lambda calculus, though.</p>

<p>EDIT: Charles asks about eta-reductions. This is promising for the kind of example he seeks, because I think in general they won't be strong enough to model the full equality theory, which I'll illustrate with a simple example involving booleans. The eta-expansion for booleans is $\mathbb{C}[e] \mapsto \mathsf{if}(e, \mathbb{C}[\mathsf{true}], \mathbb{C}[\mathsf{false}])$. (The eta-reduction is of course the other direction.) </p>

<p>Now, consider the term $\mathsf{if}(e, f, g)\;\mathsf{if}(e, x, y)$. Showing that this term is equivalent to $\mathsf{if}(e, f\;x, g\;y)$ needs to go through an eta-expansion, because we have to replace the $e$ in one of the if-then-elses with $\mathsf{true}$ and $\mathsf{false}$ in order to drive a $\beta$-reduction.  </p>

CC BY-SA 2.5
2010-09-19T15:16:37.373Z
I should have made clear that this was about the untyped lambda calculus: the logic aside might make that unclear.  In the typed case, I expect that Post completeness holds for the 〈→,×〉 theory, but I'm not at all sure at other types.  *contexts interact in complicated ways with eta-expansions* - that's a case for considering eta reduction, isn't it, because you don't need to constrain the rewrites?
Charles Stewart
CC BY-SA 2.5
2010-09-19T11:29:46.990Z
2010-09-19T17:25:15.583Z
2010-09-19T17:25:15.583Z
Neel Krishnaswami
<p>According to John C. Mitchell in Foundations of Programming Languages, both in STLC and in untyped lambda calculus, the reduction rule <code>pair (proj₁ P, proj₂ P) → P</code> breaks confluence when combined with <code>fix</code> reduction (or, I assume from looking at the proof), without such conditions for the untyped case. This is theorem 4.4.19 (page 272).</p>

CC BY-SA 3.0
2013-05-16T07:50:40.543Z
I guess this is an extended comment on Neel's answer.  [Klop & De Vrijer (1989)](http://janwillemklop.nl/Jan_Willem_Klop/Bibliography_files/51.surjectivepairing.pdf) survey the theory of the untyped lambda calculus with surjective pairing: the case with eta reductions is indeed non-confluent, but the theory is consistent (it has a model in Scott's D_inf construction), and they provide results suggesting a confluent, conservative rewrite theory for surjective pairs can be given (still an open problem, AFAIK).
Charles Stewart
CC BY-SA 3.0
2013-05-16T04:08:11.543Z
2013-05-16T04:08:11.543Z
Blaisorblade
<p>There are two main, studied theories of the lambda calculus, the beta theory and its Post-complete extension, the beta-eta theory.</p>

<p>Do these two theories have an in-between, a kind of intermediate eta rule that gives a confluent rewrite theory?  Is there some interesting notion of partial extensionality that it corresponds to?</p>

<p>This is the second question I have asked in pursuit of intermediate eta, the previous being <a href="https://cstheory.stackexchange.com/questions/246/extensions-of-beta-theory-of-lambda-calculus">Extensions of beta-theory of lambda calculus</a>, which led to question about an orthogonal notion of extension, <a href="https://cstheory.stackexchange.com/questions/398/characterising-invisible-equivalences-by-confluent-rewrite-rules">Characterising invisible equivalences by confluent rewrite rules</a>, which sought to clarify an answer to that earlier question.</p>

<lo.logic><lambda-calculus><extensionality>
Are there intermediate eta theories for the lambda calculus?
Charles Stewart
# Are there intermediate eta theories for the lambda calculus?

(Asked by: username_0 on 2010-09-17)

There are two main, studied theories of the lambda calculus, the beta theory and its Post-complete extension, the beta-eta theory.

Do these two theories have an in-between, a kind of intermediate eta rule that gives a confluent rewrite theory? Is there some interesting notion of partial extensionality that it corresponds to?

This is the second question I have asked in pursuit of intermediate eta, the previous being [Extensions of beta-theory of lambda calculus](https://cstheory.stackexchange.com/questions/246/extensions-of-beta-theory-of-lambda-calculus), which led to question about an orthogonal notion of extension, [Characterising invisible equivalences by confluent rewrite rules](https://cstheory.stackexchange.com/questions/398/characterising-invisible-equivalences-by-confluent-rewrite-rules), which sought to clarify an answer to that earlier question.

**Tags:** lo.logic, lambda-calculus, extensionality

---

## 2 answers

### Answer by username_1 on 2010-09-19. Score: 10

For typed calculi, if you consider the negative types ($1$, $\times$, $\to$), you can turn the eta rules on or off basically at will without affecting confluence.

For positive types (sums, and pairs with the pattern-matching elimination), the situation is much messier. Basically, the question is whether the term has a closed-scope elimination form, which let contexts interact in complicated ways with eta-expansions. For example, if $e$ has type $A \times B$, then its eta-expansion is $\mathsf{let}\;(a,b) = e \;\mathsf{in}\; (a,b)$. But to get the equational theory a category theorist would expect, you need to consider contexts $\mathbb{C}[-]$, and generalize the equation to be $\mathbb{C}[e] \equiv \mathsf{let}\;(a,b) = e\;\mathsf{in}\;\mathbb{C}[(a,b)]$ (with the expected scoping restrictions).

I think that you can still prove a confluence result if you don't allow the commuting conversions. But this is hearsay -- I've never tried it myself, nor looked at papers documenting it.

I don't really know anything about untyped lambda calculus, though.

EDIT: Charles asks about eta-reductions. This is promising for the kind of example he seeks, because I think in general they won't be strong enough to model the full equality theory, which I'll illustrate with a simple example involving booleans. The eta-expansion for booleans is $\mathbb{C}[e] \mapsto \mathsf{if}(e, \mathbb{C}[\mathsf{true}], \mathbb{C}[\mathsf{false}])$. (The eta-reduction is of course the other direction.)

Now, consider the term $\mathsf{if}(e, f, g)\;\mathsf{if}(e, x, y)$. Showing that this term is equivalent to $\mathsf{if}(e, f\;x, g\;y)$ needs to go through an eta-expansion, because we have to replace the $e$ in one of the if-then-elses with $\mathsf{true}$ and $\mathsf{false}$ in order to drive a $\beta$-reduction.

> **Comments:**
> **username_0**: I should have made clear that this was about the untyped lambda calculus: the logic aside might make that unclear.  In the typed case, I expect that Post completeness holds for the 〈→,×〉 theory, but I'm not at all sure at other types.  *contexts interact in complicated ways with eta-expansions* - that's a case for considering eta reduction, isn't it, because you don't need to constrain the rewrites?  

---

### Answer by username_2 on 2013-05-16. Score: 4

According to John C. Mitchell in Foundations of Programming Languages, both in STLC and in untyped lambda calculus, the reduction rule `pair (proj₁ P, proj₂ P) → P` breaks confluence when combined with `fix` reduction (or, I assume from looking at the proof), without such conditions for the untyped case. This is theorem 4.4.19 (page 272).

> **Comments:**
> **username_0**: I guess this is an extended comment on Neel's answer.  [Klop & De Vrijer (1989)](http://janwillemklop.nl/Jan_Willem_Klop/Bibliography_files/51.surjectivepairing.pdf) survey the theory of the untyped lambda calculus with surjective pairing: the case with eta reductions is indeed non-confluent, but the theory is consistent (it has a model in Scott's D_inf construction), and they provide results suggesting a confluent, conservative rewrite theory for surjective pairs can be given (still an open problem, AFAIK).  

---

