Groupe de travail Esquisses & Calcul Formel

Équipe Calcul Formel

Responsables : L. Coppey, D. Duval, C. Lair, J.-C. Reynaud, P. Sénéchaud


Présentation

Extraits du document de création du groupe de travail (octobre 1991) :

"Conception d'un langage de haut niveau pour le calcul formel à partir de la théorie des esquisses''.

Les systèmes de calcul formel actuellement disponibles, malgré tous les progrès réalisés depuis leur apparition, sont encore loin de satisfaire tous leurs utilisateurs. Les systèmes non spécialisés sont souvent répartis en deux classes, la première comportant entre autres Macsyma, Maple et Mathematica, la seconde ne comportant qu'Axiom (anciennement dénommé Scratchpad).

Les bases d'Axiom sont conçues de façon beaucoup plus cohérente que celles des autres systèmes. Pour les applications les plus élémentaires, cette cohérence se manifeste surtout en pratique par une relative lourdeur. Par contre elle se révèle fort utile dès qu'on veut manipuler des données "non triviales'', comme par exemple des nombres algébriques.

La cohérence d'Axiom provient de l'utilisation systématique d'idées proches des "types abstraits de données'', plutôt que du traitement de formules logiques "usuelles''.

C'est cette voie que nous souhaitons approfondir, en étudiant la possibilité de traiter non "logiquement'', mais à l'aide de catégories, ou plutôt d'objets plus compacts (diagrammes et esquisses), les structures habituellement définies par des formules logiques du premier (ou du second) ordre. Il s'agit en quelque sorte de généraliser l'approche des types abstraits de données à des structures non équationnelles (indispensables pour le calcul formel).

Nous proposons donc d'étudier la possibilité de construire un langage pour le calcul formel fondé sur la théorie des esquisses d'Ehresmann. Nos arguments en faveur de cette approche sont les suivants :

  • Puissance. Les esquisses permettent de décrire à l'aide de la théorie des catégories les mêmes structures que la logique du premier ordre. Les trames (qui les généralisent) correspondent à la la logique du second ordre.
  • Compacité. Contrairement à une approche utilisant uniquement les catégories, les esquisses permettent une description très concise, souvent finie pour les structures les plus courantes.
  • Fonctionalité. Comme dans toute approche utilisant les catégories, la notion de flèche est fondamentale. Ces flèches peuvent être vues comme des "termes'' sur lesquels on peut calculer par des processus qui généralisent la réécriture.
  • Simplicité et homogénéité. Avec cette approche, la distinction "théories/modèles'' (ou "syntaxe/sémantique''), relève entièrement de l'interface utilisateur. Le système ne connaît que le côté syntaxique, c'est-à-dire les esquisses et les morphismes entre esquisses. Ceci est beaucoup plus simple que la distinction "catégories/domaines'' d'Axiom, qui nécessite de distinguer les enrichissements de catégories, "coercions'' entre domaines, et appartenance d'un domaine à une catégorie.
  • Souplesse de représentation. Les esquisses permettent aussi bien une représentation purement "formelle'' de leurs objets (vus comme des "termes'') qu'une représentation à partir d'objets dans des esquisses déjà existantes (on a alors une représentation "à la Axiom''). De plus on peut passer "continûment'' d'un point de vue à l'autre, ce qui laisse place pour une notion de "symbole typé'' qui actuellement manque à tous les systèmes de calcul formel.
  • Souplesse d'évaluation. De même, pour le calcul, on peut combiner des méthodes d'évaluation relevant de la réécriture avec des méthodes algorithmiques.
  • Aspect visuel. Les esquisses sont des graphes "colorés'', qui peuvent être dessinés et ainsi fournir une interface très conviviale à un système de calcul formel.
  • Manipulation de contraintes. Cette approche semble aussi fort bien adaptée à la description de la "programmation avec contraintes'', en un sens très proche de celui qui est utilisé dans les versions récentes de Prolog. C'est une façon de voir l'"évaluation dynamique''.
  • Parallélisme. Il semble aussi que les esquisses puissent offrir un cadre pour formaliser certaines questions liées au parallélisme en informatique.

Les esquisses sont étudiées en détail depuis plusieurs années par quelques chercheurs. Les résultats et preuves sont naturellement assez techniques, le travail à faire ici est d'utiliser ces résultats "théoriques'' dans le but de construire un prototype pour un sytème de calcul formel moderne, en collaboration avec diverses personnes connaissant tous les aspects de la conception des langages de programmation.

 

Organisation

UNIVERSITE DENIS DIDEROT - PARIS 7
U.F.R. de Mathematiques

SEMINAIRE CATEGORIES ET STRUCTURES
(L. Coppey et C. Lair)

GROUPE DE TRAVAIL ESQUISSES ET CALCUL FORMEL
(L. Coppey, D. Duval, C. Lair, J.-C. Reynaud, P. Senechaud)

Tours 45-55, 5eme étage,
2 place JUSSIEU, 75251 PARIS CEDEX 05, FRANCE
bureaux 45-55-418 et 45-55-420
Tels 01-44-27-53-06 et 01-44-27-54-10

 

Programme

Vendredi 16 octobre 1998, 14 h30-16h30, Jussieu - Salle 45-55-511

 

 

J.-C. REYNAUD : Introduction à la spécification "orientée modèles"

Vendredi 20 novembre 1998, 10 h30-12h30, Jussieu - Salle 55-56-507 (sous réserve)

 

 

C. PAULIN-MOHRING : Coq : la théorie appliquée à un assistant aux preuves. I. Présentation de l'assistant : les grands principes de son langage et de son architecture

Vendredi 20 novembre 1998, 14 h30-16h30, Jussieu - Salle 45-55-511

 

 

C. PAULIN-MOHRING : Coq : la théorie appliquée à un assistant aux preuves. II. La calcul des constructions inductives

Vendredi 15 janvier 1999, 10 h30-12h30, Jussieu - Salle 55-56-507

 

 

Y. LAFONT : Logique linéaire et informatique

Vendredi 15 janvier 1999, 14 h30-16h30, Jussieu - Salle 45-55-511

 

 

Y. LAFONT & S. LIPPI : Programmation avec des réseaux d'interaction

Mars 1999

Vendredi 12 mars 1999, 14 h-15h et 15h30 - 16h30, Jussieu - Salle 45-55-511

 

 

J.-C. FILLIATRE (LRI, Orsay) : Preuves de programmes impératifs en Théorie des types.

 

Mai 1999

Vendredi 28 mai 1999, 10h30 - 12h Jussieu - Salle 55-56-507

 

 

Catherine ORIAT et Dominique DUVAL : Traduction de diagrammes UML à l'aide d'esquisses.

Vendredi 28 mai 1999, 14h30 - 16h Jussieu - Salle 45-55-420

 

 

Kazem LILLAHI et Faouzi BOUFARES : Modèles conceptuels.

Vendredi 25 juin 1999, 10h30 -12h30 et 14h - 16h - Jussieu - Salle 45-55-405

 

 

Atelier , animé par Jean-Claude REYNAUD, Co-algèbres et programmes interactifs.

 

Décembre 99

Vendredi 10 décembre 1999, 10h00 -12h00 et 14h - 16h - - 6 Rue Clisson - 75013 PARIS

 

 

10h00 - 12h00 - Bureau 6-C-24 - Réunion d'organisation

14h00 - 16h00 - Bureau 6-C-1 - C. LAIR : Existence de modèles terminaux dans les catégories esquissables et ré-esquissabilité.

 

Janvier 2000

Vendredi 14 janvier 2000, 10h30 -12h30 - 14h30 - 16h30 - 6 Rue Clisson - 75013 PARIS

 

 

10h30 - 12h30 - Salle 6-C-01 - S.K. LELLAHI : Systèmes dynamiques avec ensembles de mis à jour.

14h30 - 16h30 - Bureau 6-C-01 . D. DUVAL : Kits avec état implicite.

 

Mars 2000

Vendredi 03 Mars 2000, 11h00 -12h30 - 14h00 - 16h00 - 6 Rue Clisson - 75013 PARIS

 

 

11h- 12h30 - Salle 6-C-01 - C. ORIAT : Etude de cas en (langage) UML.

14h00 - 14h30 - Salle 6-C-01 . J.-C. RAYNAUD : Etude de cas en (langage) B.

14h30 - 16h00 - Salle 6-C-01. P. SENECHAUD : Etude de cas en termes d'esquisses.

Vendredi 24 Mars 2000, 10h00 -12h30 - 14h00 - 16h00 - 6 Rue Clisson - 75013 PARIS

 

 

Présentation du projet FOC (équipes CALFOR et SPI du laboratoire LIP6) pour construire un environnement de développement de programmes certifiés pour le Calcul Formel.

10h00 - 11h00 : T. HARDIN : Méthodologies de programmation et de certification.

11h00 - 12h00 : R. RIOBOO : Mise en œuvre pour le Calcul Formel.

14h00 - 15h00 : S. BOULME : un noyau COQ pour le Calcul Formel.

15h00 - 16h00 : R. RIOBOO : La librairie FOC.

Archives