\documentclass[a4paper]{article}
\usepackage{entete}
\author{Introduction à la logique. Théorie de la démonstration. \\ René~\textsc{David}, Karim~\textsc{Nour}, Christophe~\textsc{Raffalli}}
\title{Algorithme d'unification.}
\date{2011-2012}

\begin{document}
\maketitle

On cherche à unifier un ensemble d'équations.

On prend $E$ un ensemble d'équations, et on construit deux suites $E_n$ et $\sigma_n$ par récurrence, avec $E_0=E$ et $\sigma_0=id$.

Puis~:
\begin{enumerate}
    \item Si $E_n = E' \sqcup \{f(u_1,\ldots,u_q) \sim g(v_1,\ldots,v_p\}$, alors
    \begin{itemize}
        \item Si $f=g$, alors $E_{n+1} := E' \cup \{u_1\sim v_1,\ldots,u_p\sim v_p\}$ et $\sigma_{n+1} := \sigma_n$.
        \item Si $f \not = g$, alors renvoyer "Échec clash".
    \end{itemize}
    \item Si $E_n = E' \sqcup \{x\sim x\}$, on pose $E_{n+1}:= E'$ et $\sigma_{n+1}:=\sigma_n$.
    \item Si $E_n = E' \sqcup \{x \sim u\}$ (ou $\{ u \sim x \}$), avec $u\not = x$, alors
    \begin{itemize}
        \item Si la variable $x$ n'apparaît pas dans $u$, on pose $E_{n+1} := E'[x:=u]$ et $\sigma_{n+1} := [x :=u]\circ \sigma_n$.
        \item Sinon, renvoyer "Échec occur-check".
    \end{itemize}
\end{enumerate}

\begin{rmqs}
    \item L'algorithme n'est pas déterministe ; cependant, l'ordre des opérations n'a pas d'importance.
    \item La complexité est exponentielle.
\end{rmqs}

\begin{prop}
    L'algorithme ci-dessus termine toujours, soit par un échec, soit avec $E_n = \emptyset$.
\end{prop}

\begin{proof}
    On note respectivement $a_n,b_n,c_n$ le nombre de variables, de symboles de fonction, d'équations dans $E_n$, et $f(n)=(a_n,b_n,c_n)$. On montre que si $E_n \not = \emptyset$ et pas d'échec à l'étape $n$, $f(n+1)<f(n)$ avec $<$ l'ordre lexicographique.
    On regarde suivant les cas de l'algorithme~:
    $$
    \begin{array}{|c||c|c|c|}
        \hline
        & a_n & b_n & c_n \\
        \hline 
        \hline
        \text{Cas }1 & = & \searrow & \\ 
        \hline
        \text{Cas }2 & \searrow\text{ ou }= & = & \searrow\\
        \hline
        \text{Cas }3 & \searrow & &\\
        \hline
    \end{array}$$
\end{proof}

\begin{thm}
    Si l'algorithme termine avec $E_n=\emptyset$, alors $\sigma_n$ est le {\em mgu} de $E$. S'il échoue par clash ou occur-check, alors $E$ n'a pas d'unificateur.
\end{thm}

\begin{lem}\label{lem:}
    Soient $x$ une variable, $u$ un terme, et $\sigma$ une substitution.
    Si $x[\sigma]=u[\sigma]$, alors $\sigma=\sigma\circ[x:=u]$.
\end{lem}

\begin{proof}
    On pose $\sigma'=\sigma\circ[x:=u]$. Alors 
    $$x[\sigma'] = x[x:=u][\sigma]=u[\sigma]=x[\sigma],$$
    et si $y\not= x$, alors
    $$y[\sigma'] = y[x:=u][\sigma] = y[\sigma].$$
\end{proof}

\begin{proof}
    On montre tout d'abord.
    \begin{center}
        $H_n$ = \og{} À l'étape $n$ de l'algorithme, $\sigma$ unifie $E$ {\em si, et seulement si} il existe $\sigma'$ qui unifie $E_n$ et telle que $\sigma = \sigma' \circ \sigma_n$.\fg{}
    \end{center}

    Si $H_n$ est vraie pour tout $n$, alors, soit $m$ la dernière étape de l'algorithme
    \begin{itemize}
        \item Si $E_m=\emptyset$, l'identité unifie $E_m$, et $H_m$ nous dit alors que $\sigma_m$ unifie $E$, et que c'est bien le {\em mgu}.
        \item Si l'algorithme échoue par clash~: $E_m$ contient une équation de la forme $f(x_1,\ldots,x_p) \sim g(y_1,\ldots,y_q)$ avec $f\not= g$, et donc $E_m$ n'est pas unifiable.
        Par $H_m$, $E$ n'est pas unifiable non plus.
        \item Si l'algorithme échoue par occur-check~: il y a dans $E_m$ une équation de la forme $x\sim u$, $x$ variable de $u$, $x\not= u$.
        Alors pour toute substitution $\sigma$, la taille de $x[\sigma]$ est toujours strictement inférieure à $u[\sigma]$.

        $E_m$ n'est donc pas unifiable, et par $H_m$, $E$ non plus.

        Il ne nous reste plus qu'à montrer~:
        \begin{lem}
            Pour tout $n$ tel que $(E_n,\sigma_n)$ est défini, $H_n$.
        \end{lem}
        \begin{prooflem}
            On a $\sigma_0=id$ et $E_0=E$, et donc $H_0$ est triviale.

            Soit donc $n$ tel que $(E_n,\sigma_n)$ et $(E_{n+1},\sigma_{n+1})$ soient définis.

            Montrons alors
            $$\exists \sigma',~\sigma=\sigma'\circ\sigma_n \text{ et } \sigma'\text{ unifie }E_n$$
            $$\Longleftrightarrow$$
            $$\exists \sigma'',~\sigma=\sigma''\circ\sigma_{n+1} \text{ et } \sigma''\text{ unifie }E_{n+1}$$

            Regardons chaque cas de l'algorithme~:
            \begin{enumerate}
                \item $E_n=E'\sqcup\{f(u_1,\ldots,u_n)\sim f(v_1,\ldots,v_n)\}$, et donc $E_{n+1} = E'\sqcup\{u_1\sim v_1,\ldots,u_n\sim v_n\}$ et $\sigma_n=\sigma_{n+1}$.

                Dans ce cas, on voie bien que l'équivalence est vérifiée.
                \item $E_n=E'\sqcup\{x\sim x\}$, et donc $E_{n+1}=E'$ et $\sigma_{n+1}=\sigma_n$.

                Ici encore, l'équivalence est vérifiée.
                \item $E_n=E'\sqcup\{x\sim u\}$ ou $\{u\sim x\}$ avec $x\not= u$ et $x$ n'est pas une variable de $u$, et donc $E_{n+1}=E'[x:=u]$ et $\sigma_{n+1}=\sigma_n$.
                
                Alors
                \begin{itemize}
                    \item[$(\Leftarrow)$] On prend $\sigma' = \sigma''\circ [x:=u]$.
                    \item[$(\Rightarrow)$] Si $\sigma'$ unifie $E_n$, alors $x[\sigma'] = u[\sigma']$. Par le lemme~\ref{lem:}, on a $\sigma'=\sigma'\circ [x:=u]$, et donc on a le résultat en posant $\sigma''=\sigma'$.
                \end{itemize}
            \end{enumerate}
            

        \end{prooflem}
    \end{itemize}
\end{proof}

\end{document}
