La vie est mal configurée

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.

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 ?

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

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.

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

Lorsqu'en Coq, on a une propriété à définir sur un type inductif T, faut-il mieux définir une fonction T->Prop par point fixe, ou définir un prédicat inductif T->Prop? Le premier cas n'est évidemment pas applicable si la décision du cas à appliquer n'est pas (quasi) déterministe en fonction du constructeur de T rencontré à la racine. Le second cas oblige à utiliser des inversions, qui peuvent parfois poser problème.

Sylvain Boulmé me suggère de faire les deux en démontrant une équivalence... D'ailleurs, est-ce que ça marche bien, la réécriture Setoid par l'équivalence logique ? Je l'ai utilisée sur quelques exemples, mais y a-t-il des problèmes cachés ? Est-ce fondamentalement plus complexe ou piège que la réécriture par l'égalité de Leibniz ?

J'ai un problème d'analyse de programmes qu'il serait trop fastidieux d'expliciter ici ; il s'agit d'une généralisation du problème traité dans mon récent article avec Thomas Gawlitza. Sauf erreur (je n'ai pas mis la preuve au propre) ce problème est dans NEXPTIME. Je soupçonne qu'hélas ce problème est NEXPTIME-complet. Je m'y connais fort peu en NEXPTIME (d'habitude, je ne regarde que des problèmes dans les premiers degrés de la hiérarchie polynomiale, ou PSPACE-complets) ; connaîtriez-vous des lectures à me conseiller ?