kantien a écrit 1131 commentaires

Un générateur d'onde sinusoïdale, dans le domaine audio, c'est proche d'un "Hello World!". ;-)
Après on peut jouer sur la fréquence ("Hello @hpiedcoq!") ou même la forme du signal ("@hpiedcoq, les sinusoïdes c'est la base du traitement du signal ;-)"). :-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Ça se discute, tout dépend à qui se réfère l'adjectif épithète. Ces trois phrases me semblent correctes, mais n'expriment pas la même chose :

• une des plus brillante scientifiques du siècle dernier est, sans hésitation, Marie Curie
• une des plus brillants scientifiques du siècle dernier est, sans hésitation, Marie Curie
• une des plus brillantes scientifiques du siècle dernier est, sans hésitation, Marie Curie

dans la première, seule Marie Curie est qualifiée de brillante.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Si la phrase 'par la méthode de condorcet' fait partie de la discussion, on voit bien dans l'original anglais que c'est mentionné

Comme tu le soulignes, la référence à la méthode de scrutin à la Condorcet est mentionnée sur l'original chez Debian (fait qui est notoirement connu pour quiconque connaît un minimum le fonctionnement de l'organisation Debian).

Dans un commentaire de mon journal, je précise que la mention à cette méthode était un clin d'œil à certains journaux de l'époque (on était en pleine campagne présidentielle, et certains journaux parlaient de méthodes de votes alternatives). L'introduction même du journal est une allusion au contexte historique et aux débats de l'époque sur le site.

Dans un commentaire d'un de ces journaux, en date du 15 mai, je parle de Condorcet et Borda et de mon intérêt pour ces méthodes qui remonte au moins à l'élection de 2002 et le second tour Chirac - Le Pen.

Dans la dépêche, je développe cette partie sur les modes de scrutins avec lien vers un dossier sur le site Images des Maths du CNRS.

Je pense qu'il se peut fort bien que les deux soient de bonne foi

J'ai du mal à comprendre où l'on peut voir, de bonne foi, dans mon article (et sa version promue en dépêche) une contrefaçon du sien.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Pas du tout, à des souvenirs traumatisants du professeur qui ponctuait ses corrections par des références à l'évidence même sans réel explication.

Au temps pour moi, avec le sujet de la dépêche, j'ai du me sentir visé : dans l'autre journal j'avais fait un appel à l'évidence et tu m'avais répondu que même si cela paraissait évident, il fallait démontrer que la solution proposée apportait quelque chose.

Pour ce qui est de l'appel à l'évidence, dans l'enseignement, c'est toujours délicat : l'évidence est très subjective (ce qui est évident pour l'un, ne l'est pas forcément pour l'autre) et dans une correction, ce n'est pas le meilleur endroit pour y faire appel.

Ceci étant, même Coq a une notion d'évidence avec la tactique trivial :

Remark a : forall n, 0 + n = n + 0.
Proof.
trivial.
Qed.

mais en réalité, il trouve cela trivial car il applique directement un théorème qui est dans sa base de données (et qui énonce la même chose). En revanche, la preuve du théorème initial n'est pas triviale pour la machine, il faut la faire à la main par récurrence; là où avec un interlocuteur humain, un mathématicien serait tenté d'écrire : évident par récurrence sur n (en précisant toutefois le mode de démonstration à utiliser).

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

C'est vrai que les justifications du type mais c'est évident ! ressemble fort à un prof de maths qui ne souhaite pas expliquer la solution en détails. :-)

Hé ! ce ne serait pas une allusion déguisée à certains de nos échanges récents sur un autre journal. :-P

Je ne suis pas prof de maths, et ce à quoi je faisais allusion c'est ce genre de chose :

/*@
requires \valid_read(a + (0..n-1));
requires \valid_read(b + (0..n-1));

assigns \nothing;

behavior all_equal:
  assumes \forall integer i; 0 <= i < n ==> a[i] == b[i];
  ensures \result;

behavior some_not_equal:
  assumes \exists integer i; 0 <= i < n && a[i] != b[i];
  ensures !\result;

complete behaviors;
disjoint behaviors;
*/
bool equal(const value_type* a, size_type n, const value_type* b);

extrait du livre ACSL by example (où ACSL signifie ANSI/ISO C Specification Langage). Il me semble évident que le système de type défini par ACSL est plus riche et permet de mieux exprimer la spécification de la fonction que ne le fait celui du langage C, qui dit juste que la fonction renvoie un booléen (ce que fait également la fonction qui renvoie constamment true). Qu'il existe un logiciel qui vérifie automatiquement que le code satisfait cette spécification, c'est un fait, il suffit de le tester.

Mais restons dans le sujet de la dépêche : la contrefaçon. Kant (oui, encore lui) a écrit un article sur le sujet en 1785 : De l'illégitimité de la contrefaçon des livres, article à la lecture fort intéressante et d'actualité, comme l'illustre la première note qui rappelle furieusement le problème des DRM :

Si un éditeur essayait de soumettre quiconque voudrait acheter son édition à la condition de se voir poursuivi pour soustraction d’un bien étranger à lui confié, dans le cas où, soit par son propre fait, soit par l’effet de sa négligence, l’exemplaire qu’il aurait acheté aurait été livré à l’impression, on n’y consentirait pas volontiers, car on ne voudrait pas s’exposer à toutes les importunités des perquisitions et des justifications. L’édition resterait donc sur les bras de l’éditeur.

Le texte est aussi une illustration de la rigueur, tant logique que juridique, avec laquelle Kant pouvait faire usage de la syllogistique.

Il reprendra, en 1797, le même thème dans sa Doctrine du droit dans un annexe aux droits des contrats sous le titre Qu'est-ce qu'un livre ?

La cause de ce qu'il y a d'apparamenent légitime dans une illégitimité qui saute pourtant aussi vivement aux yeux, du premier coup d'œil, que celle de la contrefaçon des livres, tient à ceci : le livre,d'une part, est un produit matériel de l'art (opus mechanicum) qui peut être imité (par celui qui se trouve en posséder légitimement un exemplaire, et par conséquent il y a là un droit réel; mais, d'un autre côté, le livre est aussi un pur et simple discours de l'éditeur au public, que le possesseur n'a pas le droit de reproduire publiquement (praestatio operae) sans avoir pour cela été mandaté par l'auteur — ce qui définit un droit personnel, et dans ces conditions l'erreur consiste en ce que l'on confond les deux droits.

Kant, Doctrine du Droit.

Sans entrée dans le détails, le droit des contrats relève du droit personnel (droit de contraindre une personne à une certaine prestation) et le genre d'annotations de code comme illustré ci-dessus est ce que l'on appelle la programmation par contrat. Elles expriment quelque chose du type : si les entrées vérifient certaines conditions alors la sortie en vérifiera d'autres. Il se trouve que Kant a donné pour fondements aux droits personnels la forme logique des jugements hypothétiques (si A alors B), tandis que les droits réels (droit de propriété sur une chose) ont pour fondements la forme logique des jugements catégoriques (A est B), ce qui correspond à la relation de sous-typage (comme je l'ai expliqué ailleurs).

Autrement dit, les débats sur la légitimité ou l'illégitimité de la contrefaçon tourne autour de la confusions entre la relation de sous-typage et le type d'une fonction.

En espérant que ce cas d'école illustrera ce que je voulais exprimer lorsque j'ai écrit un jour : ce que font les théories des types contemporaines, Kant le faisait déjà il y a plus de 200 ans. ;-)

Pour le détail, il faut se référer au contenu des théories concernées. :-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Oui j'étais au courant, j'ai eu des échanges téléphoniques et par mails avec Benoît. En revanche je ne suis pas dans la procédure, il semble que je ne suis pas juridiquement impliqué dans l'affaire (bien que d'un point de vue moral, je le sois indubitablement). J'ai envoyé des éléments de défense pour nier la qualification de contrefaçon tant de l'article que de la dépêche.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Ou mieux : demander à kantien de le réécrire.

Ce qu'ils ont fait lors de sa promotion en dépêche.

Si le journal était purement factuel et reprenait la forme et le contenu de mes deux sources¹ :

• https://www.debian.org/vote/2017/vote_001.en.html ;
• https://bits.debian.org/2017/04/results-dpl-elections-2017.html.

La dépêche (dont je suis également l'auteur) est autrement plus fouillée et détaillée, tandis que le journal s'apparente plus à une dépêche AFP.

Ce qui repose l'éternel débat sur le choix terminologique de linuxfr entre dépêche et journal. :-P

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Je ne sais pas quelle formation tu as eu, mais la question de la qualité dans le développement logiciel c'est loin d'être généralisé même aujourd'hui, que ce soit en entreprise ou dans les formations.

C'était une formation en logique mathématique et sur les fondements de l'informatique. Personnellement, à l'époque, la partie fondements de l'informatique ne m'intéressait pas spécialement. Je voulais surtout approfondir mes connaissances en logique et voir ce qu'avaient donné les attaques contre la philosophie kantienne des mathématiques (j'ai lu la Critique de la Raison Pure à la fin de ma spé, et je suis kantien depuis cette époque). Pour ceux intéressés par l'informatique, d'après la brochure sur les débouchés, il semblerait qu'ils finissent par faire une thèse et de la recherche (dans les organismes publiques ou en R&D chez des industriels genre EDF).

J'ai bien conscience qu'une telle formation est à part par rapport aux formations courantes des ingénieurs informaticiens.

Déjà, je dirais que pour être rigoureux intellectuellement, il faut démontrer que la solution proposée apporte quelque chose. Même si cela paraît évident. Car comme je l'ai dit, ce n'est pas parce que ton travail provient de la recherche universitaire que cela est forcément bénéfique. On ne va pas lister le nombre de prédictions théoriques de la recherche fondamentale (dont sur les noyaux de système d'exploitation) qui n'ont jamais su percer dans l'industrie faute d'adéquation en réalité.

Démontrer comment, par l'exemple ? Mais, de mon point de vue, un fait ne prouve pas grand chose : je m'intéresse surtout aux méthodes et à leur limite. Je suis un obsédé de la certitude : qu'est-ce que la certitude ? de quoi peut-on être certain ? quelles méthodes peuvent espérer atteindre à la certitude, lesquelles ne le peuvent pas ? font partie des questions qui m'obsèdent. Et de ce point de vue, l'induction et la méthode expérimentale reviennent à cela :

l'expérience ne donne jamais à ses jugements une universalité vraie et rigoureuse, mais seulement supposée ou comparative, si bien que cette universalité doit proprement signifier : Pour autant que nous l'ayons perçu jusqu'ici, il ne se trouve pas d'exception à telle ou telle règle.

Kant, introduction de la Critique de la Raison Pure.

ou pour citer Einstein résumant la philosophie sceptique de Hume : « l'empirique, dans la connaissance, n'est jamais certain (Hume) ». Il ne fut néanmoins pas convaincu par la réponse kantienne aux objections de Hume : « Kant propose alors une pensée. Sous la forme présentée elle est indéfendable mais elle marque un progrès nette pour résoudre le dilemme de Hume ». Pour ma part, je la trouve on ne plus défendable, et la méthode qu'il employa est analogue à celle utilisée par tous les systèmes de types des langages de programmations. Pour pousser le distinguo à l'extrême : je n'ai aucune certitude que le soleil se couchera se soir, mais je n'ai aucun doute quant à ce qu'exprime le théorème de Pythagore.

Pour revenir aux outils d'analyses et de sécurisation de code, il ne s'agit pas nécessairement de spécifier dans les moindres détails chaque bout de code et d'apporter la preuve du respect de la spécification, mais il est peut être envisageable d'ajouter certaines annotations en commentaires (à la manière de frama-c) pour avoir un système de type à l'expressivité plus riche que celui du C. Le système de type de C, de fait, exprime des spécifications sur le code mais, comme c'est peu ou prou la logique propositionnelle du premier ordre, on ne peut pas y exprimer grand chose : ce que fait le code et comment l'utiliser est beaucoup trop sous-spécifié avec un tel système de type.

Prenons un exemple. Je ne connaissais Coccinelle que de nom, je suis allé voir un peu leur site, et sur la page consacrée aux évolutions collatérales ils donnent deux exemple : ajout d'un argument à une fonction et changement dans le protocole d'initialisation des pilotes. Il semblerait que les pilotes aient mis un certain temps à s'adapter correctement à ce changement d'interface dans le cœur du noyau. Ces changements il faut bien les documenter quelque part ? Pourquoi pas dans une langue proche par sa syntaxe et son vocabulaire de l'anglais, mais à la grammaire plus régulière, et l'écrire en commentaire du code modifié ? On pourrait alors avoir une logiciel d'aide à l'audit qui détecterait automatiquement les mauvais usages des nouveaux codes.

Entre un audit totalement manuel et un audit partiellement automatisé, dans le monde de l'informatique ça doit pouvoir convaincre (pourquoi faire à la main ce qu'une machine peut faire pour moi ?). Je ne suis membre d'aucune des deux communautés (celle du noyau et celle de la recherche), mais je sais que la seconde est en état de fournir ce genre d'outil à la première. Néanmoins, pour cela, il faudrait une coopération et une synergie entre elles qui ne semblent pas exister aux dires de gasche. Je ne peux que trouver cela dommage.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Par contre, s'il y a un comportement indéfini du source, donc sémantique non définie, je pense pas que ça dise quoi que ce soit d'utile (on obtient juste un comportement « go wrong » accompagné d'une trace dès que la sémantique bloque, donc au mieux ça dirait peut-être que jusqu'au moment où ça bloque la sémantique est préservée).

C'est sur ce point que je ne sais pas ce qui est permis par le standard du C. Il y a des exemples de undefined behavior dans le manuel mais pas celle de l'exemple du journal : les exemples sont les overflow sur l'arithmétique signée (qui sont définies dans CompCert par les règles de l'arithmétique modulaire) et les accès hors bornes pour les tableaux qui renvoient une erreur.

D'après le deuxième principe que je cite du manuel « Second, the compiler is allowed to select one of the possible behaviors of the source program », le compilateur peut choisir n'importe quel comportement possible en accord avec la norme en cas de non déterminisme; c'est sur ce point que je n'ai pas bien compris si le choix de clang est acceptable (certains disent que oui, d'autres disent non) et pour moi cela reste encore bien obscur.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

La qualité du noyau (je dirais même la qualité logicielle au sens large), honnêtement, c'est assez récent comme problématique (moins de 5-10 ans), les choses se mettent en place et les progrès sont malgré tout importants.

Je suis étonné du caractère si récent de la prise en compte d'une telle problématique. J'ai terminé mes études il y a une quinzaine d'années et ce genre de questions étaient au cœur de la formation. Personnellement, l'utilité pour l'informatique était une chose qui, à l'époque, me semblait un cas d'application amusant mais sans plus; je regardais la chose d'un air amusé, les fondements des mathématiques m'important plus que ceux de l'informatique. Ce n'est que très récemment que je me suis repenché sur le lien avec le développement logiciel. À l'époque, les deux seuls langages que l'ont m'a enseigné était OCaml et Coq : avec le premier je m'étais amusé à faire un système de calcul formel sur l'arithmétique transfinie de Cantor, et avec le second j'avais formalisé quelques résultats élémentaires d'arithmétiques. Autant dire des questions de peut d'intérêt pour du développement logiciel.

Ceci étant dit, il est connu de longue date que la qualité logicielle relève de la preuve mathématique. Les approches dignes des sciences expérimentales à coup de tests unitaires ou de fuzzer, c'est gentil : ça peut détecter la présence de bugs, mais cela n'en prouvera jamais l'absence. À un moment, quand on affirme, il faut pouvoir prouver, quitte à le faire à la main :

Vous affirmez ? j'en suis fort aise.
Et bien ! prouvez maintenant.

pourrait être la devise des kantiens.

Quand je lis, par exemple, dans ce fil, que Nicolas Boulay demande qu'il faut démontrer la supériorité d'une solution avant de la mettre en œuvre et que gasche doit lui répondre :

Ce dont je parle ici (mais c'est loin d'être la seule sorte de recherche qui pourraitêtre utile au noyau) c'est d'éliminer, par des outils d'analyse, des classes entières de bugs possibles du code du noyau (use-after-free, accès à de la mémoire non initialisée, usage incorrect des verrous…). Tu écris comme si l'utilité de ce résultat final restait à démontrer, ce qui me semble complètement fou—évidemment c'est utile, et évidemment un noyau qui a su mettre ces outils en place va se retrouver loin devant un noyau qui ne l'a pas fait sur le long terme, en terme de robustesse et de qualité.

je tombe des nues. :-O Mais enfin, c'est une évidence pour qui est un minimum rigoureux intellectuellement ! On pourrait y rajouter en écho ce passage de l'évangile selon Saint Luc (chapitre 6, versets 47-49) :

47 Quiconque vient à moi, écoute mes paroles et les met en pratique, je vais vous montrer à qui il ressemble.

48 Il ressemble à celui qui construit une maison. Il a creusé très profond et il a posé les fondations sur le roc. Quand est venue l’inondation, le torrent s’est précipité sur cette maison, mais il n’a pas pu l’ébranler parce qu’elle était bien construite.

49 Mais celui qui a écouté et n’a pas mis en pratique ressemble à celui qui a construit sa maison à même le sol, sans fondations. Le torrent s’est précipité sur elle, et aussitôt elle s’est effondrée ; la destruction de cette maison a été complète. »

ou encore cet extrait de la préface des Prolégomènes à toute métaphysique future qui pourra se présenter comme science de Kant :

D'autre part il n'est pas tellement inouï qu'après avoir longtemps pratiqué une science, si on pense avec étonnement au progrès qui y a été accompli, on finisse par se poser la question de savoir si et comment de façon générale une telle science est possible. Car la raison humaine est assez désireuse de construire pour qu'il lui soit déjà maintes fois arrivé de bâtir la tour pour, puis de la démolir pour voir de quelle nature pouvait bien être son fondement. Il n'est jamais trop tard pour devenir sage et raisonnable; mais lorsque l'enquête est tardive, elle est plus difficile à mettre en train.

Lorsque gasche affirme que c'est un investissement sur le long terme :

Long terme: je pense que si les gens s'y mettaient sérieusement aujourd'hui il faudrait de l'ordre de 10-15 ans pour ça porte ses fruits.

cela va également de soi. Mais plus le projet tarde à s'y mettre, plus la base de code (déjà très volumineuse) augmentera et plus il sera difficile, voire surhumain, de mettre en pratique ce genre d'approche de contrôle qualité. Il vient donc naturellement à l'esprit cette question : la communauté en charge du développement du noyau est-elle sensible à ces questions ou s'en moque-t-elle fondamentalement ?

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Autant le code python me parle (je ne connais pas du tout ce langage), autant le DSL ne me parle pas.

Là, il y à un truc que je ne comprends pas du tout. Je n'avais pas prêté attention au message de ta part auquel gasche t'a répondu en présentant ce DSL, mais tu y reprochais à OCaml de ne pas générer des instructions SIMD en écrivant :

De plus, ocaml pourrait faire des map et fold sur des array de nombres, et proposer des versions vectorisés des opérations en question.

Il te répond avec un langage qui fait cela pour du code sur GPU, et tu réponds que ça ne te parle pas ? C'est quoi le problème ? Qu'ils utilisent la lettre pour définir des fonctions ? Qu'ils écrivent reduce et non fold ?

Si j'écris cela :

let (<.>) f g = fun x -> f (g x);;

let dot = fun xs ys -> Array.(fold_left (+) 0 <.> map2 ( * ) xs) ys

dot (Array.of_list [1; 2]) (Array.of_list [3; 4]);;
- : int = 11

alors tu comprends, mais tu voudrais que cela génère du code optimisé avec instructions SIMD ?

Mais quand on écrit :

dot = λxs ys. (reduce (+) 0 ◦ map (∗)) (zip xs ys)

alors tu ne comprends plus ?

On pourrait rendre le code python encore plus concis avec :

dot = lambda xs,ys: sum([a * b for a,b in zip(xs, ys)])

mais quand on sait ce qu'est un fold (ou reduce), un map et une composition de fonctions, l'équivalence des deux écritures est évidente.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

L'incompréhension venait du fait que le message de Renault pouvait être compris comme : « à partir de -O2 le compilateur se réservait le droit de modifier la sémantique d'un programme [qui possède une sémantique] ».

Tu n'es pas très joueur ! Moi, quand je m'ennuie, je joue à la roulette russe; ou en plus fun, je fais comme cap'tain sports extrêmes : je fais du saut à l'élastique mais sans élastique, avec un élastique on a aucune sensas' ! :-P

Pour prendre le manuel d'un compilateur qui ne s'amuse pas à changer la sémantique du code (« Traduttore, traditore » ou « Traducteur, traître » dit son manuel) :

There are three noteworthy points in the statement of semantic preservation above:

• […]
• Second, the compiler is allowed to select one of the possible behaviors of the source program. The C language has some nondeterminism in expression evaluation order; different orders can result in several different observable behaviors. By choosing an evaluation order of its liking, the compiler implements one of these valid observable behaviors.
• Third, the compiler is allowed to improve the behavior of the source program. Here, to improve means to convert a run-time error (such as crashing on an integer division by zero) into a more defined behavior. This can happen if the run-time error (e.g. division by zero) was optimized away (e.g. removed because the result of the division is unused). […]

et à la question « qu'est-ce qu'un comportement observable ? », il précise :

More precisely, we follow the ISO C standards in considering that we can observe:

• Whether the program terminates or diverges (runs forever), and if it terminates, whether it terminates normally (by returning from the main function) or on an error (by running into an undefined behavior such as integer division by zero).
• All calls to standard library functions that perform input/output, such as printf() or getchar().
• All read and write accesses to global variables of volatile types. These variables can correspond to memory-mapped hardware devices, hence any read or write over such a variable is treated as an input/output operation.

Je ne connais pas bien la sémantique du C mais, pour l'exemple du journal, il me semble bien que l'optimisation de clang ne respecte pas ces principes.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Merci ! :-)

Je teste :

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 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 correspond à une vérification dynamique de type avant de continuer « l'exécution » vers le conséquent.

Et ça marche !! :-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Au passage, je me demande s'il n'y a pas un lien avec une autre entrée de suivie que j'avais faite. Quand on met plusieurs formules en lignes et que l'on mélange avec du texte en chasse-fixe, elles ne sont pas toutes traitées.

Un test : le (d'où le \ de Haskell ou Elm) du lambda-calcul était à l'origine en majuscule .

Je veux bien essayer de voir d'où cela vient et tenter de corriger le problème, mais je ne sais pas par où commencer dans la base de code du site.

P.S : après prévisualisation, le test semble bien traiter le , mais ce n'est pas toujours le cas. Dans ce commentaire, j'ai un $x \in \omega$ non interprété en .

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

C'est bon, ça marche. Merci ! :-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

La non constructivité induit qu’il n’existe pas forcément de moyen de former un algorithme à partir du théorème ou de la formule, et c’est bien tout…

La correspondance s'étend aussi au raisonnement par l'absurde et donc à la logique classique, ce sont les exceptions dans les langages de programmation (les blocs try-with-finally). Voir ce texte de Jean-Louis Krivine (page 3).

Je crois que tu confonds « formule de la logique du premier ordre » et « logique du premier ordre ». Ou alors c’est moi qui confond…

Ce n'est qu'une question de vocabulaire : il y a d'un côté les jugements que l'on considère (calcul des prédicats ou calcul propositionnel, au premier ou second ordre) et de l'autre les règles de déductions (classique ou intuitionniste). Comme dans une logique on considère à la fois les règles de formations des jugements et les règles de déduction, pour éviter toute ambiguïté, il serait sans doute préférable de parler de logique classique du premier ordre et de logique intuitionniste du premier ordre.

Cela dit j’ai quand même l’impression d’être grugé. Dans un cas, le connecteur « -> » est vu par correspondance de curry-howard comme le type d’une fonction, alors que dans l’autre pour un langage dynamique tu as complètement oublié cette correspondance implication/fonction et c’est le quantificateur qui joue ce rôle.

Le quantificateur universel c'est le du lambda-calcul, le\ de Haskell, le fun de OCaml… c'est lui qui abstrait sur la totalité d'un domaine et, effectivement, dans le calcul des prédicats, on abstrait sur tout le domaine du modèle — sur tout l'univers des ensembles dans ZF. Les langages dynamiques sont des langages avec typage statique… qui n'ont qu'un seul type statique. Là où dans les théories des types, comme en Coq, on peut n'abstraire que sur les valeurs d'un type donné.

L'implication est bien toujours le signe d'une fonction mais, dans mon exemple, elle ne spécifie rien sur sa sortie pour une entrée qui n'est pas un ordinal. Si on reprend mon énoncé (légèrement modifié) :

il dit qu'à tout ensemble x, il peut en associer un autre y. Lorsque x est un ordinal, l'énoncé affirme que y est son prédécesseur qui est aussi un ordinal, mais dans le cas contraire (qui peut arriver, on a quantifié sur tous les ensembles), il ne dit rien sur y. La preuve d'un tel théorème expose, dans le cas où x est un ordinal, un moyen de produire un tel y et fournit la preuve que y est aussi un ordinal. En revanche, dans le cas où x n'est pas un ordinal, elle ne dit rien sur y (si ce n'est que c'est un ensemble, donc n'importe quelle valeur possible). Ce qui me fait penser à ce code Go :

func pred(v interface{}) (uint, error) {
  var res uint
  var err error

  switch i := v.(type) {
  case uint:
    if i == 0 {
      res = uint(0)
    } else {
      res = uint(int(i) - 1)
    }
  default:
    err = errors.New("not an uint")
  }
  return res, err
}

Il prend en entrée toute valeur possible (n'importe quel ensemble pour ZF), dans le cas où c'est un uint renvoie un y selon la même spécification que l'énoncé, ou bien renvoie une erreur si l'entrée n'est pas de type uint (cas de la preuve qui ne dit rien sur y, on renvoie une erreur). Ici le procédé est totalement constructif au sens des règles de déductions intuitionnistes. Le fait que la preuve du théorème prouve aussi que y est un ordinal, quand x l'est, se retrouve sur le type de sortie de la fonction en Go.

Après réflexion, on pourrait faire quelque chose de similaire en OCaml. Pour cela, il faut un type dans lequel on puisse plonger des valeurs de n'importe quel type : on parle de type universel. La signature d'un module fournissant un tel type est :

module type Univ = sig
  type t
  val embed : unit -> ('a -> t) * (t -> 'a option)
end

Je passe les détails d'implémentations d'un tel module (il faut utiliser un type somme extensible, comme l'est celui des exceptions dans le langage) et montre juste son usage en supposant que l'on a module U : Univ, c'est à dire un module fournissant un tel type :

(* ici on a des fonctions pour injecter dans et projeter
 * depuis le type `U.t` des valeurs de type `int` ou `nat` *)
let (inj_int : int -> U.t), proj_int = U.embed()
let (inj_nat : nat -> U.t), proj_nat = U.embed()

(* on définit maintenant à partir de la fonction `pred` sur `nat`
 * une fonction `pred` générique sur le type universel `U.t` *)
 let pred_gen v = match proj_nat v with
   | None -> None
   | Some n -> Some (pred n)
;;
val pred_gen : U.t -> nat option = <fun>

(* si la valeur de type `U.t` contient un `int`, on renvoie `None` *)
pred_gen (inj_int 2);;
- : nat option = None

(* si elle contient un `nat`, on renvoie son prédecesseur *)
pred_gen (inj_nat (S (S O)));;
- : nat option = Some (S O)

Pour en revenir aux différentes logiques, le problème est bien dans le calcul des prédicats. Il est tel que, lorsqu'on l'interprète, toute les choses dont il parle sont considérées comme étant homogènes. Par exemple, si on veut formaliser la théorie des espaces vectoriels dans un tel symbolisme, il faut mettre les scalaires et les vecteurs dans un même sac fourre-tout et un modèle d'une telle théorie devra donner une signification à la somme d'un scalaire et d'un vecteur (ce qui, fondamentalement, n'a aucun sens dans un tel cadre). Raison pour laquelle je disais que les approches de la logique via la théorie des types captent bien mieux la notion de concept : le concept de scalaire ne sera nullement mélangé arbitrairement avec celui de vecteur, ce seront deux types distincts.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Je suis ingénieur, et je n'avais pas entendu parler de Lambda avant de faire un dea d'info.

Moi aussi, je n'avais jamais entendu parler de lambda-calcul avant mon DEA. Ce que je voulais dire, dans le fond, c'est que le niveau d'abstraction requis pour le comprendre relève du premier cycle en mathématique (une fois que l'on a expliqué ce que signifie le lambda, ce qui prend deux minutes). Tu trouves (si je me fie à ce que j'ai déjà lu) que elm est un bon langage pour faire du développement web : ce type de code doit être assez standard en elm. Elm a la même syntaxe que Haskell où le lambda est remplacé par l'anti-slash \, c'est tout. Après c'est du map-reduce, on ne peut plus classique en programmation fonctionnel, ce qui n'exige pas un niveau de compréhension d'un niveau doctoral.

En OCaml, on l'écrirait ainsi :

(* reduce c'est tout simplement fold_left *)
let reduce = List.fold_left

(* opérateur de composition infixe *)
let (<.>) f g = fun x -> f (g x)

let map = List.map
let zip = List.combine
let mul (a,b) = a * b
let sum = reduce (+) 0
(* le lambda c'est le mot-clé fun *)
let dot = fun xs ys -> (sum <.> map mul) (zip xs ys)

dot [1; 2] [3; 4];;
- : int = 11

L'avantage pour des chercheurs de passer par du lambda-calcul, sans ajouter trop de sucre syntaxique, est d'avoir rapidement un prototype opérationnel comme preuve de concept.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

J'imagine que les usagers de ce genre de DSL sont docteur en mathématique pour le calcul linéaire. Je ne vois pas qui d'autres pourraient s'en servir vu le formalisme mathématique retenu.

Tu ne penses pas que tu exagères un peu là ? C'est du niveau premier cycle en mathématique (allez, fin de premier cycle pour être gentil).

Exemple sur la définition du produit scalaire :

dot = λxs ys. (reduce (+) 0 ◦ map (∗)) (zip xs ys)

et sa traduction en python :

from operator import mul
dot = lambda xs,ys: sum(map(mul, xs, ys),0)

>>> dot([1,2], [3,4])
11

la fonction zip existe aussi en python :

>>> zip([1,2],[3,4])
[(1, 3), (2, 4)]

la différence étant que les fonctions map n'ont pas la même interface entre les deux langages. La définition du produit scalaire entre vecteurs en python, je l'ai prise de la documentation python officielle. Sinon, voir aussi cette réponse sur stackoverflow :

from operator import add, mul
sum_r = lambda xs: reduce(add, xs, 0)
dot = lambda *lists: sum_r(reduce(mul, data) for data in zip(*lists))

>>> dot([1,2], [3,4])
11

C'est du python on ne peut plus idiomatique.

Et ne me parle pas de je ne sais quel grade doctoral : j'ai le même grade universitaire qu'un ingénieur, à savoir un bac+5.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Je précise ici ma réponse sur ZF vu comme un langage dynamiquement typé. On pourra continuer la discussion de cette sous-question sous ce commentaire et laisser celle sur la physique à un autre fil.

Je comprend bien l’idée, mais l’analogie trouve ses limites vu que la logique du premier ordre n’est pas constructive.

Ici tu confonds deux choses : la logique du premier et la logique intuitionniste. La première concerne les règles de formation des jugements, la seconde traite des règles d'inférences ou raisonnements. J'ai déjà écrit ailleurs un commentaire, en réponse à une question de Michaël, sur la différence entre les deux notions, le rapport entre programmes et preuves de théorème (correspondance de Curry-Howard) et la distinction entre les systèmes de types de OCaml et de Coq.

Si x n’appartient pas à Oméga, ben, rien, ça ne pose pas de problème.

Si ça pose problème : dans un cas l'énoncé est prouvable dans ZF (c'est un théorème) dans l'autre il est réfutable, et cela selon les règles intuitionnistes (sans raisonnement par l'absurde). Exemples :

Le premier se paraphrase en français ainsi : tout ordinal fini est soit vide, soit le successeur d'un ordinal fini. Le second se paraphrase ainsi : tout ensemble est soit vide, soit le successeur d'un autre. Tu remarqueras, au passage, que le français est tout à fait apte à exprimer de tels énoncés, sans recourir à un symbolisme quelconque. ;-)

Le premier est trivialement vrai, le second est trivialement faux dans ZF. Le premier exprime le type de la fonction prédécesseur. En OCaml, on écrirait cela ainsi :

type nat =
  | O : nat
  | S : nat -> nat

let pred_nat n = match n with
  | O -> O
  | S m -> n
val pred_nat : nat -> nat = <fun>

En Coq, cela se formalise de manière assez similaire :

Inductive Nat :=
  | O : Nat
  | S : Nat -> Nat.

Fixpoint pred x :=
  match x with
  | O => O
  | S n => n
  end.

(* j'y adjoins la preuve du théorème *)
Theorem pred_spec :
  forall (n : Nat), n = O \/ exists (m : Nat), n = S m.
Proof.
intro n.
destruct n.
- left; reflexivity.
- right; exists n; reflexivity.
Qed.

Ici la fonction pred est sous-spécifiée (elle a pour type Nat -> Nat), mais on pourrait lui donner un type plus précis analogue à ce qu'exprime le théorème, qui est la traduction en Coq du premier énoncé pour ZF. En revanche les contraintes de typage statique de l'un ou l'autre langage ne permettent pas d'exprimer le second énoncé. Contrairement à Python :

>>> def pred(x):
...   if type(x) == int :
...     if x == 0:
...       return 0
...     else:
...       return x - 1
...   else:
...     return "not an int"
... 
>>> pred(2)
1
>>> pred("a")
'not an int'
>>> pred_unsafe = lambda x: x - 1
>>> pred_unsafe("a")
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "<stdin>", line 1, in <lambda>
TypeError: unsupported operand type(s) for -: 'str' and 'int'

La fonction pred avec vérification dynamique de type s'apparente au premier énoncé, tandis que la seconde fonction pred_unsafe s'apparente au second.

J'espère que la chose te semble plus claire maintenant. Il vaudrait mieux, du moins, car c'est une promenade de santé par rapport au problème du rapport entre le kantisme et ce qu'il entend par réalité. Ma réponse à ce sujet viendra plus tard, peut être ce midi ou en fin de journée si je trouve le temps qu'il faut pour la rédiger.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Cela dit si tu ne postules pas ça, il ne peux y avoir de sciences.

Les kantiens n'ont jamais nié une telle chose.

Je comprends pas trop en quoi tu postules que je veux me débarrasser de l’observateur.

Bah, quand on me dit que la pierre a une existence propre spatio-temporellement déterminée, j'interprète cela comme abstraction faite de tout rapport à un observateur possible, c'est-à-dire que l'on se débarrasse de l'observateur. Autrement dit, qu'il y est ou non des hommes, il existe un monde dans lequel des pierres évoluent dans l'espace et le temps et la physique est là pour découvrir les lois d'un tel monde. Ce que disent les kantiens, ce n'est rien d'autre que ce que disait Socrate : nous ne voyons que des ombres sur un mur, tels les esclaves de l'allégorie de la caverne. Qu'il y est quelque chose qui nous apparaisse comme une pierre spatio-temporellement déterminée, que cette chose soit bien réelle, nous l'accordons; nous disons juste qu'elle n'est telle que pour les êtres humains.

Je te répondrai plus en détail demain, mais j'ai l'impression que tu te méprends (comme Einstein lui-même d'ailleurs) sur ce que veulent dire les kantiens quand ils affirment que la pierre (ou tout autre objet physique) ne sont pas des choses en soi existant « sans nous ».

Donc « exécution » n’a pas trop de sens. Par contraste, en python, si tu passes un objet d’un mauvais type à une fonction, ben « boom ». Python se comportera pas bien du tout …

Disons que sans écrire un énoncé à quantificateur universelle borné (la condition ), on risque la contradiction ou l'énoncé vide de sens. ;-)

C’est une notion logique la notion de concept ?

Un peu mon neveux ! La logique s'occupe des règles pour former des concepts, des règles pour former des jugements à partir de ces concepts et des règles pour enchaîner ces jugements entre eux ou raisonnements. Le plan de la doctrine générale des éléments du traité sur la logique de Kant :

1. Des concepts
2. Des jugements
3. Des raisonnements

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

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 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.

Sommaire

• Kant et les théories des types
• Kant et la physique théorique

Kant et les théories des types

Tu peux arguer qu’il est possible de faire la même chose en langage naturel, mais il faut le contraindre de manière à ne garder que les jugements valides dans le système de règle défini. Or il n’a jamais décrit ces contraintes (enfin je te laisse l’infirmer ;).

Ce que tu me demandes (infirmer la chose) est impossible à effectuer dans un commentaire. Tout ce que je peux dire c'est que les liens entre la philosophie kantienne et les théories des types contemporaines sont une évidence pour qui les connaît : elles procèdent toutes de la même approche méthodologique.

Le mieux que je puisse faire dans un commentaire, c'est pointé du doigt quelques références : Per Martin-Löf et Jean-Yves Girard.

Le second est l'auteur, entre autre, du système F qui est un système de types génériques pour le lambda-calcul : c'est le système de type à la base de langages comme Haskell ou OCaml. Sur sa page personnelle (le lien est sur son au-dessus) tu trouveras une partie intitulée La syntaxe transcendantale :

La syntaxe transcendantale est la justification technique des thèses du fantôme de la transparence. Le programme est exposé dans l'article La syntaxe transcendantale, manifeste (Février 2011).

Le livre en question (le fantôme de la transparence) est celui dont j'ai parlé à gasche dans ce commentaire. Je ferais deux remarques là-dessus. Le qualificatif transcendantale est une référence on ne peut plus explicite à Kant, ce dernier ayant utilisé les expressions philosophie transcendantale ou philosophie critique pour qualifier son œuvre philosophique. Ensuite, à la fin de l'introduction du livre, on peut lire :

Le principal bénéficiaire de cette visite non guidée aura été l'auteur, tout surpris d'y trouver matière à de futurs développements techniques. Et de découvrir la surprenante adéquation du kantisme — au sens large — à la logique contemporaine. Ce qui n'est pas très étonnant après tout : que veut dire « raison pure », sinon logique ?

En ce qui concerne Martin-Löf, il est également l'auteur d'une théorie de types dépendants intuitionnistes. Il a participé au groupe de travail ayant écrit la théorie homotopique des types (HoTT) visant à fournir une alternative à ZF pour le fondement des mathématiques basée sur la théorie des types (ça se comprend, ZF c'est l'archétype du typage dynamique; il n'y a qu'un seul type statique : celui d'ensemble, tout le reste est dynamique, si je peux m'exprimer ainsi). Dans l'introduction du livre HoTT, on lit :

Per Martin-Löf, among others, developed a “predicative” modification of Church’s type system, which is now usually called dependent, constructive, intuitionistic, or simply Martin-Löf type theory. This is the basis of the system that we consider here; it was originally intended as a rigorous framework for the formalization of constructive mathematics.

Martin-Löf est aussi l'auteur d'un article : analytic and synthetic judgements in type theory sur la philosophie kantienne des mathématiques. De même l'omniprésence de Kant dans la première des trois conférences qu'il donna sur la logique en 1983 à Siena devrait te mettre sur la piste.

Lorsque l'on s'occupe à notre époque de théorie des types, éluder toute référence kantienne pourrait s'apparenter, pour reprendre une expression utilisée ailleurs dans les commentaires, à une faute professionnelle.

Kant et la physique théorique

Après effectivement on peut arguer que le cerveau fait des calculs de probabilité conditionnelles - http://www.college-de-france.fr/site/stanislas-dehaene/course-2012-02-21-09h30.htm très intéressant au passage - de là a dire que l’invention du concept de causalité est subordonnée à ça, ou si nous étions condamnés à l’inventer …

Je n'ai pas écouté la conférence mais seulement lu le texte qui l'accompagne. Je ferais deux remarques là-dessus :

• l'auteur occupe la chaire de psychologie cognitive expérimentale ;
• le terme « hypothèse » revient à de nombreuses reprises, comme il se doit pour une science expérimentale.

Kant et les kantiens ne pratiquent pas de science expérimentale mais de la science pure ou rationnelle, c'est-à-dire des sciences dont les principes fondamentaux ne sont pas fondés sur l'expérience et l'observation, et dans les sciences expérimentale ne considèrent que la forme nécessaire que doivent prendre leurs théories pour être adéquate à la structure de notre esprit. Tu noteras que je parles d'esprit et non de cerveau : le cerveau est aussi peu le siège de la pensée que le cœur est celui des émotions, si ce n'est par amalgame matérialiste. Dans un tel champ du savoir, le recours aux hypothèses est mal venu :

Pour ce qui concerne la certitude, voici la loi que je me suis imposée à moi-même : dans cette sorte de considération, l'opinion n'est en aucune façon permise, et tout ce qui ressemble seulement à une hypothèse est une marchandise prohibée, qui ne doit pas être mise en vente à bas prix, mais doit être saisie aussitôt que découverte. Car toute connaissance qui doit être établie a priori donne d'elle même à entendre qu'elle veut être tenue pour nécessaire; plus encore en ira-t-il d'une détermination de toutes les connaissances pures a priori, qui doit être la mesure et par la même l'exemple de toute certitude apodictique (philosophique).

Kant, Critique de la Raison Pure.

Avoir recours à des hypothèse dans ce genre d'enquête, ce serait comme vouloir fonder la mathématique sur des conjectures : ce n'est pas sérieux.

Maintenant, comme exemples de personnes ici du monde de la physique ayant écouté l'appel de Kant, je citerai :

• freejef et son laboratoire de Lille, d'après l'introdution de sa dépêche sur le recalage et la corrélation d'images ;
• Thibault Damour membre de l'académie des Sciences et spécialiste de relativité générale, d'après son texte sur la question Le temps passe-t-il ? (voir page 9)
• des épistémologues et physiciens d'après la conclusion du livre Petit voyage dans le monde des quanta d'Étienne Klein :

Certes les problèmes de fond posés par Bohr, Heinsenberg, Einstein, Schrödinger ou Pauli restent d'actualité, mais on dispose aujourd'hui pour les traiter de davantage de résultats et de davantage d'arguments. Plusieurs systèmes épistémologiques essaient d'intégrer ces nouvelles donnes : la thèse du réel voilé de Bernard d'Espagnat, le solipsisme convivial d'Hervé Zwirn, le réalisme physique de Michel Paty, et de façon plus diffuse le réalisme ouvert, l'opérationnalisme, le phénoménalisme, et enfin l'idéalisme, lui-même divisé en idéalisme radical et idéalisme modéré, les deux pouvant être plus ou moins kantiens…

E. Klein, Petit voyage dans le monde des quanta.

J'ajouterai simplement qu'une telle situation n'a rien d'étonnant quand on connaît certaines résultats de la physique quantique et le contenu de la philosophie kantienne. Je conclurai sur la réponse d'un kantien à un extrait du livre d'Étienne Klein :

En premier lieu, s'il est vrai que le vecteur d'état contient tout ce que l'on peu savoir d'un système quantique, autrement dit si le formalisme est complet, il faut admettre qu'un phénomène ne peut être interprété comme fournissant des informations concernant des propriétés qu'auraient les objets eux-mêmes, indépendamment de la connaissance que nous en avons. Songeons à une pierre. C'est un objet qui existe « pleinement » au sens où nous n'hésitons pas à lui attribuer par la pensée des propriétés bien définies : une taille, une forme, une couleur qui sont ce qu'elles sont, même en l'absence d'observateur. Les objets quantiques, eux, ne semblent pas pouvoir être considérés de la sorte puisque leurs propriétés ne sont pas toujours déterminées antérieurement à la mesure qui en est faite.

Ce qui choque un Kantien n'est pas ce qu'il dit des objets quantiques, mais ce qu'il dit de la pierre ! :-P

Les objets que nous observons, en tant qu'objets de la connaissance expérimentale, n'ont aucune existence propre indépendante de nous. Si nous voyons partout de l'espace et du temps dans l'expérience, c'est parce qu'on les y met nous-même (voir l'article de Thibault Damour). Ainsi, lorsque l'on fait abstraction de tout rapport à l'expérience possible alors l'espace et le temps s'évanouissent, ce qui nous apparaît comme une pierre dans l'expérience devient un quelque chose d'inconnu, qui nous restera à jamais inconnaissable, une chose ineffable (dont on ne peut parler). L'avantage du kantisme sur toute autre approche épistémologique est qu'il ne fait aucune distinction ontologique entre la pierre et les objets quantiques : ce ne sont que de simples phénomènes qui n'ont pas d'existence propre en dehors de leur rapport à un observateur.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Il y a quand même une légère différence dans les détails :)

Pas spécialement, le principe que je décris est celui qu'a utilisé Gödel pour démontrer son fameux théorème d'incomplétude : une théorie assez riche (au pouvoir expressif suffisant) pour parler d'elle même a toujours des énoncés indécidables (qu'elle ne peut ni prouver ni réfuter) et parmi ceux-ci figurent toujours sa propre cohérence (sa non contradiction). Ce que je dis c'est que si une théorie est assez riche (comme l'est ZF) pour exprimer les principes de la théorie des modèles et donc parler de la relation entre la forme et le contenu (ce en quoi consiste la vérité) alors elle ne peut engendrer son propre contenu (elle ne peut construire un modèle d'elle même) et fournir un critère matériel et universelle de la vérité, sous peine d'être incohérente d'après le théorème d'incomplétude. Dans ce cas, comme elle peut prouver tout et n'importe, on ne peut nullement avoir confiance dans ce qu'elle prétend affirmer.

Cette démarche consiste à réfléchir la métathéorie dans la théorie elle même, c'est le même genre d'argument qu'a utilisé Turing pour prouver l'impossibilité de résoudre le problème de l'arrêt pour sa machine universelle. D'un point de vue programmation, cela revient à dire qu'un langage ne peut se compiler lui-même sans une phase de bootstrap : il faut un coup de pouce extérieur au langage de programmation.

J’ai l’impression que tu décris une sorte de « principe de réflexion » de la pensée abstraite dans la logique formelle, comme dans l’univers constructible de Gôdel ( http://www.madore.org/~david/weblog/d.2013-03-19.2124.constructible.html ) ou les ensembles et leur structure décrit par un rang inférieur se reflètent dans les rangs supérieurs de différentes manières.

L'univers des constructibles de Gödel sert à prouver des théorèmes de consistance relative : si ZF est non contradictoire alors il en est de même de ZF augmentée de l'axiome du choix, ce dernier axiome n'introduit pas de contradiction dans la théorie. C'est du même ordre que les théorèmes de consistance relative que Poincaré a effectués au XIXème entre les géométries euclidienne et non euclidiennes. Le cercle de Poincaré, construit dans un espace euclidien, permet d'interpréter les axiomes de la géométrie hyperbolique. Autrement dit, si la géométrie euclidienne est cohérente alors il en est de même de l'hyperbolique.

En revanche aux questions : l'arithmétique est-elle cohérente ? la géométrie est-elle cohérente ? ZF est-elle cohérente ? la logique et son principe de contradiction est incapable d'y répondre. La seule chose qu'elle peut faire c'est prouver la cohérence d'une théorie en admettant la cohérence d'une autre. Par exemple, on peut prouver la cohérence de l'arithmétique à partir de ZF, mais reste la question : ZF est elle cohérente ? On peut continuer en ajoutant des axiomes de grands cardinaux qui prouvent la consistance de ZF (ils fournissent un modèle de celle-ci), mais reviens alors la question : ses nouveaux axiomes sont-ils cohérents ? Et cette approche turtles all the way down la logique formelle ne peut en sortir, pour la simple raison que, laissée à elle même, elle n'engendre que des tautologies (l'art de M. de La Palice) et est incapable de répondre à la question : comment des jugements synthétiques a priori sont-ils possibles ?

Les principes abstraits en langage naturel de Kant se reflètent dans les méthodes formelles modernes. Mais enrichis :)

Ça se discute, ils ne sont nullement enrichis, ce sont les mêmes mais exprimés dans une langue différente. Un principe ne deviendrait ni plus vrai, ni plus clair, ni plus riche sous prétexte qu'il serait exprimés en français plutôt qu'en anglais (ou vice versa). La méthode kantienne est on ne peut plus formelle (il n'y a pas plus formaliste qu'un kantien), et les langues naturelles sont tout à fait adaptées pour exprimer de tels principes. Il n'est pas nécessaire de recourir à des symbolismes compréhensibles par une machine (ce qui n'est d'ailleurs adapté qu'à la formalisation de la pensée mathématique mais nullement à la pensée philosophique, comme les problèmes de philosophie du droit) pour formaliser sa pensée : je préfère de loin l'usage du français à Coq, par exemple. Les langues naturelles ont, en leur sein, un système à type dépendant mais une grammaire plus complexe que les grammaires régulières des langages de programmation (il suffit de voir la difficulté que rencontre l'auteur de grammalecte, ou tous ceux qui travaillent sur le traitement automatique des langues).

Prenons, un principe de base de la logique de Hoare utilisée pour la formalisation des langages impératifs, celui de la composition des instructions :

{ P } S { Q }  { Q } T { R }
----------------------------
    { P }  S ; T { R }

une expression de la forme { P } S { Q } se lit : l'instruction S fait passer le système de l'état P à l'état Q. Une telle règle ce lit alors : si l'instruction S fait passer la machine de l'état P à l'état Q et que l'instruction T fait passer de l'état Q à l'état R, alors la série d'instructions S ; T fait passer de l'état P à l'état R.

Il se trouve que c'est l'analogue dans le paradigme de la programmation fonctionnelle pure de la composition des fonctions :

fun f g x -> g (f x);;
- : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c = <fun>

A --> B    B --> C
------------------
     A --> C

Autrement dit, des deux prémisses si A alors B et si B alors C, on conclue à si A alors C. Cela résulte d'une double application de la règle dite du modus ponens :

• si A alors B, or A donc B (modus ponens utilisant la première prémisse et l'hypothèse A)
• si B alors C, or B donc C (modus ponens utilisant la seconde prémisse et la conclusion du syllogisme hypothétique précédent)

ainsi en supposant A on conclue à C, c'est à dire que l'on a prouvé si A alors C. Ce genre de preuve, quelque peu pédante, est ce que nous oblige à écrire Coq (il offre quand même des techniques pour éviter de rentrer autant dans les détails).

Ce que Kant a prouvé, par exemple, dans la Critique de la Raison Pure c'est que le concept de cause (qui sert à expliquer les changements d'états des choses réelles dans le monde physique) n'est pas un concept d'origine empirique, mais un concept que nous imposons nous même à la nature en vertu de la structure formelle de notre esprit et qu'il a pour type (là j'emploie une terminologie contemporaine) la forme logique des jugements hypothétiques (si A alors B).

On pourrait exprimer le principe fondamentale de la dynamique de Newton ainsi dans un tel symbolisme : { p } F { p + F * dt}. Autrement dit, un corps dans l'état de mouvement p et soumis à une force F se retrouve dans l'état { p + F * dt } au bout d'un temps infiniment petit dt. L'on retrouverait ainsi les considérations entre les sémantiques petit pas (small step) ou grands pas (big step), auxquelles gasche faisait allusion dans ce commentaire, et la distinction entre les lois différentielles et les lois intégrales en physique théorique. La première étant une approche discrète (sémantique des langages de programmation), là où la seconde est continue (physique théorique).

Et c'est ce lien formel entre le principe de causalité et la forme des jugements hypothétiques qui explique que l'on peut construire des machines qui « exécutent » les calculs automatiquement.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

La logique peut aussi vérifier la cohérence interne des connaissances des experts sur leur sujet. […] Mais du point de vue de la cohérence, ça peut lever des lièvres.

Oui car telle est son affaire, elle peut montrer l'incohérence d'une formalisation. Pour ce qui est de prouver la cohérence, par contre…

Ça me rappelle ce passage humoristique dans la partie remerciements de la thèse de Perthmâd (qui, s'y j'en crois les notes de publication de la toute récente dernière version de Coq, a fait un gros travail de nettoyage et d'optimisation du langage des tactiques) :

— Un thésard demanda à Hugo Herbelin : « Coq est-il cohérent ? »
— Anomaly: Uncaught exception Mu.

Par malheur, l’histoire omet de raconter si l’étudiant fut illuminé ou bien s’il l’était déjà à l’instant même où il songea à passer un doctorat d’informatique fondamentale 5 [1].

[1]Par contre, l’histoire précise bien que le rapport de bug qui s’en suivit fut marqué WontFix par un certain kgoedel. Ce n’est pas dans le privé qu’on verrait ça.

Dans une démarche également historique, le passage que j'ai cité de la Critique de la Raison Pure est extrait du paragraphe sur la question « Qu'est-ce que la vérité ? » qui commence ainsi :

La vielle est célèbre question, par laquelle on se figurait pousser les logiciens dans leur retranchement et on cherchait à les amener, ou à devoir se laisser surprendre dans un pitoyable diallèle, ou bien à devoir avouer leur ignorance, et par la suite la vanité de tout leur art, est celle-ci : Qu'est-ce que la vérité ? La définition nominale de la vérité, qui en fait la conformité de la connaissance avec son objet, est ici accordée et supposée; mais on veut savoir quel est le critère universel et sûr de la vérité de toute connaissance.

C'est déjà une grande et nécessaire preuve de sagesse et de pénétration que de savoir ce que l'on doit raisonnablement demander. En effet, si la question est absurde en soi et si elle appelle parfois, outre la confusion de celui qui la soulève, l'inconvénient de porter à des réponses absurdes l'auditeur qui n'est pas sur ses gardes, et de donner ainsi le ridicule spectacle de deux personnes, dont l'un trait le bouc (comme disaient les anciens), tandis que l'autre tend un tamis.

Si la vérité consiste dans l'accord d'une connaissance avec son objet, cet objet doit être par là distinguer des autres; car une connaissance est fausse, si elle ne s'accorde pas avec lequel elle est rapportée, alors même qu'elle pourrait bien valoir pour d'autres objets. Or, un critère universel de la vérité serait celui qui vaudrait pour toutes les connaissances, sans distinction de leurs objets. Mais il est clair, puisqu'on y fait abstraction de tout contenu de la connaissance (du rapport à son objet), et que la vérité à trait justement à ce contenu, qu'il est tout à fait impossible et absurde de demander une marque de la vérité de ce contenu des connaissances, et qu'on ne peut donc proposer une caractéristique suffisante et en même temps universelle de la vérité. Comme nous avons déjà nommé plus haut le contenu de la connaissance sa matière, on devra dire : On ne peut demander aucune caractéristique universelle de la vérité quant à sa matière, parce que c'est en soi contradictoire.

Kant, Critique de la Raison Pure.

On trouve des considérations identiques dans le traité qu'il consacra à la logique. Premièrement, ce qu'il appelle la définition nominale de la vérité est celle que l'on utilise toujours de nos jours sous le nom de définition tarskienne de la vérité à la base de la sémantique tarskienne (utilisée en théorie des modèles). Ensuite, si l'on combine le théorème de Gödel auquel Perthmâd fait allusion (le théorème d'incomplétude) à une autre théorème fondamentale de Gödel (son théorème de complétude : une théorie est cohérente si et seulement si elle a un modèle), on aboutit à la conclusion du texte kantien cité ci-dessus. Une théorie (disons ZF, la théorie axiomatique des ensembles) qui fournirait un critère matérielle de sa vérité serait en mesure d'engendrer son propre contenu (fournirait un modèle d'elle-même), serait donc cohérente (en vertu du théorème de complétude) ce qui contredirait le théorème d'incomplétude.

Le théorème d'incomplétude clos une période historique au cours de laquelle la thèse centrale de la Critique de la Raison Pure fut attaqué de toute part par des logiciens, et Gödel finit par donner raison à Kant. :-)

On gagne déjà beaucoup à pouvoir faire tenir une foule de recherche sous la formule d'un seul problème. Par là, en effet, on ne facilite pas seulement pour soi-même son propre travail, en se le déterminant avec précision, mais on rend aussi plus facile à quiconque veut l'examiner de juger si nous avons ou non satisfait à notre dessein. Le problème propre de la raison pur est donc contenu dans la question suivante : Comment des jugements synthétiques a priori sont-ils possibles ? […]

Dans la solution du problème précèdent est engagée en même temps la possibilité du pur usage de la raison pour fonder est développer toutes les sciences qui contiennent une connaissance théorique a priori des objets, c'est-à-dire la réponse à ces questions :

• Comment la mathématique pure est-elle possible ?
• Comment la physique pure est-elle possible ?

Kant, ibid.

À cette subdivision de la question, précède le texte suivant :

Les jugements mathématiques sont tous synthétiques. Cette proposition semble avoir échappé jusqu'ici aux observations des analystes de la raison humaine, et même être exactement opposée à toutes leurs conjectures, bien qu'elle soit incontestablement certaine et très importantes dans ses conséquences. En effet, comme on trouvait que tous les raisonnements mathématiques procédaient tous d'après le principe de contradiction (ce qu'exige la nature de toute certitude apodictique) on se persuada que les principes étaient connu aussi étaient connus à partir du principe de contradiction : en quoi ces analystes; car une proposition synthétique peut bien être saisie d'après le principe de contradiction, mais seulement de telle sorte qu'une autre proposition synthétique soit supposée, d'où elle puisse être déduite, mais jamais en elle-même.

Kant, ibid.

Ce qu'a prouvé Gödel, c'est que la logique formelle (et donc le principe de contradiction) ne peut légitimer à elle seule le raisonnement par récurrence : le principe du raisonnement par récurrence est un pur jugement synthétique a priori.

Il y a un membre de linuxfr qui a pour signature quelque chose du style : «BeOS le faisait déjà il y a vingt ans ». Pour ma part, d'une manière générale, je dirais : ce que font les théories des types contemporaines, Kant le faisait déjà il y a plus de 200 ans. Par exemple, la logique de Hoare utilisée par frama-c, c'est dans la Critique de la Raison Pure; ou bien la programmation par contrat, la gestion de propriété des espaces mémoires par Rust ou Mezzo, c'est dans la Doctrine du Droit (que l'on peut voir comme une théorie de typage du droit romain). :-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Tout le monde doit avoir une adresse email non-pipeau chez pasBig pasBrother

Tu sous-entend que pasBillpasGates devrait administrer un serveur mail et offrir une adresse à chaque membre de linuxfr ? :-D

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.