Sciences et Technologies de l'Information
Sommaire : Trois questions à Jean-Louis Krivine | L'actualité de la semaine | Théories et concepts | La recherche en pratique| Enseignement | Manifestations | Le livre de la semaine | Détente
ABONNEMENT/DESABONNEMENT | RETOUR A LA PAGE D'ACCUEIL | NUMEROS PRECEDENTS.
Asti-Hebdo
: Vous intervenez à la
journée Asti "Apports et relations
des sciences de l'information aux connaissances scientifiques".
En quoi l'informatique contribue-t-elle au développement de vos
recherches en mathématiques.
Jean-Louis Krivine : Mes recherches appartiennent à la logique mathématique, et mon objectif personnel est de répondre à une question que je me suis posée dès que j'ai commencé à faire des mathématiques, c'est à dire vers 15 ou 16 ans : pourquoi sont-elles si efficaces, alors qu'elles semblent a priori tourner à vide ? Je crois avoir trouvé la réponse que je cherchais,
La "déraisonnable efficacité des mathématiques" (une formule du physicien Wigner) a toujours intrigué. Les logiciens de l'antiquité ont apporté une première réponse. Un pas décisif a été franchi dans les années 30-40, notamment avec le théorème de complétude de Gödel, moins connu, mais peut-être aussi important que son célébrissime théorème d'incomplétude. A partir de cette époque, on sait que toute démonstration peut se réduire à une suite d'opérations mécanisables.
Un autre découverte, beaucoup moins connue mais capitale, est la remarque faite par Curry et Howard, deux logiciens, dans les années 50 : à toute démonstration correspond un programme (en l'occurrence, un terme du lambda-calcul). Leur remarque se limite alors au calcul propositionnel intuitionniste, c'est à dire à un ensemble de tautologies sans intérêt mathématique, d'autant plus qu'on s'interdit le tiers exclu (autrement dit, le raisonnement par l'absurde).
Puis, au fil des ans, la correspondance de Curry-Howard a été étendue à la logique (intuitionniste toujours) des prédicats (logique du second ordre). Des logiciens français comme Jean-Yves Girard ont participé à ces extensions. C'était cependant encore insuffisant pour concerner les mathématiciens, qui ne savent pas se passer du tiers exclu.
C'est en 1990 que Matthias Felleisen, un spécialiste de Lisp, cherchant à typer l'instruction CallCC de Scheme (instruction de traitement des erreurs), en écrivit le type sous la forme :
((A implique B) implique A) implique A) (loi de Peirce)
Son collègue Timothy Griffin lui fit observer que cette formule ne peut être valable, puisque la correspondance de Curry-Howard ne s'appliquait pas au tiers-exclu. Jusqu'à ce que, poursuivant sa réflexion, il ne conclue que, justement, ce typage permettait cette extension, dépassant ainsi la logique intuitionniste, et publia sa découverte notamment dans les Communications de l'ACM
Ma contribution a consisté à étendre cette correspondance de Curry-Howard jusqu'à la théorie des ensembles (plus précisément, aux axiomes de Zermelo-Fraenkel, car l'axiome du choix pose des problèmes redoutables). Elle s'applique maintenant à la quasi-totalité des mathématiques. On peut donc dire aujourd'hui qu'à toute démonstration mathématique correspond un programme informatique. Et comme les mathématiciens ont, en 2500 ans, accumulé un capital considérable de démonstrations, il y a là un trésor où nous n'avons plus qu'à puiser.
Mais il y a une difficulté majeure : en général, quand on trouve l'équivalent en programmation d'une preuve mathématique, ce qu'on trouve est totalement inattendu, inimaginable, même. Nous sommes un peu comme les égyptologues avant Champollion : nous savons bien que ces hiéroglyphes forment un langage, mais nous ne savons pas le traduire.
Les logiciens, et moi-même en particulier, se sont donc attelés à la constitution progressive d'un dictionnaire, dont je vous ai donné quelques exemples. Ajoutons-en quelques autres qui, vous allez le voir, n'ont rien d'intuitivement évident :
- à preuve (ou démonstration) correspond programe,
- à axiome correspond déclaration de variable,
- à application d'une règle de déduction correspond instruction de programme
- à théorème (proposition prouvée) correspond spécification (d'un programme
fonctionnant correctement),
- au modus ponens correspond l'application d'une instruction à un
argument,
- ...
A force d'enrichir le lexique, nous finirons, je l'espère, par décoder le langage lui-même et par donner ainsi à un accès efficace à ces trésors. Mais nous n'en sommes pas là. Actuellement, je cherche simplement les théorèmes de mathématiques pour lesquels j'ai bon espoir de trouver la spécification informatique correspondante (Vous trouverez sur le web mes publications sur ce thème). Ainsi, l'informatique est-elle pour moi une source permanente d'inspiration pour le développement de mes travaux de logique mathématique
Hebdo : Ces travaux ont-ils un intérêt pour l'informatique et plus généralement les Stic ?
J.-L.K. . : Le développement des techniques de preuve de programmes est plus important que jamais, en raison des quantités toujours plus grandes de logiciels intégré par exemple aux moyens de transport. Le futur Airbus A 380 emportera encore dix fois plus de logiciel que les séries précédentes. Il en va de même pour les logiciels enfouis (comme on dit aujourd'hui) dans les objets de grande consommation et en particulier les téléphones portables. Le volume même de ces applications ne permet plus d'en tester que d'infimes parties.
Seules les preuves formelles sont à la mesure des besoins. Comme toutes ces applications deviennent de plus en plus vitales (et, dans le cas des transports, mettent souvent des vies humaines en jeu), la fiabilité garantie par les preuves s'impose donc absolument.
Hebdo : Mais cela répond-il à votre objectif initial : montrer pourquoi le jeu intellectuel des mathématiques est si efficace en réalité ?
J.-L.K. : Tout à fait, bien qu'il soit difficile de s'en convaincre, car il faut pousser le raisonnement à bout. Cette masse de théorèmes qu'ont prouvé les mathématiciens, c'est un peu comme le contenu de la ROM de mon Oric, le micro-ordinateur sur lequel j'ai appris la programmation en langage machine, dans les années 80. Je me disais : il y a un trésor là-dedans, comment le récupérer ?
Tous ces théorèmes peuvent être considérés comme programmes. Et pour quel ordinateurs ont-ils été écrits, et par quel programmeur ? La réponse est évidement : pour le cerveau humain, et par l'évolution. Leur efficacité tient à cela. Le rôle du mathématicien est de décoder ces programmes, il fait ce qu'on appelle du "reverse engineering". Je considère donc la logique comme un moyen d'accès privilégié pour comprendre le cerveau humain. Les perspectives de recherche en ce domaine sont proprement fascinantes.
C'est la fin du règne des éditeurs et l'arrivée de sociétés de services "différentes" : "Nos clients ont le droit de modifier les logiciels, tout en gardant notre support complet, - hot line, veille, consulting", résume Jean-François Gomez, directeur marketing d'Open Care. "On ne travaille pas sur un produit figé. L'entreprise adapte le logiciel Open Source à ses besoins. C'est pour les grands groupes, le meilleur moyen d'apporter la nouveauté à des ressources existantes hétérogènes".
Alain Lefevre, directeur de SQLI, confirme : "A l'heure du tout Internet, le passage de l'ère des éditeurs à l'ère des prestataires de services. La notion d'Open Source monte en puissance, parce que les briques Open Source ont une meilleure qualité, un meilleur design, une meilleure pérennité que les noyaux propriétaires. Dans notre logiciel de gestion de contenu web, Interligo, tout est publié."
Sentant le vent, les éditeurs chevronnés accélèrent leurs ralliements à Linux. Une intrigue intéressante se joue au niveau des développeurs sous Linux. Ceux-ci développent en général en lignes de commande PHP ou en C++. IBM, Oracle, Borland, Magic, Rational, etc.. veulent les faire aller plus vite, et lancent un grand nombre d'outils RAD sous Linux, du Kylix de Borland au Visual Age for Java d'IBM. Il s'agit d'amener ces développeurs de masse à des outils de productivité.
Pour que Linux se démocratise dans les années à venir, et réponde aux besoins des entreprises soumises à des problèmes de temps, les spécialistes du code vont devoir passer au développement sans code...
Parallèlement, la communauté Open Source met en avant ses méthodes de développement collectif. VA Linux annonce la commercialisation de "SourceForge OnSite", un service par abonnement basé sur le système de développement de groupe (Collaborative Development System, CDS) utilisé sur SourceForge.net qui est le plus grand centre de développement Open Source actuel (près de 100000 développeurs). Ce système est adopté par Agilent Technologies, l'ancienne division Mesure et Instrumentation de HP. Une initiative du monde l'Open Source qui peut inspirer, voire inquiéter, les grands spécialistes du développement en ligne, de Microsoft à Oracle.
Mireille Boris
Le numéro s'ouvre sur une introduction aux processeurs asynchrones, qui ne se contente pas des principes, mais fait un tableau des produits actuels. Parmi les avantages de ces circuits, on note d'abord la réduction des consommations, essentielle aujourd'hui avec le développement des systèmes enfouis et notamment de la téléphonie portable.
Les philosophes apprécieront l'article consacré au prix du routage dans les FPGA (Field programmable gate arrays), qui signale : "la quantité de silicium consacrée au routage croît beaucoup plus vite que celle consacrée aux portes elles-mêmes". Chacun sait qu'il en va de même à l'échelle macroscopique, et que les opérateurs de télécoms ont repris le haut du pavé aux constructeurs informatiques...
D'un point de vue conceptuel, la notion de "compilation reciblable" (retargeting, en américain) introduit une souplesse précieuse pour les processeurs de traitement du signal et, de manière plus récente, pour les Asip (Application specific instruction processor), eux aussi recherchés pour les systèmes enfouis. Et le vocabulaire de l'article, à lui seul, est assez décoiffant pour qu'on puisse en conseiller la lecture même à des informaticiens d'autres spécialités. Je cite : "Pour qu'un compilateur flexible soit adapté à l'exploration architecturale... ".
Dans un prochain numéro d'Asti-Hebdo, Hubert Tardieu (VP Innovation, Sema), nous montrera que ces innovations conceptuelles arrivent à point nommé pour répondre à des exigences impératives des marchés.
Le numéro se termine sur des vues prospectives, mais bien concrètes : Et demain, quel PC ? Avec un petit tableau chiffré pour les années 2000, 2005, 2010 et 2015.
Le numéro 19 de TSI était intitulé "Parallélisme, distribution et approches objets". Ici encore, matériel et logiciel s'entrelacent et adoptent des approches réseau, ne serait-ce que dans l'approche introductive "Mise en oeuvre d'un algorithme parallèle sous Corba et PVM" (expérimentation sur un réseau de micro-ordinateurs).
Pierre Berger
- Pour les terminaux mobiles, quels outils et quels contenus pour
quels supports ?
- Le "rich media" au plan technologique (environnement auteur de
production…) et éditorial (programmes composites, droits…).
- Le traitement et la création numérique des images, savoir-faire
stratégique pour les jeux vidéos, les séries d’animation, les effets
spéciaux au cinéma...
-Les outils de recherche et de navigation dans des bases de
données de grande dimension.
Exemples de thèmes majeurs : indexation automatique, codage et compression des images, langages hypermédia (intégration textes-images-sons), comportements intelligents dans l'interface homme-machine, stockage et la diffusion des objets audiovisuels et multimédias
Ce projet a réuni le ministère de la Recherche, la SFSIC et la fondation Maison des sciences de l'homme, partenaires auxquels est venu se joindre la Librairie Tekhne.
Trois parties principales structurent le site :
- Communauté : les formations infocom en France, la recherche, les
associations, des services et ressources (base de pré-publication, annuaire, revues...),
l'actualité...
- InfoCom et... : un ensemble de liens répartis par thématiques :
institutions, médias, esthétique, éducation-formation,
citoyenneté, organisations, stratégie, information spécialisée...
- Les plus : sélection hebdomadaire d'un site web, ressources pour la
création de sites, téléchargement.
Bernard Espiau remplace Jean-Pierre Verjus à la tête de l'Inria Rhône-Alpes, et Hélène Kirchner remplace Michel Cosnard à l'Inria Lorraine et au Loria.
Une direction de l'Information scientifique et de la communication (DISC), dont la responsabilité échoit à Jean-Pierre Verjus, remplace la précédente délégation à la communication, et une direction des Relations internationales succède, avec toujours à sa tête Stéphane Grumbach, à l'ancienne délégation aux Relations internationales.
Délivré aussi notamment à l' université de Rennes, ce DESS "permet à des informaticiens de niveau Bac+4 de comprendre les fondements et approches des techniques d'interface homme-machine. Cette formation met l'accent sur les interactions homme-machine et le traitement des informations numériques multimédia. Elle apporte les bases requises pour une adaptation aux technologies actuelles."
Les approches différentes de ces deux grandes figures du domaine devraient rendre le débat passionnant pour ceux qui s'intéressent à l'histoire de ce grand mouvement mathématique et à sa portée épistémologique.
Dear editor : If you prefer to receive press releases by email, please return the form below by fax. Thank you !
... in english dans le texte.