% vim:expandtab:sts=4:sw=4
% anaseto@bardinflor.perso.aquilenet.fr, licence cc-by-sa
% dernière version sur :
% http://bardinflor.perso.aquilenet.fr/elsxutajxoj/agreg/developpements
\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{lmodern}
\usepackage{microtype}
\usepackage[french]{babel}

%%% outils mathématiques {{{
\usepackage{amsmath,amssymb,amsfonts,mathtools,dsfont}

%%%% ensembles 
\newcommand{\ensemblenombre}[1]{\ensuremath{\mathbb{#1}} }
% complexes, entiers, rationnels, réels, etc...
\newcommand{\C}{\ensemblenombre{C}}
\newcommand{\D}{\ensemblenombre{D}}
\newcommand{\F}{\ensemblenombre{F}}
\newcommand{\K}{\ensemblenombre{K}}
\newcommand{\N}{\ensemblenombre{N}}
\newcommand{\Q}{\ensemblenombre{Q}}
\newcommand{\R}{\ensemblenombre{R}}
\newcommand{\U}{\ensemblenombre{U}}
\newcommand{\Z}{\ensemblenombre{Z}}
\renewcommand*{\P}{\ensemblenombre{P}} % L'ensemble P
\renewcommand*{\S}{\mathfrak{S}} % L'ensemble S (groupe symétrique)
\newcommand*{\A}{\mathfrak{A}} % L'ensemble A (groupe alterné)

% lettres caligrafiées
\renewcommand*{\cal}{\mathcal} % pour les A,B ronds etc..

%% restrictions
\newcommand*{\res}{\mathclose{}|\mathopen{}}

%%%%%%%%%%%% fonctions pratiques %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%% classiques
\newcommand*{\abs}[1]{\ensuremath{\left| #1 \right|}} %valeur absolue
\newcommand*{\di}{\ensuremath{\mathop{}\mathopen{}\mathrm{d}} } % le «d» de dx
\newcommand*{\implique}{\ensuremath{\Rightarrow}} % mieux \implies
\newcommand*{\mdl}[1]{\ensuremath{\left|  #1  \right|}} %module
\newcommand*{\norminf}[1]{\ensuremath{\left\| #1 \right\|_{\infty}} } %norme infinie
\newcommand*{\norm}[1]{\ensuremath{\left\| #1 \right\|}} %norme
\newcommand*{\pe}[1]{\ensuremath{\lfloor  #1  \rfloor}} %partie_entière
\newcommand*{\ps}[2]{\ensuremath{\big( #1|#2\big)}} % produit scalaire.
\newcommand*{\ssig}{\ensuremath{\Longleftrightarrow}} %si et seulement si: la grande
\newcommand*{\ssi}{\ensuremath{\Leftrightarrow}} % si et seulement si: petite flèche
\newcommand*{\vide}{\phi} % ensemble vide
\newcommand{\ind}{\mathds{1}}

%%% moins classiques
\newcommand*{\leg}[2]{\ensuremath{\left( \frac{#1}{#2} \right)}} % legendre

% dérivée partielle #1-ième de #2 par rapport à #3, pareil mais sans l'ordre. Idem pour
% les dérivées totales.
\newcommand*{\dpto}[3][ ]{\ensuremath{\frac{\partial^{#1} #2}{\partial #3^{#1} }} }
\newcommand*{\dpt}[2]{\ensuremath{\frac{\partial #1}{\partial #2}} }
\newcommand*{\dto}[3][ ]{\ensuremath{\frac{d^{#1} #2}{d^{#1} #3}} }
\newcommand*{\dt}[2]{\ensuremath{\frac{d #1}{d #2}} }

\renewcommand*{\vec}{\ensuremath{\overrightarrow}} %pour les vecteurs 

% A --> B
% x |-> y
\newcommand{\fun}[4]{%
    \begin{matrix}
        #1 & \to & #2 \
        #3 & \mapsto & #4
    \end{matrix}}
% fonction avec le nom en plus
% f: A --> B
%    x |-> y
\newcommand{\nfun}[5]{%
    \begin{matrix}
        #1\colon & #2 & \to & #3 \
           & #4 & \mapsto & #5
    \end{matrix}}

%%%%% nom de fonctions courantes %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% operators
\DeclareMathOperator{\isom}{Isom}
\DeclareMathOperator{\gal}{Gal}
\DeclareMathOperator{\Ir}{Ir}
\DeclareMathOperator{\cov}{Cov}
\DeclareMathOperator{\card}{Card}
\DeclareMathOperator{\argch}{Argch}
\DeclareMathOperator{\pgcd}{pgcd}
\DeclareMathOperator{\Poin}{Poin}
\DeclareMathOperator{\var}{Var}
\DeclareMathOperator{\com}{com}
\DeclareMathOperator{\rang}{rang}
\DeclareMathOperator{\id}{id}
\DeclareMathOperator{\sh}{sh}
\DeclareMathOperator{\conv}{Conv}
\DeclareMathOperator{\aut}{Aut}
\DeclareMathOperator{\Int}{Int}
\DeclareMathOperator{\residu}{Res}
\DeclareMathOperator{\disc}{disc}
\DeclareMathOperator{\supp}{supp}
\DeclareMathOperator{\adh}{adh}
\DeclareMathOperator{\im}{Im}
\DeclareMathOperator{\stab}{Stab}
\DeclareMathOperator{\ch}{ch}
\DeclareMathOperator{\mat}{mat}
\DeclareMathOperator{\diag}{diag}
\DeclareMathOperator{\argth}{Argth}
\DeclareMathOperator{\tr}{tr}
\DeclareMathOperator{\argsh}{Argsh}
\DeclareMathOperator{\vect}{Vect}
\DeclareMathOperator{\ppcm}{ppcm}
\DeclareMathOperator{\indice}{Ind}
\DeclareMathOperator{\spec}{Spec}
\renewcommand*{\ker}{\ensuremath{\mathrm{Ker}} } % noyau
\newcommand*{\rond}[1]{\ensuremath{\overset{\hphantom{l}\circ}{#1}} } % ex: pour l'intérieur

\renewcommand*{\th}{\ensuremath{\mathrm{th}} }

% pour «e»
\newcommand{\e}{\mathrm{e}}

%% plus joli
\renewcommand{\leq}{\leqslant}
\renewcommand{\geq}{\geqslant}

% compatibilité
\newcommand{\ensemble}[2]{{#1 \mid #2}}
% }}}

%%% Théorèmes {{{
\usepackage{amsthm}
\usepackage{ifthen}

% Styles
\newtheoremstyle{note}%
    {4pt}% space above
    {4pt}% space below
    {}% body font
    {}% indent amount
    {}% theorem head font
    {.}% punctuation after theorem head
    {.5em}% space after theorem head
    {\textsc{\thmname{#1}\thmnumber{~#2}}\thmnote{~(\textit{#3})}}

\newtheoremstyle{theorema}%
    {4pt}{4pt}{}{}{}{.}{.5em}
    {\textbf{\thmname{#1}\thmnumber{~#2}}\thmnote{~(\textit{#3})}}

% Théorèmes:
% \theoremstyle{style}
% \newtheorem{nom}[compteur]{texte}[compteur réinitialiasant]
\theoremstyle{theorema}

\newtheorem{theoreme}{Théorème}

\newtheorem{proposition}[theoreme]{Proposition}
\newtheorem{lemme}[theoreme]{Lemme}
\newtheorem{axiome}{Axiome}
\newtheorem{corollaire}[theoreme]{Corollaire}
\newtheorem{conjecture}[theoreme]{Conjecture}

\theoremstyle{note} %définitions

\newtheorem*{definition}{Définition}
\newtheorem*{exemple}{Exemple}
\newtheorem*{application}{Application}
\newtheorem*{remarque}{Remarque}
\newtheorem*{notation}{Notation}
\newtheorem*{notations}{Notations}
\newtheorem*{probleme}{Question}
\newtheorem*{rappel}{Rappel}
\newtheorem*{conclusion}{Conclusion}
\newtheorem*{resume}{Résumé}
\newtheorem*{contrexemple}{Contre-exemple}
% }}}

%%% Misc {{{

% Remarques
% a)
% b)
\newcounter{remarques}
\newenvironment{remarques}{\refstepcounter{remarques}\smallskip%
\par\noindent\textbf{Remarques} \par}{\smallskip}
% pour chaque remarque dans l'environnement remarques
\newcounter{remarque}[remarques]
\newcommand{\rem}{\par\noindent\refstepcounter{remarque}\alph{remarque})\;}

% Exemples
% a)
% b)
\newcounter{exemples}
\newenvironment{exemples}{\refstepcounter{exemples}\smallskip%
\par\noindent\textbf{Exemples} \par}{\smallskip}
% pour chaque remarque dans l'environnement exemples
\newcounter{exemplec}[exemples]
\newcommand{\ex}{\par\noindent\refstepcounter{exemplec}\alph{exemplec})\;}

% Propriétés
% a)
% b)
\newcounter{propsc}
\newenvironment{props}{\refstepcounter{propsc}\smallskip%
\par\noindent\textbf{Propriétés} \par}{\smallskip}
% pour chaque remarque dans l'environnement exemples
\newcounter{propc}[propsc]
\newcommand{\prop}{\par\noindent\refstepcounter{propc}\alph{propc})\;}

% (i)
% (ii)
\newenvironment{equivalences}
    {\begin{enumerate}
            \renewcommand{\theenumi}{\roman{enumi}}
            \renewcommand{\labelenumi}{(\theenumi)}}
    {\end{enumerate}}

%%%%%%%%%%%%% Mise en forme %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%% pour les mots de vocabulaire
\newcommand*{\voc}{\textbf} % pour les mots nouveaux
\newcommand*{\code}{\texttt} % pour le code
\newcommand*{\hyp}{\textit} % pour les hypothèses (si on veut)

% }}}

\title{Algorithme de Hopcroft : correction et terminaison }
\author{}
\date{}

\begin{document}

\maketitle

On se donne un automate déterministe, complet et émondé $\cal{A} = (Q,
A, E, I, F)$. La preuve qui suit est tirée de \cite{CA}, à part pour
l'invariant de boucle.

\paragraph{Terminaison.} À chaque itération du \texttt{while}, soit $\cal{P}$
est raffinée, soit $S$ diminué d'un élément : ces opérations ne peuvent
arriver qu'un nombre fini de fois.

\begin{definition}[congruence]
   Une \voc{congruence} est une relation d'équivalence $\sim$ sur $Q$
   qui vérifie pour $q,q'\in Q$ et $a\in A$:
   \begin{align*}
       q \sim q' &\implies (q \in F \ssi q'\in F), \\
       q \sim q' &\implies q \cdot a \sim q' \cdot a
   \end{align*}
\end{definition}

\begin{definition}[stabilité]
    Soit $a\in A$, et $B, C\subset Q$. Alors $B$ est stable pour $(C,a)$
    ssi $B \cdot a \subset C$ ou $B \cdot a \cap C = \vide$. Sinon $(C,
    a)$ coupe $B$ en $B_1 = \{q \in B \mid q\cdot a \in C\}$ et $B_2 = \{ q
    \in B \mid q \cdot a \not\in C\}$. Une partition de $Q$ sera dite
    stable pour $(C,a)$ si chacune de ses parts l'est.
\end{definition}

\begin{remarque}
    $\{P_1,\ldots,P_k\}$ partition de $Q$ compatible avec $F$ est une
    congruence ssi elle est stable pour chaque $(P_i, a), i\in
    \{1,\ldots,k\}, a\in A$.
\end{remarque}

\begin{lemme}
    \label{lem_arbre} Supposons $B \subset Q$, et $C = C_1 \sqcup C_2$.
    Alors $B$ est stable pour $(C_1,a)$ et $(C,a)$ implique $B$ est
    stable pour $(C_2,a)$.
\end{lemme}

\begin{lemme}
    \label{lem_fils}
    Si $B$ est stable sous $(C,a)$, alors tout $P \subset B$ aussi, donc
    en particulier ses fils s'il y a une coupure.
\end{lemme}

\paragraph{Correction.} Remarquons tout d'abord que la congruence de
Nérode raffine toujours $\cal{P}$ : en effet, toutes les coupures sont
nécessaires. Reste à montrer qu'on en a suffisamment, c'est-à-dire qu'à
la fin $\cal{P}$ est une congruence, et celle de Nérode étant la plus
grossière on pourra conclure.

On remarque qu'à chaque itération de la boucle \texttt{while}, une
partie de $\cal{P}$ est laissée identique ou coupée en deux, donc
$\cal{P}$ est l'ensemble des feuilles d'un arbre binaire de racine $Q$,
initialement avec juste deux fils $F$ et $Q \setminus F$. Notons $R$
l'ensemble des éléments qui ont été retirés de $S$. On appellera $T$
l'arbre binaire des parties générées successivement par l'algorithme,
qui contient en particulier $\cal{P}$ et les parties apparaissant dans
$S\cup R$.

Remarquons que $S\cup R$ ne fait que croître au cours de l'algorithme.
De plus, toute partie de $\cal{P}$ est stable sous $R$, un élément étant
dans $R$ si on l'a déja utilisé pour couper les éléments de $\cal{P}$
(la remarque vaut pour les nouveaux fils d'après le
lemme~\ref{lem_fils}).

Montrons l'invariant $I$ de la boucle \texttt{while} suivant par
induction sur le nombre d'étapes : « Si $P \subset Q$ est stable sous
$S\cup R$, alors $P$ est stable sous $T$ » (au sens pour tout $(C,a)$,
$C\in T$ et $a\in A$).

Remarquons tout d'abord que si $I$ est vérifié, à la fin $S$ est vide
donc comme $\cal{P}$ est stable sous $R$, $\cal{P}$ est stable sous $T$
donc en particulier sous les $(C,a), C\in \cal{P}, a\in A$ donc
$\cal{P}$ est la congruence de Nérode.

\emph{Étape 0.} Si $P \subset Q$ est stable sous $(F,a)$ (resp.
$(Q \setminus F, a)$), alors comme $P$ est stable sous $(Q,a)$
(évident), d'après le lemme~\ref{lem_arbre}, $P$ est stable sous $(Q \setminus F, a)$
(resp.  $(F,a)$).

\emph{Induction.} On suppose $I$ à une certaine étape. Montrons $I$
à la fin du \texttt{while}.  À cette fin on fait une autre induction sur le
nombre de coupures effectuées par la première boucle \texttt{for}. Si
aucune coupure n'est effectuée, $T$ (donc $\cal{P}$ aussi) et $S \cup R$
ne changent pas, donc l'invariant est toujours vérifié par hypothèse
d'induction.

Sinon, on a une coupure de $B$ en $B_1$ et $B_2$ pour un $a\in A$ et on
va montrer que $I$ est conservé.  Si $P$ est stable sous $S\cup R$ il
est stable sous $T \setminus \{B_1,B_2\}$ (pour tout $b\in A$) par
hypothèse d'induction. Pour $b\in A$, si $(B,b)\in S$, alors ses deux
fils sont aussi dans $S$, donc $P$ stable sous $T$ par hypothèse. Sinon
par exemple $(B_1,b)$ est dans $S$, et on peut appliquer le
lemme~\ref{lem_arbre} à $P$ pour $(B,b)$ et $(B_1,b)$ : $P$ est donc
stable sous $(B_2,b)$ donc sous $T$ entier, ce qui achève la preuve.

\begin{thebibliography}{1}
   \bibitem{CA}
    O.Carton, \emph{Langages formels, Calculabilité et Complexité}.
\end{thebibliography}

\end{document}