15
$\begingroup$

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, which led to question about an orthogonal notion of extension, Characterising invisible equivalences by confluent rewrite rules, which sought to clarify an answer to that earlier question.

$\endgroup$
10
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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? $\endgroup$ – Charles Stewart Sep 19 '10 at 15:16
4
$\begingroup$

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).

$\endgroup$
  • 2
    $\begingroup$ I guess this is an extended comment on Neel's answer. Klop & De Vrijer (1989) 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). $\endgroup$ – Charles Stewart May 16 '13 at 7:50

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.