D’autant plus qu’on peut faire des maths pas seulement dans la théorie des ensembles, mais aussi dans la théorie des types.
Les assistants de preuves comme Coq ou Lean qui a fait récemment parler de lui, cf. https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/ par exemple sont basés sur des théories des types. Les théories des types sont un sujet de recherche actif du point de vue mathématique, et pas seulement pour les maths-infos mais aussi pour des choses purement mathématiques. Cf. la théorie homotopique des types dont il a déjà été question ici je crois.
Si on travaille dans la théorie des ensembles un meilleur exemple pour montrer l’ambiguité serait peut être de parler de l’ensemble vide : il peut représenter assez naturellement ... l’élément neutre de l’opération d’union de la théorie des ensemble, mais aussi si on code des nombres il peut coder le nombre 0 dans les entiers naturels dans la construction classique.
Mathématiquement 0 et l’ensemble vide sont bien évidemment des objets totalement différents, en théorie des ensembles, si on applique les axiomes et le codage classique des entiers naturels, ils sont ... égaux (deux ensemble sont égaux si ils ont les même éléments).
C’est souvent un exemple d’absurdité qui est utilisé pour introduire la théorie des types aux mathématiciens qui sont habitués à travailler avec la théorie des ensembles. Le truc à noter c’est qu’en choisissant un autre codage des entiers naturels dans la théorie des ensembles le paradoxe disparait (mais d’autres pourraient apparaitre). Tout dépend de comment on choisit de coder les objets sur lesquels on veut travailler.
Je pense que ce qui pourrait manquer à la présentation, également, c’est une définition de ce que sont les « objets ». Ils sont pas introduits ni définis dans la présentation actuellement. Et il semble y avoir une confusion entre « objet » et « littéral » : le littéral « 5 » peut être utilisé pour représenter l’entier naturel 5 dans le code d’un programme. L’entier naturel a naturellement un type, par contre les littéraux c’est à définir. On peut très bien convenir que dans un contexte de calcul vectoriel ou sur les flottants on donne au littéral « 5 » d’autre significations ... Et soit interprétés comme deux objets (dans le sens de valeur manipulées par le langage, des valeurs que peuvent prendre les variables) différents.
Dernier point sur le paradoxe de Russel : en quoi est-ce un problème en pratique ? Les classes pourraient être manipulables en tant que valeur du langage (« objet ») sans avoir la possibilité que le langage soit assez puissant pour pouvoir définir une collection de ces valeurs. Si tu veux avoir des variables « non déterministes » qui pourraient avoir comme valeur plusieurs « objet classes » possibles ça doit pouvoir rester possible en faisant attention à ce que cet ensemble de classe soit « fermé », ou alors faire en sorte que les variables qui contiennent des classes soient « déterministes » dans le sens ou il ne peuvent avoir qu’une seule valeur possible.
[^] # Re: théorie des ensembles pas naives
Posté par thoasm . En réponse au journal [Letlang] Et si on rédigeait la spec ?. Évalué à 5.
D’autant plus qu’on peut faire des maths pas seulement dans la théorie des ensembles, mais aussi dans la théorie des types.
Les assistants de preuves comme Coq ou Lean qui a fait récemment parler de lui, cf. https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/ par exemple sont basés sur des théories des types. Les théories des types sont un sujet de recherche actif du point de vue mathématique, et pas seulement pour les maths-infos mais aussi pour des choses purement mathématiques. Cf. la théorie homotopique des types dont il a déjà été question ici je crois.
Si on travaille dans la théorie des ensembles un meilleur exemple pour montrer l’ambiguité serait peut être de parler de l’ensemble vide : il peut représenter assez naturellement ... l’élément neutre de l’opération d’union de la théorie des ensemble, mais aussi si on code des nombres il peut coder le nombre 0 dans les entiers naturels dans la construction classique.
Mathématiquement 0 et l’ensemble vide sont bien évidemment des objets totalement différents, en théorie des ensembles, si on applique les axiomes et le codage classique des entiers naturels, ils sont ... égaux (deux ensemble sont égaux si ils ont les même éléments).
C’est souvent un exemple d’absurdité qui est utilisé pour introduire la théorie des types aux mathématiciens qui sont habitués à travailler avec la théorie des ensembles. Le truc à noter c’est qu’en choisissant un autre codage des entiers naturels dans la théorie des ensembles le paradoxe disparait (mais d’autres pourraient apparaitre). Tout dépend de comment on choisit de coder les objets sur lesquels on veut travailler.
Je pense que ce qui pourrait manquer à la présentation, également, c’est une définition de ce que sont les « objets ». Ils sont pas introduits ni définis dans la présentation actuellement. Et il semble y avoir une confusion entre « objet » et « littéral » : le littéral « 5 » peut être utilisé pour représenter l’entier naturel 5 dans le code d’un programme. L’entier naturel a naturellement un type, par contre les littéraux c’est à définir. On peut très bien convenir que dans un contexte de calcul vectoriel ou sur les flottants on donne au littéral « 5 » d’autre significations ... Et soit interprétés comme deux objets (dans le sens de valeur manipulées par le langage, des valeurs que peuvent prendre les variables) différents.
Dernier point sur le paradoxe de Russel : en quoi est-ce un problème en pratique ? Les classes pourraient être manipulables en tant que valeur du langage (« objet ») sans avoir la possibilité que le langage soit assez puissant pour pouvoir définir une collection de ces valeurs. Si tu veux avoir des variables « non déterministes » qui pourraient avoir comme valeur plusieurs « objet classes » possibles ça doit pouvoir rester possible en faisant attention à ce que cet ensemble de classe soit « fermé », ou alors faire en sorte que les variables qui contiennent des classes soient « déterministes » dans le sens ou il ne peuvent avoir qu’une seule valeur possible.