[Haute priorité] Section Prolog

[adethise]

(section 7.11.2 et 7.12 à fin du chapitre, partie 15) La partie qui présente le fonctionnement de Prolog manque d'explications sur les exemples - et de clarté en général. Par exemple, il faudrait indiquer plus d'itérations avec des explications, expliciter sur base de quelle règle un certaine substitution est faite, etc.

[suelambot]

Pour moi il y a aussi un problème avec la condition de sortie de l'algo tel que défini. Il spécifie "while r est non vide do" et à la fin du while, on test si r est vide ou non. Il est claire qu'il manque une condition de sortie dans la boucle while. Pour moi ça devrait être quelque chose comme while r non vide et il reste des axiomes dans P a évaluer do. Dans le cas contraire, il est impossbile de sortir sans avoir trouvé une solution ce qui n'a pas de sens.

[petervanroy]

On 15/01/15 19:06, suelambot wrote:

Pour moi il y a aussi un problème avec la condition de sortie de
l'algo tel que défini. Il spécifie "while r est non vide do" et à la
fin du while, on test si r est vide ou non. Il est claire qu'il manque
une condition de sortie dans la boucle while. Pour moi ça devrait être
quelque chose comme while r non vide et il reste des axiomes dans P a
évaluer do. Dans le cas contraire, il est impossbile de sortir sans
avoir trouvé une solution ce qui n'a pas de sens.

—
Reply to this email directly or view it on GitHub
#9 (comment).

Oui, il y effectivement une autre sortie de la boucle: cela a un rapport
avec les retours en arrière s'il n'y a plus de clauses unifiables (ce
qui s'appelle un échec - "failure"). 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. Pendant l'exécution de la
boucle, il y a donc une séquence de choix qui sont faits. Si au
dernier choix il n'y a plus de clauses unifiables, on retourne à
l'avant-dernier choix et on continue avec un nouveau choix. Cela se
fait récursivement: si à l'avant-dernier choix il n'y a plus de choix
qui donne une solution, on retourne à l'avant-avant-dernier choix. Et
ainsi de suite. 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.

Toute cette gestion de choix et de retours en arrière n'est pas codée
explicitement dans l'algorithme, sinon cela devient incompréhensible.
Il est plus facile de comprendre l'algorithme tel quel, et supposez
qu'il y a une gestion des choix qui est imposée dessus. Chaque fois que
l'on fait un choix, on sauvegarde l'état actuel de l'exécution dans la
séquence de choix. Un retour en arrière fera une restoration de cet
état (qui contient toutes les anciennes valeurs des variables utilisées
dans la boucle y compris r et G).

Vous pouvez ajouter cette explication dans le texte. Dans l'exemple
append(l,m,cons(1,nil)) on voit comment cela marche en pratique: cela
permet effectivement d'obtenir plusieurs solutions (pour cet exemple,
une solution avec l=nil et m=cons(1,nil) et une autre solution avec
l=cons(1,nil) et m=nil).

Peter