NarrowVision
NarrowVision

Reputation: 118

SLD resolution tree, Which predicate applies to give first re-solvent

I was thinking I can solve SLD trees till I found this question in past papers.

Which predicate will be picked for the first time?

I assume it is the third rule, but could someone explain to me how to approach this question, by simply showing a procedure of solving swap([1,2], U)

How do we unify ([S,H|U]) with U?

EDIT Assuming I tried to unify:

swap([H,S|T], [S,H|U]) with swap([1,2], U)

[H,S|T] = [1,2], [S,H|U] = U
H = 1, S = 2, T = [], [S,H|U] = U
H = 1, S = 2, T = [], [2,1|U] = U
H = 1, S = 2, T = [], U = [2,1|U]

and I end up with swap([], U']) but how does this unify with 3 given facts/rules in order to result in U = [2,1]

Logic Program Question

Upvotes: 1

Views: 766

Answers (2)

Will Ness
Will Ness

Reputation: 71065

When selecting a predicate's clause from the knowledge base you're supposed to rename its variables, consistently, so that they are all "fresh", i.e. new, i.e. no new name in the selected clause was yet seen in the process. For instance,

solving:  swap([1,2], U).
selecting: 
          -> swap([], []).   
             <- doesn't match
          -> swap([H0], [H0]).
             <- doesn't match
          -> swap([H1,S1|T1], [S1,H1|U1]) :- swap( T1, U1).
             = matches, with
               { [H1,S1|T1] = [1,2]
               , [S1,H1|U1] = U }
               i.e.
               { H1 = 1, S1 = 2, T1 = [], U = [2,1|U1] }
             -> now solve the body
                swap( T1, U1)
                i.e.
                swap( [], U1) 
                ->
          ........

To finish up the example you have to solve swap( [], U1) by the same procedure as in this answer, selecting each of the three clauses of the predicate swap/2:

  1. swap([], []). (does it match swap( [], U1)?)
    • yes, it does, unifying U1 = []. this is then used in the unification for U, i.e.
      U = [S1,H1|U1] = [2,1|U1] = [2,1|[]] = [2,1].
  2. swap([H2],[H2]). (does it match swap( [], U1)?)
  3. etc.

If course you could rename the vars as anything, like swap([A99],[A99])., as long as the renaming is consistent (i.e. rename a variable only once, and use the new name in place of the old one, consistently).

Upvotes: 4

Pierre Carbonnelle
Pierre Carbonnelle

Reputation: 2615

([S,H|U]) and U are not supposed to share the variable U. Before applying a rule, you have to 'freshen' its variables, e.g. by adding an underscore or prime. You would then unify ([S',H'|U']) and U.

Upvotes: 1

Related Questions