restivo@POLYA.STANFORD.EDU (Chuck Restivo) (07/19/88)
Date: Tue 19 Jul 1988 02:53-PST
From: Chuck Restivo (The Moderator) <PROLOG-REQUEST@POLYA.STANFORD.EDU>
Reply-to: PROLOG@POLYA.STANFORD.EDU>
US-Mail: P.O. Box 4584, Stanford CA 94305
Subject: PROLOG Digest V6 #51
To: PROLOG@POLYA.STANFORD.EDU
PROLOG Digest Tuesday, 19 July 1988 Volume 6 : Issue 51
Today's Topics:
Implementation - Style & Unification
--------------------------------------------------------------------------------------------------------------------------
Date: 17 Jul 88 04:32:41 GMT
From: rochester!daemon@cu-arpa.cs.cornell.edu
Subject: Need style advice
Summary: More information about intended behavior
References: <1988Jul14.231619.22145@cs.rochester.edu>, <170@quintus.UUCP>
> Richard O'Keefe responds to my query with:
> Note that the code as written is not steadfast:
> ?- foo_value(X, value_3).
> will succeed for ANY value of X, even when forced_to_be_1(X).
> Remember: a cut at the end of a clause is almost always in the wrong place.
Ok, that's the first problem. My intent is to use the
value in the head of the first satisfied clause, using value_3 only
when no previous clause can be satisfied.
Your reminder is appreciated, but it would be more useful if I were
also made acquainted with how things *should* be done.
> Would it be possible for you to tell us what the relation is supposed to
> _mean_, rather than showing us the current version of the code?
Yes, my apologies if this description includes irrelevant detail. I
have a graph with two colors of arcs, and two kinds of colors of
nodes. foo_value/2 is to give values to nodes based on graph
connectivity and coloring.
The first kind node color distinguishes between "forced_to_be_1" and
otherwise. If a node is forced_to_be_1, it receives value_1, otherwise
we consider its neighbors. We look, first, for neighbors from whom X
can inherit value_2. If no such neighbors can be found, we look for
neighbors from whom to inherit value_1. If we fond no neighbors from
whom value_2 or value_1 can be inherited, we give X the value_3.
This is what I intended to express through the ordering of clauses.
(1) Is the decision forced, (2) Can we find a value_2, (3) Can
we find a value_1, (4) In all other cases, value_3.
There are two ways for X to inherit a value from a neighbor, and that
is what the pairs of clauses (2&3 and 4&5) were intended to express.
relation_one(X, Y) is satisfied when node X is connected to node Y by
an arc of the first color, and node Y has a particular value of the
second kind of node color. X receives a value based directly on
the first kind of node coloring of Y.
relation_two(X, Y) is satisfied when node X is connected to a node _
by an arc of the first color, and node _ is connected to node Y by
an arc of the second color. (The second kind of node coloring is
irrelevant in this case.) X receives the same value that Y receives.
> For example, the following values for forced_to_be_1/1 and relation_one/2
> [ some clauses deleted ]
> appears to satisfy the description given, yet both
> relation_one(tom, mary), \+forced_to_be_1(mary)
> and relation_one(tom, jim), forced_to_be_1(jim)
> are true, so should foo_value(tom, value_2) or foo_value(tom, value_1)?
foo_value(tom, value_2). My intent is to try the four steps I gave
above, stopping the first time a step succeeds. I suppose I should stress
that I want foo_value to succeed exactly *once* in all cases.
> Presumably there is some finite number of Xs which you intend to assign
> foo_values to. If that number is not too big, why not just write a
> program to generate the table and write the results to a file, then
> compile that file?
Well, if there were only one graph of interest, I'd do that, but this
*is* a (evidently incorrect) program to generate the table! (Actually,
it's my attempt to express more-or-less declaratively what a C program
is busy doing on a dynamically changing graph structure, but you get
the idea.)
****************
Clearly, I have not gone about things the right way. My suspicions
that things could be improved motivated my query in the first place.
I frankly hadn't noticed the "steadfast"ness bug. So, what is the
recommended form for simple decision trees in Prolog? How do I
obtain the intended behavior?
Unless I receive strong urging to the contrary, I would like to *avoid*
rewriting the clause bodies to something like the following:
foo_value(X, a) :- pred_a(X).
foo_value(X, b) :- \+pred_a(X), pred_b(X).
foo_value(X, c) :- \+pred_a(X), \+pred_b(X), pred_c(X).
foo_value(X, d) :- \+pred_a(X), \+pred_b(X), \+pred_c(X).
This is "pure", but I find it harder to read and understand. I suspect
that it's also considerably less efficient. If not so, please urge otherwise.
-------------------------------
Date: Sun, 17 Jul 88 14:33:46 BST
From: Fernando Pereira <pereira%cam.sri.com@ai.sri.com>
Subject: Unification Algorithms
> John Lloyd, in "Foundations of Logic Programming" 2nd extended edition, gives
> 3 references for linear time/space unification algorithms with the
> occur check.
> I haven't studied any of them, and Lloyd says that none of them are used
> in PROLOG systems (surely there must be one somewhere that uses one of these
> algorithms). He doesn't say why they aren't used, perhaps the basic
> multiplier for their expense is too high, even though they are linear
> in complexity.
The reason why most (if not all) Prolog systems do not use any of
these algorithms but rather the Robinson algorithm with the occurs
check removed (RWOC) is not ignorance on the part of the implementers,
but the fact that the algorithms are linear on the _sum_ of the sizes
of the two terms being unified. If this seems modest, consider the
execution of
append([], L, L).
append([X|L1], L2, [X|L3]) :- append(L1, L2, L3).
with the first argument instantiated to a list of length N. If one of
the algorithms in question is being used for all unifications, then
the execution time will be O(N^2), while it is just O(N) in a normal
Prolog system. In addition to this problem, the cost per basic
unification step in those algorithms is higher than that in the RWOC
algorithm, both because of the more complex data structures used and
the larger amount of information that has to be saved ("trailed") for
backtracking. In the original design of Prolog as a _programming_
_language_ based on Horn-clause logic, it was (correctly) believed
that the potential unsoundness and non-termination caused by the
choice of "unification" algorithm was a lesser evil than using a sound
and always terminating algorithm that made the language unpractical
compared with, say, Lisp -- the obvious counterpart of append/3 in
Lisp is clearly O(N).
Now, it would be nice to have a sound and terminating algorithm and
still maintain the practical efficiency of unification. It would also
be nice to avoid the exponential worst-case performance of the RWOC
algorithm in problems like
exp(N) :- reentrant_term(N,T1), reentrant_term(N,T2), T1 = T2.
reentrant_term(0, 0).
reentrant_term(s(N), f(T,T)) :-
reentrant_term(N, T).
The problem here is that the textually the term corresponds to the
full binary tree of height N, with size O(2^N), but it only contains
O(N) distinct subterms. Unfortunately, the RWOC algorithm knows
nothing about shared subterms and spends O(2^N) time unifying T1 with
T2, when O(N) would be sufficient.
The above problems have been attacked in two distinct ways. The first,
more widely available (Prolog-II, SICStus Prolog and probably others),
is based on changing the universe of terms so that the circular
structures created by an algorithm without occurs check are allowed.
This may appear a dirty trick, but in fact work by Colmerauer, van
Emden, Jaffar and others shows that it can be given a reasonable
logical interpretation, in which programs are interpreted not as usual
over the Herbrand universe but rather over a domain of _rational
graphs_, defined by a particular equational theory. However, although
the RWOC algorithm can build such creatures, it may loop if given
them, eg. try
?- X = f(X,X), Y = f(Y, Y), X = Y.
in C-Prolog, Quintus Prolog, and probably most other current Prolog
systems. Instead, what is needed is an algorithm that recognizes when
it is trying to unify a pair of subterms it tried to unify before and
just skip that pair. Various techniques have been proposed for this,
mostly refinements, variations or reinventions of the worst-case
O(N^2) algorithm presented by Fages in his dissertation. The best
algorithm I know for this purpose is the obvious adaptation of the
UNION-FIND algorithm for FSA equivalence (consult standard textbooks
for this), but it has the problem that a lot of information may have
to be saved for restoring terms on backtracking.
The other alternative is to stick to the usual theory of terms, bring
in the occurs check, but recognize situations in which the full
algorithm is not needed, eg. when unifying the first occurrence of a
variable in the head against the corresponding argument. Ideas of this
nature have been pursued by various people, eg. David Plaisted, but I
don't know of the latest results on its practical application. It
clearly seems a good idea for clausal theorem provers based on Prolog
technology (eg. Stickel's PTTP and Plaisted's prover distributed on
this digest a couple of years ago), but it is unclear to me whether it
is really practical for Prolog execution, eg. whether it will reduce
the execution of append/3 above to O(N).
I apologize to those people who have worked on this problem but were
not mentioned above (I'm composing this without access to a library),
and I would appreciate any corrections, updates and new references on
the topic.
-- Fernando Pereira
--------------------------------
End Of PROLOG Digest