EPITA

Introdution à Prolog, cours n° 3 (fin)

Jean-François Perrot

Prolog comme moteur d'inférences du premier ordre en marche arrière.

  1. Ouverture : vers le 1er ordre
    1. Point de départ
    2. Point d'arrivée

  2. Unification
    1. Le problème
      1. Équations entre termes du 1er ordre
      2. Unificateur plus général
      3. Résultats
    2. Emploi de l'unification en Prolog
      1. Le symbole d'égalité "="
      2. L'égalité stricte "=="
      3. L'égalité structurelle "=@="
      4. Le problème du test d'occurrence (occur-check).
    3. Une réalisation de l'algorithme d'unification de Robinson en Prolog
      1. Représentation des termes
      2. Substitutions
      3. Essai

  3. α-conversion

  4. Le prédicat d'appel

  5. Essais

Ouverture : vers le 1er ordre


Unification

  1. Le problème


  2. Emploi de l'unification en Prolog

    Prolog utilise l'unification dans son mécanisme d'interprétation, mais il la met aussi à la disposition du programmeur. Il en résulte plusieurs notions d'égalité dans le langage.
    1. Le symbole d'égalité "="
      "t1 = t2" dénote l'unifiabilité des termes t1 et t2, non leur égalité verbatim.
      Le but "X = toto." réussit, avec justement X valant toto.

      Sa négation est "\=" : "t1 \= t2" équivaut à "not(t1 = t2)"
    2. L'égalité stricte "=="
      Cette fois, le but "X == toto." échoue,
      de même que "f(X) == f(Y).", mais "f(X) == f(X)." réussit.
      Sa négation est "\==" : "t1 \== t2" équivaut à "not(t1 == t2)"

    3. L'égalité structurelle "=@="
      Succeeds if Term1 is `structurally equal' to Term2.
      Structural equivalence is weaker than equivalence (==/2), but stronger than unification (=/2). Two terms are structurally equal if their tree representation is identical and they have the same `pattern' of variables.
      Examples:
      a    =@=    A    false
      A    =@=    B    true
      x(A,A)    =@=    x(B,C)    false
      x(A,A)    =@=    x(B,B)    true
      x(A,B)    =@=    x(C,D)    true

      Sa négation est "\=@=" : "t1 \=@= t2" équivaut à "not(t1 =@= t2)"
    4. L'égalité numérique "=:="
      Expr1 =:= Expr2 : True if expression Expr1 evaluates to a number equal to Expr2.
      Le mot equal doit être pris en un ens mathématique, indépendant des questions de type.
      La documentation de SWI-Prolog poursuit :
      Note that normally, is/2 should be used with unbound left operand. If equality is to be tested, =:=/2 should be used.
      For example:
      ?- 1 is sin(pi/2).    Fails!. sin(pi/2) evaluates to the float 1.0, which does not unify with the integer 1.
      ?- 1 =:= sin(pi/2).    Succeeds as expected.

      Sa forme négative est "=\=" : "t1 =\= t2" True if expression t1 evaluates to a number non-equal to t2.
    5. Le problème du test d'occurrence (occur-check).
      Si on unifie une variable avec un terme contenant cette variable, on obtient un terme infini :
      la solution de l'équation "au point fixe" X = f(X) est f(f(f(...( )))).
      C'est pourquoi l'algorithme d'unification officiel vérifie que cette circonstance n'a pas lieu,
      et dans le cas contraire déclare les termes non-unifiables.

      Pour des raisons d'économie, l'unification de Prolog ne fait pas ce test, et engendre donc des termes infinis que Prolog sait manipuler (évaluation paresseuse).
      ?- X = f(X).
      X = f(**).

      En contrepartie, SWIProlog offre au programmeur un prédicat standard unify_with_occurs_check.

      ?- unify_with_occurs_check(X, f(X)).
      false.

  3. Une réalisation de l'algorithme d'unification de Robinson en Prolog

    1. Représentation des termes
      Ce sont des termes Prolog ordinaires, sans variables Prolog.
      Les atomes Prolog sont les constantes de nos termes, 
      sauf ceux qui sont explicitement  déclarés comme variables par le predicat "isvar"
      (N.B. "var" est un prédicat réservé de Prolog ).

      :- dynamic isvar/1. % sera modifié plus tard pour alpha-conversion

      isvar(a). isvar(b). isvar(c). isvar(d).
      isvar(u). isvar(v).
      isvar(x). isvar(y). isvar(z).

      Exemples d'école, pour essais :
      • rob1( p(a, f(g(b)),  f(a)) ).
        rob2( p(h(b, c), f(c), f(h(u, v))) ).
      • jg1( p(g(z), y) ).
        jg2( p(x, f(u)) ).
      • jgg1( p(a, x, f(g(y))) ).
        jgg2( p(z, f(x), f(u)) ).  /* avec occur-check */

      Le test d'occurrence (en anglais "occur-check") d'une variable dans un terme :
      nocc(Var, Terme) et son itéré dans une liste de termes : locc(Var, LTermes)

      nocc(Var, Var) :- !, fail.
      nocc(Var, Atom) :- atomic(Atom),!.
      nocc(Var, Terme) :- Terme =..[Fonc|LArgs], locc(Var, LArgs).
      locc(Var, []).
      locc(Var, [A|S]) :- nocc(Var, A), locc(Var, S).

    2. Substitutions
      On les représente comme des listes de couples [variable, valeur] (en Lisp, on dirait des A-listes).
      Mais on convient que la valeur d'une variable est sa "valeur ultime",
      c'est-à-dire une valeur où n'apparaît aucun atome ayant lui-meme une valeur dans la substitution,
      sans quoi on ira chercher la valeur ultime de cet atome..
      Exemple : la valeur de a dans [[a, f(b)], [b, g(c)], [c, x]] est f(g(x)) et non pas f(b).

      Cette convention facilite le calcul des substitutions par composition
      (puisqu'il suffit alors de les concaténer), mais alourdit leur application.

      Valeur d'une variable : conformément a la convention ci-dessus,
      on teste la présence de la variable et on applique la substitution :

      aval(Atome, Subst, Val) :-
                      isvar(Atome), present(Atome, Subst, Val1),!,
                      appsub(Subst, Val1, Val).
      aval(Atome, Subst, Atome).

      present(Var, Env, Val) :- member([Var, Val], Env).

      Appliquer une substitution à un terme : appsub(Subst, Terme, Res)
      et son itérée sur une liste de termes: lappsub(Subst, LTermes, LRes)

      appsub(Subst, Terme, Val) :-
                      atomic(Terme),!, aval(Terme, Subst, Val).
      appsub(Subst, Terme, Val) :- Terme=..[Fonc|LArgs],
                      lappsub(Subst, LArgs, LVals),
                      Val =.. [Fonc|LVals].

      lappsub(Subst, [], []).
      lappsub(Subst, [A|S], [V|LV]) :- appsub(Subst, A, V),
                          lappsub(Subst, S, LV).

    3. Le prédicat-maître :  unif(Terme1, Terme2, Subst)
      et son itéré sur des listes de termes lunif(L1, L2, Subst)

      unif(Terme1, Terme2, []) :- Terme1 = Terme2,!.
      unif(Terme1, Terme2, [[Terme1, Terme2]]) :- isvar(Terme1),!,
                              nocc(Terme1, Terme2).
      unif(Terme1, Terme2, [[Terme2, Terme1]]) :- isvar(Terme2),!,
                              nocc(Terme2, Terme1).
      unif(Terme1, Terme2, Subst) :- Terme1 =.. [Fonc|LArgs1],
                      Terme2 =.. [Fonc|LArgs2],
                      lunif(LArgs1, LArgs2, Subst).

      lunif([], [], []).
      lunif([A1|S1],  [A2|S2], Subst) :-
                  unif(A1, A2, Sub),
                  lappsub(Sub, S1, L1),
                  lappsub(Sub, S2, L2),
                  lunif(L1, L2, LSub),
                  append(Sub, LSub,Subst).
    4. Essai

      | ?- rob1(X), rob2(Y), unif(X,Y, S),
      |    appsub(S,X, NX), appsub(S, Y, NY), NX=NY.

      X = p(a,f(g(b)),f(a))
      Y = p(h(b,c),f(c),f(h(u,v)))
      S = [[a,h(b,c)],[c,g(b)],[b,u],[v,g(u)]]
      NX = p(h(u,g(u)),f(g(u)),f(h(u,g(u))))
      NY = p(h(u,g(u)),f(g(u)),f(h(u,g(u))))

      | ?-

α-conversion


Le prédicat d'appel

prolog(LButs, LRef) :- resoudre(LButs, LRef, LRef, Subst),
    liste-var(LButs, LVar), sort(LVar, SLVar),
    lappsub(Subst, SLVar, SLVal),
    display(SLVar, SLVal).

liste-var(Terme, [Terme]) :- isvar(Terme), !. /* sans duplication */
liste-var(Terme, []) :- atomic(Terme), !.
liste-var(Terme, LV) :- Terme=..[Fonc|LArgs], lliste-var(LArgs, LV).

lliste-var([], []).
lliste-var([T|S], LV) :- liste-var(T, LT), lliste-var(S, LS),
             add(LT, LS, LV). /* evite les duplications */
add([], X, X).
add([A|S], X, Y) :- present(A, X), !, add(S, X, Y).
add([A|S], X, [A|Y]) :-  add(S, X, Y).

present(A, [B|S]):- A=B, !.
present(A, [_|S]):- present(A, S).

display([], []) :- write('OK !'), nl. /* pour voir les jeux de valeurs */
display([Var|SVar], [Val|SVal]) :- write(Var), write(' = '), write(Val),
                    nl, display(SVar, SVal).

Essais

/* Exemples de programmes pour Quasi-Prolog */

base1([
    [pere(jules, cesar)], [mere(silvia, cesar)],
    [pere(cesar,adrienne)], [mere(lea,adrienne)],
    [pere(cesar,marc)], [mere(lea,marc)],
    [pere(marc, antoine)], [mere(enza, antoine)],
    [pere(marc, paul)], [mere(enza, paul)],

    [parents(x,y,z), pere(x,z), mere(y,z)],

    [gdparents(x,y,z), pere(u,z), parents(x,y,u)],
    [gdparents(x,y,z), mere(u,z), parents(x,y,u)],

    [gdpere(x, y), pere(x, z), pere(z, y)],
    [gdmere(x, y), mere(x, z), pere(z, y)],
    [gdmere(x, y), mere(x, z), mere(z, y)],
    [gdpere(x, y), pere(x, z), pere(z, y)],

    [ancetre(x,x)],
    [ancetre(x,y), pere(x,z), ancetre(z,y)],
    [ancetre(x,y), mere(x,z), ancetre(z,y)]
]).

base2([
    [entier(o)], [entier(succ(x)), entier(x)],

    [add(o, x, x)], [add(x, o, x)],
    [add(succ(a), succ(b), succ(succ(x))), add(a,b,x)]
]).

/* Les predicats d'appel */

plg1(B) :- base1(R), prolog(B, R), fail.
plg2(B) :- base2(R), prolog(B, R), fail.

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

| ?-  plg1([pere(cesar, x), mere(lea, x)]).
x = adrienne
OK !
x = marc
OK !
false

| ?- plg1([ancetre(x, paul), mere(x, y)]).

x = silvia
y = cesar
OK !
x = lea
y = adrienne
OK !
x = lea
y = marc
OK !
x = enza
y = antoine
OK !
x = enza
y = paul
OK !
false

| ?- plg2([entier(succ(succ(succ(o))))]).
OK !
false

| ?- plg2([entier(suc(0))]).
false

| ?- plg2([add(x, y, succ(succ(o)))]).
x = o
y = succ(succ(o))
OK !
x = succ(succ(o))
y = o
OK !
x = succ(o)
y = succ(o)
OK !
x = succ(o)
y = succ(o)
OK !
false
| ?-