Follow

Est-ce que vous connaissez une page qui liste tous les axiomes connus et lesquels sont (in)compatibles les uns avec les autres.

Il y a bien cette page là qui en liste quelques uns, mais elle ne parle pas de l’axiome d’univalence (incompatible avec l’axiome K) : github.com/coq/coq/wiki/CoqAnd

En particulier, je cherche à comprendre avec quels axiomes connus la η-équivalence (func_ext dans la page) est inconsistante. (J’ai bien des modèles du calcul des constructions qui ne la respecte pas, mais ce n’est pas un exemple très méchant, quoi.)

C'est le genre de choses qui passeraient bien sur Wikidata, je trouve 😊 Je prends note pour quand j'aurais du temps.

@MartinShadok Il me semble que func_ext n'est pas l'eta-équivalence, si ? Je croyais d'ailleurs que l'eta-équivalence était en Coq sans axiomes...

@nore Bon, d’accord, c’est l’η-équivalence pour les types fonctionnels, pas l’η-équivalence en général ☺ En Coq, on a effectivement cette équivalence pour les types produits (et peut-être plus généralement pour tous les (co)-inductifs ?). (Ou alors je confonds les réductions, ce qui n’est pas impossible du tout ! 😅​)

L’axiome func_ext n’est pas en Coq par défaut, mais il est compatible avec sa logique. Un exemple de modèle où il n’est pas valide est celui où on prend en compte le temps de calcul : avec func_ext, un tri bulle et un tri rapide, c’est la même chose (ce qui est souhaitable dans certains contextes, mais pas dans d’autres).

Mais comme en général, ajouter deux axiomes connus en Coq peut générer des incompatibilités (enfin, ce n’est pas particulièrement spécifique à Coq, en fait)… je crains le piège si je ne fais pas attention 😅​

@MartinShadok Pour moi l'eta-équivalence, c'est "fun x -> f x" qui est convertible avec "f", ce qui n'est pas la même chose que de dire "forall x, f x = g x -> f = g".
Par contre je suis d'accord qu'il peut y avoir des incompatibilités entre différets axiomes connus (par exemple, la logique classique et l'univalence).

@nore Ah, je vois. Je n’avais pas saisi la partie convertible (le fait qu’elles soient égales me suffisait). Du coup je ne pense même pas que Coq ait l’η-conversion pour les paires : il a l’égalité, mais je ne sais pas pour la convertibilité (a priori, je dirais non).

Sign in to participate in the conversation
Aleph

Generalistic Mastodon instance for open-minded people. Instance Mastodon généraliste pour personnes ouvertes d'esprit.