Planche 1
Cours 6
Prolog
Jean-Jacques.Levy@inria.fr
http://jeanjacqueslevy.net

secrétariat de l'enseignement:
Catherine Bensoussan
cb@lix.polytechnique.fr
Laboratoire d'Informatique de l'X
Aile 00, LIX
tel: 34 67
http://w3.edu.polytechnique.fr/informatique

Planche 2
Références
Planche 3
Plan

  1. Datalog
  2. Prolog sur des termes structurés
  3. Syntaxe de Prolog
  4. Termes, Clauses
  5. Principe de résolution
  6. Unification
  7. Unification rapide
Planche 4
Programmation
=
Logique

Planche 5
Un peu de Prolog

Faits


pere(charles,napoleon).              male(charles).
pere(charles,lucien).                male(napoleon).
pere(charles,joseph).                male(lucien).
pere(napoleon,aiglon).               male(joseph).
pere(lucien,charlotte).              male(charles_lucien).
pere(lucien,charles_lucien).         
pere(lucien,christine).              femelle(charlotte).
                                     femelle(christine).
mere(josephine,aiglon).              femelle(josephine).
Requêtes 

femelle(napoleon)?
pere(josephine,aiglon)?
La prèmière répondra oui, la deuxième non.

Planche 6
Un peu de Prolog

Requêtes existentielles   $ X. pere(lucien, X)


pere(lucien,X)?
X=charlotte
X=charles_lucien
X=christine
Réversibilité   $ X. pere(X, charles_lucien)


pere(X,charles_lucien)?
X=lucien
Planche 7
Un peu de Prolog

Requêtes avec conjonction 

pere(charles,napoleon),femelle(josephine)?
Le système répond oui.
Requête conjonctive plus intéressante  $ X. pere(lucien, X) Ù male(X) 

pere(lucien,X), male(X)?
X=charles_lucien

Autre Requête conjonctive   $ X.$ Y. pere(charles, X) Ù pere(X,Y) 

pere(charles,X), pere(X,Y)?
X=napoleon, Y=aiglon
X=lucien, Y=charlotte
X=lucien, Y=charles_lucien
X=lucien, Y=christine
Planche 8
Règles -- Clauses

On peut définir des règles grâce aux clauses suivantes


fils(X,Y) <- pere(Y,X), male(X).
fille(X,Y) <- pere(Y,X), femelle(X).
grandpere(X,Y) <- pere(X,Z), pere(Z,Y).

signifiant
" X." Y.pere(Y,X) Ù male(X) É fils(X,Y)
" X." Y.pere(Y,X) Ù femelle(X) É fille(X,Y)
" X." Y." Z.pere(X,Z) Ù pere(Z,Y) É grandpere(X,Y)
et lancer les requêtes 

fils(napoleon,X)?
fille(X,charlotte)?
grandpere(charles,X)?

Un programme Prolog est un ensemble fini de clauses.

Planche 9
Récursivité

La disjonction de deux clauses permet d'écrire 

parent(X,Y) <- pere(X,Y).
parent(X,Y) <- mere(X,Y).

Rien de plus que l'application de la tautologie (B Ú C) É A  º  (B É A) Ú (C É A)
Inductivement, on a
" X.ancetre(X,X)
" X." Y." Z.parent(X,Z) Ù ancetre(Z,Y) É ancetre(X,Y)
D'où le programme récursif 

ancetre(X,X) <-.
ancetre(X,Y) <- parent(X,Z), ancetre(Z,Y).
Planche 10
Structures de données et termes

Les prédicats peuvent porter sur des objets structurés. Par exemple des listes 

append([],Y,Y) <-.
append(X::Xs,Y::Ys,Z::Zs) <- append(Xs,Ys,Zs).
Requêtes possibles 

append(3::4::[],Y) ?
append(X, 3::4::Y, 1::2::3::4::Z) ?
Exercice 1Écrire member, reverse.
De même sur les entiers unaires, on peut écrire 

plus(X,0,X) <-.
plus(X,s(Y),s(Z) <- plus(X,Y,Z).
times(0,X,0) <-.
times(s(X),Y,Z) <- times(X,Y,W), plus(W,Y,Z).
Exercice 2Écrire factorielle, Fibonacci, Ackermann.

Planche 11
Syntaxe de Prolog
P ::= C1, C2, ... Cn programme
C ::= P ¬ P1 Ù P2 Ù ... Pn clause de Horn
P ::= p(M1,M2,... Mn) littéral (n arité de p)
M ::= f(M1,M2,... Mn) terme (n arité de f)
  | X variable
    P ¬ Fait

FV(M), FV(P), FV(C) sont les ensembles des variables de C, P, C.

Exercice 3En donner la définition récursive.

Planche 12
Faits et Clauses

Les faits sont donc des clauses sans prémisses. Les clauses sont des assertions universelles. Si X = FV(C), la clause C représente le prédicat "X.C.
Buts

Les buts sont existentiels. Si X = FV(P1 Ù P2 Ù ... Pn), le but à montrer est $X.P1 Ù P2 Ù ... Pn.
Raisonnement par contradiction

On essaie de montrer que ¬$X.P1 Ù P2 Ù ... Pn aboutit à une contradiction.

On rajoute donc le fait "X.¬ P1 Ú ¬ P2 Ú ... ¬ Pn

C'est à dire la clause "X.  ¬ P1 Ù P2 Ù ... Pn

Montrer des buts consiste à rajouter une clause dont les prémisses sont les buts et la conclusion est vide, et montrer que le tout aboutit à une contradiction.

Planche 13
Résolution propositionnelle

En logique, la règle de coupure suivante est valide

|- P Ú Q    |- ¬ P Ú R
|- Q Ú R

Soit une clause P ¬ P1 Ù P2 Ù... Pn, alors on peut réduire les ensembles de buts comme suit
{P, Q2, ... Qm} ¾® {P1, P2,... Pn,Q1,Q2,... Qm}

Exercice 4Montrer que ce remplacement est valide.

Comme n ³ 0, après un certain nombre de coupures on peut se retrouver avec un ensemble vide de buts. Equivalent au prédicat faux. Donc contradiction.

Cette méthode [Robinson] est le principe de résolution.

Planche 14
Substitutions

Une substitution s est une fonction des variables dans les termes. On écrira s = [X1 \ M1, X2 \ M2, ··· Xn \ Mn] quand son graphe est fini. On l'étend naturellement comme fonction des termes dans les termes. On écrit Ms pour le terme obtenu en appliquant s à M. De même, pour la composition s ° s' de deux substitutions s et s'.

Posons M £ M' ss'il existe s tel que M' = Ms
et s £ s' ss'il existe f tel que s' = f ° s.

On peut remarquer que les termes ont une structure de treillis vis à vis de £.

De même, tout système d'équations sur les termes admet une solution minimale.

Un terme sans variable est un terme clos. Une substitution close remplace des variables par des termes clos.

Deux formules F et F' sont disjointes si FV(F) È FV(F') = Ø

Planche 15
Résolution

On peut avoir à tenir compte des variables pour arriver à une réfutation. La règle de coupure correspondante est
|- P Ú Q    |- ¬ P' Ú R    Ps = P's    PÚ Q et ¬ P' Ú R disjointes
|- Qs Ú Rs

Résolution SLD

Soit un ensemble de buts {Q1, Q2,...Qn}. Les règles de calcul de Prolog sont les suivantes
Succès { } ¾® succes
SLD {Q1, Q2... Qm} ¾® {P1s, P2s,... Pns,Q2s,... Qms}
  où P ¬ P1 Ù P2 Ù... Pn est une clause disjointe des buts
  telle que Q1s = Ps
Echec {Q1, Q2... Qm} ¾® echec sinon

Planche 16
Exemples 


fils(napoleon,X)
pere(X,napoleon),male(napoleon)
male(napoleon)   [X=charles]
succes   [X=charles]


append(X,2::Y,1::2::Z)
append(Xs,2::Y,2::Z)  [X=1::Xs]
succes   [X=1::[], Y=Z]


append(X,2::Y,1::2::Z)
append(Xs,2::Y,2::Z)  [X=1::Xs]
append(X1s,Y,Z)  [X=1::2::X1s]
succes   [X=1::2::[], Y=Z]
Planche 17
Non déterminisme

Plusieurs solutions sont possibles car on peut choisir arbitrairement les buts à remplacer, et les règles à utiliser.

Théorème [correction] L'ensemble des solutions trouvées est correct.

Théorème [complétude] Par résolution, on trouve toutes les solutions.
Retour en arrière et stratégie de Prolog

Un des choix peut aboutir à une impasse. On doit revenir en arrière (bactracking) pour en essayer un autre.

L'ensemble des solutions trouvées dépend de la stratégie de réduction. Prolog fait une stratégie en profondeur d'abord. Il peut louper des solutions.

Par exemple, deviner l'ensemble des solutions trouvées pour 

ancetre(X,X).
ancetre(X,Y) <- ancetre(X,Z),parent(Z,Y).
Planche 18
Unification sur les termes

C'est le même problème que celui déjà vu pour l'inférence de types. Seule l'algèbre des termes à considérer diffère.

mgu(E) est la plus petite solution du système d'équations E si elle existe. Le résultat est donc echec ou une substitution. (most general unifier)

Algorithme de Robinson
mgu (Ø) = identite
mgu ({X=X} È E) = mgu (E)
mgu ({X=M } È E) = mgu (E[X \ M]) ° [X \ M] si X ÏFV(t)
mgu ({ M=X} È E) = mgu (E[X \ M]) ° [X \ t] si X ÏFV(t)
mgu ({ F(M) = F(N)} È E) = mgu ({M1 = N1,... Mn = Nn } È E)
sinon    mgu (E) = echec

Planche 19
Unification rapide

Algorithme [Martelli-Montanari; Huet-Kahn]

Equations sur les arbres rationnels (sans occur-check pour les variables) et on évite l'élimination des variables qui fait augmenter la taille des termes.

Exemple: M = f(g(y,h(t,y)), x), N = f(x, g(h(h(t,t),h(a,b))))

On génère un ensemble de classes d'équivalence sur les sous-termes de M et de N.
n1 = f(n2, x) n3 = f(x, n5)
n2 = g(y, n4) n5 = g(n6, y)
n4 = h(t, u) n6 = h(n7, n8)
  n7 = h(t, t)
  n8 = h(a, b)

Planche 20
En TD A la maison et prochaine fois

This document was translated from LATEX by HEVEA.