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
"XP1 Ú ¬ 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}
  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.