Bonjour,
Dans le cadre de ma recherche, je suis confronté aujourd’hui à des problèmes techniques liés au web. Comme j’ai assez peu de connaissances dans le domaine et que pour le moment, mes recherches n’ont pas donné grand chose, j’en viens à poster ici mon problème afin de voir si vous aurez des avis/suggestions à émettre.
Contexte
Mon équipe de recherche Deducteam est spécialisé en preuve formelle. C’est à dire qu’on crée des outils dans lesquels il est possible d’exprimer des preuves mathématiques. Évidemment, on est pas les seuls sur Terre à faire ce genre d’outils, et parmi les plus connus on trouve entre autre Coq, Isabelle/HOL, Agda, PVS par exemple.
Cependant, comme pour les langages de programmations, on trouve aujourd’hui une grande variété d’outils pour faire de la preuve formelle, et aujourd’hui il est quasiment impossible de faire communiquer ces outils. C’est à dire que si on a une preuve d’un théorème faite en Coq, on ne peut pas la réutiliser dans un système tel que PVS. Il faut reprouver ce théorème à la main.
Ceci est extrêmement pénible, surtout quand on sait que certaines preuves demandent des années de travail à des équipes de chercheurs spécialisés dans le domaine. De plus, il faut savoir qu’on est un des rare domaine de l’informatique où il existe littéralement $0$ standard ! Ce qui rend les choses encore plus compliquées : chaque outil utilise son propre langage, avec sa propre sémantique etc…
L’intéropérabilité
Ma recherche consiste principalement à construire des ponts entre ces systèmes. Pour le moment, on a pu produire une librairie d’arithmétique d’environs $300$ lemmes que l’on peut partagé entre $5$ systèmes différents. Cette librairie contient principalement de l’arithmétique élémentaire niveau terminal :
- Définition des entiers et des opérations basiques comme plus, fois, diviser, …
- Théorèmes basiques sur les propriétés des opérateurs ci-dessus
- Définition du PGCD, des nombres premiers etc…
- Point culminant de la librairie : preuve du petit théorème de Fermat
Avec cette librairie intéropérable, notre but maintenant est de construire une encyclopédie de preuves en ligne.
Logipedia
Logipedia est le nom de cette encyclopédie de preuves en ligne. Sur cette encyclopédie, on pourrait trouver les différents théorèmes prouvés dans la librairie ainsi que toutes ses dépendances. Par exemple, prouver la commutativité de la multiplication demande d’abord de prouver la commutativité de l’addition. Mais on pourrait aussi trouver "l’axiomatisation" utilisée pour prouver un théorème. Par exemple, pour prouver la commutativité de l’addition on a besoin de l’axiome $0 + n = n$. Enfin, cette encyclopédie permet de télécharger les preuves dans différents systèmes (quand c’est possible).
Cette description assez grossière devrait être suffisante pour comprendre les problèmes que l’on rencontre.
Problèmes
Aujourd’hui, les preuves sont exprimées dans un langage ad-hoc Dedukti. Puis, à l’aide d’un bout de programme écrit en OCaml on traduit ces preuves vers d’autres systèmes comme Coq, PVS, etc…
Comme on a besoin de stocker ces énoncés quelque part, on s’est dit qu’utiliser une base de données serait une bonne idée. Sauf que l’utilisation d’une base de données SQL pose au moins deux problèmes :
- La taille des champs est fixe. Or, a priori la taille d’une preuve n’est pas bornée.
- La structure même d’une preuve est en général un arbre plutôt qu’une chaîne de caractères (un peu comme un arbre généalogique mais en plus compliqué). Or, on ne sait pas bien stocker des arbres en SQL.
Pour le moment, on a choisi d’utiliser $MongoDB$ en passant par des fichiers JSON. Cela permet de contourner le premier problème mais pas vraiment le second (nos preuves sont stockées comme des chaînes de caractères).
Comme on souhaite afficher les dépendances de théorèmes, on stocke aussi les dépendances dans des fichiers JSON. Cependant on stocke que les dépendances directes : si foo dépend de bar et que bar dépend de baz, alors cela créera deux entrées :
- foo <- bar
- bar <- baz
Par contre, quand on affiche la page du théorème foo, on veut voir toutes les dépendances, il faut donc affichier bar et baz. Dans notre jargon, on appelle cette opération faire la clôture transitive.
Aujourd’hui, cette clôture transitive est effectuée côté serveur à chaque fois que le client affiche la page du théorème foo. Mais c’est un peu idiot car a priori, les dépendances ne vont pas changer tous les jours.
On a une ébauche d’un site qui est en ligne, mais vu l’état actuel du site, on ne souhaite pas encore rendre ça publique. Si vous êtes curieux, je peux vous envoyer un lien en PM.
Donc voici nos principales problèmes/questions actuellement :
- L’utilisation d’une base de données est-elle justifiée ? Le site web étant pour le moment statique je ne suis pas tout à fait convaincu. Sur le long terme, certainement que le site web sera dynamique afin que les utilisateurs puissent faire des ajustements, mais ce n’est pas prévu pour le moment.
- Si on utilise une base de données, MongoDB est-il un bon choix ? N’existe-t-il pas de meilleurs façons de faire ce que l’on souhaite faire ?
- Le calcul des dépendances qui peut changer ponctuellement ne devrait-il pas se faire statiquement ?
- D’un point de vue maintenabilité, on souhaite avoir un maximum de choses faite en OCaml.
Notre but aussi, c’est évidemment que nos choix techniques passent à l’échelle. Pour le moment, le site contient quelques centaines de preuves, mais à court terme voir moyen terme, on va très rapidement en avoir quelques milliers.
Je ne sais pas si j’ai donné assez d’informations ou pas, en tout cas je suis ouvert à toutes vos suggestions ! J’ai posté mon problème ici car il me semble que le public du forum "sciences" sera plus adapté.
Merci d’avoir pris le temps de me lire en tout cas.
Saroupille
