\section{Sujet \thesujet : L(A)=L(B)?}\refstepcounter{sujet}\label{preuve}

\subsection*{Fiche signalétique}

\begin{tabular}{llll}
{\bf Responsable} & Paul-Yves Gloess & 05 56 84 69 27 & Paul.Gloess@labri.u-bordeaux.fr \\
{\bf 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\\
{\bf Equipe} & \multicolumn{3}{l}{Programmation symbolique}\\
{\bf Titre} & \multicolumn{3}{l}{\begin{tabular}{p{4in}}L(A)=L(B)?\end{tabular}}\\
{\bf Catégorie} & \multicolumn{3}{l}{Théorique}\\
{\bf Position/AltaRica} & \multicolumn{3}{l}{Outil satellite d'une version ultérieure}\\
 & \multicolumn{3}{l}{Prospectif}\\
{\bf Financement} & \multicolumn{3}{l}{Bourse de thèse MENRT}
\end{tabular}

\subsection*{Présentation du sujet}

\begin{description}
\item[Objectifs]

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

\item[Contexte]

La preuve rédigée par Géraud Sénizergues dans \verb+~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.

\item[Démarche et travail demandé]

Il ne s'agit pas uniquement d'obtenir une preuve du Théo\-rè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
\latex{$\rightarrow$}\html{->} D] et [[D1, ..., Dn] \latex{$\rightarrow$}\html{->} 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 (\verb+~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éo\-rème~9.3, à l'aide de l'outil choisi.

La troisième phase visera l'objectif de réutilisabilité.

\end{description}

