# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorMike Shulman
• CommentTimeMar 24th 2012

Started a general page about beta reduction, and a stub for eta reduction but I have to run now.

• CommentRowNumber2.
• CommentAuthorMike Shulman
• CommentTimeMar 25th 2012

Now a bit more at eta reduction.

• CommentRowNumber3.
• CommentAuthorTobyBartels
• CommentTimeMar 25th 2012
• (edited Mar 25th 2012)

Since the version with symbols is definitely ‘$\beta$-reduction’, I’ve moved the name without symbols to beta-reduction (with a hyphen). This triggers the cache bug, so I mention it here. The same with eta-reduction … but can I try to convince you that $\eta$-reduction is wrong and $\eta$-expansion is correct? ETA: No, the cache bug did not appear!

• CommentRowNumber4.
• CommentAuthorTobyBartels
• CommentTimeMar 25th 2012

I put in a stub for alpha-equivalence.

• CommentRowNumber5.
• CommentAuthorMike Shulman
• CommentTimeMar 26th 2012

Thanks. I’m glad you brought up the reduction/expansion issue. What about calling the page eta-equivalence or eta-conversion? I know there are situations in which $\eta$-expansion seems to match better with $\beta$-reduction than $\eta$-reduction does (looking like the unit and multiplication of a monad or something, I don’t recall the details), but I don’t recall being convinced that that is a universal phenomenon. Is there a reason to believe that $\eta$-conversion has a well-defined “correct” directionality at all?

Also, by the “trivial type” do you mean the unit type? If so, I don’t understand your remark about it. Are you thinking of a positive or a negative definition of the trivial type?

• CommentRowNumber6.
• CommentAuthorTobyBartels
• CommentTimeMar 26th 2012

I like eta-conversion so moved the page. However, I understand that term a bit differently from you; see my edits.

Yes, I meant the unit type, defined negatively. I altered your material on the product type to produce material on the unit type, so you can see for yourself.

• CommentRowNumber7.
• CommentAuthorMike Shulman
• CommentTimeMar 26th 2012

Thanks; your meaning of $\eta$-conversion is better. And I see what you mean about the unit type. Interestingly, the positive definition of the unit type does have a well-defined $\eta$-reduction; I added some details to unit type.

Now I’m wondering about the empty type. Its positive presentation is “dual” to the negative unit type in that there are no constructors, and a single eliminator

$e:\varnothing ⊢{\mathrm{abort}}_{C}\left(e\right):C.$

So there can again be no $\beta$-reduction, but it seems like the $\eta$-conversion should be $e\phantom{\rule{thickmathspace}{0ex}}{↔}_{\eta }\phantom{\rule{thickmathspace}{0ex}}{\mathrm{abort}}_{\varnothing }\left(e\right)$, which makes sense both as an expansion and as a reduction. Am I wrong? If not, why the asymmetry, I wonder? Is it because we’ve already broken the symmetry by formulating everything with variables and terms instead of covariables and coterms?

• CommentRowNumber8.
• CommentAuthorMike Shulman
• CommentTimeMar 26th 2012

Ah, no, I’m wrong. The $\eta$-conversion for the positive empty type says that (in the context of a term $e:\varnothing$), any term $c:C$ of any type is convertible to $\mathrm{abort}\left(e\right)$. This also only makes sense as an expansion.

• CommentRowNumber9.
• CommentAuthorMike Shulman
• CommentTimeMar 26th 2012

I’ve updated empty type with this, and also corrected the $\eta$-rule at sum type in the corresponding way.

• CommentRowNumber10.
• CommentAuthorMike Shulman
• CommentTimeMar 27th 2012

I added some comments to eta-conversion about propositional $\eta$-conversions and how they are related to dependent eliminators. I also expanded function type and dependent product type to describe not only the usual negative presentations, but also the “higher-order” positive presentations and their relationship.

• CommentRowNumber11.
• CommentAuthorTobyBartels
• CommentTimeMar 30th 2012

I’ve never seen the positive approach to dependent product types seriously considered, although it’s implicit (in my opinion) in Martin-Löf’s earliest work. So I’m glad to see that people have worked it out (even though I don’t really like it for requiring a stronger metatheory).

• CommentRowNumber12.
• CommentAuthorMike Shulman
• CommentTimeMar 30th 2012

Yeah, the stronger metatheory is a shame. But as Richard’s paper shows, the resulting dependent eliminator sheds a useful light on the propositional eta conversion rule.