DISCLAIMER: Je ne suis pas mathématicien de profession, juste quelqu'un de très curieux qui a lu beaucoup de choses sur le sujet.
Moui.
This creates a strong coupling between the structure of data and the implementation of the operations manipulating such data.
However, in mathematics, objects have no type. Instead, the mathematician will define a collection with rules indicating which objects are part of said collection.
Franchement j’ai du mal avec ta justification sur les types. Je trouve ça casse-gueule de vouloir parler mathématiques aussi fondamentales et surtout pas très pertinent pour un système de types informatiques.
De base, par exemple :
N se définit par l’existence d’une application successeur : les naturels sont aux mathématiciens ce que les listes chainées sont aux informaticiens ; idem pour l’opérateur d’addition (appelons-le +0) ; les naturels sont définis à travers ces opérateurs (cf. arithmétique de Peano). Il y a couplage entre l’ensemble et les opérateurs admis sur ses éléments.
En ZF, de même tu as la relation d’appartenance ∈ qui est explicitement une primitive ;
Tout le reste est construit par-dessus, et là ta remarque a effectivement une certaine pertinence : par exemple on définit Q à partir de N, R à partir de Q, etc. puis on définit des opérateurs et des relations sur ces ensembles.
Mais dire qu’il n’y a pas de "types" en mathématiques est toujours faux. C’est même à la base de toute l’algèbre générale : on parlera plutôt de structures, c’est-à-dire des ensembles munis d’opérateurs, +, ×ばつ, etc.
Si tu dis ∀x ∈ Q tel que x = 42, ∀y ∈ R tel que y = 42 : en toute rigueur x ≠ y.
Il faut définir un injecteur i : Q → R, c’est-à-dire une fonction telle que y = i(x). Cette injecteur a les bonnes propriétés pour que les opérateurs usuels définit sur Q collent avec les opérateurs usuels sur R: ainsi i(x +1 z) = i(x) +2 i(z) où +1 est l’addition dans Q et +2 l’addition dans R, et = est complètement défini car on compare bien un réel avec un réel (et pas des choux et des carottes). On parle de i comme d’un homomorphisme de groupes (Q +1) → (R +2). Et si on y adjoint les multiplications (×ばつ1 et ×ばつ2) on parle des corps Q et R et d’homomorphismes de corps.
Par abus les mathématiciens finissent par dire que x = y. Mais c’est pas si évident que ça et ça demande tout un travail algébrique pour arriver à dire que ce raccourci d’écriture est légitime.
Ajoute à cela que tes opérateurs +0, +1, etc. n’existent pas sur les ensembles en tant que tels. En réalité dire ∀x,y ∈ N, x +0 y = ... est un pur abus de langage. Il est admis parmi les mathématiciens qu’on parle en réalité ici de "N muni de son addition usuelle...". Pour Q et R c’est leur structure de corps qui est implicite ; Q muni de +1 et ×ばつ1, R de +2 et ×ばつ2. Si je mets un exposant, c’est pas pour faire joli :
c’est parce qu’il ne s’agit pas du même opérateur : c’est l’injecteur, parce qu’il est un homomorphisme, qui permet d’identifier +1 à +2) ;
c’est parce qu’on ne peut pas mixer un rationnel et un réel pour faire une addition.
Pour les espaces vectoriels tu es obligé de faire la distinction. Parler de 42 comme d’un vecteur ça veut rien dire, tu voulais probablement dire : 42 = 42 · 1 où le gras est un vecteur, en admettant que tu prennes la base canonique. La structure de l’espace vectoriel R n’est pas celle du corps R (le 42 non-gras : c’est le scalaire, c’est une coordonnée qui appartient par définition au corps R, le 42 gras : c’est un vecteur, il appartient au R-espace vectoriel R). Le 42 que tu as donné c’est la coordonnée du vecteur : pour ce faire, tu as considéré R muni d’une structure de (corps-R)-espace vectoriel, avec une base qui plus est.
C’est une erreur classique que de confondre les coordonnées d’un vecteur et le vecteur lui-même.
[^] # Re: théorie des ensembles pas naives
Posté par PR . En réponse au journal [Letlang] Et si on rédigeait la spec ?. Évalué à 3. Dernière modification le 08 mai 2022 à 13:36.
Moui.
Franchement j’ai du mal avec ta justification sur les types. Je trouve ça casse-gueule de vouloir parler mathématiques aussi fondamentales et surtout pas très pertinent pour un système de types informatiques.
De base, par exemple :
Mais dire qu’il n’y a pas de "types" en mathématiques est toujours faux. C’est même à la base de toute l’algèbre générale : on parlera plutôt de structures, c’est-à-dire des ensembles munis d’opérateurs, +, ×ばつ, etc.
Si tu dis ∀x ∈ Q tel que x = 42, ∀y ∈ R tel que y = 42 : en toute rigueur x ≠ y.
Il faut définir un injecteur i : Q → R, c’est-à-dire une fonction telle que y = i(x). Cette injecteur a les bonnes propriétés pour que les opérateurs usuels définit sur Q collent avec les opérateurs usuels sur R: ainsi i(x +1 z) = i(x) +2 i(z) où +1 est l’addition dans Q et +2 l’addition dans R, et = est complètement défini car on compare bien un réel avec un réel (et pas des choux et des carottes). On parle de i comme d’un homomorphisme de groupes (Q +1) → (R +2). Et si on y adjoint les multiplications (×ばつ1 et ×ばつ2) on parle des corps Q et R et d’homomorphismes de corps.
Par abus les mathématiciens finissent par dire que x = y. Mais c’est pas si évident que ça et ça demande tout un travail algébrique pour arriver à dire que ce raccourci d’écriture est légitime.
Ajoute à cela que tes opérateurs +0, +1, etc. n’existent pas sur les ensembles en tant que tels. En réalité dire ∀x,y ∈ N, x +0 y = ... est un pur abus de langage. Il est admis parmi les mathématiciens qu’on parle en réalité ici de "N muni de son addition usuelle...". Pour Q et R c’est leur structure de corps qui est implicite ; Q muni de +1 et ×ばつ1, R de +2 et ×ばつ2. Si je mets un exposant, c’est pas pour faire joli :
Pour les espaces vectoriels tu es obligé de faire la distinction. Parler de 42 comme d’un vecteur ça veut rien dire, tu voulais probablement dire : 42 = 42 · 1 où le gras est un vecteur, en admettant que tu prennes la base canonique. La structure de l’espace vectoriel R n’est pas celle du corps R (le 42 non-gras : c’est le scalaire, c’est une coordonnée qui appartient par définition au corps R, le 42 gras : c’est un vecteur, il appartient au R-espace vectoriel R). Le 42 que tu as donné c’est la coordonnée du vecteur : pour ce faire, tu as considéré R muni d’une structure de (corps-R)-espace vectoriel, avec une base qui plus est.
C’est une erreur classique que de confondre les coordonnées d’un vecteur et le vecteur lui-même.
Mort aux cons !