La théorie homotopique des types 🌶🌶
ฝัง
- เผยแพร่เมื่อ 29 ก.ย. 2024
- Cette vidéo est une brève introduction à la théorie homotopique des types.
0:25 L'univers des types
5:29 Les quantificateurs
10:52 Le tiers exclus
16:03 L'axiome du choix
19:13 L'égalité propositionnelle
25:16 Types, groupoïdes et homotopie
L'infini et les fondations mathématiques | Playlist Science4All
• L'infini et les fondat...
Homotopy Type Theory | Book
homotopytypeth... - วิทยาศาสตร์และเทคโนโลยี
j'ai déjà envie de pleurer
Je ne sais pas pour les autres, mais tu m'as perdu depuis quelques vidéos déjà :p
Et pourtant, je ne suis pas le dernier dans la compréhension du tiers-exclus ^^'
Produit, somme, groupoïde, foncteur... Ça me rappelle quelque chose, mais quoi ? ;)
je me sens trop con face à tes videos Hardcore x)
T'es pas le seul !
Se sentir con, c'est le quotidien du mathématicien...
Simple réflexion : serait-il possible de créer un algorithme capable de trouver seul des théorèmes mathématiques encore non prouvé / non découvert à partir de cette formalisation homotopique des types ? Si je pose cette question, c'est que le sujet m'intéresse, que je ne comprends pas grand chose à tout ça mais j'y vois un intérêt probant à l'automatisation des preuves mathématiques (un peu comme le nez au milieu de la figure ... :D).
+Yarflam oui et non. Il existe déjà des algorithmes qui prouvent des nouveaux théorèmes. La théorie homotopique des types et son implémentation en Coq permettent même de compléter certains bouts de preuves pas trop difficiles.
Cependant, étant donné un théorème, en trouver une preuve est un problème algorithmique difficile, en un sens très précis. Il s'agit en fait d'un problème indécidable (il n'y a pas d'algorithmes qui y arrive à tous les coups). Et même si on se restreint à des preuves "pas trop longues", ça reste un problème NP-complet (on pense qu'aucun algorithme n'y arrivera en quelques milliards d'années)
+Science4All (français) tout ça n'exclut pas la possibilité de créer des intelligences artificielles qui soient meilleures que les meilleurs mathématiciens humains pour prouver des théorèmes...
Merci pour ta réponse. Ainsi prouver des théorèmes n'est pas totalement facilité par la théorie homotopique. Je ne pensais pas forcément à un algorithme déterministe, mais plutôt heuristique. Amener des formules à partir d'axiomes (ou équivalent), prouver qu'elles sont vraies et continuer à construire des objets toujours plus complexes - le tout en ajoutant un facteur (pseudo-)aléatoire qui déterminerait des ensembles de tests.
La difficulté, ce serait de savoir avec certitude si notre modèle de base permet de trouver suffisamment rapidement n'importe quel théorème jusqu'à maintenant démontré pour aller beaucoup plus loin. Peut-être que j'utilise mal le mot théorème ... je pense plutôt à l'idée de preuve par la formule, l'équivalence et la logique. Pas par des rapports de 1500 pages. :)
je ne vois pas en quoi ce serait incompatible avec le platonicisme. Au fond toutes ces belles constructions (que je n'ai pas réussi a suivre en totalité) ne font que redéfinir des objets des mathématiques plus classiques.
Et même les objets bien spécifiques (qu'on n'a pas encore découverts) sont finalement déjà existants, juste pas encore identifiés (une sphère existe indépendamment de comment on la définit ou on l'appelle, et ses propriétés aussi).
Soit dit, je pense que c'est certainement intéressant de se pencher sur cette nouvelle interprétation des bases de la mathématique.
... est ce qu'on aura ça au contrôle?
ce n'est pas au programme, mais ça pourrait être utile au contrôle...
Science4All (français) étant étudiant de math spé, j'ai beaucoup trop entendu cette phrase...
hardcore ça je confirme !
"... je ne peux pas résumé un livre de 400 pages dans une vidéo de 20 mn..." Haha mais dans une vidéo dans 30 mn ?!? ah bah non
Bonjour,
J'ai l'impression que dire qu'on ne peut pas créer un élément de A+B sans passer par les constructeurs (inleft et inright) est impropre.
En fait, j'ai l'impression que rien n'impose dans la théorie des types que tout passe par un constructeur ; pour un contre exemple trivial, il est indiqué dans le livre qu'il n'est pas possible de construire un élément de 0 directement, mais qu'il est possible de le faire indirectement pour une théorie inconsistante ; évidemment, la construction d'un tel élément ne pourrait pas passer par un constructeur (0 n'en ayant pas).
Pour un contre-exemple moins trivial... Je dirais, à l'aide des axiomes que l'on peut ajouter genre le LEM ? Le LEM va permettre de peupler des types sans passer par leurs constructeurs : par exemple, de peupler tous les théorèmes qui ne peuvent pas se démontrer sans le LEM. Mais l'on va peupler ces théorèmes non avec leurs constructeurs propres (...As a side note, je suis pas du tout assez loin dans le livre pour savoir si un théorème a vraiment des constructeurs propres : peut-être je suis en train de dire une ineptie), mais en faisant arriver une fonction dedans (fonction qui nous est donnée par le LEM). Me trompe-je ? (c'est une vraie question, j'ai pas l'impression de comprendre assez la théorie pour pouvoir dire un truc sensé dessus)
Bref, on arrive à un truc que j'arrive pas comprendre dans le livre, et qui est sensée être élémentaire (c'est donc très frustrant) : les propriétés d'induction de A+B, AxB et autres structures "de base" sont-elle des théorèmes, issus des règles fixées au départ, ou des axiome ? J'ai l'impression que c'est le second ; entre autre, parce que pour AxB, le livre indique que l'on va *montrer* que AxB ne contient que des paires - or cette démonstration part de la propriété d'induction, et je ne vois absolument pas comment on pourrait montrer la propriété d'induction sans partir du principe qu'il n'y a que des paires (... En fait je ne vois pas comment on pourrait la montrer tout court, mais c'est une autre histoire). Et seconde chose, justement lorsque AxB est défini dans le livre (chapitre 1.5), le livre semble définir comment on va définir une fonction dessus ; mais définir une fonction d'un type quelconque, mettons AxB (et allant où on veut), on sait déjà le faire depuis la partie 1.2 qui défini les fonctions A->B comme des lambda-expression.
Bref, j'ai l'impression que l'on ne part même pas du principe qu'un élément de AxB (ou A+B ou n'importe quoi) devra passer par un constructeur ; plutôt, on définit des constructeurs arrivant dans AxB, on décide que la propriété d'induction a un habitant, et de là, sachant toutes les façon dont on peut mapper AxB dans un autre type, on en déduit qu'il ne contient que des paires, ie des trucs qui sont passés par le constructeur (... ce qui ne me semble pas supposé vrai pour d'autres types - on l'espère plutôt, "constructivity, if attained, will be an added bonus"). Sauf que c'est absolument pas expliqué comme ça et que j'ai pas l'impression d'avoir bien compris.
Et bref, du coup pour A+B, j'ai la même impression que l'on ne suppose pas que tout habitant est forcément issu des deux constructeurs, mais plutôt qu'on suppose la propriété d'induction, laquelle implique que tout habitant est issu d'un des deux constructeurs (ou plutôt, est égal à un habitant issu des constructeurs, et en plus on sait retrouver lequel etc...).
Sinon j'ai essayé de mettre des messages sur votre site (ça me semble plus simple qu'une vidéo youtube pour des trucs techniques que je pense pas avoir compris), mais je ne sais pas si ça marche (ou si vous n'avez juste pas le temps et je suis juste en train de vous harceler :s auquel cas je m'en excuse).
Bien à vous,
Stéphane
+Le Roux Stéphane je ne maîtrise pas assez le sujet pour te répondre. En effet, le livre n'est pas très clair sur s'il s'agit d'axiomes...
Je réponds beaucoup trop tard et je ne suis pas expert ou quoi que ce soit d'ailleurs, mais de ce que j'ai compris, il est effectivement impossible de créer un élément d'un type sans en passer par un de ses constructeurs, mais l'appel à ce constructeur peut être implicite. Par exemple si on a le type Nat avec les 2 constructeurs 0 : Nat et succ : Nat -> Nat, ainsi qu'une fonction f : A -> Nat, alors on peut effectivement construire un élément de Nat avec f, donc sans directement utiliser un constructeur de Nat, mais on suppose que f fait appel à un constructeur en interne.
Donc au final on peut bien se permettre cette hypothèse que tout élément de Nat vient forcément d'un de ses 2 constructeurs.
Quand on suppose LEM, on suppose qu'il existe un moyen de construire un élément de type X via ses constructeurs. Et si ce n'est pas le cas, alors l'univers est inconsistant.
J'espère ne pas avoir répondu à côté
Drôle que AC (bon une variante, certes) soit vrai en théorie des types, alors qu'en logique intuitionniste il implique le tiers exclu 😆
Il n'y a pas de sommaire dans la description mdr
Bah si: "Cette vidéo est une brève introduction à la théorie homotopique des types." c'est ça le sommaire. Il y a juste une seule entrée, pas besoin de sous chapitres.
+Mourad Qqch ah merde j'ai oublié... Je peux pas la mettre right now. Ce sera là demain
Science4All (français) pas de soucis, ce sont des choses qui arrivent :-)
Très intéressant ! Effectivement ça donne envie de commander le livre, et j'ai trouvé courageux que tu présentes tout ça sachant que ça pourrait perdre ton public.
Pour la forme cependant j'ai trouvé la vidéo pour le moins austère, entre les hésitations et l'absence de musique. Tu es si impatient que ça de passer à la prochaine série ? ^^
Les épisodes Hardcore n'ont jamais été très travaillés visuellement ^^
Mais OUI, je suis impatient de commencer la prochaine série ;)
Hé hé ! Depuis que j'ai moi-même commencé à faire des vidéos je me rends compte de la somme de travail que tu abats, donc vraiment je te souhaite bon courage !
Je me sens tout bête, je ne comprends RIEN à tes vidéos Hardocore. Mais j'aime comme même tes vidéos.(Je ne sais pas pourquoi)
La vidéo est quand même géniale
Type 0 évolue en silvalié
Ça me semblait important
On peut étudier la théorie homotopique des types à l’epfl?
a quand des nouveaux hardcore ?
Bonjour,
J'ai quelques petites questions. J em présente, Gabriel Mattucci et cela fait quelques vidéos que je regarde de vous et que je trouve vraiment intéressant. De plus je ne suis vraiment pas ferré en Maths par contre j'aime bien les maths. Dans cette video, au niveau de la commutativité. Je me suis dit que la commutativité existe toujours entant que nous faisons référence à des nombre qui ne sont pas irrationnel. par exemple 1+2 = 2+1 par contre peux-ton prouver que 1+racine carré de 2 = racine carré de 2 étant donné que racine de 2 est irrationnel? une autre question concernant lettres exclu. Vous avez dit que s'il existe une fonction f de X vers 0, c'est absurde car O ne contient rien. Effectivement, mais peut-on dire que tout de meme cette fonction existe pour n'importe quel X car cela signifierait que X se ferait absorber par 0 et donc que 0 annihilerait tout X.Il doit bien y avoir des trous noir en Maths aussi oui? :) :) :) enfin ..... voilà mérite pour votre réponse.
Déjà 4 minutes que je regarde et je sais absolument pas ce qu'il se passe
Ça ne serait pas plutôt les types qui sont homotopiques et pas la théorie ? Mauvaise traduction de l'anglais...
15'26'' y au rait - il pas une petite coquille : "supposer l'AC" (au lieu de TE) ?
J'ai un peu du mal à suivre le formalisme de la théorie des types, à propos des jugement
Franchement c'est super intéressant et tout et tu doit sûrement bien expliquer les choses (puisque j'ai l'impression d'avoir compris des trucs) mais je sais pas pourquoi j'arrive pas à comprendre :'(
J'ai quelques questions pour essayer de comprendre un peu plus du coup:
- Qu'est-ce que veulent dire ces symboles exactement : := ≡ ?
- Quand tu écrit U c'est en quelque sorte l'univers de tout les types ? c'est pas un peu platonicien du coup ?
- Si j'ai bien compris, pour démontrer une propriété P il faut créer un type P et montrer qu'il est non vide ?
- Est-ce que les Π et les Σ peuvent être vu de la même façon que dans la théorie des ensembles (cad resp. un produit cartésien et une somme disjointe) ?
- Quel est la réponse à la grande question sur la vie, l'univers et le reste ?
En tout cas merci et continu comme ça c'est vraiment génial ce que tu fait ;)
OFumealO j'ai l'impression que les sigma et pi sont plus comme des quantificateurs mais avec plus de "matière" en quelque sorte. J'ai vraiment pas tout compris de la vidéo, mais je vois bcp de liens avec la programmation orientée objet où au final tout est sujet à être construit (ou pas) et rien que ça ça me fait kiffer :D
et je commence à capter en quoi cette théorie est vraiment cool. on dirait presque qu'on pourrait "programmer" des preuves. Quand j'aurai le niveau je lirai ce bouquin
Je me sens un peu comme toi j'ai l'impression que cette théorie est vraiment géniale et ultra avantageuse mais malheureusement j'arrive pas encore à bien la cerner --'. J'aimerais bien pouvoir lire se livre mais j'ai l'impression que je vais être larguer dès la préface, l'anglais aidant pas vraiment à la compréhension.
Mes réponses (imparfaites) aux questions :
- Tout objet doit appartenir à un unique type, et le type auquel appartient un objet doit être défini dès la définition de l'objet. Si j'écris a:A, ça revient à la phrase "j'instancie un objet a de type A". Ça a des similarités avec l'appartenance mais c'est pas la même chose. En particulier, ça n'a pas de sens que de "prouver" a:B. Le symbole := ne me dit rien. J'ai peut-être loupé quelque chose. Le symbole ≡ est l'égalité définitionnelle (judgemental equality en anglais). On peut écrire :≡ pour parler de définition au moment de l'instanciation. Par exemple, si je veux construire un objet à l'aide d'une fonction f, je peux écrire y :≡ f(x). Il s'agit ainsi d'une définition. D'une certaine manière, je n'ai le droit d'écrire "y ::≡" qu'une seule fois. Je ne peux plus redéfinir y une fois qu'il a été défini. Mais ça n'empêche pas y d'être égal par définition à z, auquel cas je peux écrire y≡z.
- oui.
- oui.
- en première approximation, oui. Mais Π et Σ ont aussi des constructeurs et des principes d'induction.
- Je crois l'avoir lu quelque part mais je ne m'en souviens plus ;)
Science4All (français) Merci pour ta réponse ^^ je vais reregarder la vidéo pour essayer de mieux la comprendre en sachant ça.
Hello !
Là je suis en train d'étudier la théorie des catégories, et je vois que il y a plein de points communs entre ce que tu nous raconte et les constructions sur la théorie des catégories (par exemple, avec la somme disjointe, on voit vraiment les flèches, que tu appelles "constructeurs"). Y-a-t-il des liens entre la théorie homotopique des types et la théorie des catégories ?
Oui ! Beaucoup même. Le chapitre 9 du livre s'appelle "Category Theory".
Merci pour la réponse ! Mais du coup la théorie des catégories c'est un cas particulier de la THT ou alors c'est quelque chose qu'on va axiomatiser avec. Ou alors la THT s’appuie dessus ?
@@le_science4all ça aurait été bien de le dire.
Mais du coup, il n'y a qu'une seule manière de formuler la négation en théorie des types ? Parce que dit comme ça on croirait qu'il suffirait d'exprimer une proposition absurde par sa définition, et qu'elle serait capable d'exprimer la négation, ou plutôt la fausseté
C'est bizarre...
J'ai vrrraiment de la peine à rentrer dans le livre o_o
La vidéo m'aide un peu mais il me manque sûrement des étapes intermédiaires ou des prérequis
C'est vachement chaud -_-
Faut que je reregarde les anciennes vidéos sur les types
Il ÿ a moÿen d' être soi sans moi ; ça va faire des malheureux mais pas énormément !
p^-1 c'est le chemin inverse
lol
j'ai pas aces au sommaire :)
Le Biactol et le shampoing existent ^^
Bravo super vidéo bien expliqué
Mais je me demande quelque chose, si j'ai bien compris la théorie des types est en grande partie constructiviste. Mais en maths constructive le tiers exclu et l'axiome du choix sont rejetés. Ma question fondamentale ( pour moi), c' est de savoir si en quelque sorte la théorie des types ne serait pas le lien parfait entre mathématique classique et mathématiques constructiviste. Le lien trouvé entre physique quantique et relativité générale par analogie
D'une certaine manière, la théorie des types est plus un langage mathématique, "une façon de parler maths", qu'une fondation mathématique. À partir du langage de la théorie des types, on peut tout faire. Et on peut tout faire joliment (mais ça c'est subjectif)...
Merci pour cette réponse.
Personellement je trouve ce langage très beau et très efficace.
Hate de voir la nouvelle série, j'espère que c'est les probabilités
Génial
Coucou Science4All sauf si je me trompe pas une bonne partie de tes vidéos( si ce n'est la totalité) traite de sujets compliqués et inaccessibles sans beaucoup de prérequis feras tu des vidéos sur des sujets plus simples qui peuvent être compris niveau postbac ? ou bien quelque chose avec une mini progression ? :D
+Gabriel Pizzo (dj gab) lundi on commence une nouvelle série beaucoup plus compréhensible
Science4All (français) merci bien, continue de faire des vidéos de qualités haha ^-^
il y a l'égalité relationnel et l'égalité ***** ? j'ai oublier
+Seb16120 égalité definitionnelle (même construction) et égalité propositionnelle (c'est un type et prouver l'égalité revient à construire un élément du type)
D'accord ^^
j'utilise tes termes ici : www.ilemaths.net/sujet-10-1-2-y-1-2-740197.html#msg6456241
Dois-je cité ton nom ?
C'est étonnement beaucoup plus abscon. Quelque chose ne passe pas en terme de vulgarisation.
Le fait de noter des fonctions en indiquant juste leur ensembles de départ et d'arrivée, les produits avec " : " en bas (c'est juste pour pas mettre le "appartient à" sous prétexte qu'on fait pas de la logique classique ? plus tard tu le réutilise aussi dans " f(x) : x=x", si quelqu’un comprend, je suis admiratif, parce que des égalités qui ont des types différents, c'est pas simple à suivre.), et les mots en anglais balancés sans raison ("input", le nom des fonctions left et right qui vient semer la confusion avec inputLeft et inputRight, la où des fonctions f,g,h, ça plait très bien à tout le monde (enfin j'imagine...) PS : je suis mauvaise langue : ça ne dure pas.), et de plus tu passe très vite sur ce qu'est l'univers U, alors que je pense que ça doit vraiment être fondamental à visualiser vu la suite. Bref à 5 min j'étais déjà paumé même en repassant la vidéo en vitesse normale (*1.25, habituellement je suis assez bien) et pourtant je suis en MP* dans un bon lycée.
Bon à 6:20 ça s'améliore. 7:33, la notation en somme est hermétique, tu décris à côté d'elle un doublet (ce qui soyons clair ne fait pas sens), et tu parle de valeur de vérité sur les types, "si on veut"... et à 8:58, j'ai bien peur que l'analogie ne soit qu'un vulgaire moyen de passer au dessus de l'échec de communication des minutes précédentes... 9:30 tout va mieux mais je m’arrête néanmoins, j'ai déjà passé trop de temps à écrire ce commentaire.
Peut-être serais-je plus récéptif une prochaine fois mais bon, pour l'heure je suis déçu.
8 mois plus tard, en me refaisant tout l’intuitionnisme à la suite, ça passe, mais les notations restent lourdes. Finalement, ça ne me convainc pas de quitter la logique classique, mais je comprends ce que tu raconte : tu viens de perdre un pouce rouge.