The Coq mailing list

[Jonathan Chan <jcxz AT cs.ubc.ca>]

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

Le 25/09/2021 à 00:43, Jonathan Chan a écrit :

Hello all,

I'm trying to determine convertibility rules for a CIC that adhere to those of Coq (untyped, with universe cumulativity), and I'm using the Coq manual on convertibility as reference.
It appears that these are the rules:

Γ ⊢ e₁ ⊳* e
Γ ⊢ e₂ ⊳* e
----------- =-⊳*
Γ ⊢ e₁ = e₂

Γ ⊢ e₁ ⊳* λx: t. e
Γ ⊢ e₂ ⊳* e'₂
Γ, x: t ⊢ e = e'₂ x
------------------- =-η₁
Γ ⊢ e₁ = e₂

Γ ⊢ e₁ ⊳* e'₁
Γ ⊢ e₂ ⊳* λx: t. e
Γ, x: t ⊢ e'₁ x = e
------------------- =-η₂
Γ ⊢ e₁ = e₂

+ congruent closure rules

I have two questions about these rules:

1. Is there a source for this formulation of eta-equivalence? Some paper that uses this kind of convertibility that isn't merely citing the Coq manual?
   So far I've only found papers that use the reflexive–symmetric–transitive closure of β- and η-reduction.
2. Does transitivity hold directly from these rules? And if so, is there some paper that states to have proven it? I'm mostly just looking for something to cite.

Jonathan