Information Technology Reference
In-Depth Information
(2) p(a).
Let “?-p(Y)” be the goal. Then it is obvious that the SLD resolution process will
fall into an endless loop. However, if we exchange the order of clause (1) and
clause (2), then we will get the result Y=a, Y=f(a), ….
Consider another program:
(1) q(f(X)) :- q(X).
(2) q(a).
(3) r(a).
Let “G: ?-q(Y), r(Y)” be the goal. Then the SLD resolution process will fall into
an endless loop. However, if we exchange the order of sub-goals contained in G
and get the goal “G: ?- r(Y),q(Y)”, then we will get the result Y=a after the SLD
resolution process.
In order to guarantee the completeness of the SLD resolution process, the
width-first search strategy must be embodied in search rules of Prolog. Howerev,
as a result, both the time and space efficiency of the process will be decreased, as
while as the complexity of the process is increased. A trade-off is to maintain the
depth-first seach strategy that is used in Prolog, and supplement it with some
programs which embody other search strategies and are written with the Prolog
language.
3. Soundness of SLD resolution is not guaranteed without occur-check.
Occur-check is a time-consuming operation in the unification algorithm. In the
case that occur-check is called, the time needed for every unification process is
linear to the size of the table, consequently the time needed for the append
operation on predications is O(n 2 ); here n is the length of the table. Since little
unification process in the Prolog program use occur-check, the occur-check
operator is omitted form unification algorithms of most Prolog systems.
In fact, without the occur check we no longer have soundness of SLD
resolution. A sub-goal might can not be unified with a clause in the case that
some variables occurring in the term. However, since the occur-check is omitted,
the unification will still be executed and reach a wrong result. For example, let
“p(Y, f(Y))” and “?-p(X, X)” be the program and the goal respectively. Then the
unification algorithm will generate a replacement θ={Y/Xf(Y)/Y} for the pair
Search WWH ::




Custom Search