La vie est mal configurée

Aller au contenu | Aller au menu | Aller à la recherche

jeudi, mai 18 2017

Équivalence des représentations de polyèdres convexes

On sait qu’un polyèdre convexe borné peut s’exprimer aussi bien comme l’enveloppe convexe V d’une famille de points que comme l’intersection H d’une famille finie de demi-espaces. On peut donc vouloir vérifier que deux telles représentations sont équivalentes.

On montre facilement que ce problème est dans co-NP :

  1. L’inclusion V ⊆ H se vérifie aisément (produit de matrices).

  2. H ⊊ V si et seulement si il existe un sommet de H (choix non déterministe sur les contraintes à intersecter) qui sort de V (test par programmation linéaire sur les coordonnées barycentriques).

Apparemment, la complexité de ce problème est inconnue ! Pas d’algorithme polynomial connu, pas de preuve de complétude…

PS L'algorithme suivant (pour polyèdres bornés) ne fonctionne pas :

  1. On minimise les représentations sommets et contraintes (un appel de programmation linéaire pour chaque sommet ou contrainte par rapport aux autres, soit temps polynomial).
  2. On vérifie l'inclusion des sommets dans les contraintes (produit de matrices).
  3. On vérifie que chaque contrainte sature au moins d sommets et chaque sommet au moins d contraintes et qu'aucune contrainte (resp. sommet) ne sature un sur-ensemble des sommets (resp. contraintes) saturés par une autre contrainte (resp. sommet).
En effet, la condition 3. est validée par un cube dont on a ôté un des sommets de la liste des générateurs.

mercredi, juillet 20 2016

Algorithmes, apprentissage et usages sociaux

Le mot « algorithme », jadis inconnu du grand public, est maintenant à la mode. Moi qui suis professionnellement très familier des « algorithmes », je ne comprenais pas certains débats, certaines réactions. Il me semble, à la réflexion, que le sujet mérite clarification, ce que je vais tenter de faire ici.

Un algorithme c'est, rappelons-le, un procédé de calcul automatique et effectif. Il existe des algorithmes pour réaliser des tâches extrêmement variées ; citons par exemple, comme sujet classique étudié dans les premières années d'informatique, les algorithmes de tri (comment trier des millions de données par ordre alphabétique, par exemple). Un algorithme se distingue d'un logiciel au sens qu'il s'agit d'une description « théorique » d'un procédé de calcul, tandis qu'un logiciel est la mise en œuvre « pratique » de divers algorithmes sous une forme effectivement exécutable par une machine.

Deux conceptions

Dans l'approche classique, le ou les concepteurs d'un algorithme étudient le problème, au besoin le découpent en sous-tâches réalisées par des algorithmes déjà connus, et conçoivent l'algorithme avec des idées assez précises justifiant son bon fonctionnement. Souvent, ils produisent une preuve mathématique que l'algorithme fait effectivement ce qu'il est censé faire, par exemple trier des données. En tout cas, les concepteurs de l'algorithme comprennent pourquoi celui-ci fait ce qu'il est censé faire et ont fait des choix conscients en ce sens.

Dans les approches par apprentissage, l'algorithme (par exemple, un algorithme qui reconnaît des objets sur une photographie) n'est pas directement le résultat de la réflexion de concepteurs humains. Son fonctionnement découle du choix d'un très grand nombre de paramètres par un processus automatisé d'apprentissage (par exemple, en « montrant » des images et des listes d'objets y figurant). À l'issue de ce processus, le concepteur humain du système ne comprend pas forcément les critères qui ont été retenus par l'apprentissage, et n'est donc pas forcément en mesure d'expliquer l'action de l'algorithme dont il a dirigé la conception.

Nuançons

Bien sûr, les deux cas cités ci-dessus sont quelque peu caricaturaux. Même dans le cas où un humain a conçu toutes les étapes d'un algorithme et peut justifier mathématiquement qu'il donne un résultat acceptable, il ne comprend pas forcément d'autres aspects — par exemple, il peut ne pas savoir combien d'étapes de calcul l'algorithme nécessite dans le pire cas, ou pourquoi l'algorithme, sur les cas intéressants en pratique, nécessite moins de pas de calculs que ce qu'il nécessite dans le pire cas. Ou encore, il peut ne pas savoir justifier qu'un algorithme est plus précis « en pratique » que ce qu'il est capable de démontrer. Enfin, dans le cas de la conception de logiciels complexes, si l'on peut souvent justifier précisément du fonctionnement de tel ou tel algorithme, on sait rarement démontrer le bon fonctionnement de l'ensemble.

Quant à l'apprentissage automatique, il nécessite souvent des ajustements et réglages conscients par des personnels spécialisés. L'étendue des choix et des ajustements humains dépend de la méthode d'apprentissage utilisée. Notamment, certaines nécessitent que le concepteur du système prévoie un important recodage et sélection des données d'entrée pour les rendre acceptables par l'apprentissage automatique proprement dit. Par ailleurs, même dans le cas de techniques d'apprentissage profond, où le résultat de l'apprentissage est un immense volume de paramètres, on peut parfois identifier que certaines couches du système de traitement de données identifient telle ou telle particularité des données en entrée.

Avertissement : si l'on peut dire que je m'y connais en algorithmes, je n'ai sur l'apprentissage d'autre expérience que des lectures, l'écoute de conférences et des jurys de stages utilisant ce genre d'approches. En aucun cas il ne s'agit donc de l'avis d'un spécialiste.

Sur les usages sociaux

Les débats sur « les algorithmes » portent en fait sur leur utilisation à des fins « culturelles » (tri d'information par les moteurs de recherche) et « sociales » (profilage des individus à des fins de recrutement, de prêts bancaires… ou d'estimation du risque de délinquance). Il n'y a pas, ou du moins très peu, de débat public sur des sujets comme la conduite, en bonne partie automatisée, des avions de ligne.

Pour ma part, je vois quatre sujets importants :

  1. Les algorithmes « classiques » et la sélection des données et autres réglages des algorithmes d'apprentissage reflètent des choix humains : ce que l'on considère ou non comme pertinent comme critère de choix. La sortie de l'algorithme n'est donc pas un résultat « scientifiquement objectif ». Or, on utilise souvent « c'est ce que dit la machine » comme argument d'autorité interdisant la discussion.

  2. Les critères, les choix définis humainement sont généralement gardés secrets, ce qui interdit tout débat public à leur sujets.

  3. Les choix produits automatiquement par l'apprentissage peuvent ne pas répondre à certains objectifs de société. Par exemple, il est possible qu'un algorithme issu d'apprentissage qui devrait prédire la probabilité de « petite délinquance » d'un jeune au vu de ses données personnelles (lieu de naissance, de résidence, catégorie socioprofessionnelle des parents…) à des fins de recrutement ou non recrutement conclurait, au fond (et sans que cela ne soit explicité), qu'un jeune d'une famille pauvre de Stains a moins de probabilité de commettre des vols à la tire qu'un jeune d'une famille riche de Passy. Certes, mais est-ce bien raisonnable ou sain d'utiliser cela comme critère ?

  4. L'utilisation de mécanismes politiques ou sociaux hors de la compréhension des citoyens pose un problème en démocratie. Déjà, une bonne partie des français ne comprennent pas le calcul de l'impôt sur le revenu (les « tranches ») et les ordres de grandeur du budget de l'État.


dimanche, juillet 17 2016

La plus grosse preuve des mathématiques

La presse s'est faite l'écho de la publication de « la plus longue preuve des mathématiques » — attention surprenante pour un domaine, la preuve mathématique formelle assistée par ordinateur, qui n'est pas franchement grand public. Il se trouve que j'assistais à la conférence où résultat a été présenté ; j'aimerais ici en donner un résumé accessible et quelques commentaires.

Un public plus averti pourra se rapporter à l'article de recherche publié aux actes de la conférence ; mentionnons aussi la page « everything's bigger in Texas » où les auteurs ont rassemblé diverses informations et articles de presse.

Le problème du coloriage des triplets de Pythagore

Le problème qui se posait est de savoir si l'on peut colorer (disons, en bleu ou en rouge) les nombres entiers en respectant certaines règles. Par exemple, on peut imposer qu'on ne peut colorer de la même couleur les nombres 3, 4 et 5, au motif qu'il s'agit d'un « triplet de Pythagore » : 5 est la longueur du plus long côté d'un triangle rectangle dont les deux autres côtés sont de longueur 3 et 4. En d'autres termes, si on prend a=3, b=4, c=5 alors on a la relation a²+b²=c². On va s'interdire de colorer de la même couleur les triplets de Pythagore, et on va tenter de colorier les entiers 1, 2, 3… en respectant ces règles. La question est alors de savoir jusqu'à quel entier on va pouvoir colorier, ou en d'autres termes jusqu'où on pourra aller jusqu'à rencontrer une impossibilité. Bref, il s'agit de savoir à partir de quand on sera forcé d'avoir un triplet de Pythagore d'une seule couleur.

(Petite parenthèse. Je n'ai pas la moindre idée de pourquoi les gens s'intéressent à ce problème, s'il sert à quelque chose, s'il a des ramification ailleurs en mathématiques. Voir à la fin de l'article pour plus de discussion sur l'impact et la position de ce résultat.)

La force brutale ?

Une approche « par la force brutale » serait d'énumérer tous les cas de coloriage. Par exemple, si on essaye de colorier tous les entiers de 1 à 5, alors on a deux choix (bleu ou rouge)pour 1, deux choix pour 2, deux choix pour 3, deux choix pour 4, deux choix pour 5, et donc 2×2×2×2×2, soit 32, choix au total. Si on avait voulu colorier de 1 à 16, on aurait eu 2×2×2×2×2×2×2×2×2×2×2×2×2×2×2×2, soit 65 536, choix au total. Et pour 1 à 40, on aurait 1 099 511 627 776 possibilités. Le nombre de combinaisons croît vertigineusement !

Oh, certes, on peut y faire quelque chose. Un constat : si on a un coloriage en bleu et rouge, alors on en obtient un autre « opposé » en intervertissant le bleu et le rouge. On peut donc s'économiser un peu de travail en décidant qu'un nombre (par exemple 42) sera coloré en bleu, puisque s'il existe une solution où il est coloré en rouge, alors il existe la solution « opposée » où il est coloré en bleu. Ceci ne nous change cependant pas la vie, car il y a toujours un nombre vertigineux de combinaisons.

(Petite parenthèse de vocabulaire. Le nombre de coloriages possibles des entiers de 1 à n c'est 2×…×2 n fois, c'est-à-dire « 2 puissance n », noté 2n. On dit aussi « 2 exposant n », d'où le terme de « croissance exponentielle ». On entend parfois dans les médias ce terme appliqué à toute croissance rapide, mais le sens mathématique est celui que j'explique ici.)

En l’occurrence, les chercheurs cités on démontré que l'on peut colorier les nombres de 1 à 7824 avec deux couleurs de façon à ce qu'aucun triplet de Pythagore ne soit colorié d'une seule couleur, mais que cela est impossible pour 7825. Il est clair qu'il ne peut s'agir d'une preuve par la seule force brute : en effet, il faudrait alors énumérer 27825 combinaisons, soit un nombre à 2356 chiffres. Même en employant tous les ordinateurs disponibles actuellement pendant un temps égal à l'âge de l'Univers, on est très, très loin du compte. Pareil nombre pourrait paraître « astronomique » mais est même au-delà de tout ce que l'on peut envisager dans le monde astrophysique…

Un peu plus astucieux

On peut tenter d'être plus adroit. Si l'on sait, par exemple, que l'on doit colorier 3 et 4 en bleu, alors on peut immédiatement en conclure que 5 doit être coloré en rouge. On peut ainsi propager facilement des informations… un peu comme le joueur de Sudoku qui dit « la seule possibilité pour cette case, vu les cases déjà remplies, c'est de valoir 7, mais alors je sais que cette autre case doit valoir 8… ».

Toutefois, comme le savent les joueurs de Sudoku qui s'attaquent aux grilles « difficiles », cette propagation simple ne suffit pas. Il est parfois nécessaire de faire une hypothèse (« cette case peut être 5 ou 6, alors j'essaye 5 »), et de travailler ensuite sous celle-ci. On peut alors aboutir à une contradiction : une case pourrait n'avoir aucune valeur possible ! Il faut alors rétracter l'hypothèse faite (« comme ce ne peut pas être 5, j'essaye 6 »). Dans le problème du coloriage, on va donc être amené, lorsque la simple propagation ne suffit pas, à décider d'essayer qu'un nombre soit bleu, et si on aboutit à un conflit (une propagation conclut qu'un nombre doit être colorié en bleu et une autre propagation conclut que le même nombre doit être colorié en rouge) on se dit qu'on aurait dû choisir le rouge.

On explore ainsi une sorte d'arbre de choix : de la racine partent deux branches correspondant au premier choix (p.ex. branche de gauche, « 5 est colorié en bleu », branche de droite « 5 est colorié en rouge »), puis dans la première branche on trouve deux sous-branches (p.ex. branche de gauche, « 7 est colorié en bleu », branche de droite « 7 est colorié en rouge »), dans la deuxième deux sous-branches (p.ex. branche de gauche, « 8 est colorié en bleu », branche de droite « 8 est colorié en rouge »).

Ce que je viens de décrire est l'algorithme de Davis, Putnam, Logemann & Loveland (DPLL) (par algorithme, on entend « description d'un procédé de calcul automatique »). Mais il y a mieux !

L'apprentissage

Imaginons qu'il soit impossible d'avoir à la fois 47 et 49 en rouge et 70 et 5 en bleu. Cette règle n'apparaît pas dans les règles données initialement, qui ne parlent que de triplets de Pythagore, mais en est une conséquence. Malheureusement, l'algorithme DPLL ne s'en rendra pas compte, et pourra essayer plusieurs fois des combinaisons du style « 4, 47 et 49 en rouge et 99, 70 et 5 en bleu » ou « 3, 47 et 49 en rouge et 122, 70 et 5 en bleu ».

L'algorithme DPLL rétracte sa dernière hypothèse lorsqu'il rencontre un conflit. Ce conflit peut être analysé : « si je voulais colorier 84 en rouge, c'est parce que j'ai une règle qui dit que je n'ai pas le droit de colorier le triplet de Pythagore 80, 84 et 116 de la même couleur, or j'ai déjà colorié 80 et 116 en bleu ; j'ai colorié 80 en bleu parce que j'avais fait l'hypothèse que 60 et 100 étaient rouges, or 60, 80 et 100 forment un triplet de Pythagore ; et j'ai fait l'hypothèse que 116 était bleu. Par ailleurs, j'avais fait l'hypothèse que 84 était bleu. ». Ainsi, on est arrivé au conflit en raison des hypothèses « 84, 116 sont bleus, 60 et 100 sont rouges ». On peut donc apprendre une nouvelle règle : on ne peut jamais avoir à la fois 84 et 116 en bleu, 60 et 100 en rouge. Cette règle n'était pas initialement connue, mais je l'ai obtenue en analysant un conflit.

Ici, nous avons appris une règle supplémentaire à partir seulement de quelques étapes de raisonnement, mais en général, on peut ainsi déduire des règles qui « résument » une exploration assez fastidieuse, qu'on n'aura donc pas à refaire par la suite. Ici, une fois cette règle connue, on sait, une fois avoir sélectionné 84 en bleu, 116 en bleu, 60 en rouge, que 100 doit être bleu.

Ceci est la base de l'algorithme conflict-driven clause learning (CDCL). Je n'ai d'ailleurs pas évoqué diverses subtilités, comme par exemple comment éviter d'avoir à rechercher dans toutes la listes de règles celles qu'il faut considérer…

Je n'ai pas non plus évoqué comment les auteurs de l'article cité ont décomposé leur problème d'origine en un million de sous-problèmes, chacun résolu par CDCL, et comment ils ont réparti le million de problèmes sur 800 unités de calcul (ils travaillaient sur un super-calculateur composé de milliers d'unités de calcul, dont ils n'avaient loué que 800).

La preuve

On peut objecter qu'une telle preuve « par ordinateur » n'a guère de valeur, parce que le logiciel utilisé peut contenir des bugs.

Sur l'aspect « il est possible de colorier jusqu'à 7824 », il n'y a pas de problème. En effet, le logiciel, lorsqu'il répond positivement, produit le coloriage, qu'il est alors très aisé de vérifier.

Le problème est sur « il est impossible de colorier jusqu'à 7825 ». En effet, a priori, la correction de cette réponse repose sur le fonctionnement d'un logiciel très complexe. Il arrive que des logiciels mathématiques donnent des réponses fausses ou douteuses ; par exemple j'ai eu affaire à des logiciels qui, suivant leur version et la façon dont le même problème était présenté, répondaient « vrai » ou « faux ». On peut difficilement croire sur parole un logiciel qui se contente de répondre « il n'y a pas de solution ».

C'est là qu'intervient la fameuse « plus grosse preuve des mathématiques ». En effet, l'outil utilisé note les étapes de déduction qu'il effectue. Il produit ainsi une preuve (certes très longue, encore qu'on puisse la simplifier et la compacter) que l'on peut vérifier avec un logiciel indépendant. Il semblerait assez improbable que le logiciel ayant rédigé la preuve et le logiciel de relecture (voire les logiciels de relecture) aient tous des bugs qui laissent passer cette preuve, si elle était incorrecte, tandis qu'ils ont été abondamment testés par ailleurs.

Futile ?

On peut se dire que colorier des triplets de Pythagore est bien futile. En réalité, savoir « colorier » de deux couleurs suivant des règles d'incompatibilité, c'est extrêmement utile industriellement, car cela sert notamment à la recherche de bugs dans des circuits électroniques. Un « coloriage » réussi correspond alors typiquement à des valeurs électriques dans le circuit qui font que celui-ci produit un comportement indésirable. On dit souvent qu'un bug dans un circuit découvert uniquement après réalisation d'un prototype matériel coûte de l'ordre d'un million d'euros ; et un bug découvert après livraisons chez les consommateurs peut coûter largement plus (la société Intel, en 1995, avait dû organiser un rappel de microprocesseurs défectueux au coût de 475 millions de dollars des États-Unis).

Le tour de force des chercheurs ici a été non pas de développer un nouvel algorithme ou nouveau logiciel (encore qu'il y a eu certainement des développements spécifiques liés au découpage en un million de sous-problèmes), mais de tout mettre en œuvre pour résoudre un problème mathématique existant. On pourra objecter qu'il s'agit alors d’ingénierie ou du moins de recherche technologique et non de recherche scientifique.

Est-ce que cela en valait la peine ? Des mathématiciens comme Timothy Gowers objectent que, certes, on a une preuve d'impossibilité de coloriage en deux couleurs pour 7825, mais que cette preuve ne nous apprend rien sur le problème mathématique sous-jacent. Une vision naïve des mathématiques est que les mathématiciens cherchent à démontrer des théorèmes et que ce sont ceux-ci qui sont le but final, comme une sorte de grand prix. En réalité, avec la recherche de la preuve d'un grand théorème vient toute une réflexion, une compréhension, une théorisation ; pour reprendre une analogie assez cliché, ce n'est pas le but final qui fait l'intérêt du voyage, mais le trajet. De ce point de vue, la « grosse preuve » évoquée est assez pauvre : la produire n'a nécessité aucune compréhension de la structure des triplets de Pythagore.

Bien entendu, on peut rappeler que l'objectif posé par le président Kennedy d'aller sur la Lune, peut-être futile voire puéril en lui-même (allons-y pour montrer qu'on est plus fort que les Russkis !), a eu de nombreuses retombées technologiques, qui ne seraient peut-être pas arrivées, ou du moins pas aussi vite, s'il n'y avait pas fallu répondre au défi. Un défi peut lui aussi être intéressant non tant par son objectif final que parce qu'il a fallu réfléchir à comment le surmonter.

De ce point de vue, on pourra objecter que ni les approches ni les outils logiciels mis en œuvre n'étaient vraiment nouveaux pour cette preuve. Le logiciel CDCL utilisé, Glucose, de Laurent Simon (professeur à Bordeaux-INP) et Gilles Audemard (professeur à l'Université d'Artois), préexistait ; celui-ci met en œuvre plusieurs décennies d'idées et d'algorithmes dans le domaine de la satisfiabilité propositionnelle. L'approche cube-and-conquer de division en millions de sous-problèmes préexistait également.

Je pense cependant qu'avoir un résultat défi, identifié, visible, et qui parle aux mathématiciens professionnels, est une bonne chose pour la communication entre domaines scientifiques (je suppose que l'immense majorité des mathématiciens n'ont jamais entendu parler de preuve automatique, ou ont de fausses idées dessus ; encore que ce soit moins vrai de nos jours). Par ailleurs, du point de vue des mathématiciens, il est utile de savoir si un théorème est vrai ou faux avant de tenter d'en chercher une preuve élégante.

La couverture médiatique

Il est inhabituel qu'un résultat assez technique de mathématiques ou d'informatique sorte dans les médias grand public. Il semble qu'ici, l'origine de cette attention ait été un article dans la partie magazine de la revue Nature. J'ignore pourquoi Nature s'est penché sur le sujet (un communiqué des auteurs ? du service communication de leur université ?). Le Journal du CNRS a, avec un certain retard il est vrai, lui aussi évoqué le sujet, puis l'AFP et les médias qui suivent l'AFP. On a ici une illustration du suivisme des journalistes, qui parlent d'une chose parce que d'autres en ont parlé.

Ce qui, semble-t-il, a marqué les esprits, c'est qu'il s'agisse de « la plus grosse » ou « la plus longue » preuve des mathématiques. On pourra ironiser sur l'aspect « c'est moi qui a la plus grosse » de ces titres. On pourra également rappeler comment Richard Feynman se moquait de ces journalistes qui, pour évoquer une expérience de physique des particules, se concentraient sur un détail comme le fait que l'appareillage expérimental pesait 7 tonnes plutôt que sur le fond scientifique. Bref, ici, c'est le « record » qui est le motif.

Certains médias français ont évoqué « un algorithme de conception française » au sujet du logiciel Glucose (passons sur la différence à faire entre logiciel et algorithme). L'aspect « bien que cela ait été fait en Amérique, le fond est français » est important, un peu comme on souligne que telle ou telle région vinicole dont son succès en partie à l'expertise française exportée.

La théorie

J'ai dit l'importance des problèmes de « coloriage » (en réalité, des problèmes de satisfiabilité propositionnelle) pour l'industrie. Ces problèmes sont également très importants à titre théorique.

On l'a vu, la méthode naïve pour les résoudre consiste à énumérer un nombre exponentiel de possibilités. Les méthodes que j'ai évoqué plus bas (DPLL, CDCL) ne font pas mieux dans le pire cas. Une question légitime est donc de savoir si l'on pourrait trouver une méthode dont la croissance du coût du calcul avec la taille du problème soit seulement polynomiale (je ne définirai pas ce terme ici, mais, d'une certaine façon, ça croît bien moins vite qu'un exponentielle) — ou, à l'inverse, si l'on pourrait démontrer mathématiquement que cela est impossible. Cette question n'a pour le moment pas de réponse. On conjecture qu'il n'y a pas de méthode polynomiale, mais on ne sait pas le démontrer.

Cette question, aussi connue sous le nom de « P=NP ? » est considérée comme un problème central en informatique théorique. L'Institut Clay l'a listé parmi une liste de sept grand problèmes mathématiques « du millénaire », chacun doté d'un prix d'un million de dollars.

Le problème de la satisfiabilité propositionnelle est particulièrement important parce qu'un très grand nombre de problèmes lui ont été démontrés comme étant équivalents en un certain sens — si l'on trouve un algorithme polynomial pour l'un, alors il existe un algorithme polynomial pour les autres, et vice-versa. On peut dire (même si cette formulation est très discutable et doit être prise avec un grand de sel) qu'il s'agit de séparer ce qui est infaisable dans le pire cas, car trop coûteux, de ce qui est faisable.

Ces questions sont particulièrement importantes parce qu'elles ne dépendent pas de la technologie précise de calcul (sauf d'éventuels ordinateurs quantiques) et notamment ne se démodent pas avec le temps. Contrairement à un cliché répandu, les questions de science informatique ne sont pas forcément dépendantes d'une technologie en perpétuelle évolution à court terme je dirais même, le sont rarement.

mercredi, février 18 2015

A question regarding the a variant of the separation oracle model of linear programming

I have unresolved theoretical questions. Please see this very drafty explanation.

lundi, février 9 2015

Le théorème de Gödel pour les nuls

Suite à la publication d'un billet où j'évoquais des mystifications autour des théorèmes d'incomplétude de Gödel, on m'a demandé si je pouvais écrire une présentation « grand public » de ceux-ci. C'est ce que je vais tenter ici, en utilisant le moins possible de notations et de jargon mathématiques.

Malheureusement, c'est un sujet qui demande, pour être compris sans contresens, des explications assez conséquentes, et je m'excuse donc d'avance de la longueur de ce billet.

TL;DR : Comprendre ce que disent les théorèmes d'incomplétude de Gödel demande certaines bases exposées dans cet article, et si vous n'avez pas fait un minimum d'effort pour les acquérir vous ne comprendrez pas ce qu'ils disent. Ce n'est pas un drame, on vit très bien sans.

Lire la suite...

lundi, janvier 26 2015

Comment (ne pas) conclure à l'existence de Dieu à partir du théorème d'incomplétude de Gödel

Dans l'émission Tout et son contraire du 19 janvier 2015, les frères Bogdanov (en fait, sans doute un seul des frères et j'ignore lequel) ont tenté de convaincre Philippe Vandel et les auditeurs de l'existence de Dieu :

« (P. Vandel) […] Êtes-vous bien certain que Dieu existe ? Je vous pose la question, vous qui avez écrit Le Visage de Dieu, êtes-vous bien certain que Dieu existe ?

- (I. ou G. Bogdanov) On est certain en fait de trois choses, à propos de ce que l'on appelle Dieu.

- Encore ? Trois ?
- La première, c'est que l'Univers n'est pas né par hasard. C'est une certitude aujourd'hui, et même les scientifiques qui ont des tendances matérialistes ou qui refusent cette idée, évidemment, d'une causalité à l'origine, reconnaissent, admettent que l'Univers est très bien réglé à l'origine. La deuxième conclusion c'est qu'il existe un avant Big Bang.

- On est certain, vous les Bogdanov, ou la communauté scientifique ?

- La communauté scientifique dans son ensemble !

- Et le troisième argument ?

- Troisième point ! Il faut remonter en 1931. À cette époque là, un tout jeune homme — il a 24 ans — c'est un mathématicien brillant, brillantissime, il s'appelle Kurt Gödel, il est autrichien, découvre — il n'invente pas, il découvre — un théorème qui porte son nom. Que dit ce théorème ? Il dit « Tout système logique est nécessairement incomplet. » Si nous considérons maintenant que l'Univers — et c'est incontestable — est un système logique, alors il est nécessairement incomplet, et sa cause se trouve à l'extérieur de lui. Il a une cause, cette cause est à l'extérieur de lui, elle est différente de lui. L'Univers est matériel et temporel, alors cela signifie que la cause est immatérielle et intemporelle, on est quelque part tout près de Dieu. »

Si je mentionne cet échange, c'est parce qu'il me semble un très bon exemple d'une certaine façon de traiter de la science. Sans examiner de près les arguments, certains points doivent déjà nous alerter :

  1. Le locuteur prétend résoudre une question philosophique importante, qui occupe l'humanité depuis des millénaires.

  2. Il utilise un argument d'intimidation : « et c'est incontestable ».

  3. Il utilise des arguments d'autorité : la « communauté scientifique dans son ensemble ».

  4. Il essaye de récupérer l'aura d'un grand scientifique, à savoir Kurt Gödel, dont il rappelle le génie précoce.

  5. Il utilise des arguments de plusieurs domaines scientifiques dont la maîtrise conjointe est rare (ici, la cosmologie et la logique mathématique).

Contrairement à M. Bogdanov, je ne prétends pas m'y connaître en cosmologie. Oh, certes, j'ai bien lu quelques présentations de vulgarisation sur le Big Bang, mais je ne me hasarderais pas à discuter de ce qui a bien pu arriver avant (si toutefois cela avait du sens, ce dont je ne suis pas convaincu). En revanche, j'enseigne les théorèmes d'incomplétude de Gödel (ainsi que son théorème de complétude, mais c'est un autre sujet) et on me pardonnera donc mes objections à ce sujet. (*)

Rappelons ce dont il s'agit. Le premier théorème d'incomplétude de Gödel se résume en effet par « tout système logique est incomplet », mais cela est trompeur car on n'explique pas ce que l'on entend par système logique. L'énoncé suivant, trouvé sur Wikipédia, est plus précis :

Dans n'importe quelle théorie récursivement axiomatisable, cohérente et capable de « formaliser l'arithmétique », on peut construire un énoncé arithmétique qui ne peut être ni prouvé ni réfuté dans cette théorie.

Les systèmes logiques dont il est question sont des systèmes de règles destinés à formaliser les raisonnements en arithmétique entière, c'est-à-dire les raisonnements sur des énoncés comme « pour tout n, il existe un nombre premier entre n et 2n ».

On ne voit donc pas très bien le rapport avec l'Univers et en quoi celui-ci serait un « système logique » dans ce sens, fait que M. Bogdanov estime pourtant « incontestable ».

Il est possible que M. Bogdanov joue sur plusieurs sens de l'expression « système logique ». On l'a vu, dans l'énoncé du théorème d'incomplétude de Gödel, ce terme a un sens précis et très technique (et encore, j'ai épargné au lecteur les définitions possibles de la cohérence et de ce que veut dire « formaliser l'arithmétique »). Peut-être que son argument sur l'Univers se réfère à l'idée que l'Univers évolue selon des lois mathématiques, donc « logiques ». Bien entendu, tout raisonnement qui prétend démontrer un résultat en changeant le sens d'un mot entre deux étapes est un sophisme trompeur !

Quant à l'incomplétude logique, elle ne se réfère pas à l'existence d'une « cause » (notion non définie pour un système logique) mais à celle d'un énoncé qui ne peut être prouvé dans le système logique considéré et dont le contraire ne peut pas non plus être prouvé dans le système logique. Là encore, on glisse du sens technique du mot « incomplet » à une idée différente : « a besoin d'un objet extérieur comme cause ».

La suite ne vaut pas mieux. « Il a une cause [...] différente de lui. L'Univers est matériel et temporel, alors cela signifie que la cause est immatérielle et intemporelle. » Ce raisonnement est douteux, il suffit pour s'en convaincre de remplacer « cause » par « mère » et « Univers » par « bébé » : « Il a une mère différente de lui. Le bébé est matériel et temporel, alors cela signifie que sa mère est immatérielle et intemporelle. ». Absurde, non ?

Je pense, et cela est triste, que les raisons du succès des frères Bogdanov sont justement les points que j'ai relevés comme des signaux d'alerte :

  1. Le locuteur prétend résoudre une question philosophique importante, qui occupe l'humanité depuis des millénaires. Le public aime bien qu'on parle des « grandes questions », le reste fait mesquin.

  2. Il utilise un argument d'intimidation. Visiblement, le public aime bien les personnes assurées d'elles-mêmes, tandis que les scientifiques aiment souvent nuancer ou restreindre la portée de leurs propos.

  3. Il utilise des arguments d'autorité. Le public aime bien l'autorité.

  4. Il essaye de récupérer l'aura d'un grand scientifique. Le public a une vision de la science très « grands hommes » (Einstein etc.). À côté, l'universitaire lambda passe pour un médiocre, aigri et mesquin.

  5. Il utilise des arguments de plusieurs domaines scientifiques dont la maîtrise conjointe est rare (ici, la cosmologie et la logique mathématique). Cela fait érudit et donne l'impression d'une pensée vaste, à l'inverse de la « spécialisation » souvent tant décriée.

Il me semble, à ce point, assez vain de vouloir lutter. De toutes façons, ceux qui se laissent prendre à ce genre de divagations sur la Vie, l'Univers et le Reste ne lisent sans doute pas mon blog…

(*) Il me semble que les frères Bogdanov reprennent sur ce point un raisonnement douteux dû à Régis Debray.

jeudi, septembre 25 2014

Une question sur les modèles chez Alain Badiou

Comme le savent sans doute déjà certains de mes lecteurs, j'enseigne parfois la logique. Je trouve la logique du premier ordre difficile à enseigner non pas tant techniquement que conceptuellement : j'entends par là que la difficulté n'est pas dans la connaissance de théorèmes compliqués, d'astuces de démonstration ou de calcul, mais dans la compréhension des définitions que l'on utilise. Expérimentalement, dans un cours où figurent logique, calculabilité, et complexité, c'est la partie qui suscite le plus d'incompréhension.

J'ai donc voulu chercher comment les autres expliquaient les bases de ce sujet. J'ai bien entendu des ouvrages de logique mathématique (par exemple le Cori-Lascar, dont je déteste malheureusement la typographie) mais je voulais voir s'il y avait une façon différente d'exposer, peut-être moins « technique ». La logique étant enseignée, selon des divisions quelque peu administratives et artificielles, à la fois en informatique, mathématique et philosophie, il m'a paru intéressant de regarder un cours de logique de philosophe. Par ailleurs, bien conscient de mes lacunes en épistémologie, j'ai voulu améliorer mes connaissance sur ce sujet.

J'ai donc emprunté le Concept de Modèle, par Alain Badiou (un petit ouvrage publié en 1968 chez Maspéro dans la série « théorie — cours de philosophie pour scientifiques », collection dirigée par Louis Althusser, mais il y a une réédition récente).

Alain Badiou oppose dans cet ouvrage deux sens scientifiques du mot « modèle » (j'espère ne pas faire de contre-sens en résumant son propos avec mes propres mots et exemples) :

  1. D'une part, en sciences expérimentales, le modèle est l'appareil mathématique qui est censé refléter la réalité expérimentale : par exemple, pour rendre compte des phénomènes électromagnétiques, on parle des champs électrique et magnétique, reliés par les équations de Maxwell… ou, plus simplement lorsqu'il s'agit d'un circuit électrique, de tensions et intensités.

  2. D'autre part, le mot « modèle » désigne un concept mathématique précis en logique du premier ordre, qui donne une sémantique ou interprétationaux symboles (Badiou emploie plutôt le mot « marques ») des énoncés mathématiques : par exemple, qui associe au + des formules mathématiques l'opération d'addition usuelle sur les entiers.

Badiou développe plutôt ce second aspect. J'aime bien la façon dont il compare un travail très technique comme la construction d'un modèle « alternatif » de la théorie des ensembles avec une construction plus concrète : la construction d'un modèle de la géométrie riemannienne au sein de la géométrie euclidienne, tout simplement en prenant la sphère comme « plan » et ses grands cercles comme « droites ». En revanche, le vocabulaire employé est parfois inhabituel (peut-être est-ce seulement une question d'époque), et certaines explications me semblent un peu obscures.

Badiou relève également une limitation de la théorie des modèles, que certains de mes étudiants relèvent d'ailleurs d'eux-mêmes : construire un modèle d'une logique dans la mathématique « naturelle », « informelle », c'est le construire dans une méta-logique qui pourrait fort bien être elle même incohérente, autrement dit repousser d'un cran le problème de la cohérence sans l'épuiser.

En annexe, Badiou donne une démonstration du théorème de complétude de la logique du premier ordre (démontré par Gödel dans sa thèse de doctorat) par les témoins de Henkin (personnellement j'ai plutôt tendance à donner la construction d'un modèle de Herbrand, mais les goûts et les couleurs…).

Il y a en revanche quelque chose que je n'ai pas compris, c'est l'opposition maintes fois évoquée dans l'ouvrage entre l'« épistémologie bourgeoise » et une supposée épistémologie prolétarienne ou marxiste, basée sur le « matérialisme dialectique ». J'apprécierais donc sur ce sujet l'éclairage de spécialistes de philosophie, quand bien même l'ouvrage évoqué se voulait un cours d'initiation à la philosophie pour scientifiques.

Je conçois bien que toute modélisation mathématique suppose un choix de ce qui est important (et reflété dans le modèle) et de ce qui est négligeable ou hors champ. Pour prendre un exemple tiré de l'informatique, la modélisation des calculs informatiques par sémantique dénotationnelle fait disparaître le temps nécessaire au calcul, de sorte que deux programmes qui calculent la même fonction, mais l'un considérablement plus longtemps que l'autre, sont considérés comme équivalents par cette sémantique. On comprend bien que, s'agissant de tout problème se rapportant à l'humanité ou à la société, le choix de ce qu'il est important ou non d'observer et d'intégrer dans le modèle est politique, et que ce choix, intériorisé dans des modèles qui prétendent à une objectivité scientifique, relève bien d'une idéologie qui dépend d'un temps, d'un lieu, d'une histoire.

Il s'agit cependant ici d'une reconstruction personnelle de ce que Badiou aurait bien pu vouloir dire. Il me semble fort probable que, s'agissant d'un ouvrage cité et réédité d'un philosophe français reconnu, il devrait y avoir quelques lecteurs capables de m'éclairer !

Si je pense avoir une certaine idée de la lutte des classes, j'avoue notamment une certaine incompréhension du « matérialisme dialectique », bien que j'aie vu le terme dans l'introduction d'un ouvrage chinois de mathématiques. Là encore, toute aide serait appréciable, sachant que l'article Wikipédia ne m'aide guère.

mardi, juin 3 2014

2+4=6

Attention, ce billet parlera de logique mathématique, du Grand prix de philosophie de l'Académie française, de canards, de brocolis, de djender, et de Gottfried Wilhelm Leibniz.

La logique, en mathématiques, c'est quand après avoir fini de creuser à la pelle, on continue à la foreuse, toujours plus bas. Janine, sur son blog, énonce comme une évidence rationnelle que 2+4=6. Je voudrais ici expliquer en quoi cette « évidence » met en jeu un certain nombre de présupposés.

Lire la suite...

samedi, avril 26 2014

Honnêteté et moralité dans les définitions mathématiques

Il me semble bien que dans Les petits cailloux de Bruno Poizat, il est dit qu'un problème en calculabilité est juste un ensemble d'entiers naturels, dans une idéologie (ou est-ce une téléologie ?) qui veut que ce problème soit décidé.

C'est un peu plus subtil que cela. La plupart des problèmes de décision sont décrits non pas en termes d'entiers naturels, mais de structures finies comme des graphes, des automates, des formules, qui sont codées par des entiers naturels ; autrement dit l'ensemble d'entiers naturels dont il est question dépend du codage choisi.

Le codage est laissé implicite parce que, la plupart du temps, celui-ci n'a aucune importance du point de vue des propriétés de calculabilité et de complexité tant qu'il est raisonnable. Par exemple, un codage raisonnable d'un graphe est sa matrice d'adjacence, et pour encoder celle-ci en entiers naturels on peut utiliser un codage « raisonnable » des tableaux d'entiers, lui-même basé sur un codage « raisonnable » des couples d'entiers.

En revanche, du point de vue de la théorie de la complexité, est « déraisonnable » un codage qui occuperait une taille bien supérieure à celle d'un codage « raisonnable », par exemple un codage du graphe par la matrice d'adjacence suivi d'un nombre de zéros exponentiel en la taille du graphe. En effet, un tel codage fait artificiellement baisser la complexité des algorithmes proposés, puisque celle-ci est mesurée par rapport à la taille de l'entrée : si cette taille est artificiellement enflée, l'algorithme apparaît moins cher (c'est un peu comme la malhonnêteté d'une entreprise qui se prétendrait peu chère car avec un coût horaire un peu plus faible que ses concurrences, mais qui gonflerait considérablement le nombre d'heures nécessaires).

J'ai employé le mot « malhonnête », et effectivement, certains peuvent jouer sur les définitions pour présenter leurs travaux sous un jour meilleur (et notamment planquer des exponentielles sous le tapis, ce qui m'inciterait presque à raconter la blague sur l'exponentielle qui va dans un bar). Un grand classique : écrire les entiers en unaire et non en binaire (c'est-à-dire écrire IIIIIIIIIIIIIIII, soit 15 caractères, au lieu de 15, soit 2 caractères), ou, dans le même genre, formuler la complexité en fonction du nombre d'états et non du nombre de bits qui les encodent.

On peut également proposer des codages malhonnêtes où l'entrée devrait, sous peine d'être refusée comme mal formée, contenir tout ou partie de la solution du problème.

Certains codages, en revanche, rendent plus dur la tâche de l'algorithme de décision, par exemple les codages implicites ou succincts de graphes où la matrice d'adjacence est représentée par une formule logique prenant en entrée les numéros (en binaire) des sommets concernés, et produisant en sortie un booléen indiquant si oui ou non l'arête est présente. De tels codages, le plus souvent, font passer un problème de NP-complet à NEXPTIME-complet (voir Papadimitrou & Yannakakis, 1986). Là encore, par défaut on considère n'est pas dans un tel cas et qu'on utilise un encodage « explicite ».

Nous en concluons donc que les définitions usuelles de calculabilité et complexité font appel à des notions de bon sens et d'honnêteté tant chez l'auteur que chez le lecteur ! Surprenant pour des mathématiques, que l'on imagine déconnectées des intérêts humains...

mercredi, mars 12 2014

Évolution de ma position sur la NP-complétude

Comment la vision d'un scientifique sur un problème peut évoluer : prenons le cas de mon opinion sur la NP-complétude.

Lire la suite...

dimanche, avril 14 2013

Réductionnismes

Lire la suite...

samedi, avril 13 2013

Combinatoire de l'accouplement

Je voudrais revenir, plus sérieusement, sur le sujet du billet précédent, à savoir l'interprétation du mariage en théorie des graphes.

Lire la suite...

mardi, avril 2 2013

Scientificité des mathématiques

Récemment, au détour d'une conversation s'est posée la question de la scientificité des mathématiques, notamment selon les critères de Popper. Le point de vue de mon interlocutrice — j'espère ne pas le trahir — était que les objets mathématiques n'étant pas des objets physiques, le critère de réfutabilité de Popper ne s'applique pas : on ne peut pas réfuter une propriété mathématique par une expérience du monde réel. La droite mathématique (le corps des réel) est certes une idéalisation d'objets physiques (une règle, la trajectoire d'un rayon lumineux...) mais n'est pas un objet réel. Les axiomes mathématiques peuvent d'ailleurs décrire des objets mathématiques sans rapport avec le monde réel (par exemple, le groupe de classes d'idéaux d'un anneau de nombres).

J'entends cette critique et j'y suis sensible. J'aurais toutefois deux objections.

Lire la suite...

mercredi, mars 6 2013

Problème d'intuition

En ce moment, je travaille (entre autres) sur des algorithmes mettant en jeu des projections de polyèdres convexes. Une difficulté est de se représenter ce qui se passe : pour concevoir un algorithme, de prouver sa correction ou ses propriétés, il vaut mieux avoir une idée (au moins intuitive) de ce qui se passe, avant de passer au formel.

Nous nous représentons bien ce qui se passe en 1 dimension (une ligne), 2 dimensions (un plan, ce qui permet de tracer les choses sur une feuille ou un tableau), déjà un peu moins ce qui se passe en 3 dimensions quand la forme est un peu complexe, et nettement moins ce qui se passe en dimension supérieure.

Le problème est que les polyèdres en petite dimension ont des propriétés géométriques et combinatoires particulières. C'est particulièrement flagrant en 2 dimensions (polygones) : on peut arranger faces et sommets des polyèdres bornés en une liste circulaire sommet - face - sommet - face etc. Projeter 1 dimension à la fois a également des propriétés particulières.

Bref, pour ne pas me laisser guider par de fausses intuitions, il fallait au moins réfléchir à un polyèdre 4 dimensions qui s'envoie en 2 dimensions, et là je n'ai pas de vision graphique. Je dois m'en tenir à des espèces d'intuitions combinatoires (« il existe une solution basique du problème de programmation linéaire ») et des calculs sur le système d'inégalités.

Et vous, comment faites-vous ?

lundi, novembre 12 2012

Interprétation des résultats de Nate Silver

Tout le monde a déjà parlé de Nate Silver, cet analyste américain qui, s'appuyant sur des statistiques et un modèle mathématique assez simple (accumuler les résultats de sondages en privilégiant les plus récents et les plus fiables), a prédit correctement les 50 états de l'élection présidentielle américaine, après des succès pour d'autres élections et le baseball.

Je me demande quel est le sens à accorder aux « chances » affichées, du type « Obama a 80% de chances de gagner, Romney 20% ». Pour moi, c'est un modèle bayésien : il s'agirait en quelque sorte de probabilités conditionnées par les observations précédentes, avec comme espace des évènements les votes pour tous les électeurs. Dans ce cas, quelle est la distribution initiale supposée (et a-t-elle même une quelconque importance) ? Chaque électeur a une probabilité indépendante 50/50 de voter pour l'un ou l'autre ?

En revanche, je n'arrive pas à attribuer une interprétation fréquentiste. Si Silver s'était contenté de donner un chiffre pour Obama avec un intervalle de confiance, aucun problème (interprétation fréquentiste : si on refaisait un très nombre de fois les sondages et on appliquait l'algorithme de Silver, on obtiendrait plus d'une certaine proportion des résultats dans l'intervalle de confiance), mais là, je ne vois pas.

lundi, novembre 5 2012

Argument anti-réductionnisme

Le « réductionnisme épistémique » revient (si j'ai bien compris — je ne suis pas philosophe, faut-il le rappeler) à affirmer que les connaissances sur les parties élémentaires nous permettront de comprendre le tout. En exagérant un peu, la connaissance des comportements des composants élémentaires de la matière nous permettront de comprendre les comportements de celle-ci, la connaissance du comportement des neurones nous permettra de comprendre la pensée et les comportements humains, etc.

Je n'ai jamais compris le succès de pareil point de vue (succès au sens de : beaucoup de personnes y souscrivent, pas au sens des retombées positives sur notre compréhension des choses), notamment au regard des résultats de base de la calculabilité, par exemple le problème de l'arrêt.

Sans rentrer dans des détails inutiles, il s'agit de systèmes dont le comportement est régi par des règles élémentaires parfaitement simples et connues, et dont on peut cependant prouver qu'il n'y a pas de méthode automatique qui permette de prédire leur comportement global.

Prenons un exemple simple. Vous me donnez un mot (une succession quelconque de lettres, peu importe qu'il soit dans un dictionnaire), par exemple AZKWUJZ, ainsi que des règles « rechercher et remplacer », par exemple UJHW→OWPZ et vous vous posez la question de savoir si, par application successive de ces règles, on peut finir par obtenir un mot constitué uniquement de la lettre A. On montre qu'il n'y a pas de processus automatique qui, au vu du mot de départ et de la liste de règles, réponde à cette question. (*)

Si la connaissance d'étapes élémentaires aussi simples ne permet pas de conclure mécaniquement quoi que ce soit concernant le comportement global du système, je me demande comment on peut affirmer que connaître des phénomènes microscopiques incertains, difficiles à mesurer, suffira à prédire la globalité.

(*) On me fait remarquer que ma définition n'est pas claire pour certains. Réessayons. Le problème se pose de la façon suivante : si on donne un mot initial, un mot final et une liste de règles rechercher/remplacer, alors soit il y a une façon d'obtenir le mot final par une suite d'application des règles (et on répond « vrai »), soit il n'y en a pas et on répond « faux ». Par exemple, si le mot initial est AAABC, le mot final ZX et qu'on a une règle AAB→AB et une règle ABC→ZX, alors la réponse est « vrai » parce qu'on peut y arriver par AAABC→AABC→ABC→ZX. Notons que certaines suites d'applications de règles, comme AAABC→AAZX restent ensuite « coincées », mais cela n'a pas d'importance : il suffit qu'une suite convienne.

Le résultat de calculabilité est qu'il n'y a pas de moyen mécanique/automatique/informatisable/exécutable par un individu sans faire appel à son inventivité qui, au vu d'un triplet (mot initial, mot final, règles), donne cette réponse « oui / non ».

jeudi, novembre 1 2012

NP inter co-NP

Que connaît-on comme problèmes (si possible « naturels ») qui soient dans NP et co- NP mais n'aient pas été prouvés dans P ? (Dans le temps, il y a eu la programmation linéaire et la primalité, mais dans les deux cas on a des algorithmes P.)

mercredi, mai 30 2012

Non terminaison et indécidabilité

Considérons le problème suivant : étant donné une logique L permettant d'exprimer l'arithmétique, est-ce que pour tout programme qui ne termine pas sur l'entrée vide, on peut exhiber une preuve de ce fait dans L ? (Pour préciser la question : à tout programme on peut associer une formule Σ1 de l'arithmétique, exprimant qu'il termine, par exemple par la construction de Cook dans son théorème de complétude relative de la logique de Hoare à coup de codage de Gödel. Il s'agit de prouver cette formule.)

La réponse est négative (sauf délire de ma part) : il existe des programmes qui ne terminent pas, mais L n'arrive pas à prouver cela car il existe des modèles non standards de L où il y a un témoin de terminaison (une instanciation des quantificateurs existentiels).

Bien entendu, on peut toujours concocter des modèles, mais existe-t-il un exemple raisonnable de programme (à part un programme qui énumère des preuves..) qui produit cela ? Ceci rejoint un domaine de recherche : pondre des problèmes indécidables dans Peano sans avoir recours à la théorie de la preuve... il me semble avoir vu un exemple de suite dont le passage à zéro (donc la terminaison du programme associé) est dans ce cas.

jeudi, mars 8 2012

Une surprenante similitude de raisonnement

J'ai parfois lu ou entendu le raisonnement suivant de la part de chrétiens : « Si Dieu n'existe pas, cela veut dire que la vie serait vide de sens, ce qui serait horrible ; donc Dieu existe. »

Quand je lis des documents scientifiques traitant de classes de complexité, je lis parfois des raisonnements du type « Si P est vrai, alors la hiérarchie polynomiale s'effondre et beaucoup d'études de complexité deviennent vides de sens, ce qui serait horrible ; on pense donc que P est vrai ».

(SURGEON GENERAL'S WARNING: Lack of humor causes Heart Disease, May Complicate Pregnancy, and May Hamper your Enjoyment of Reading this Blog.)

mardi, mars 6 2012

Types construits dans le système F

Il arrive parfois que l'on se pose une question, qu'on ne trouve pas la réponse sur le moment, puis que cette question se rappelle à notre souvenir longtemps après.

Quand j'étais en DEA en 1998, et que j'apprenais l'encodage des types de données inductifs dans le système F (ou dans le Calcul des Constructions, même problème), je m'étais demandé si ces types pouvaient être « trop gros », c'est-à-dire contenir des termes qui ne seraient pas obtenus par application des constructeurs de ce type.

Rappelons de quoi il s'agit. On connaît bien l'encodage de Church des entiers naturels dans le λ-calcul pur : l'entier n est encodé comme une fonction qui à f associe la composée n fois de f avec elle même, soit λfλz f ( f ( … z) ). Dans le système F, on obtient ΛX λ(f: X→X) λ(x: X) f ( f ( … z) ). De même, le type des booléens peut se coder avec ΛX λ(a: X) λ(b: X) a pour « vrai » et ΛX λ(a: X) λ(b: X) b pour « faux » ; et le type Caml A of int | B of string se coderait comme le type ∀X (int→X)→(string→X)→X, avec le terme (A toto) codé par ΛX λ(a: int→X) λ(b: string→X) (a toto) et le type (B tata) codé par ΛX λ(a: int→X) λ(b: string→X) (b tata).

Selon ce même principe, le type Caml à un constructeur A of foo, trivialement isomorphe au type foo, s'encode comme ∀X (foo→X)→X, le terme (A x) s'encodant comme ΛX λ(f: foo→X) (f x). Permettez-moi maintenant une analogie (qui d'ailleurs peut sans doute se formaliser en théorie des catégorie) avec un autre domaine, l'analyse linéaire : si E est un espace vectoriel sur le corps K, et A→B désigne l'espace des applications linéaires de A dans B, alors (E→K)→K est le bidual de E, et pour tout élément x de E, λ(f: E→K) (f x) est l'élément associé par l'injection canonique de E dans son bidual. E et son bidual sont isomorphes quand E est de dimension finie, mais le bidual de E est « plus grand » que l'image de l'injection canonique de E quand E est de dimension infinie. Transposons notre doute aux types inductifs codés dans le système F : n'est-il pas à craindre que le type soit « plus gros » que l'ensemble des termes effectivement constructibles (les constructeurs étant les analogues de l'injection canonique, ce qui se comprend d'ailleurs bien dans l'interprétation catégorielle des types sommes) ?

La même question m'est revenue longtemps après, alors que je préparais un cours sur la théorie des types pour l'enseignement d'approfondissement dont je suis responsable à l'X. Ma distinguée collègue Christine Paulin a eu l'excellente idée de mettre sa remarquable thèse (de 1989 !) en ligne sur l'archive « thèses en ligne » et la réponse est au §4.3.1, p. 112 : en utilisant des types très polymorphes, il est possible de construire dans un type de la forme ∀X (N→X)→X des termes qui ne sont pas de la forme ΛX λ(f: N→X) (f n) où n est un terme clos de type N ; l'idée est que le terme n peut utiliser l'argument X dans des quantifications imprédicatives un peu compliquées.

Et là m'est arrivé une autre question, à laquelle je n'ai pas de réponse et pour laquelle je ne vois pas non plus de réponse dans la thèse de Christine Paulin...

Les constructions évoquées plus haut sont certes des termes non construits, mais je conjecture, d'une certaine façon, ils sont équivalents à des termes construits : sauf erreur de ma part, pour tout terme a du type en question, il existe un terme construit a' tel que pour tout h tel que (h a) soit d'un type construit « simple » (disons, les booléens), alors (h a)=(h a'). Autrement dit, tant qu'on ne fait pas des choses trop bizarres, les termes « en plus » ne produisent pas de comportements « inattendus ».

Il est 21 h et j'ai mal à la tête, je laisse mes lecteurs cogiter.:-)

Pour ceux que cela intéresserait, voici l'exemple de Christine Paulin, en notations pour Coq 8.3.

(Si vous voulez retrouver l'exacte définition proposée par Christine Paulin, il vous faut remplacer Type par Set et lancer Coq avec l'option -impredicative-set ; Set était naguère imprédicatif, sans doute pour permettre les codages inductifs par polymorphisme, en plus des types inductifs natifs rajoutés dans le Calcul des constructions inductives par rapport au Calcul des constructions, mais dans les versions actuelles de Coq il ne l'est plus, parce que ça posait un problème de compatibilité avec je ne sais plus quel axiome éventuellement désirable.)

Definition M (A : Type) := forall X : Type, (A->X)->X.

Definition c {A : Type} (a : A) : (M A) := fun X: Type, fun f : A->X, (f a).

Definition T := forall X : Type, X->X.

Definition t : T := fun X : Type => fun x : X => x.

Definition N := (forall D: Type, (D->T))->T.

Definition m : (M N) := fun (C : Type) (f : N -> C) => f (fun y : (forall D : Type, D->T) => y C (f (fun _ : (forall D : Type, D->T) => t))).

- page 1 de 2