| Responsable | Paul-Yves Gloess | 05 56 84 69 27 | Paul.Gloess@labri.u-bordeaux.fr | |
| Collaborateurs | Pierre Castéran | 05 56 84 69 31 | Pierre.Casteran@labri.u-bordeaux.fr | |
| Géraud Sénizergues | 05 56 84 60 48 | ges@labri.u-bordeaux.fr | ||
| Equipe | Programmation symbolique | |||
| Titre |
| |||
| Catégorie | Théorique | |||
| Position/AltaRica | Outil satellite d'une version ultérieure | |||
| Prospectif | ||||
| Financement | Bourse de thèse MENRT | |||
L'objectif essentiel de la thèse est d'obtenir une version "mécanisée" de la preuve du théorème de Géraud Sénizergues: "L(A)=L(B) est décidable, A et B étant des automates à pile finis déterministes", sous une forme convaincante pour le mathématicien ou le théoricien de l'informatique. Il faut noter l'importance du résultat obtenu par Géraud Sénizergues, résultat qui fut pendant longtemps une conjecture intéressant la communauté scientifique internationale. Au delà de cet objectif, qui constitue en lui même un véritable "challenge", on s'efforcera d'abstraire les principes généraux de la preuve, sous la forme d'une bibliothèque de théories et de stratégies de preuve applicables à d'autres résultats de décidabilité.
La preuve rédigée par Géraud Sénizergues dans ~ges/public_html/lalb_l.ps
(version améliorée du rapport LaBRI RR-1161-97) compte 84 pages de
texte, jusqu'au résultat principal, le Théorème 9.3, qui énonce la
décidabilité du problème d'équivalence, pour des automates à pile finis
déterministes. Le texte est dense, et les preuves des différents lemmes
non triviales, mais il est relativement auto-suffisant: les objets
mathématiques du domaine sont pour la plupart définis; les théorèmes
extérieurs au texte sont en petit nombre: ce sont des résultats
classiques dont les preuves sont facilement accessibles dans les livres.
Cet aspect, renforcé par la présence au LaBRI de l'auteur de la preuve,
rend l'entreprise de mécanisation envisageable, au moyen d'assistants de
preuves internationalement reconnus tels que PVS (SRI International) ou
Coq (INRIA) disponibles au LaBRI.
Il ne s'agit pas uniquement d'obtenir une preuve du Théorème 9.3 au moyen de PVS ou Coq. Encore faut-il que le théoricien (tel que l'auteur de la preuve) et le praticien (utilisateur de PVS ou Coq) puissent être convaincus du bien-fondé de la preuve mécanique, et de l'identité du résultat mécaniquement démontré avec le Théorème 9.3. Cette exigence implique en particulier qu'aucun axiome ne soit introduit, pour pallier la preuve de résultats extérieurs utilisés, et que les définitions des notions sous-jacentes (par exemple, les automates à pile, la décidabilité) soient présentées sous une forme accessible et indiscutable au théoricien.
En pratique, on aura intérêt à suivre de près la preuve humaine, sous peine de la réinventer, ce qui pourrait prendre beaucoup plus de temps, et n'est pas demandé. D'autre part, dans une perspective de réutilisabilité des théories PVS ou Coq, et plus généralement d'intéressement du théoricien aux résultats de la thèse, il est impératif d'établir une correspondance limpide entre le texte initial et la version mécanisée.
Bien que le résultat principal soit un résultat de décidabilité, de nombreux lemmes utilisent des preuves non constructives, de sorte que le choix du meilleur outil n'est pas évident. L'impact des différences entre les logiques de PVS et Coq, sur la faisabilité de l'entreprise, devra être finement analysé avant de prendre une décision. Certaines de ces différences sont majeures: distinction existant en Coq (pas en PVS) entre les sortes Set et Prop; notion d'égalité; typage décidable en Coq et indécidable en PVS. Elles ont un impact sur le langage des fonctions récursives, et la nature des preuves. D'autres différences plus mineures peuvent néanmoins prendre de l'importance en pratique, étant donné l'ampleur du domaine à traiter: surcharge possible en PVS, pas en Coq; currification implicite en Coq, identification des types [D1, ..., Dn -> D] et [[D1, ..., Dn] -> D] en PVS.
On comparera dans une première phase de quelques mois d'expérimentation
les deux logiques sur un échantillon représentatif du texte de Géraud
Sénizergues, incluant en particulier l'échantillon abordé par une étude
préliminaire de faisabilité sous PVS (~gloess/pvs/ges/README). Le choix
de l'outil reposera sur une confrontation des résultats de cette
comparaison avec les objectifs énoncés plus haut. La confiance que l'on
peut avoir dans l'outil lui-même est liée à la conception de celui-ci:
c'est un aspect à ne pas négliger.
On achèvera dans une seconde phase la formalisation et les preuves, jusqu'au Théorème 9.3, à l'aide de l'outil choisi.
La troisième phase visera l'objectif de réutilisabilité.