Le truc qui me choque à chaque fois que je croise ce genre de philosophie : et quand il y a 2 observateurs ? Et que par hasard ils sont d’accord, ce qui n’est pas systématique, mais assez commun. On peut donc arguer qu’ils tirent les mêmes conclusions sur l’objet en question, ce qui tend à montrer que ces phénomènes ont une existence propre.
Tu prends là une condition suffisante (l'existence propre de l'objet expliquerait l'accord des observateurs), pour une condition nécessaire (leur accord ne peut s'expliquer que par une existence propre de l'objet, abstraction faite du rapport à l'observateur).
Premièrement, l'accord entre observateurs sur les determinations spatio-temporelles des objets est tout sauf commun : voir les principes fondamentaux des relativité restreinte et générale. Deuxièmement, dans la connaissance expérimentale on ne pose jamais de questions sur ce que sont les choses en elles-même, mais seulement sur les résultats de nos observations; et parler d'observation sans observateur (c'est-à-dire en faisant abstraction du rapport entre l'observateur et l'objet observé) est une contradiction dans les termes.
Je pourrais développer ce point en faisant une analyse comparée d'un texte d'Enstein (un article qu'il a écrit sur Bertand Russel) et de la plaidoirie de Kant pour se défendre d'être un idéaliste (au sens que ce terme à en philosophie), si tu souhaites plus de précisions. La plaidoirie de Kant est, dans le fond, une réponse à l'objection que tu m'opposes.
Je suis intéressé par une explication là dessus. ZF est bien fondée dans le sens ou toute compréhension est associée à un ensemble préexistant « Étant donné un ensemble A et une propriété P exprimée dans le langage de la théorie des ensembles, il affirme l'existence de l'ensemble B des éléments de A vérifiant la propriété P. » ce que j’interprète (librement) comme une relation de sous typage. Étant donné que le « x ∈ A » ressemble quand même pas mal à une assertion de type et qu’elle est nécessaire dans une théorie des ensemble, j’ai du mal à comprendre en quel sens ça correspond à un langage dynamique.
Ton interprétation (libre) ne tombe pas loin de la réalité : telle était l'intention primordiale de la théorie, mais c'est « mal » fait. L'idée étant de voir un ensemble comme un concept dont l'extension (la totalité de ses éléments) dénote les objets tombant sous le concept (d'où, par exemple, l'axiome d'extensionnalité affirmant que deux ensembles ayant les mêmes éléments sont égaux), et l'inclusion entre ensembles exprimant alors la subordination entre concepts, c'est-à-dire du sous-typage.
Ma comparaison avec le typage dynamique (comparaison à laquelle j'ajoutais si je peux m'exprimer ainsi) vient du fait que lorsque l'on prend un énoncé universellement quantifié de la théorie, on quantifie sur tout l'univers des ensembles qui se comporte alors à la manière du interface{} du Go. ;-) Raison pour laquelle les auteurs de HoTT écrivent en introduction de leur ouvrage :
In type theory, unlike set theory, objects are classified using a primitive notion of type, similar to the data-types used in programming languages. [...]
This rigidly predictable behavior of all objects (as opposed to set theory’s more liberal formation principles, allowing inhomogeneous sets) is one aspect of type theory that has led to its extensive use in verifying the correctness of computer programs.
Ce que j'ai graissé est à mettre en lien avec les reproches adressées à Go d'utiliser le interface{} pour la généricité du code, ce qui ne permet pas de garantir statiquement l'homogénéité d'une liste : il faut écrire des fonctions de constructions qui font du typage dynamique à base de switch sur les types des paramètres.
Ceci est à mettre en parallèle avec les énoncés que l'on ferait sur l'encodage des entiers naturels dans ZF, où on écrirait \forall x (x \in \omega \Rightarrow ...) pour énoncer une propriété des entiers. Ici le quantificateur universel sur x parcourt la collection de tous les ensembles (intreface{}) puis l'énoncé est une proposition hypothétique dont l'antécédent $x \in \omega$ correspond à une vérification dynamique de type avant de continuer « l'exécution » vers le conséquent. Je vois alors l'énoncé comme une fonction qui prend en entrée un interface{} et qui fait du typage dynamique : une assertion de type ou un switch (comme tu veux), comme en Go. En Coq ou en HoTT, on écrirait tout simplement forall (x : Nat) ..., soit pour tout entier, .... La notion de type capture bien mieux que celle d'ensembles (au sens de ZF) la notion logique de concept.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Le cerveau n'est pas logique
Posté par kantien . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 2. Dernière modification le 30 octobre 2017 à 12:21.
Tu prends là une condition suffisante (l'existence propre de l'objet expliquerait l'accord des observateurs), pour une condition nécessaire (leur accord ne peut s'expliquer que par une existence propre de l'objet, abstraction faite du rapport à l'observateur).
Premièrement, l'accord entre observateurs sur les determinations spatio-temporelles des objets est tout sauf commun : voir les principes fondamentaux des relativité restreinte et générale. Deuxièmement, dans la connaissance expérimentale on ne pose jamais de questions sur ce que sont les choses en elles-même, mais seulement sur les résultats de nos observations; et parler d'observation sans observateur (c'est-à-dire en faisant abstraction du rapport entre l'observateur et l'objet observé) est une contradiction dans les termes.
Je pourrais développer ce point en faisant une analyse comparée d'un texte d'Enstein (un article qu'il a écrit sur Bertand Russel) et de la plaidoirie de Kant pour se défendre d'être un idéaliste (au sens que ce terme à en philosophie), si tu souhaites plus de précisions. La plaidoirie de Kant est, dans le fond, une réponse à l'objection que tu m'opposes.
Ton interprétation (libre) ne tombe pas loin de la réalité : telle était l'intention primordiale de la théorie, mais c'est « mal » fait. L'idée étant de voir un ensemble comme un concept dont l'extension (la totalité de ses éléments) dénote les objets tombant sous le concept (d'où, par exemple, l'axiome d'extensionnalité affirmant que deux ensembles ayant les mêmes éléments sont égaux), et l'inclusion entre ensembles exprimant alors la subordination entre concepts, c'est-à-dire du sous-typage.
Ma comparaison avec le typage dynamique (comparaison à laquelle j'ajoutais si je peux m'exprimer ainsi) vient du fait que lorsque l'on prend un énoncé universellement quantifié de la théorie, on quantifie sur tout l'univers des ensembles qui se comporte alors à la manière du
interface{}du Go. ;-) Raison pour laquelle les auteurs de HoTT écrivent en introduction de leur ouvrage :Ce que j'ai graissé est à mettre en lien avec les reproches adressées à Go d'utiliser le
interface{}pour la généricité du code, ce qui ne permet pas de garantir statiquement l'homogénéité d'une liste : il faut écrire des fonctions de constructions qui font du typage dynamique à base de switch sur les types des paramètres.Ceci est à mettre en parallèle avec les énoncés que l'on ferait sur l'encodage des entiers naturels dans ZF, où on écrirait \forall x (x \in \omega \Rightarrow ...) pour énoncer une propriété des entiers. Ici le quantificateur universel sur
xparcourt la collection de tous les ensembles (intreface{}) puis l'énoncé est une proposition hypothétique dont l'antécédent $x \in \omega$ correspond à une vérification dynamique de type avant de continuer « l'exécution » vers le conséquent. Je vois alors l'énoncé comme une fonction qui prend en entrée uninterface{}et qui fait du typage dynamique : une assertion de type ou un switch (comme tu veux), comme en Go. En Coq ou en HoTT, on écrirait tout simplementforall (x : Nat) ..., soitpour tout entier, .... La notion de type capture bien mieux que celle d'ensembles (au sens de ZF) la notion logique de concept.Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.