La théorie des types | Infini 24
ฝัง
- เผยแพร่เมื่อ 12 ก.พ. 2017
- La théorie des types est une alternative à la théorie des ensembles. J'essaie de vous en présenter quelques grandes idées ici.
L'infini et les fondations mathématiques | Playlist Science4All
• L'infini et les fondat...
The Homotopy Type Theory Book
homotopytypetheory.org/2013/0...
The Universal Turing Machine (ft. Rachid Guerraoui) | ZettaBytes
• The Universal Turing M...
Les machines de Turing | Math&Magique
• Les machines de Turing...
La machine de Turing | Passe-Science
• La machine de Turing, ...
The LEGO Turing Machine
• The LEGO Turing Machine
Théorie des types dépendants et axiome d'univalence | Thierry Coquand (Séminaire Bourbaki)
• Séminaire Bourbaki - 2...
Univalent foundations subsume classical mathematics | Andrej Bauer
math.andrej.com/2014/01/13/uni...
Sometimes all functions are continuous | Andrej Bauer
math.andrej.com/2006/03/27/som... - วิทยาศาสตร์และเทคโนโลยี
Vidéo très intéressante, merci beaucoup.
Mais du coup, est-ce que la "théorie des types" se rapproche du "lambda-calcul" ? Le lambda-calcul part du principe que tout est fonction (y compris un nombre ou une constante) et on peut imbriquer des fonct° "basiques" pour obtenir des fct° plus complexes, que l'on peut à leur tour combiner... Donc on pourrait définir des lambda fct° de base sur l'arithmétique (definir un nombre, sont successeur, l'égalité) et redéfinir/recalculer des fct° complexes (puissance, modulo, ...). Même si ce n'est pas la référence ultime, l'article Wikipédia sur le lambda-calcul semble dire la même chose que ta vidéo : fr.wikipedia.org/wiki/Lambda-calcul . Les notations est complétement différente mais le vocabulaire proche et les idées diablement proches.
Ensuite, les mots types, constructeurs et fonctions existent en informatique (langages c++ et dérivés par exemple) depuis longtemps et leurs sens s'adaptent bien à la façon dont tu les définis. Il y a les types de base (booléeen, entier, à virgule flottante, ...) que l'on peut assembler pour en faire de plus complexes. Par exemple un point du plan en combinant 2 flottants puis un segment à partir de 2 points (donc 4 flottants). Un constructeur n'est qu'une fonct° qui créer un nouvel objet à partir d'objets plus élémentaires. De ce fait, je peux faire plusieurs constructeurs de "segment" (l'un prends 2 points en entrée, l'autre 4 flottants) mais tous donnent des segments "comparables". Il y a ensuite la possibilité de faire des fonctions qui vont travailler/calculer sur des segments. Par une fonction intersection : on lui donne 2 segments et nous dit s'ils se coupent (et si oui, on quel point). Une autre fonction pourrait, a partir d'un segment retourner l'équation de la droite sur laquelle se trouve un segment.
Oui, en fait les lambda-expressions sont des "habitants" des types. Je sais pas si c'est très clair mais par exemple le type A -> A est habité par le terme λx : A.x (fonction identité) : elle prend un objet de type A et renvoie un objet de type A (lui-même en l'occurrence), elle est donc de type A -> A.
Autre exemple λx : A.λy : B.x prend un objet de type A (appelé ici x) et renvoie un objet de type B -> A (ici la fonction constante λy : B.x), ce qui en fait un objet de type A -> (B -> A).
En terme de programmation, le type représente le comportement de la fonction, tandis que le lambda-terme est une implémentation particulière.
D'un point de vue logique, un type est un énoncé logique, par exemple le type A -> A correspond à l'énoncé "A implique A", et le lambda-terme correspond à une démonstration constructive de cet énoncé.
Pourquoi parles-t-on de lambda calcul non typé ?
Le lambda calcul non typé est la forme la plus simple du lambda calcul, par exemple λx.xx (fonction qui prend un argument et retourne le résultat de l'argument appliqué à lui même) est un terme qui ne peut pas être simplement typé.
Les règles pour typer un terme sont assez intuitives : si x est de type A et u de type B, alors λx.u est de type A -> B (prendre du A et faire du B). Si u est de type A -> B et v est de type A, alors uv (appliquer u avec l'argument v) est de type B.
On peut se convaincre que selon ces règles λx.xx ne peut pas avoir de type.
En lambda calcul typé, les termes correspondent à des programmes qui terminent toujours, ce n'est pas le cas en lambda calcul non typé. Par exemple, l'exécution de λx.xx avec lui-même en argument va boucler indéfiniment.
Je me demandais aussi quel lien il y avait entre la theorie des types et le lambda-calcul, mais ça m'a tout de même l'air très différent.
sinon, le lambda-calcul type est extrêmement faible et loin d'être turing-complet.
En fait Mitch parle plus particulièrement du lambda-calcul simplement typé, qui est effectivement plus faible que les machines de Turing. On peut considérer des extensions qui sont toujours typées et qui soient aussi puissantes que le lambda-calcul non typé (qui est lui effectivement équivalent aux machines de Turing). C'est en fait ce qu'on fait pour créer un "vrai" langage de programmation fonctionnel fortement typé : on rajoute une manière de créer des récursions non-bornées qui reste correctement typées. Au contraire, dans la théorie des types dont parle la vidéo (qui est plus puissante que le lambda-calcul simplement typé), on ne rajoute pas un tel opérateur car ça rendrait la théorie incohérente. Mais ça n'empêche pas que la théorie nous permette de parler de toutes les fonctions calculables, même si en pratique on ne peut pas toutes les construire dans cette théorie...
Je comprend mais alors, strictement rien à tes vidéos. J'ai une vraie allergie aux maths, mais tes vidéos sont tellement travaillées, bien ficelées, avec un bon montage et un très bon son, je sais pas j'adore les regarder et les re-regarder^^
En tous cas, du très beau travail !
Si si ! ça me fascine ! hahahaha ! encore une très bonne vidéo ! la série sur l'infini est parfaite ! Merci pour le lien d'Andrei Bauer. En quelque sorte la conclusion est que si une fonction est constructible au sens intuitionniste alors elle sera continue, les jolis contre-exemples étant construits à coups de tiers exclus. Résumé par la jolie formule d'Andrej : “It ain’t a function if it can’t be computed”.
Même si j'ai commencé à lâcher vers 9/10 minutes, cela vaut vraiment le coup de te suivre. J'ai bien "senti ce qui t'a séduit dans cette théorie des types". Et en effet cela a l'air assez élégant, et Dieu sait que les scientifiques aiment l'élégance ! Donc GJ, et merci encore pour tes vidéos.
Génial, je suis informaticien mais j'ignorais que de tels idées existaient. J'ai retrouvé les principes qui initiait toute la POO (Programmation Orientée Objet). C'est une bonne base théorique pour suivre son étude de SmallTalk, Java ou Python.
Très bonne vidéo, je suis en première et je te suis toutes les semaines, j'avoue que je dois m'accrocher pour tout bien saisir mais tu es assez clair et du fait du bon boulot ! Continue comme ça !
Je suis complètement paumé. Mais ça a l'air passionnant :D
Merci !
On est sur de la vulgarisation mais de très haut niveau, je vous tire mon chapeau.
Petit teasing sur les éléctions, système de vote, ta recherche au GERAD... que du bon ! :D Je vais enfin pouvoir comprendre vraiment ce dont il s'agit... :)
symbole TRIPLE égal donc *=* est un double égal, donc *-* est un simple égal donc une soustraction est une égalité ! oh mon dieu donnez moi la médaille Fields
:P oui je troll , en réalité va falloir que je regarde a nouveau la vidéo x)
mdrrrr perso c'est le truc que j'ai compris dans la vidéo mdr
=== est strict au sens ou les deux choses comparées sont de même construction.
Ce que j'ai compris (?), très grossièrement, 3x2 n'est pas === à 2x3 bien que les 2 donnent 5 en terme de nombre mais on n'y est pas arrivé de la même façon.
En informatique on utilise aussi === mais c'est pas vraiment pareil, bien que ça vérifie une équivalence stricte de comparaison soit de booléens, soit de nombres qui pourraient être en texte. Comme 0 == false (vrai) et 0 === false (faux car on compare un nombre à un booléen bien que les 2 ne valent "rien") ...
C'est des congruences ;)
punaise ma connerie qui fait popper un message constructif :D
3x2 = 5 ?? ^^
c cool que t'aies expliqué le fait que toutes les fonctions sont continues si on a que toutes les fonctions sont calculables.
C est sympas mais je commence à en avoir un peu marre des bases axiomatiques différentes, ce serais bien si tu faisais des épisodes sur des thèmes différents (sans pour autant lâcher les épisodes sur les axiomes) , ou si tu faisais une "séance de TP" comme dans le dernier épisode hardcore, pour qu'on comprenne mieux comment on manipule les objets.
La grammaire n'est pas vraiE, elle est avantageuse ^^
(Coquille dans ta citation de Poincaré ;) )
Sinon, super vidéo, merci !
Haha
J'ai un point de vue assez différent sur ces questions.
La récursion est à la base de beaucoup de paradoxes (l'ensemble de tous les ensembles doit se contenir). Pour éviter ça, on peut avoir envie de « stratifier » les choses en définissant des ensembles de niveau n+1 comme des ensembles qui ne contiennent que des ensembles de niveau ≤ n.
Prenons un point de vue informatique. Si on a une fonction f, il est peut probable que f(f) ait du sens. On peut donc vouloir interdire ce genre de chose. Pour cela, on introduit la notion de type. Par exemple on va dire qu'une fonction f qui donne la longueur d'une chaîne de caractère est de type chaîne de caractère -> entier. Ainsi, si on essaye de calculer f(vrai), on pourra détecter directement qu'il y a un problème car vrai n'est pas une chaîne de caractère.
Si on fait un truc très basique, on a des éléments de base qui ont un type (vrai est de type booléen, 12 est de type entier). Et si x est de type A (noté x:A) et M:B alors la fonction qui à x associe M est de type A->B. Ce genre de chose interdit un objet de la forme f(f). En effet, si on essaye de calculer le type de f, clairement comme est est une fonction f est de type A->B. Mais l'argument est f. Donc A=A->B et cette équation n'a pas de solution.
Le problème, c'est que ce système de typage n'est pas assez puissant. Par exemple, pour calculer la longueur d'une liste de machin, on se moque des machins. On aimerait n'avoir qu'un programme pour cela. Or avec ce système, on doit avoir un programme différent pour une liste d'entier, une liste de réels… On essaye de construire des systèmes de types plus évolués qui garantissent toujours la terminaison du programme mais qui sont plus souple. On a donc des systèmes de typage polymorphes. Une fonction peut être de type liste(A)->entier dans lequel A est un type quelconque. Le polymorphisme est quelque chose de très important parce que cela permet la réutilisabilité des programmes. On n'a pas besoin de recoder 40 fois la même chose.
Déjà là, on peut remarquer quelque chose d'amusant. Si on a une fonction f de type A->B et un objet x de type A, alors f(x) est un objet de type B. Ça ressemble furieusement au fait que si on a une preuve de A->B et une preuve de A, alors on a une preuve de B. Idem, si on a un objet x:A et un objet y:B, alors le couple (x, y) est de type A*B. Ça ressemble furieusement au fait que si on a une preuve de A et une preuve de B, alors on a une preuve de A et B. Une union (comme en C par exemple), c'est un ou…
On peut donc interpréter ces types comme des propositions logiques et les programmes comme des preuves de ces propositions. On va dire que c'est un point de vue matheux sur ces objets. Mais les propositions qu'on peut exprimer sont assez bébêtes. On ne peut notamment absolument pas faire de récurrence. C'est un peu le but pour éviter les paradoxes mais on aimerait quand même.
Il y a toute un champ de la recherche en informatique qui s'est intéressé à ce problème. Et dans certains système comme COQ, on peut faire de la récursion, mais seulement dans certains cas. Et le système de type assure structurellement la terminaison du programme, ou, ce qui est équivalent, si on prend un point de vue matheux, qu'il n'y a pas de paradoxe. Certaines personnes ont déjà démontré de vrais gros résultats dans COQ (le théorème des 4 couleurs ou le théorème de Feit-Thompson).
On pourrait déjà sans doute refonder toutes les maths juste dans un système comme COQ. Mais un élément clef des maths, c'est la réutilisabilité des notions. Si on a construit les entiers de deux façons différentes, le matheux n'aura aucun problème pour dire qu'un entier, c'est un entier et point barre. Il utilise une forme de polymorphisme très évoluée. Mais même si COQ est déjà très polymorphe, il ne l'est pas assez. C'est ce qui a conduit Voevodsky à proposer l'axiome d'univalence qui serait, selon lui, LA bonne notion de polymorphisme utilisée par les matheux. En ajoutant cet axiome à la théorie des type, et en touillant avec un peu d'homotopie, on obtient une théorie qui serait LA bonne façon de refonder les maths.
En fait, ce qui est très amusant, c'est qu'on peut utiliser ce formalisme pour programmer.
Par exemple,si on démontre le théorème: pour tout type t ordonné, il existe une fonction de tri des listes d'éléments de type t. Alors comme la preuve est constructive, on peut extraire automatiquement un programme qui réalise ce tri. Et ce programme est certifié sans bugs.
Il y a donc deux aspects duaux de cette approche. D'un côté, on peut voir tout ceci comme un moyen de faire des maths de telle sorte qu'un ordinateur puisse vérifier qu'on ne s'est pas trompé. Mais on peut aussi voir ça comme une façon d'obtenir des programmes dont on est sûr qu'ils font bien ce qu'on veut et qui ne contiennent pas de bugs.
pourrais-tu refaire une ou plusieurs vidéos sur la théorie des types, s'il te plaît ? Je suis très intrigué par cela !
Très bonne vidéo !
ça mériterait un épisode hardcore pour aller un peut plus loin.
ça vient ;)
Excellent comme tjrs
Il me faut ce livre !! Ce sera ma Bible à moi ♥
Tu as fini par le trouver ? Je suis également intéressé par ce livre ^^
Eh bien je viens de voir que Lê a mis un lien pour se procurer le livre dans la description de sa vidéo.
Désolé ^^'
Bonne journée.
Très bonne vidéo comme d'habitude ! C'est très intéressant de pouvoir approcher cette autre conception des mathématiques. J'aimerais cependant faire une remarque. Je suis plutôt dérangé par ce coup de "pied de biche", pour en quelque sorte "forcer" l'adhésion à l'intuitionnisme. Je parle ici très personnellement, je tiens à le préciser. Tu présentes un peu l'objet, comme s'il devait y avoir une "bonne" manière d'appréhender les choses, alors que pour moi elles sont complémentaires. Il s'agit là pour moi des valeurs profondes de la science, l'ouverture au champ des possibles. Même si je reste platonicien convaincu, je suis intéressé par l'approche intuitionniste étant donné qu'elle ouvre sur un autre aspect des mathématiques, comme tu l'as expliqué dans ta précédente vidéo. Je rajouterai même que le fait de pencher à l'un ou l'autre aspect de la pièce devrait dépendre uniquement du ressenti de la personne face aux choses et non de la manière dont on lui a enseigné.
En remarque notemment à ta première réponse aux commentaires, j'ajouterais que la théorie des catégories et particulièrement la théorie des topos permet de travailler de façon intuitonniste. L'avantage étant de pouvoir se rattacher facilement aux reste des mathématiques dans le langage catégorique.
t vrmt le best toi
en somme les mathématique et la programmation fusionner en un seule concept
c'est plutôt simple je trouve, vue que c'est exactement ce genre de problème qu'on y
rencontre (en prog) avec le même niveaux d'abstraction (surtout en langage haskell)
C’est l’idée ☺ Après, le système de types d’Haskell reste assez basique (les types dépendants n’existent pas (il existe des modules permettant d’en ajouter un support partiel, certes, mais ils ne sont pas complets), pour ne citer que le plus évident des exemples (à noter tout de même que pour un langage de programmation, Haskell est très bien placé question gestion des types)). Les types homotopiques ajoutent encore plus à la complexité relative de la logique. Mais sinon, oui, l’idée est là ☺
Je connaissais ce bouquin et cette théorie et avait hâte de m'y plonger, mais tu y as mis ton intuitionnisme et ça m'a un peu refroidi :P
Quant à l'insécable continuité de la droite réelle constructiviste, elle pique certes ma curiosité... Mais comme une curiosité ;P
...bon.... il faut....doliprane....je crois... j'ai pas le niveau.. :(
Ces mathématiques constructives sont très intéressantes, j'aimerais beaucoup les étudier !
En revanche, elle semblent singulièrement manquer de Puissance...
Absolument pas. Si tu veux démontrer un théorème classique T dans un cadre constructiviste, il te suffit de prouver le théorème T': Tier exclu et axiome du choix et tout ce que tu veux -> T.
Oui évidemment mais c'est strictement équivalent à la logique classique, donc sans intérêt.
@@MagicSerwyn Ce n’est pas sans intérêt car ta logique est alors constructible : tu peux extraire toutes tes prevues en une fonction prenant un argument de type A → A \/ ¬A (l’axiome temporairement supposé) et renvoyant ce que tu as démontré. Le fait de pouvoir extraire les preuves (et donc d’obtenir son contenu calculatoire) est un atout majeur : tes preuves peuvent se transformer en programme.
Bon, exécuter ces programmes est assez compliqué parce que construire un élément de type A → A \/ ¬A est impossible en logique intuitionniste (sous couvert de cohérence de la logique). Pourtant… elle reste possible dans des langages de programmation modernes. On pourrait par exemple bricoler une fonction qui étant donné A sauvegarde l’environement courant et renvoit quelque chose qui prétend être de type ¬A. Il faut savoir que ¬A, c’est pareil que A → Faux. Autrement dit, c’est une fonction qui ne termine pas. La fonction que l’on peut renvoyer reçoit un A, par contre : au lieu de terminer, elle pourrait réinvoquer l’environnement sauvegardé (au moment où on demandait de renvoyer soit A, soit ¬A)… sauf que cette fois, elle a bien reçu un élément de type A ! Bon, c’est difficile d’expliquer tout cela dans un commentaire TH-cam, mais en gros, cela correspond à la réalisabilité classique. Et c’est super cool : dans ce cadre (en quelque sorte basé sur la logique constructiste), on peut calculer avec de la logique classique.
Je te suis depuis le début, et je trouve que la série sur l'infini est très complexe par rapport à la relativité. Ou peut-être moins ''vulgarisée'' ?
J'espère que ta prochaine série sera un peu plus ''parlante'' à mes yeux !
Merci pour tout ce beau travail en tout cas !
EDIT : je viens de voir ton petit mot de la fin ! ;) J'ai hâte maintenant ..!
Bonjour je m'appelle Mossa Assibit Eleve Ingenieur Statisticien Economiste à l'Ensae de Dakar j'adore vos videos de vulgarisation et je voulais vous demander si pouvez prendre un peu de temps pour nous faire une serie des videos sur la theorie de la mesure tres utile pour les ingenieurs Merci et je vous encourage à continuer sur cette lancée vous donnez envie de ne faire que des maths
Salut Lê est ce qu'à ce jour un résultat important a été trouvé avec la théorie des types et qu'on arrive pas à montrer avec les autres théories.
Ca sent la série sur les statistiques ou les probas ou je sais plus quoi...
Le fameux second choix qu'on avait quand on avait voté entre l'infini et autre chose :P ! Le fameux thème qui nous a couté une vidéo sur les différents systèmes de votes il me semble (c'est pour ça que quand t'as dit "Quelque chose d'actualité" ça m'a mit la puce à l'oreille ;)
En tous cas c'est une excellente vidéo: comme d'habitude j'ai du mal à comprendre mais c'est justement ça qui est plaisant
Et c'est justement le fait d'observer ces monstres mathématiques qui n'ont rien d'intuitif que je trouve passionant en fait
Vu que je suis passionné par l'informatique, je sens que je vais m'intéresser aux mathématiques constructivistes pour voir ;)
D'ailleurs, j'ai une petite question...
Pourquoi ne pas faire la fonction f(x) = 0 si x > 0 sinon f(x) = 1
Si le si n'est pas vérifié, c'est le sens propre du mot sinon qui ne laisse pas le choix d'une autre possibilité non?
Et si le si est ni vrai ni faux ?
On applique le sinon quand on sait que c'est juste pas vrai sans de savoir que c'est faux?
Bah honnêtement je ne cherche vraiment pas à mettre en doute cette logique, je veux surtout le comprendre et pour cela je cherche des limites jusqu'à ce que je me convainc :/
Tu fais bien :)
Le problème, c'est que tu ne sais pas forcément si x>0 est indécidable.
Il y a des théorèmes qui montrent qu'une fonction est vraiment une sorte de boîte noire dont on n'apprend pas forcément grand chose en lisant le code : images.math.cnrs.fr/Que-calcule-cet-algorithme.html
Est-ce la même chose que la Category Theory? Sinon comment ça s'y compare?
De mémoire, on perd l'unicité de la droite des réels en logique intuitioniste : on peut toujours prouver tout plein de choses sur eux, mais on ne peut pas montrer qu'il n'existe qu'une structure (à isomorphisme près) qui satisfait les axiomes des réels ☺️
Vidéo sympa. Vous ne présentez que les définitions inductives (et ça se comprend bien, vu que c'est déjà bien assez compliqué ☺️) et non les définitions coinductives : en un certain sens, on peut toujours manipuler l'infini en logique intuitioniste… il faut juste faire attention à ce que « en un certain sens » signifie ! 😁
À noter aussi que malgré la citation initiale sur la théorie des types homotopiques, la vidéo ne présente en fait que des idées beaucoup plus anciennes. On peut voir dès 1989 dans le papier de Frank Pfenning et Christine Paulin-Mohring intitulé « Inductively Defined Types in the Calculus of Constructions » des notions très proches de celles actuellement présentes dans Coq, sans avoir besoin de parler d’homotopie. Bon, le papier est un petit peu daté maintenant, mais il se lit très bien pour qui a déjà lu des papiers du domaine (ou manipulé Coq, au choix). ☺
La théorie des types homotopiques va beaucoup plus loin : tout ceci restent de très bonnes lectures ☺
J'ai eu du mal à suivre la vidéo mais de mon côté, je vois qu'il est très intéressant de comparer le = et le 3= ("Triple égale") à ce qu'on trouve en Développement Info.
Le 3= est une égalité qui affirme qu'en tout point, (valeur et type) les deux variables sont identiques. Alors que = est une égalité des valeurs. Je pense que c'est plus via ce raisonnement qu'on peut saisir plus simplement la différence entre une "égalité propositionnelle" et une "égalité définitionnelle"
Youpi je passe 2 fois dans les commentaires ! Par contre ça se prononce foumil (il faut pas prononcer les O ouai je sais c'est bizarre :p)
Et vidéo super méga intéressante comme d'habitude ^^ continu comme ça c'est génial !
"C'est vrai puisque beaucoup de gens y croient". C'est un axiome, ça ? Il me semble bien que Gandhi a enseigné que ce n'est pas parceque l'erreur est répandue qu'elle devient vérité.
Si on n'avait pas d'axiomes, on pourraît pas faire de math, malheuresement...
J'ai une question... existe-t-il une version de ce livre en français ? (si oui, pas trouvé sur les internets :-) ). Si non, ça me motive assez bien de le traduire (la licence cc le permet et ce sera une motivation pour essayer de comprendre cette théorie).
Alors ?
@@dappermink j'ai un peu laissé tomber par manque de temps... On devrait avoir plusieurs vies pour pouvoir faire tout ce qui nous motive (ou alors vivement la pension 😉 )
@@michelthayse5928 Tristement d'accord : (
Y'a pas un lien entre le problème P=NP et la logique intuitionniste et la logique constructiviste?
Les fondations mathématiques !!!
Petite question, je suis en MPSI et j'aimerais faire mon TIPE sur la théorie homotopique des types et notamment son lien fort avec l'informatique et la vérification informatique des preuves. Est-ce un sujet trop ambitieux pour un élève de sup ?
+Eusaebus la théorie homotopique des types, oui, je pense que c'est trop ambitieux. Mais la théorie des types, c'est peut-être jouable ;)
Je te conseillerais de commencer à lire le livre et voir jusqu'où tu arrives à aller. Je sortirai aussi un épisode hardcore jeudi prochain et tu pourras avoir un ressenti
+Science4All (français) Merci beaucoup pour ta réponse. J'attends du coup avec impatience ton épisode hardcore !
Je me trompe où avec les briques proposées, il est impossible de créer la fonction qui va de N vers {A,B,C} et qui vaut A pour les multiples de 3, qui vaut B pour les non-multiples de 3 pairs et qui vaut C pour les non-multiples de 3 impairs (impossible de construire l'image par récurrence, car tantôt un multiple de 3 est suivi d'un nombre pair, tantôt il est suivi d'un nombre impair) ?
Simple question, si les math constructive sont conçus pour l'informatique permettrait-elle de résoudre l'hypothèse de rieman?
+Anthony De macedo non. A priori, les maths constructives ont moins de chance de prouver l'hypothèse de Riemann
Une fonction est elle bien quelque chose a qui on donne une input et qui nous sort un output comme un programme ?
Perso je fait de l'info et j'ai toujours vus une fonction comme ca mais j'ai peut être pas bien compris un truc
Y a des gens en théorie des ensembles qui croient qu'une fonction E -> F est un sous-ensemble G de ExF tel que pour tout x de E, il existe un unique y de F tel (x,y) appartient à G... Et du coup, ils arrivent à construire des fonctions non calculables.
Bonjour, sait tu si en loguique intuitionniste les fonctions suivantes sont définissables et/ou dérivables :
0 puissance x
racine carrée
exponentielle
valeur absolue
Exponentielle et valeur absolue ne posent aucun problème.
La racine carrée est un peu plus subtile car on doit pouvoir vérifier x≥0. Mais du coup, on peut la définir pour l'ensemble des réels dont on dispose d'une preuve que x≥0.
0 puissance x, je ne suis pas sûr de comprendre ce que ça signifie, notamment pour x≤0...
Science4All (français) J'essaye de fabriquer la fonction f qui donne 1 pour les x positif ou nul et 0 pour les x négatifs avec cette logique.
Si on a à disponibilité l'égalité 0^0=1 et pour x>0, 0^x=0 alors on peut poser une fonction sgn de R dans R tel que pour tout x réel elle donne :
sgn(x)= 0^|x| + x / ( 0^|x| + (1-0^|x|)*|x| )
c'est à dire qui donne 1 pour tout x positif ou nul et -1 pour tout x négatif
ainsi on peut construir f de R dans R par :
f(x)=0^(1-sgn(x))
Cette deffinition de f n'étant pas réalisé par morceaux mais visiblement non continue, existe t elle ?
sinon, je suppose que c'est 0^0=1 qui pose problème. On pourait supposer que 0^0=0 mais le resonnement reste viable
( il suffit de remplacer 0^|x| par 1-|x|^0 )
Donc si f n'est pas definissable cela veut-il dire que 0^0 est un probleme de ces math intuitionnistes ?
Utilise Géogébra pour visialisé tes fonctions et les modifié par exemple :
f1 = 0^x ; f2 = 0^|x| ; f3 = |0^x| ^^
exemple que j'ai fait : www.geogebra.org/m/FCKbxChn
j'adore ces vidéos j'y comprend rien leurs je les adore
la théorie des jeux et les systèmes de vote \o/
dans cette théorie, le théorème d'incomplétude est il valide ?
est se qu'il a un sens ?
Oui ! Mais comme je l'ai dit dans l'épisode 22, ce théorème ne pose aucun problème métaphysique à l'intuitionniste ;)
Honnêtement ça demande de bien relativiser mais j'aime bien :) je me demandais simplement : est ce qu'il existe une règle du "quart" exclu en intuitionnisme ? Du genre quelque chose est ou vrai, ou faux, ou on ne sait pas et c'est tout.
Oui ! La quatrième possibilité est qu'un théorème soit vrai et faux... et ça, c'est la merde ! Ça veut dire que la théorie est inconsistante...
Ca m'embrouille cette histoire de double égal et triple égal après avoir fait des congruences...
Est-ce que ces deux théories (ZF et théorie homotopique) pourrais être isomorphe? Ou bien je suis en plein délire?
+Big Eyes l'intérêt justement de la théorie des types, c'est qu'elle n'est pas isomorphe à ZF, tout en proposant des objets et des structures très naturelles
C l'ensemble des nombres complexe est clos a prouvé Monsieur Gauss.
Les maths intuitionnistes confirment elles la validité du theoreme qui fonde l'algebre.?
Pour le rapport avec l'actualité... tu vas parler systèmes de votes ? ou pas du tout ?
(dialogue de chatons prévu ?)
Que signifie le signe ressemblant à un grand pi (par exemple à 9:05 en bas de l'écran)? Merci!
C'est un pi majuscule, normalement c'est pour un "grand produit" (dans le sens ou le sigma majuscule serait une "grande somme" (je ne suis pas clair, non?))
Mais là ça n'a pas vraiment l'air d'être le cas :\
Ici ça correspond à un "pour tout" ∀. Pour voir le rapport intuitif avec le grand produit, il faut se rappeler que ∀ x, P x donne pour chaque x une preuve de P x, c'est donc comme un grand produit de toutes les preuves de P x. Et pour le grand sigma, c'est en effet une somme qui correspond à un quantificateur existentiel, un élément de la somme ∃ x, P x est un élément (a, P a) pour un certain a. Le type somme est en gros la somme (disjointe) de chacun des types P x.
Peut on construire une théorie ou système mathématiques sans axiomes? Quelque soit la réponse j'aimerais savoir pourquoi .
+Edouard Menigault En gros, oui, les axiomes sont toujours nécessaires. Il s'agit de fondations sur lesquelles la théorie est construite.
question ! La théorie des type peut elle être générale ? je veux dire : peut-on apprendre de nouvelle choses à partir des fonction propositionnelles ?
Tout ce qui est prouvé sans le tier exclus peut être prouvé avec (il suffit de l’ignorer). Ce n’est pas là que réside la force de la logique intuitionniste. Ça force réside dans la possibilité d’interpréter les preuves comme un contenu lui-même calculatoire. Ceci donne un modèle naturel à la logique (qui en plus peut servir à faire tourner de vrais logiciels !), alors que la logique de ZFC demande des modèles plus complexes. Certains diront que cela nous permet de mettre plus de confiance dans les axiomes intuitionnistes. Une autre manière de le dire, c’est qu’il est assez compliqué de traduire les maths habituels dans ZFC, et que les traduire dans une logique constructiviste est comparablement plus simple : cela aide grandement à savoir si on a « le droit » de définir certains objets au milieu d’une preuve. (À noter que tout cela sont globalement des affaires de goût : il est parfaitement acceptable de préférer une logique à une autre.)
Y a t-il une version française du livre ?
pas à ma connaissance...
Le fait que tu parles de la "représentation" (=définition?) de PI en logique intuitionniste incite à la proposition suivante pour "représenter" une fonction discontinue.
On connait des suites de fonctions continues f_n convergeant simplement vers une fonction discontinue f, pourrait-on passer par (f_n) à la manière de PI pour représenter f : la version intuitionniste de f serait alors une fonction donnant un moyen de calcul à tout erreur près en chaque réel.
Quel est le problème de ce raisonnement naïf ? Peut être que l'on pourrait montrer que l'on ne peut connaître l'erreur d'approximation au rang n, je ne sais pas trop.
Ce raisonnement utilise un passage à la limite… ce qui est typiquement non calculable en général en logique constructiviste. Pour pouvoir le calculer, il faudrait pouvoir savoir quand une décimale (si on utilise une représentation par décimale) est stabilisée. Le problème, c’est qu’il est assez difficile de donner un tel moyen de calculer la stabilisation sans empêcher le phénomène même qui génère la discontinuité. Bien essayé ☺
(C’est un argument assez informel : c’est bien entendu plus compliqué que cela formellement.)
Ca a pas mal rapport au Lambda Calcul ou bien je me trompe ? Tout est fonction, on définit tout par des "briques" très primaires, avec des constructeurs et de l'induction, etc.
bah en même temps il parle de machine de turing... tu t'attendais bien à ce que le lambda calcul ne sois pas loin xD
Oui ! Le livre définit les fonctions via le lambda-calcul
Y a t ils de livres qui parlent de ça en français ??
T'as esquivé la question du 1/x à la fin pour la continuité de toute fonction réelle, et je vois pas comment faire le lien avec le fait que R est "insécable".
Sinon, excellente vidéo, c'est certainement la plus difficile de toutes celles sur l'infini !
La fonction 1/x est problématique. Imagine que x soit donné par une machine de Turing qui n'en donne que des approximations successives. En particulier, imagine que tu sois incapable d'affirmer si x est strictement négatif, nul ou strictement positif. Que vont donner les approximations successives 1/x ? Elles vont donner n'importe quoi, et ne convergeront pas vers un nombre réel.
Science4All (français) Ah d'accord, merci. Je raisonne pas assez en machine de Turing ^^
Merci pour ta réponse aussi rapide en tout cas :D
À vouloir parler très rapidement de ce qui est très complexe et inhabituel, tu finis par faire des vidéos incompréhensibles.
. Imagine toi regarder cette vidéo avant que tu lises ce livre...
Dire que je n'ai pas tout compris était un doux euphémisme... C'est des maths de très, très, très haut niveau tout ça.
Heureusement, c'est bientôt fini. On va bientôt aborder des sujets beaucoup plus terre à terre ^^
TheBaroker salu piero
on est bien loin de mon BEP MSMA la ^^
deuxième vidéo où j'ai rien compris en fait :/ (la première etant les hard cores)
Vas-tu nous parler de la théorie des jeux ? :)
Victor Santet Sûrement mais dans une autre série. Au début de celle sur l'infini il nous avais laisser le choix entre 3 série potentielle : celle sur l'infini, une sur la théorie des jeux et une autre dont je ne me souviens pas le thème
+Enguerrand de Gentile l'autre c'était les nombre.
A mon avis la théorie des jeux c'est le prochain thème (vu qu'on peut parler du système d'élection, qui est pas mal d'actualité :) )
Oui je m'en souviens, c'est pour ça que je lui demande s'il va s'agir de la théorie des jeux ;) Personnellement, j'aimerais beaucoup !
Victor Santet Pareil :)
mdr ça se voit que ce commentaire date
Je ne sais pas si Poincaré employait le mot "avantageuse", je crois qu'il employait le mot "commode",
Pour la thèse Church-Turing, vaut mieux prendre une position minimaliste : nul besoin de dire que l'univers serait calculable en soi, il suffit que ce soit ce qu'on peut théoriser en physique qui le soit pour que ce soit fondamental. Et dès lors que la physique est science expérimentale, alors elle tend au constructivisme, elle produit des expériences, des modèles, des mesures déterminées qui sont critères de physicalité par rapport à la pure théorie. C'est donc d'abord une interaction cognitive entre nous et l'univers qui est possiblement toujours calculable, le scientifiquement pensable en sciences expérimentales, ce qui est l'essentiel... pour les scientifiques.
Pour le reste, il s'agit d'options métaphysiques voire poétiques, même si il y a des métaphysiques classiquement plus en accord avec ces thèses, par exemple un déterminisme à la Spinoza qui avait quasiment une théorie qualitative des types pour sa description du monde (ce qu'il appelle les "Attributs", extensio ou cogitatio, dont sa conception rappelle le matériel/logiciel, l'univers vu comme machine productive expérimentable par l'humain en deux modalités hétérogènes, un peu comme on peut regarder le fonctionnement d'un ordinateur en électronicien ou en programmeur, un même effet expliqué par des échanges électrique dans le matériel ou par le programme qui tourne).
"Toute fonction est continue" Voilà comment je me le représente:
Donc les images de réels par une fonction, ou en tout cas quand on la calcule n'est qu'une approximation qui semble être presque vraie? En disant ça une fonction qui n'est pas définie sur un intervalle I serait juste non-défini car l'approximation de l'image est fausse? En tout cas s'est comme ça que je le comprends de prime abord.
Si ce n'est pas vraiment ça tu pourrais l'expliquer un peu plus en détail.
Bonjour, je me demandais comment caractériser l'ensemble des R via construction et ce malgré son caractère dense et infini
On peut le faire par décimales : un nombre réel (entre 0 et 1 on va dire) est « équivalent » à une fonction de N dans {0;1;…;9} (c’est à dire, un ensemble avec aux moins deux symboles différents). Mieux, on peut le faire en binaire, on a alors une fonction de N vers un booléen. Bon, il y a plusieurs problèmes de représentations avec ça (voir le célèbre 0,99999… = 1), mais ça donne une idée : R = N → bool.
Une manière plus directe consiste à utiliser les axiomatisations algébriques de R sous forme de corps. Ça se fait aussi ☺
Merci infiniment monsieur ! Svp, est-ce qu'on peut avoir votre email ?
Je vois bien le Type N comme de l'ADN
Problème : Considérons un graphe G où les nœuds de G sont les vidéos de Science4All, et les arêtes de G correspondent aux liens qui renvoient vers d'autre vidéo de Science4All dans ces même vidéos. A quel type de graphe correspond G ? Vous avez 4 heures !
10:22 Je ne comprend pas dans quel sens comprendre la fonction, est-ce qu'on multiplie une égalité ? Non je ne pense pas . . .
Pareil
NanoStorm À ce que je vois le sigma remplace le "il existe" et le pi "pour tout", mais je ne comprend pas pourquoi . . .
Non c'est plus comme un produit cartésien en théorie des ensembles
Le Sigma est un produit (dépendant). Le Pi est une flèche (dépendante). Pourquoi ? Parce que, constructivement, la preuve d'une existentielle (exist x : T, P x) est une paire (v, p) où v est un habitant (élement) de T et p une preuve de (P t) --- on voit ici la dépendance: le type du second élément de la paire dépend du premier. Idem, la preuve de (forall x : T, P x) est une fonction qui prend un habitant (élement) t de T et renvoie une preuve de (P t) --- ici encore, on voit la dépendance.
Salut salut,
Je ne comprends pas vraiment à qui tu t'adresses. Tes vidéos sont super intéressantes, les sujets le sont aussi, mais une fois dans une vidéo, moi qui suis assez profane en math, je suis complètement largué... Sinon au niveau du montage et tout c'est top, félicitations, mais voilà une petite pensée pour les moins forts d'entre nous ce serait merveilleux.
Bonne continuation!
pq pas utiliser =_{def} a la place d'utiliser le signe pour la congruence ? o.O
C'est une notation d'informaticien, ils utilisent '%' pour la congruence vu qu'on a pas crée de touche '≡' sur le clavier.
Question 1 : Quelle différence de sens ou d'utilisation tu vois entre les signes "=:" et le "triple signe égal" ?
Question 2 : Quelle définition donnes-tu à "fonction" sachant qu'il y a une certaine indétermination dans l'utilisation du terme, soit comme "application numérique", application ayant ses valeurs dans R, est donc pour tout antécédent ayant "une et une seule image dans R" lorsque restreinte à l'ensemble de définition de la fonction, soit comme un processus général de transformation qui a "au plus" un seul et unique résultat" ? Je te pose cette question du fait de l'importance apparemment de la notion de "fonction" dans les Mathématiques Constructives et du fait qu'il vaut donc mieux savoir de quoi l'on parle lorsqu'il s'agit d'un concept de base dans une théorie.
Question 3 : Tu parles "d'implication" mais il y en a de plusieurs ... types ; parles-tu de "l'Implication Intuitionniste", de "l'Implication Matérielle", voir de l'Inférence (implication à Prémisse donnée nécessairement Vraie) ? Et quelle différence, fais-tu toi-même entre "l'Implication Intuitionniste" et "l'Implication Linéaire" ?
Question 4 : Quelles différence voies-tu entre les "Types" de La Théorie Des Types" et les "Catégories" de la Logique Linéaire ?
En tout cas, Merci encore, Lê, pour ton Excellente Vidéo :)
TsuikoWillyil y a 5 jours
J'ai eu du mal à suivre la vidéo mais de mon côté, je vois qu'il est très intéressant de comparer le = et le 3= ("Triple égale") à ce qu'on trouve en Développement Info.
Le 3= est une égalité qui affirme qu'en tout point, (valeur et type) les deux variables sont identiques. Alors que = est une égalité des valeurs. Je pense que c'est plus via ce raisonnement qu'on peut saisir plus simplement la différence entre une "égalité propositionnelle" et une "égalité définitionnelle"
je pensais a autre chose j’étais entrain de pensé a la matière noir et l’énergie sombre, et bon je sais que ça n'a rien a voir mais quand même ! es que le problème ne serais pas fondamentalement plus simple que ce qu'on le crois ?! non parce que l'on dit ok la galaxie a t'en de masse t'en de matière ça capacité d'attraction est donc = a t'en PROBLÈME ça force de gravité n'est pas asse forte en théorie pour garder la galaxie t'elle quelle est la maintenant seulement bah elle est pas comme elle devrait l’être ... mais jetais entrain de me dire oui effectivement c'est un problème mais pas vraiment puisque si je dit que les corps sont tous rentré dans une sorte d’harmonie gravitationnel qui fais qu'il sont tous attiré les un des autres et qu'en faite l'on ne pas pas dire ok j'ai une masse qu'elle est ca force gravitationnel parce que bon je dit peut être surement de la merde mais ... il serait peut être plus judicieux de d’abord calculer toute les trajectoire des corps un par un voir qui est plus attiré a qui pourquoi chaque objet a ca trajectoire et faire un putain de calcule d'un googolplex de mètre mdr et la peut être nous serons fixé ... en faite je suis une bite on est d’accord mais ce que je veux dire pour essayer d’être claire je pense pas qu'il suffise de mesuré la masse de notre galaxie et de mesuré ça force de gravitation pour avoir le droit de dire ce n'est pas normal quelle soit comme ca elle ne devrais pas l’être ... ce que l'ont appel énergie sombre c'est peut être simplement le fais qu'on cherche a regarder le comportement d'un gaz et non pas de comprendre ce que font simultanément l'ensemble des particule une après l'autre les unes par rapport a toutes les autres ... CES SUREMENT STUPIDE CE QUE JE DIT (surtout que mon exemple est parlent mais absolument pas vrais puisque pour déterminer le mouvement d'un gaz il vos mieux regarder l'ensemble des particules et non pas une c'est impossible) ALORS SI TU VEUX ME DÉTRUIRE TE GENE SURTOUT PAS MAIS EXPLIQUE MOI POURQUOI JE DIT DE LA MERDE STP !
(a ~ b) ~ (a = b)
SPOILER x)
Tout ça c'est passionnant! Mais cette construction des types me paraît un peu naïve... n'y a t'il pas de risque de voir surgir un gros paradoxe des enfers (un peu à la Russel :3)
Autre chose, si bon nombre de propriété de la logique intuitionniste ne sont pas décidables, peut on quantifier cette décidabilité? A l'aide d'une fonction qui vaudrait 1 si la propriété est constructiblement (oui, j'invente un mot) vraie et 0 si elle est constructiblement fausse?
Je pense que la fonction que tu décris ne peut pas exister, que faire si un propriété est ni constructiblement (oui, je réutilise ton mot ;) ) vraie ni constructiblement fausse ? Et ouais on a pas le droit au tiers exclu
Justement elle serait partiellement constructible avec des valeures entre 0 et 1 comme une probabilité
Pour le paradoxe de Russel, j'ai bien peur que le tiers exclu soit central : soit X l'ensemble des ensembles qui ne se contiennent pas eux-mêmes. 1er cas il se contient lui-même : contradiction ; 2e cas il ne se contient pas lui même : ça plante aussi. Mais les intuitionnistes ont aussi le 3e cas : on sait pas et veut pas savoir (ni vrai ni faux), qui leur permet de s'en tirer.
Oui Russel ne marche pas mais qu'en est d'un autre paradoxe?
Bah, donne le moi ton autre paradoxe, et je te dis s'il est valide. :p
Je suis même à peu près sûr qu'en logique classique on n'arrive pas ) montrer l'existence non constructive d'une contradiction alors ...
Bonjour,
Encore une fois votre vidéo mets mon cerveau en ébullition. Continuez comme ça !
Concernant la thèse de Church-Turing, j'ai une grosse objection (qui est sans doute due à ma méconnaissance des machine de Turing) : il semble, lorsqu'on fait de la physique quantique, qu'il existe des opérations fondamentalement aléatoires, tout ce qui est lié à l'effondrement de la fonction d'onde. Est-ce qu'une machine de Turing est capable de générer ainsi de l'aléa ? Il me semble intuitivement que quelque chose de fondamentalement imprévisible est fondamentalement non-calculable...
Je sais qu'il existe d'autre hypothèses méta-physique sur la quantique, la rendant pleinement déterministe - ie virant l'aléatoire de cet effondrement. Cependant, si je ne me trompe pas, l'hypothèse d'un aléa fondamental est cohérent avec tout ce que l'on sait, et cette hypothèse a l'avantage d'impliquer un indéterminisme - et donc ce que ça implique sur une possibilité de libre arbitre. Comme ils disent dans la Tronche en Biais, c'est donc ce que j'ai choisi de croire - jusqu'à preuve du contraire.
A noter, qu'il me semble que l'indéterminisme intervient aussi à grande échelle (parce que la quantique, c'est pas spécialement applicable à notre échelle), via les considération de la théorie de l'information sur l'entropie ; pour le coup, je ne connais pas bien le sujet, je suis donc persuadé de dire au moins 80% de conneries (j'écris ici aussi pour qu'on me corrige). L'idée est que l'entropie est la quantité d'information qu'il faut pour décrire parfaitement un système, ainsi que (je crois que c'est équivalent) la quantité d'information que peut stocker un système. Ainsi, l'entropie de l'Univers étant croissante, il est impossible de décrire parfaitement l'état de l'univers au temps t+dt à partir de l'état de l'Univers au temps t : l'Univers ne contient tout simplement pas assez d'information au temps t pour ceci. Il faut donc que l'Univers "invente" sans cesse de la nouvelle information - ce qui est cohérent avec les considérations quantiques précédentes, l'effondrement de la fonction d'onde créant une nouvelle information en forçant un système quantique à "choisir" ou à "préciser" son état.
Bref bref bref, la thèse de Church-Turing semble intéressante, mais est-elle capable de rendre compte d'un Univers potentiellement partiellement indéterministe ?
... J'ai sinon d'autres réflexions qui me viennent sur votre explication de "toute les fonctions sont continues" (et là, je trouve votre argument parfaitement convainquant sur la force des maths constructivistes), en lien avec ce que je que j'avais mis en commentaire dans votre vidéo précédente sur les complétions en logique classique. J'essaierais d'organiser mes pensées si cela vous intéresse.
Vaste question... Il y a plusieurs réponses à apporter.
(1) Et si la mécanique quantique n'était pas aléatoire ? Certains physiciens croient encore en l'existence de variables cachées non locales...
(2) On peut modifier légèrement la thèse de Church-Turing en une thèse de Church-Turing markovien, où le calcul de la machine à chaque étape est désormais aléatoire.
(3) Il y a une version légèrement différente de la thèse de Church-Turing qui dit que toute machine physique ne peut calculer que des choses qu'une machine de Turing peut calculer. Or, les ordinateurs quantiques (ou "machines de Turing quantique") ne peuvent pas calculer ce que les machines de Turing classiques ne peuvent pas calculer : en.wikipedia.org/wiki/Quantum_Turing_machine
Pour le (1)... Je sais, mais il me semble que cette hypothèse n'est pas scientifiquement plus forte (ou moins forte) que l'hypothèse "dieu joue aux dés". C'était justement l'objet de ma digression : je préfère croire qu'il y a un aléa, un indéterminisme fondamental - jusqu'à ce que peut-être la science tranche en ma défaveur, ou en ma faveur.
Pour le dire autrement, mon objection n'est pas un problème de cohérence de la thèse de Church-Turing, mais plutôt que ses conséquences me font préférer une autre thèse tout aussi cohérente.
Pour le (3) j'ai vraiment du mal à comprendre la théorie des machines de Turing (et donc le lien wiki) ; je ne comprends qu'en surface.
Un truc qui m'échappe, c'est si la définition d'une machine de Turing quantique permet comme opération d'effondrer la fonction d'onde. Pour ce que j'en sais, sur les ordinateurs quantiques on tente d'éviter ça (conserver une superposition d'état impose d'éviter une décohérence) (au moins jusqu'à la fin du calcul ? Je suppose qu'à un moment, faut bien faire une mesure...), ça ne m'étonnerait donc pas que le formalisme des machines de Turing quantique ne permettent pas cette opération (ce formalisme ne décrirait donc pas ce que peut faire un système quantique, mais uniquement les opérations que l'on souhaite voir dans un ordinateur quantique). Et sur le lien je ne vois pas ce qui correspondrait à une telle opération...
...Or cette opération est justement au coeur de mon objection.
Le (2) enfin et convainquant, du coup je vais essayer de me renseigner.
C'est normal que je ne puisse pas cliquer sur les vidéos suggérées ?
Il vient de sortir la vidéo, ça va arriver
NanoStorm dacc
Est ce que ca implique que la preuve par l'absurde n'est plus valide ? C'est pas vraiment constructif comme preuve il me semble
Tout à fait, la preuve par l’absurde (c’est à dire (A → Faux) → A) est équivalente au tier exclu (A \/ ¬A) et est donc à banir en logique intuitionniste. Ça implique de repenser certaines preuves. Heureusement, pas de panique : le tier exclu est valide (et donc la preuve par l’absurde aussi) sur tous les types comparables. Autrement dit, pour continuer d’utiliser la preuve par l’absurde sur un type A donné, il suffit de montrer qu’étant donné a et b et type A, on peut décider si a = b ou non. C’est souvent le cas en pratique ☺
La théorie des types: c'est la théorie de la démonstration qui cherche à éliminer la théorie des modèles ^^ Tant qu'on reste dans le cadre intuitionniste ou dans le cadre finitiste de l'informatique: pourquoi pas. Ceci dit, tout ça sent la Position Latérale de Sécurité d'une partie des physiciens et des informaticiens face au grand malaise du théorème de Godel.
D'ailleurs, la fascination de OP pour les machines de turing traduit une mauvaise compréhension du 2nd Théorème de Turing et la différence profonde qu'il y a entre un calcul et une démonstration. Nous, nous savons démontrer: nous ne sommes pas des machines de Turing. Nous, nous manipulons des significations, nous ne sommes pas coincés dans une chambre chinoise. Notre vécu conscient est une durée, un continuum, pas une approximation sacadée de qualias discrets.
« Notre vécu conscient est une durée, un continuum » si le temps est granulaire, c'est une illusion de continu.
La géométrie pure est plus une soeur des mathématiques qu'une de ses parties.
que ce soit 1/x ou f(x) = 0 pour x =0 je vois un moyen de voir que c'est continue :
si les 2 foncctions sont tracer sur un feuille et que l'on la met a l'horizontale et que l'on s'aligne avec le plan de la feuille on voit les sur chacun des fonction les droite se prolonger / s'aligner :www.geogebra.org/o/ycYskdeR
Désolé de ma question qui peut paraître stupide mais je ne trouve jamais le résultat pour un calcul pourtant très simple:
10-10x10+10=? Je trouve plusieurs résultats
D'accord la multiplication est prioritaire mais ensuite fait on juste le calcul de gauche à droite? cad 10-100+10-> -90+10-> -80 ou peut on faire 10-100+10-> 10-110-> -100
la soustraction à la priorité apres la multication donc 10-100+10 ; -90+10 ; -80
(la soustraction n'est pas commutative)
Seb16120 elle à la priorité car elle est placé avant ou de façon plus général ?
parce qu'elle est à gauche ^^
*elle est non commutative et non associative
associativité : ∀(x , y , z) ∈ E^3, (x ✳ y) ✳ z = x ✳ (y ✳ z).
commutativité : ∀(x , y) ∈ E^2, x ✳ y = y ✳ x.
E : Ensemble
E^2 = ExE = Produit cartésien de 2 ensemble
E^3 = ExExE = Produit cartésien de 3 ensembles
Seb16120 oula commutative je comprends mais pas associative...dsl mais j'ai un niveau scolaire assez faible (tu devais t'en douter xD) en tout cas merci pour ton temps seb
Mais il y a de la disjonction de cas dans f (x) =1/x ??
après c'est sûr que quand on cherche une approximation pour x trop près de zéro ça va beuguer... Ça compte comme disjonction de cas (ou truc du même style )??
c'est un peu handicapant de faire une théorie où on peut pas utiliser la plupart des fonctions inverse/rationnelles/trucs comme ça...
non ?
Bon tu as aussi dit que c'est une théorie pour étudier les machines de Turing pas les nombres...
Comment on étudie une machine de Turing avec ça en fait ?
Edit En même temps si toi avec bac +beaucoup en maths tu comprends pas grand chose... C'est pas étonnant que ce soit ultra flou pour nous !
(ce commentaire est bien trop long en fait... pour ne rien dire...)
c'est très intéressant, mais je trouve téméraire de croire que l'univers est une machine de turing, étant donné la place du hasard, défini par l'absence de loi, autant que la somme complète de toutes les lois, comme dans le cas de la simple liberté. Ainsi, l'univers macroscopique, champ où la logique simple est suffisante, et certes prévisible, mais dès qu'on étudie des champs microscopiques où l'indéterminisme est un facteur d'action, la logique simple (ou légèrement améliorée) est insuffisante. Donc ce qu'il faut c'est une logique qui ne soit pas construite à l'intérieur du cadre des mathématiques dans le but de se prouver elle-même, mais opérationnelle dans les calculs indéterministes. C'est d'ailleurs amusant que ces cas aient été implicitement pris en compte par Gödel alors qu'il ne pouvait qu'à peine les imaginer. c'est à dire qu'il y a quelque chose au-delà de la logique intuitionniste. Mais bon, je dis juste ça comme ça, lol
Video hyper intéressante - j'ai une question de grossier personnage : est-ce que ce type de maths a abouti à des nouveautés transposables en physique - par exemple ?
En tout cas, la continuité des réels est vraiment superbe !
Et sur la question de la vérité des maths, ça me paraît une question mal posée - les maths ne sont pas là physique ni la philo...
19:10 désolé mais dans l'ensemble des machines de turing qui regardent tes vidéos admettons la fonction f(x)={"pas des matheu quoi" si x=0} X étant la fascination de chaque machine de turing qui te regarde ce que tu dis n'est pas vérifiable pour la même raison que tu explique à 17:40
Ce type est vraiment balaize. Ce n'est pas pour rien que l'on dise que ceux qui ont le type chinois sont supérieurement intelligents. Nous avons ici la démonstration de cette intuition car pour devenir fort en math, il faut bosser. Comme dans la théorie des types, le savoir, ça se construit, donc les chinois qui sont tellement plus vaillants que les autres, n'arrêtent jamais de construire et de bosser, par conséquent finiront par dominer le monde en tout et pour tout. CQFD
Salut Lê, et félicitations pour la qualité de tes productions. Tu parles trop souvent de la logique sans préciser que tu parles de la pseudo-logique mathématique. C'est dommage parce que ça renforce de plus en plus l'incompréhension épistémologique de la logique surtout parmi les plus scientifiques d'entre nous.
th-cam.com/video/ba4E6EMagj0/w-d-xo.html
10.000 € où je spoil ta décision dictatoriale -_-
Tu kaamelot et’tu bit coin
Théorie des jeux ? Théorie des jeux ???
Oui je pense, en plus je crois que c'était son sujet de thèse non ?
Tu fais co.me pastoi #palper tines
cette chaine devient trop perchée pour moi
First
La vidéo était bien partie, jusqu'à ce que tu parles du type "x=y" que tu ne définis pas vraiment, c'est très frustrant car à partir de ce moment on t'écoute simplement parler, sans trop rien comprendre... j'aurais aimé que tu rentres en profondeur dans le type (x=y) et donne des exemples, dommage.
J'aime bien tes vidéos en général, mais par moment tu j'ai l'impression que tu ne cherches plus à instruire mais à montrer tes connaissances.
Je fais ce que je peux en 10 minutes...
Il y a un épisode hardcore pour les détails :
th-cam.com/video/uV5W38TdWX0/w-d-xo.html
Oui je comprends, la vidéo est bien et m'a fait découvrir la théorie HoTT, c'est déjà ça! J'en ai vu aucune autre sur TH-cam dans ce format "straight-to-the-point".
Je suis curieux de savoir combien de temps tu as consacré à l'étude de ce bouquin pour avoir ces bases ?
J'avoue que je n'ai pas regardé l'épisode Hardcore, je me suis dit que si je ne comprenais déjà pas bien certaines notations (p.ex. sommes et produits de types) et constructions (exemple de construction d'un élément de (x=y)) alors l'épisode Hardcore serait imbuvable.
Toutefois, je jeterai un oeil au bouquin HoTT (du moins, l'intro...) avec ce mini bagage, je reviendrai certainement sur tes vidéos pour ressayer de creuser plus.
Je reconnais que tes vidéos sont très bien dans l'ensemble, j'ai tout un tas de sujets que j'aurais aimé voir vulgarisé car peu le temps de m'y investir si jamais t'es en recherche de sujets.... Selon moi, la partie questions est un peu trop longue, quand on lit certaines questions d'internautes qui sont inintelligibles... on a envie de se facepalmer à deux mains.
Magloire mac zott # b.liev