The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

Just some comments: the eta rule is a way to implement extensionality for pure functions, hence it is not really a form of computation unlike beta. Hence we shouldn’t think of it as a form of reduction it is an equivalence and reduction isn’t the best way to decide it. Also it makes very little sense on untyped terms, this seems to be rather some formalist game.

 

Thorsten

 

From: <coq-club-request AT inria.fr> on behalf of Jonathan Chan <jcxz AT cs.ubc.ca>
Reply to: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Tuesday, 28 September 2021 at 19:03
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Convertibility with η-equivalence

 

Thanks for the detailed reply Meven! The η-conversion rule in Abel's paper looks like it could be adapted to be untyped by checking that either side is a lambda (like in the Coq manual) instead of checking the type...

Out of curiosity, how would the η laws be incorporated into α-equivalence? What were the issues you ran into?

On 2021-09-28 02:17, Meven LENNON-BERTRAND wrote:

[CAUTION: Non-UBC Email]

Hello Jonathan,

As far as I know, the theory of η-conversion in the Coq setting is quite muddy. I've been working on this recently with the people in the Gallinette team in Nantes and the MetaCoq team, so here are my two cents.

η-reduction cannot be adopted as such, because it would not respect subject reduction, as the cumulativity of product types in Coq is equivariant on domain (that is, Π x : A . B <= Π x : A' . B' when A = A' and B <= B'). Indeed, if A' < A then f : Π x : A . B |- λ x : A'. f x : Π x : A' . B (because by cumulativity x : A' |- x : A) but λ x : A' . f x ->η f and it is not the case that f : Π x : A . B |- f : Π x : A' . B. Also, it is quite an annoying rule to work with, since it is very non-local, as one has to test for variable freeness.
η-expansion also poses its own problems in the setting of Coq, notably that without types to know when to trigger it one could a priori fire it indefinitely (defeating normalization), and that generating the correct typing annotation on the variable bound by the λ is impossible (and so again this threatens subject reduction).
A third option, which is closer to what Coq does, is to not see η as a reduction in one or the other direction, but only as an equality rule, i.e. incorporate it in α-equality. But this also has some weird technical issues (again because of untyped terms).
So in the end, I am not aware of any satisfactory ways to treat η laws in the untyped CIC setting, and this is why MetaCoq still does not have η-conversion in its theory...

The only way out I see, which is how I've come to think of those rules, is that they are actually an algorithm for typed conversion, but one that does not maintain types as they are in fact not needed, since for rules η1 and η2 you only need to look at the other side to perform η expansion. In fact, those rules are very close to the ones for algorithmic conversion in Abel et al.'s Decidability of Conversion for Type Theory in Type Theory.

As for transitivity, no it does not hold directly. I guess the closest you can get is the paper above, where transitivity is proven for the typed, algorithmic system by induction on the conversion derivation – a proof that should adapt reasonably well to the untyped setting.

Best,

Meven LENNON-BERTRAND

Doctorant, Équipe Gallinette – LS2N – Université de Nantes

www.meven.ac

han

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.