Les matheux sont dans la place - pt=prout

[corentintilde]

Bon j'ai une question bête, mais un "type" c'est quoi ? C'est du jargon d'informaticien ? C'est un méta mot pour désigner tout et n'importe quoi (un nombre, une addition, une proposition logique, un ensemble...) ?

[ducon]

En tant qu'informaticien, ce qui me gène avec la définition extensionnelle est que c'est une propriété indécidable. Je ne sais pas dire si deux fonctions sont égales en tout point, je sais juste passer de l'une à l'autre par une suite finie d'identifications f = h = ... = g d'où par transitivité f = g, ou par induction en démontant f et g en un nombre fini de petits morceaux pour vérifier qu'elles sont construites avec les mêmes morceaux dans le même ordre.

Si, parce qu’une fonction est une partie G d’un ensemble produit E×F qui vérifie ∀x∈E ∃!y∈F tel que (x,y)∈E×F.

Oui mais l'environnement ne fait rien pour t'aider à vérifier la consistance de tes règles. Tu peux écrire des raisonnements contradictoires sans problème. De ce point de vue ce n'est pas mieux qu'un bloc-notes.
Contraste ça avec Prolog ou Coq, où tu as un noyau minimal d'axiomes de la logique, tu peux aussi définir les objets comme tu le souhaites par dessus, mais le système ne te laissera pas écrire des choses contradictoires impunément.

À quel genre de contradiction penses-tu ?

Mais ça ne me dit pas explicitement quand est-ce que j'ai le droit ou pas de remplacer a par b et b par a. Ça sous-entend : il n'existe pas de contexte dans lequel remplacer a par b aboutisse à une contradiction ? Donc a et b ont des propriétés non contradictoires, mais est-ce que ça implique que a et b ont exactement les mêmes propriétés ?

Il n’y a pas de droit en mathématiques. Toutes les propriétés où tu remplaces a par b ou b par a sont équivalentes.

Bon j'ai une question bête, mais un "type" c'est quoi ? C'est du jargon d'informaticien ? C'est un méta mot pour désigner tout et n'importe quoi (un nombre, une addition, une proposition logique, un ensemble...) ?

En maths ou en informatique ?
En maths, OSEF. En informatique, c’est une manière de stocker (et donc de manipuler) l’information.

[corentintilde]

Ah non mais si on confond fonction et application, ensemble produit et partie d'un produit ça va pas aller.

[ducon]

Je corrige si tu veux, je simplifiais.
Cela dit, fonction et application, pour la plupart des gens, fonction=application (même pour le dictionnaire des maths de Bouvier, George et Le Lionnais).

[Møgluglu]

Oui. Quelque soit la propriété X, alors la proposition "a a la propriété X", est équivalente à la proposition "b a la propriété X". Donc l'ensemble des propriétés de a est le même que celui de b.

Merci, ça se tient.

Bon j'ai une question bête, mais un "type" c'est quoi ? C'est du jargon d'informaticien ? C'est un méta mot pour désigner tout et n'importe quoi (un nombre, une addition, une proposition logique, un ensemble...) ?

Ce sont les objets de base en théorie des types, qui sont construits par induction. La théorie des types est une alternative à la théorie des ensembles. On sait construire (de plus en plus) des mathématiques "classiques" par dessus, mais les axiomes, définitions et concepts de base sont assez différents de ceux de la théorie des ensembles. Dont justement le concept d'égalité : en théorie des ensemble l'égalité entre ensembles est "codée en dur" comme vous me l'expliquez, en théorie des types l'égalité entre types est elle-même un type.

Le terme type n'est pas choisi au hasard, il correspond au concept de type de données en informatique. C'est un résultat important.
D'une part, ça veut dire que la théorie des types en mathématiques permet d'analyser et démontrer des propriétés sur des programmes informatiques.
D'autre part, les preuves des résultats mathématiques en théorie des types peuvent être représentées sous forme de programmes compréhensibles et vérifiables par les ordinateurs (c'est possible de faire des preuves formelles aussi en théorie des ensembles, mais ça demande de coder en dur toute la logique classique, tandis qu'en théorie des types on peut se contenter d'une axiomatique très légère et construire tout le reste par dessus).
On a toute une école française qui travaille là dessus depuis un moment, dont les fers de lance sont Ocaml côté programmation et Coq côté preuve formelle.

Ah non mais si on confond fonction et application, ensemble produit et partie d'un produit ça va pas aller.

Oui, c'est ma faute.

[darkpoulp]

https://ncatlab.org/nlab/show/identity+type

Je suis tombé là-dessus. Ça a l'air passionnant, peut être tu y trouveras quelque chose.

[Møgluglu]

Merci, c'est exactement ça que je cherche. Je passe à la pharmacie faire un stock d'aspirine et je m'y attaque.

[Vautour]

Merci, c'est exactement ça que je cherche. Je passe à la pharmacie faire un stock d'aspirine et je m'y attaque.

Non mais le nlab, c'est pas un stock d'aspirine qu'il faut...

[corentintilde]

Dont justement le concept d'égalité : en théorie des ensemble l'égalité entre ensembles est "codée en dur" comme vous me l'expliquez, en théorie des types l'égalité entre types est elle-même un type.

Ca donne pas des abominations à la "l'ensemble de tous les ensembles" ?

[Møgluglu]

Non mais le nlab, c'est pas un stock d'aspirine qu'il faut...

Genre la première phrase ça va, la deuxième tu lis chaque mot 3 ou 4 fois et ça va, la troisième tu ouvres une demi-douzaine d'onglets wikipedia, et puis après tu vois que ça continue à monter dans les tours dans les 10 pages suivantes ?...

Ca donne pas des abominations à la "l'ensemble de tous les ensembles" ?

Non, à la base la théorie des types vient justement des travaux de Russell pour construire une théorie qui évite son paradoxe.
Suivant la solution du Russell, tu peux classer les types dans une hiérarchie d'univers : l'univers U_n contient l'univers U_{n-1} ainsi que les types qui parlent des propriétés de l'univers U_{n-1}, et ainsi de suite à l'infini. Ça évite de mélanger les torchons et les serviettes et créer des boucles d'autoréférence.

[Møgluglu]

À quel genre de contradiction penses-tu ?

Par exemple tu peux définir ton opérateur == tel que ce ne soit pas une relation réflexive, transitive et symétrique, tout en utilisant ces propriétés ailleurs dans le code. Ou n'importe quelle boulette de raisonnement qui fait que ton programme peut planter à l'exécution, ou ne jamais se terminer, ou faire totalement n'importe quoi (l'équivalent de pouvoir prouver tout et son contraire à partir d'une contradiction).

Essaie de faire ça en Prolog.

Spoiler Alert!

Il te répondra FALSE. et tu seras bien avancé.

Il n’y a pas de droit en mathématiques. Toutes les propriétés où tu remplaces a par b ou b par a sont équivalentes.

Ça reporte la question sur la définition d'équivalence entre deux propriétés. Mais OK, vous m'avez convaincu qu'en théorie des ensembles l'égalité c'est comme ça et pas autrement.

[Vautour]

Par exemple tu peux définir ton opérateur == tel que ce ne soit pas une relation réflexive, transitive et symétrique, tout en utilisant ces propriétés ailleurs dans le code. Ou n'importe quelle boulette de raisonnement qui fait que ton programme peut planter à l'exécution, ou ne jamais se terminer, ou faire totalement n'importe quoi (l'équivalent de pouvoir prouver tout et son contraire à partir d'une contradiction).

Essaie de faire ça en Prolog.

Spoiler Alert!

Il te répondra FALSE. et tu seras bien avancé.

Ça reporte la question sur la définition d'équivalence entre deux propriétés. Mais OK, vous m'avez convaincu qu'en théorie des ensembles l'égalité c'est comme ça et pas autrement.

L'égalité c'est nul, les règles de réécriture c'est la vie !
Gloire à l'orientation !

[darkpoulp]

Non mais le nlab, c'est pas un stock d'aspirine qu'il faut...

Vrai. Mais du coup, tu connais une meilleure introduction (en douceur) à la théorie des catégories, n-catégories, et ∞-catégories?

[ducon]

Par exemple tu peux définir ton opérateur == tel que ce ne soit pas une relation réflexive, transitive et symétrique, tout en utilisant ces propriétés ailleurs dans le code. Ou n'importe quelle boulette de raisonnement qui fait que ton programme peut planter à l'exécution, ou ne jamais se terminer, ou faire totalement n'importe quoi (l'équivalent de pouvoir prouver tout et son contraire à partir d'une contradiction).

Oui, l’opérateur == est plus souple que l’opérateur is qui n’a pas de méthode spéciale et qui compare en plus le type (la classe).

[Vautour]

Vrai. Mais du coup, tu connais une meilleure introduction (en douceur) à la théorie des catégories, n-catégories, et ∞-catégories?

Pour les catégories, il y a whatmille bouquins. Déjà dans le MacLane, il y a de quoi faire.
Avant de passer aux catégories supérieures, il faut bouffer des catégories homotopiques, donc on commence par le Dwyer-Spalinski (aka les catégories de modèles pour les nuls), et on continue par le Hovey. Il faut aussi s'y connaitre en simplicial, donc on bouffe le Goerss-Jardine.
Et les n-catégories, ce n'est rien d'autre que les infini-catégories tronquées. Et il y a en a 4 voire 5 modèles différents (à la Joyal, à la Lurie, via des localisations plus ou moins barbares, etc). Suivant le cas, c'est entre 500 et 2000 pages à lire. Et après il y a des papiers qui montrent que ces modèles sont "les mêmes".

Et il y a aussi les versions via les catégories globulaires ...

Le nlab, ça se lit quand on maitrise une bonne partie de tout ça et qu'on veut combler des trous. Ce n'est pas les infini-catégories pour les nuls.

[darkpoulp]

...

Merci!

[corentintilde]

Quand j'entends le mot catégorie, je sors mon revolver.

[Vautour]

Quand j'entends le mot catégorie, je sors mon revolver.

Et moi quand j'entends le mot dérivée partielle.

[darkpoulp]

Moi c'est le mot arrosoir.


Je sais pas pourquoi.

[Enyss]

Et moi quand j'entends le mot dérivée partielle.

Pourtant, ça c'est utile

[Vautour]

Pourtant, ça c'est utile

Justement. C'est quoi ces gens qui font des maths qui sont utiles ? Vous voudriez en plus nous faire croire que vous avez les pieds sur terre ?

(et puis une catégorie aussi c'est super utile )

[Tarsiz]

Justement. C'est quoi ces gens qui font des maths qui sont utiles ? Vous voudriez en plus nous faire croire que vous avez les pieds sur terre ?

C'est tellement triste les maths "utiles"...

Quelle désillusion en quittant le monde magnifique des maths de prépa pour le monde triste et sale des maths d'école d'ingé

[BentheXIII]

Sur le chemin vers la corruption chaotique, il y a pire: faire un doctorat dans une université US et parler maths avec certains locaux.

[corentintilde]

Après faut pas croire que les math de prépa c'est les math... c'est des trucs vieux, digérés, recrachés, retravaillés enseignés par des gens fort méticuleux en général.
Ca donne une impression de beauté et de perfection des arguments qui est assez loin des articles de recherche qui pour une idée jolie ont droit à de nombreuses pages de notations et de calculs infames...

[Anonyme20240202]

Putain la culture mathématique de certains fait peur parfois.

Aujourd'hui entretien dans une "grande" banque française, on me demande d'écrire un algo qui trouve le n-ième nombre premier.

Après avoir entamé la réflexion je vois qu'en face ça connait ni le chiffrement RSA ni la fonction zêta, on n'était pas au même niveau d'entente concernant la qualité de la fonction...

Du coup je pense qu'on peut dire adieu à la théorie des nombres premier parce que je vous ai pissé l'algo du siècle, Turing peut retourner jouer aux Lego.

[ducon]

Je parie qu’il te demandait un algorithme bourrin.

[Møgluglu]

Pas de bol, ton algo ne correspond pas au crible d'Eratosthène du corrigé, et en plus on a rien compris à tes explications ni à tes commentaires dans le code. Suivant.

[Anonyme20240202]

Pas de bol, ton algo ne correspond pas au crible d'Eratosthène du corrigé, et en plus on a rien compris à tes explications ni à tes commentaires dans le code. Suivant.

C'est tellement ça

Je parie qu’il te demandait un algorithme bourrin.

Ouais j'étais parti bien trop loin, du coup j'ai pondu une horreur et basta

[Molina]

Ce que je déteste en fait chez les matheux... C'est qu'il te sorte des indices, dont tu sais même pas d'où ça sort....

Voilà mon problème : Je recherche à calculer un coefficient de variation (=CV=écart type/ moyenne) mais en multivarié.

Je cherche un petit peu, déjà il y a plusieurs formules et chacun se tire le bouchon... Mais en plus, je suis pas certain de bien comprendre ce qu'il se passe. J'ai trouvé une formule assez facile à utiliser :


Ok. Pour vérifier, je regarde ce qu'en dise d'autres publis...



POURQUOI C4EST PAS LA MEME CHOSE §§§§ C'est quoi ce putain de 'tr' et cet indice de "t" sortie de mon cul !

Alors je repars chez l'auteur (van valen là...)



Quelqu'un pourrait me dire si c'est la même chose ? Parce que dans un cas, j'ai une formule simple, qu'un biologiste peut utiliser, et dans l'autre une formule à la con qui demande d'avoir fait au moins une License de math.

[Aghora]

Les 2 derniers c'est pas tout à fait la même chose, puisqu'il manque le "100" je dirais. Parce que le symbole Sigma représente une matrice (tu sais ce qu'est une matrice déjà ?), le tr représente la "trace" de la matrice c'est à dire la somme des éléments diagonaux de cette matrice. Et le "t" sortie de ton cul signifie "transposé" (marche pour des vecteurs et des matrices), ce qui signifie dans ce cas précis la somme des éléments au carré du vecteur µ (qui a l'air d'être la moyenne de tes observations).

Enfin bref, à part le "100" qui manque, ce sont les mêmes formules.