partie15-16.tex

\chapter{Introduction à la programmation logique}
\label{prolog}

Depuis l'arrivée des ordinateurs, il y a eu la vision d'automatiser le raisonnement.
La programmation logique est née dans le contexte de cette vision.
Pour la programmation logique, l'exécution d'un programme correspond à un raisonnement logique dans une théorie logique.
Elle propose l'approche suivante:
\begin{itemize} 
\item Le programme est un {\em ensemble d'axiomes} en logique des prédicats.
\item L'exécution du programme est fait par un {\em prouveur de théorèmes} (similaire à notre algorithme de preuve).
\item L'exécution démarre avec une {\em requête}, une formule à prouver en logique des prédicats.
\end{itemize}
Est-ce que cette approche peut donner un système de programmation pratique?
C'est la grande question de la programmation logique.
Une réponse affirmative à cette question pourrait réaliser plusieurs rêves:
\begin{itemize}
\item La vérification des programmes: si le programme est lui-même un ensemble d'axiomes, sa vérification devient facile.
\item L'intelligence artificielle: si le prouveur est sophistiqué, l'exécution pourrait faire le travail d'un mathématicien.
\end{itemize}
La réponse pour le deuxième rêve est {\em oui, en partie}: les prouveurs de théorèmes sont devenus
des assistants très utiles pour les mathématiciens, mais ils ne les remplacent pas (encore!).
Mais la réponse pour le premier rêve est un {\em oui} très clair.
On peut même dire que c'est là une des plus grandes réalisations de l'informatique au 20ème siècle.
Les systèmes actuels (le langage Prolog n'est que la partie visible d'un iceberg très grand)
sont complètement utilisables pour les applications pratiques:
ils sont performants et robustes, avec une multitude d'outils pratiques.

\section{La voie vers la programmation logique}

Nous allons d'aord suivre le raisonnement qui a mené à l'invention de Prolog
et nous allons montrer les bases théoriques de son exécution.
Principalement, il y a un {\em compris entre expressivité et efficacité}:
un langage trop expressif devient lent.
Si le langage permettrait de résoudre la logique des prédicats complètement,
dans certains cas l'algorithme d'exécution ne pourra rien déduire (parce qu'il est semi-décidable).
Est-ce que l'on peut trouver un langage moins puissant, qui est assez expressif pour la programmation
et assex {\em peu} expressif pour avoir une implémentation efficace?
La réponse à cette question est un oui très clair.
Nous allons dans ce chapitre voir comment on obtient cette réponse.
Il y a trois problèmes majeurs à résoudre:
\begin{enumerate}
\item {\em Limitations théoriques du prouveur}.
Il y a des limites théoriques à ce qu'un prouveur peut faire en tant qu'algorithme.
Nous avons vu une partie de ces limites avec notre algorithme de preuve:
il est semi-décidable: si $p \models q$ l'algorithme termine mais si $p \not\models q$ il ne termine pas toujours.
Si l'algorithme prend beaucoup de temps, on doit à un moment l'arrêter et on ne sait rien.
\item {\em Efficacité du prouveur}.
Même si on peut trouver une preuve, le prouveur peut être inefficace (temps exponentiel).
Le prouveur doit avoir une sémantique opérationnelle (= exécution) efficace et prévisible, pour être pratique.
\item {\em Construction du résultat}.
Même si le prouveur est efficace, on doit {\em construire} une réponse et pas seulement dire que la réponse existe.
Tout programme pratique calcule des résultats et ne dit pas simplement que le résultat existe.
\end{enumerate}

\subsection{Limitations théoriques du prouveur}

Notre algorithme de preuve a les propriétés suivantes:
\begin{itemize}
\item Il est adéquat (consistent): si $p \vdash q$ alors $p \models q$.
C'est-à-dire, si l'algorithme peut prouver la reqûete $q$ à partie du programme $p$,
alors $q$ est effectivement vrai quand $p$ est vrai.
\item Il est complet: si $p \models q$ alors $p \vdash q$.
C'est-à-dire, si $q$ est vrai quand $p$ est vrai, alors l'algorithme peut trouver une preuve.
\end{itemize}
Où est donc le problème?
C'est le ``si'' dans le deuxième point: l'algorithme ne peut pas savoir si $p \models q$.
Si ce n'est pas le cas, alors l'algorithme pourrait ne rien nous dire.

\subsection{Efficacité du prouveur}

Même si l'algorithme peut trouver un résultat, il est souvent hautement exponentiel.
Pour pallier à ce problème on va faire deux choses:
\begin{itemize}
\item Mettre des restrictions sur la forme des axiomes.
On ne permettra que des axiomes pour lequel l'algorithme sait raisonner efficacement.
Typiquement, on ne permettra dans une clause $C_i$ qu'un littéral sans négation:
	$$C_i = (\forall X_{1}) ... (\forall X_{n}) A_{1} \wedge A_{2} \wedge ... \wedge A_{n} \Rightarrow A$$
En forme normale cela donne:
	$$C_{i} = \neg A_{1} \vee \neg A_{2} \vee ... \vee \neg A_{n} \vee A$$
Pour prouver $A$, il faut prouver $A_{1}$ et $A_{2}$ et ... et $A_{n}$).
Le programme tout entier est donc une conjonction de clauses $C_i$:
	$$C_{1} \wedge C_{2} \wedge ... \wedge C_{k}$$
\item Permettre au programmeur de donner des heuristiques (des ``indices'') pour aider le prouveur.
Typiquement, on donne de l'importance à l'ordre des clauses et l'ordre des littéraux dans les clauses.
Le prouveur essaiera les clauses dans l'ordre et les littéraux dans l'ordre.
	$$\text{ordre des axiomes}\left \{
	\begin{array}{l}
	C_{1} = \neg A_{1} \vee \neg A_{2} \vee ... \vee \neg A_{n} \vee A \\
	C_{2} = \underbrace{\neg B_{1} \vee \neg B_{2} \vee ... \vee \neg B_{k} \vee A}_{\text{ordre des littéraux dans un axiome}}\\
	\ldots
	\end{array}
	\right.$$
\end{itemize}
Le langage Prolog utilise ces deux techniques pour obtenir un langage efficace.

\subsection{Construction du résultat}

Notre algorithme de preuve construit de nouvelles clauses à partir des anciennes.
La résolution utilise l'unification, ce qui instantie les variables.
Pour obtenir un résultat final d'une reqûete, il suffit de garder la reqûete
pendant le calcul et de l'instantier avec les mêmes substitutions utilisées
par la résolution.
À la fin du calcul, les variables de la reqûete contiendront alors le résultat.

\subsection{Bref historique}

\begin{enumerate}
	\item 1965 : 	La règle de résolution est inventée par Alan Robinson.
On commence à voir comment la logique peut devenir la base d'un langage de programmation.
	\item 1972 :	Invention du langage Prolog et implémentation de la première interprète
par Alain Colmerauer, Robert Kowalski et Philippe Roussel. 
On démontre que Prolog est un langage utile avec lequel on peut écrire des vrais programmes
avec les axiomes de logique.
Ils inventent le nom Prolog qui vient de {\bf Pro}grammation {\bf Log}ique.
        \item 1977 :    Premier compilateur Prolog par David H. D. Warren.
Un énorme pas en avant, on démontre qu'une implémentation de Prolog peut être compétitif
avec les implémentations des autres langages symboliques comme le Lisp.
        \item 1990 :    Premier compilateur Prolog compétitif avec C par Peter Van Roy et Andrew Taylor.
On démontre qu'il n'y a rien dans le langage Prolog qui empêche une efficacité complète.
\end{enumerate}
Le succès de Prolog vient du fait qu'il fait
un compromis très intéressant par rapport à la tension entre efficacité et expressivité.
Aujourd'hui, on peut faire une implémentation extrêmement efficace de Prolog, qui est même compétitif avec
l'implémentation d'un langage de très bas niveau comme le C.

\section{Introduction au langage Prolog}

Un programme en Prolog est un ensemble de clauses (règles; axiomes):
En Prolog, on a des clauses (règles):
	\begin{equation}
		 A_1 \leftarrow B_1, … , B_n
	\end{equation}
L'intuition d'une clause est que l'on peut prouver $A$ en prouvant $B_1$ jusqu'à $B_n$.
En transformant à la forme normale, cette clause devient d'abord:
	 \begin{equation}
	 	\neg (B_{1} \wedge ... \wedge B_{n}) \vee A_{1}
	 \end{equation}
et ensuite:
	 \begin{equation}
	 	 (\neg B_{1} \vee \neg B_{2} \vee ... \vee \neg B_{n} \vee A_{1})
	 \end{equation}
Avant d'expliquer l'exécution de Prolog, nous allons montrer un exemple d'un programme.

\subsection{Exemple de programme Prolog}

Écrire un programme en Prolog, c'est formuler les algorithmes avec des axiomes en logique.
En voici un premier exemple, extrait du livre « The Art of Prolog » par L. Sterling et E. Shapiro \cite{pro}.
Le voici en syntaxe Prolog:
\begin{verbatim}
   grandpere(X,Z) :- pere(X,Y), pere(Y,Z).

   pere(terach, abraham).
   pere(abraham, isaac).
   pere(haram, lot).
\end{verbatim}
Cet exemple utilise la syntaxe usuelle de Prolog introduit par David Warren.
Les noms des variables sont en majuscule et
le symbole $\leftarrow$ est représenté par les deux caractères \verb+:-+.
Cette syntaxe représente la forme normale suivante:
\begin{equation}
\begin{array}{l}
(\forall x) (\forall y) (\forall z)\ \mathrm{grandpere}(x,z) \vee \neg \mathrm{pere}(x,y) \vee \neg \mathrm{pere}(y,z) \\
\wedge \\
\mathrm{pere}(\mathrm{terach},\mathrm{abraham}) \\
\wedge \\
\mathrm{pere}(\mathrm{abraham},\mathrm{isaac}) \\
\wedge \\
\mathrm{pere}(\mathrm{haram},\mathrm{lot})
\end{array}
\end{equation}
En regardant ce programme, il est claire qu'il y a une correspondance entre Prolog et les bases de données relationnelles.
Un programme Prolog peut être vu comme une base de données relationnelle augmentée avec la déduction.
Le modèle relationnel a été inventé à peu près au même moment que Prolog par E. F. Codd.
Par la suite
il y a eu beaucoup d'influence mutuelle entre la programmation logique et les bases de données.
En particulier, une forme simplifiée de Prolog sans symboles de fonction, appelée Datalog,
est utilisée jusqu'à aujourd'hui pour modéliser la sémantique
des bases de données relationnelles.

\section{Algorithme d'exécution de Prolog}

L'algorithme d'exécution de Prolog est basé sur l'algorithme de preuve de la logique des prédicats,
modifié avec les techniques nécessaires pour obtenir l'efficacité et pour construire les résultats.
Dans la version originale de cet algorithme, l'ensemble $S$ grandit toujours, ce qui n'est pas très efficace.
Pour augmenter l'efficacité, on va remplacer $S$ par une seule clause $r$ qui s'appelle la {\em résolvante}.
Pendant l'exécution de l'algorithme, on va utiliser la résolution sur $r$ pour la modifier.
On ne va donc jamais augmenter le nombre de clauses.
On ne garde que trois choses:
les axiomes de base (le programme $P=\{Ax_1, ..., Ax_n\}$),
la résolvante $r$
et la reqûete originale $G$ (le ``{\em but}'' ou {\em goal})
qui correspond au théorème à prouver.

\subsection{Explication de l'algorithme}

L'exécution de l'algorithme se fait comme ceci:
\begin{itemize}
\item On commence par mettre le but $G$ que l’on veut prouver dans $r$ (sans négation).
\item Ensuite, jusqu’à ce que $r$ soit vide, on prend le premier littéral dans $r$ (par exemple, $A_1$).
\item Puis, on parcourt un à un les axiomes de $P$
pour trouver une clause $Ax_{i}$ unifiable avec $A_{1}$ au moyen de l'upg $\sigma$.

\begin{itemize}
\item Si on trouve une telle clause, on ajoute à $r$ les littéraux de $Ax_{i}$ après unification
avec $A_{1}$, et on continue la boucle dès le début.
\item Si on ne trouve pas de clause unifiable, on revient sur le dernier choix.
Par exemple, pour un littéral $A_{1}$ qui aurait plusieurs clauses unifiables dans $P$, on a dû en choisir une.
On choisit la clause suivante, sans oublier d'abord de remettre $r$ dans sa forme originale.
\item Si on épuise tous les choix sans que $r$ soit vide alors nous sommes en cas d’échec.
La reqûete $G$ ne peut pas être prouvée.
\end{itemize}

\item L'exécution s'arrête quand $r$ est vide ou quand il n'y a plus de choix à faire.
Si $r$ est vide, on a un résultat qui se voit dans $G$.
\item Il est possible aussi d'avoir une boucle infinie (l'algorithme ne s'arrête jamais).
Ceci est considéré comme une erreur: le programmeur doit veiller à définir les axiomes
pour que cela n'arrive pas.
\end{itemize}

\subsection{Définition de l'algorithme}

\begin{algorithm}[H]
$r :=\ <G>$ … résolvante initiale (séquence initiale contient $G$) \\
… pendant l'exécution $r= <A_{1},A_{2},...,A_{m}>$ (séquence de littéraux)\\
\While{r est non vide}{
	\begin{itemize}
		\item Choisir le premier littéral $A_{1}$ dans $r$.
		\item Choisir une clause $Ax_{1}=(A \leftarrow B_{1},...,B_{k})$ dans $P$. D’abord on prend la première clause, puis la suivante jusqu’à ce qu’on trouve une clause unifiable avec $A_{1}$. Si aucune clause n’est unifiable on revient sur le dernier choix (backtrack).
		\item Nouvelle résolvante $r := <B_{1},..., B_{k}, A_{2},...,A_{m}> \sigma$
		\item Nouveau but $G := G \sigma$
	\end{itemize}
}
\If{r est vide}{Le résultat est OUI. Le résultat de l'exécution est le tout dernier $G$.
Si on le souhaite, on peut faire un retour en arrière pour que l'algorithm calcule d'autres solutions.}
\If{On épuise les choix sans que $r$ soit vide}{Le résultat est NON. On n’a pas prouvé $G$. (Attention : $G$ est peut-être vrai, mais les heuristiques ne suffisent pas pour le prouver.)}
\end{algorithm}

\subsection{Gestion des choix}

Il est important de comprendre comment cet algorithme gère les choix des clauses.
L'algorithm fait parfois du retour en arrière (qui s'appelle {\em backtrack} en anglais) pour changer un choix.
Chaque fois que l'on choisit une clause à unifier avec le début de la résolvante,
cela marque un endroit où l'on peut faire un retour en arrière. 
Pour faire le retour en arrière,
il remet ses structures de données internes ($r$ et $G$) à l'état avant le choix
et il recommence son exécution à l'endroit du dernier choix.
S'il n'y a plus de clauses possibles à ce choix,
on revient à l'avant-dernier choix, et ainsi de suite.
La gestion des choix est donc {\em récursive}.
Il y a donc une {\em pile} de choix qui est gérée par l'algorithme.
Pour simplifier la présentation, la gestion de cette pile n'est pas montrée dans la définition de l'algorithme.

Si on arrive au tout premier choix qui a été fait quand on a commencé la boucle et il n'y a plus de clauses unifiables,
alors on sort de la boucle avec une résolvante qui n'est pas vide. Et dans ce cas l'algorithme n'a pas trouvé de solution. 
Il y a donc deux manières de sortir de la boucle: (1) $r$ est vide, et (2) il n'y a plus de choix.
La première manière correspond à une exécution réussie.
La deuxième manière correspond à un échec (``failure'').
Attention, cet échec fait partie de l'algorithme d'exécution, il n'y a rien d'anormal à ce que l'algorithme sort avec un échec.

Une conséquence intéressante de la gestion des choix est que
l'algorithme permet à un programme de trouver plusieurs solutions, s'il existe plusieurs possibilités
de solution pour $G$ dans le programme $P$.
Dans l'exemple $\mathrm{append}(l,m,\mathrm{cons}(1,\mathrm{nil}))$ plus bas,
on voit comment cela marche en pratique.
Pour cet exemple, on trouve une première solution avec $l=\mathrm{nil}$ et $m=\mathrm{cons}(1,\mathrm{nil})$ et une deuxième solution
avec $l=\mathrm{cons}(1,\mathrm{nil})$ et $m=\mathrm{nil}$.
Pour obtenir plusieurs solutions, il suffit après que l'algorithm ait trouvé une solution,
de demander un retour en arrière, c'est-à-dire, de revenir sur le dernier choix et continuer l'exécution.
Ainsi, l'algorithme trouvera plusieurs solutions si la reqûete $G$ à plusieurs solutions avec le programme $P$.
C'est une propriété très puissante de la programmation logique qui n'existe pas dans la programmation traditionnelle.

% Ancienne partie 16

\section{Exemples de programmes Prolog}

Maintenant que nous avons vu l'algorithm d'exécution de Prolog,
regardons quelques programmes pour voir comment on peut programmer en Prolog.
L'idée de base est qu'un programme est un ensemble d'axiomes qui énoncent des propriétés vraies
des algorithmes que l'on veut programmer, tout en permettant l'exécution de procéder de façon efficace.

L'invention de Prolog a donné naissance à un nouveau style de programmation.
La programmation de Prolog est l'art de faire une spécification logique qui possède en même temps une exécution efficace.
Dans cette section nous ne pouvons montrer qu'une toute petite partie de ce style,
mais vous êtes encouragés à explorer d'autres programmes en Prolog et à télécharger
un des nombreux systèmes Prolog pour les exécuter.

\subsection{Exemple 1: Factorielle}

Ce premier exemple montre comment on peut faire des calculs avec des nombres en Prolog.

\subsubsection{Programme en Prolog}

Ce programme permet de calculer la factorielle d'un nombre.
La définition est un ensemble de clauses exprimant des propriétés de la fonction factorielle.
Le code commence par un fait: 0!==1.
Ensuite, il définit une clause pour les factorielles de façon généralisée.
Attention, les virgules et les points sont importants.
Les virgules sont les séparateurs entre les littéraux dits négatifs tandis que le point marque la fermeture de la clause.
\begin{verbatim}
fact(0,1).
fact(N,F) :- N>0, 
        N1 is N-1,
        fact(N1,F1), 
        F is N*F1.
\end{verbatim}
Pour les mordus des langages de programmation, nous mentionnons que ce programme Prolog n'est pas
récursif terminal.  Comme pour la programmation fonctionnelle, il est avantageux aussi pour un prédicat
en programmation logique
d'être récursif terminal, parce que l'exécution dépend aussi d'une pile
et la taille de la pile n'augmentera pas pendant l'exécution.
Ceci ne se voit pas avec une interprète Prolog, comme notre algorithme d'exécution de Prolog, mais devient important pour
un compilateur Prolog.
Il est tout à fait possible d'écrire une autre définition de factorielle en Prolog qui est récursive terminale
et qui garde la sémantique logique.

\subsubsection{Requête}

Nous allons maintenant exécuter le programme fact afin de trouver la factorielle de 5 et stocker la réponse dans la variable F.
Le prompt Prolog est représenté par ``\verb+|?-+'' et la sortie standard par ``\verb+->+''.
En Prolog on peut mettre des commentaires après les ``\verb+%+'' ou entre ``\verb+/* */+''.
Il ne faut pas oublier le point à la fin de la requête.
\begin{verbatim} 
|?- fact(5,F). % Requête de l'utilisateur
-> F=120       % Réponse du système
\end{verbatim}

\subsubsection{Forme clausale}
Voici le programme écrit en forme clausale:
\begin{equation}
\begin{array}{l}
\mathrm{fact}(0,1) \\
\wedge \\
(\forall n) (\forall f) (\forall n_1) (\forall f_1) \\
\quad \quad \mathrm{fact}(n,f) \vee \neg(n>0) \vee \neg \mathrm{minus}(n_1,n,1) \vee \\
\quad \quad \neg \mathrm{fact}(n_1,f_1) \vee \neg \mathrm{times}(f,n,f_1)
\end{array}
\end{equation}
Les trois prédicats mathématiques font partie du système et sont prédéfinis:
$a>b$ est vrai si $a>b$,
$\mathrm{minus}(a,b,c)$ est vrai si $a=b-c$,
$\mathrm{times}(a,b,c)$ est vrai si $a=b \times c$.

\subsubsection{Exécution} 

Le but de l'exécution est de prouver la requête $G$ avec $G = \mathrm{fact}(5, r)$.
Pour y arriver, Prolog construira au fur et à mesure de l'exécution
une substitution finale $\sigma_{res}$ en faisant les résolutions qui feront évoluer $r$.
La substitution finale, appliquée à $G$, donnera le résultat final.

\begin{equation}
\begin{array}{l}
\mathit{Requête\ initiale:}\\
r =\ < \mathrm{fact}(5, r) > \\
\mathit{Résolution\ 1:} \\
\sigma = \{ (n, 5), (f, r) \} \\
r =\ < (5>0), \mathrm{minus}(n_1, 5, 1), \mathrm{fact}(n_1, f_1), \mathrm{times}(r, 5, f_1) > \\
\mathit{Résolution\ 2:} \\
\sigma'=\sigma \\
r =\ < \mathrm{minus}(n_1, 5, 1), \mathrm{fact}(n_1, f_1), \mathrm{times}(r, 5, f_1) > \\
\mathit{Résolution\ 3:} \\
\sigma''= \sigma' \cup \{ (n_1, 4) \} \\
r =\ < \mathrm{fact}(4, f_1), \mathrm{times}(r, 5, f_1) > \\
\ldots \\
\sigma_{res} = \{(r,120), \ldots\} \\
r =\ <\ >
\end{array}
\end{equation}
Le résultat final est donc $\mathrm{fact}(5, 120)$, ce qui donne en syntaxe Prolog \verb+fact(5,120)+.

\subsection{Exemple 2: Append de deux listes}

Cet exemple montre comment on peut faire des calculs avec des structures de données en Prolog.
Le but de ce programme est de faire la concaténation de deux listes.

\subsubsection{Programme en Prolog}

\begin{verbatim}
append([],L,L).
append([X|L1],L2,[X|L3]) :- append(L1,L2,L3).
\end{verbatim}

\subsubsection{Requête}

La requête initiale $G = \mathrm{append}(\mathrm{cons}(1,\mathrm{nil}), \mathrm{cons}(2,\mathrm{nil}), l)$.
On veut faire la concaténation des listes \verb+[1]+ et \verb+[2]+ (en syntaxe Prolog).
La paire de liste, écrite \verb+[X|L1]+ en Prolog, s'écrit $\mathrm{cons}(x,l_1)$ en syntaxe logique.

\begin{verbatim}
|?- append([1], [2], L).
-> L=[1,2]
\end{verbatim}

\subsubsection{Forme clausale}

Voici le programme écrit en forme clausale:
\begin{equation}
\begin{array}{l}
\mathrm{append}(\mathrm{nil},l',l') \\
\wedge\\
(\forall l_1) (\forall l_2) (\forall l_3) (\forall x) \\
\quad \quad \mathrm{append}(\mathrm{cons}(x,l_1),l_2,\mathrm{cons}(x,l_3)) \vee \neg\mathrm{append}(l_1,l_2,l_3)
\end{array}
\end{equation}

\subsubsection{Exécution}

La première valeur de $r$ contient la requête initiale.
\begin{equation}
\begin{array}{l}
\mathit{Requête\ initiale:} \\
r =\ < \mathrm{append}(\mathrm{cons}(1,\mathrm{nil}), \mathrm{cons}(2,\mathrm{nil}), l)> \\
\mathit{Résolution\ 1:} \\
\sigma = \{(x,1), (l_1,\mathrm{nil}), (l_2,\mathrm{cons}(2,\mathrm{nil})), (l,\mathrm{cons}(x,l_3))\} \\
r =\ < \mathrm{append}(\mathrm{nil}, \mathrm{cons}(2,\mathrm{nil}), l_3) > \\
\mathit{Résolution\ 2:} \\
\sigma_{res} = \sigma \cup \{ (l',\mathrm{cons}(2,\mathrm{nil})), (l_3,l') \} \\
r =\ <\ > \\
\end{array}
\end{equation}
Expliquons en plus de détail ce qui se passe lors de résolution 1:
\begin{quote}
Il y a une unification entre le premier élément de $r$,
c'est-à-dire $\mathrm{append}(\mathrm{cons}(1,\mathrm{nil}), \mathrm{cons}(2,\mathrm{nil}), l)$,
et la tête d'une clause (un littéral positif) dans le programme,
c'est-à-dire ici $\mathrm{append}(\mathrm{cons}(x,l_1),l_2,\mathrm{cons}(x,l_3))$.
Cette unification donne lieu à une substitution: une liste de paires (variable,terme)
nécessaire pour que les deux littéraux deviennent égaux.
C'est la substitution $\sigma$.
La nouvelle résolvante après la résolution 1 est le littéral négatif de la clause,
c'est-à-dire $\mathrm{append}(l_1,l_2,l_3)$, où l'on a remplacé les variables par leurs substitutions.
C'est la valeur de $r$ juste en dessous de $\sigma$.
\end{quote}
Après la résolution 2,
l'exécution s'arrête avec réussite parce que $r$ est vide.
Le résultat final est:
\begin{equation}
\begin{array}{l}
\sigma_{res} = \{(x,1), (l_1,\mathrm{nil}), (l_2,\mathrm{cons}(2,\mathrm{nil})), (l,\mathrm{cons}(x,l_3)), (l',\mathrm{cons}(2,\mathrm{nil})), (l_3,l') \} \\
G = \mathrm{append}(\mathrm{cons}(1,\mathrm{nil}), \mathrm{cons}(2,\mathrm{nil}), \mathrm{cons}(1,\mathrm{cons}(2,\mathrm{nil})))
\end{array}
\end{equation}
Pour trouver le résultat $G$ on a simplement appliqué $\sigma_{res}$ à la requête initiale.
La seule variable dans la requête initiale est $l$: la valeur de $l$ est à trouver dans $\sigma_{res}$
(il faut suivre les substitutions jusqu'au bout!).

\begin{center}
\noindent\fbox{
\parbox{0.8\textwidth}{Attention, chaque fois que l'on fait la résolution
avec une clause du programme il faut {\em renommer} les variables de la clause.
Dans le cas ci-haut ce sont $l_1$, $l_2$, $l_3$ et $x$.
Ceci est nécessaire pour éviter d'utiliser le même nom pour deux variables différentes pendant l'exécution.}}
\end{center}

\subsection{Exemple 3: Append avec plusieurs solutions}

Le programme de l'exemple précédant peut calculer plusieurs solutions,
si plusieurs solutions existent et on demande à l'algorithme de nous les calculer.
Pour notre dernier exemple on va regarder cela de plus près
en donnant comme requête $\mathrm{append}(l_1, l_2, \mathrm{cons}(1,\mathrm{nil}))$.
On voit bien qu'il y a deux solutions:
\begin{itemize}
\item La première solution est $l_1=\mathrm{nil}$ et $l_2=\mathrm{cons}(1,\mathrm{nil})$.
\item La deuxième solution est $l_1=\mathrm{cons}(1,\mathrm{nil})$ et $l_2=\mathrm{nil}$.
\end{itemize}
Regardons si l'algorithme les trouve aussi!

\subsubsection{Requête}

La requête initiale est $G = \mathrm{append}(l_1, l_2, \mathrm{cons}(1,\mathrm{nil}))$.
On la donne au système avec la syntaxe \verb+append(L1,L2,[1])+.
L'exécution du système donnera d'abord la première solution.
L'utilisateur pourra demander une deuxième solution en tapant le caractère \verb+;+ (point-virgule).
\begin{verbatim} 
|?- append (L1,L2,[1]).
-> L1=[], L2=[1] ;
-> L1=[1], L2=[]
\end{verbatim}

\subsubsection{Exécution}

La première valeur de $r$ contient la requête initiale.
\begin{equation}
\begin{array}{l}
\mathit{Requête\ initiale:} \\
r =\ < \mathrm{append}(l_1, l_2, \mathrm{cons}(1,\mathrm{nil})) > \\
\mathit{Résolution\ 1:} \\
\sigma = \{ (l_1,\mathrm{nil}), (l_2, l'), (l',\mathrm{cons}(1,\mathrm{nil})) \} \\
r =\ <\ >
\end{array}
\end{equation}
L'algorithme commence par choisir la première clause, $\mathrm{append}(\mathrm{nil},l',l')$.
Cela donne un résultat (obtenu en remplissant la requête avec $\sigma$):
\begin{equation}
\begin{array}{l}
G = \mathrm{append}(\mathrm{nil}, \mathrm{cons}(1,\mathrm{nil}), \mathrm{cons}(1,\mathrm{nil})) \\
\end{array}
\end{equation}
En syntaxe Prolog, c'est le résultat \verb+append([],[1],[1])+.
Si on demande un autre résultat,
l'algorithme fera un retour en arrière pour faire un autre choix de clause.
Le dernier choix fait par l'algorithme a été fait lors de la première résolution,
où il a choisi la première clause.
On peut re-exécuter cette résolution, en choisissant la deuxième clause.
Ensuite on continue jusqu'à ce que la résolvante est vide:
\begin{equation}
\begin{array}{l}
\mathit{Résolution\ 1bis:} \\
\sigma = \{ (l_1,\mathrm{cons}(x',l_1')), (l_2,l_2'), (x',1), (l_3',\mathrm{nil}) \} \\
r =\ < \mathrm{append}(\mathrm{cons}(1,l_1'), l_2', \mathrm{nil}) > \\
\mathit{Résolution\ 2bis:} \\
\sigma' = \sigma \cup \{ (l'',\mathrm{cons}(1,l_1'), (l'',l_2') \} \\
r =\ < \mathrm{append}(l_1', l_2', \mathrm{nil})> \\
\mathit{Résolution\ 3bis:} \\
\sigma'' = \sigma' \cup \{ (l_1',\mathrm{nil}), (l_2',l'''), (l''',\mathrm{nil}) \} \\
r =\ <\ >
\end{array}
\end{equation}
Cela donne un autre résultat (obtenu en remplissant la requête avec $\sigma''$):
\begin{equation}
\begin{array}{l}
G = \mathrm{append}(\mathrm{cons}(1,\mathrm{nil}), \mathrm{nil}, \mathrm{cons}(1,\mathrm{nil}))
\end{array}
\end{equation}
En syntaxe Prolog, c'est le résultat \verb+append([1],[],[1])+.
Cela donne deux résultats qui satisfont tous les deux la requête initiale.
On peut essayer de trouver un troisième résultat, en faisant un nouveau retour en arrière
(c'est possible parce que {\em 3bis} a choisi la première clause),
on verra que l'unification échouera: il n'y a que deux résultats pour notre requête.

\subsection{Dernières remarques}

Voici ce qui termine notre introduction à la programmation logique et au langage Prolog.
Nous n'avons expliqué qu'une petite partie de ce que peut faire un système Prolog.
Je voudrais terminer par attirer votre attention sur les
deux manières de percevoir l'exécution d'un programme Prolog:
\begin{enumerate}
\item {\em La vue opérationnelle}: l'exécution est vue comme une séquence de calculs.
On se concentre sur l'exécution de l'algorithme de preuve.
Le résultat d'un calcul est une séquence d'opérations, avec ses problèmes de temps
d'exécution et d'espace mémoire utilisé.
\item {\em La vue logique}: l'exécution est vue comme une preuve en logique des prédicats.
On oublie l'algorithme et on se concentre sur la logique.
Le résultat d'un calcul est un théorème, donc une conséquence logique des axiomes du programme.
\end{enumerate}
Prolog est un des rares langages à offrir ces deux vues sur une même exécution.
Cela donne beaucoup de puissance: on peut raisonner sur l'exactitude de façon (presque) complètement
indépendante de l'efficacité.

\subsubsection{L'équation de Kowalski}

La relation entre la vue logique et la vue opérationnelle
est résumée par la célèbre équation de Kowalski:
\begin{quote}
Algorithm = Logic + Control
\end{quote}
La logique et le contrôle peuvent être vus de façon séparées.
Pour une même définition logique, on peut changer l'efficacité
en changeant le contrôle.
Cela change l'algorithme mais ne change pas ce que calcule l'algorithme.

\subsubsection{L'influence de Prolog}

La programmation logique, le langage Prolog et ses successeurs,
gardent une grande influence sur l'informatique.
L'esprit de Prolog est toujours présent
dans beaucoup de domaines de l'informatique, par exemple:
\begin{itemize}
\item Les bases de données (modèle relationnel et Datalog).
\item La sémantique Web (basée sur un langage logique OWL et un modèle d'exécution).
\item La programmation par contraintes (on remplace les substitutions par des relations quelconques).
\end{itemize}