Reputation: 118
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]
Upvotes: 1
Views: 766
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
:
swap([], []).
(does it match swap( [], U1)
?)
U1 = []
.
this is then used in the unification for U
, i.e.U = [S1,H1|U1] = [2,1|U1] = [2,1|[]] = [2,1]
.swap([H2],[H2]).
(does it match swap( [], U1)
?) 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
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