🚀 go-pugleaf

In article <1989Oct10.170254.9642@cs.rochester.edu:, miller@CS.ROCHESTER.EDU (Brad Miller) writes:
(I wrote)
:     Prolog does *not* find solutions.  Prolog finds **proofs**, and shows you
:     (part of) the substitution it found for each proof.  The goal
: 	    ?- member(a, [a,a,a]).
:     has three proofs.

: On the other hand, it seems perfectly reasonable for a Prolog or any logic
: language implementation to note that in the variable case above, reproving
: the member doesn't change the binding of X and refuse to do it, rather
: simply fail. This is what would happen if "intelligent backtracking" were
: being used. Similarly, in the last example, since no variable can be rebound
: by the current frame, fail should exit the proof immediately after the first
: write.

Reasonable?  I'd be happy for NU Prolog to do something like that because
NU Prolog has the ":- pure" declaration.  In the absence of such a declaration,
it is NOT reasonable for a Prolog system to do that.  (Think: repeat/0 has 
ONE solution but infinitely many proofs; it's used precisely because of the
latter property.)

There's another sense of "reasonable"; intelligent backtracking ranges from
outrageously costly to unpleasantly costly.  There are affordable versions
of intelligent backtracking around, but they become affordable by sacrificing
much of the intelligence.  You can avoid repeated solutions to a goal _this_
simple, but the problem is going to come right back in more complicated
situations.  Another method is to use extension tables (applicable only to
:- pure predicates), which have their own problems.

: I think part of the issue is that Prolog really doesn't find "proofs" in the
: logical sense, rather it does SLD resolution. That is to say, one shouldn't
: confuse Prolog, which is a programming language, with LOGIC which isn't.
: That is, it does not return proof trees. If it did, then techniques like
: intelligent backtracking could not be used, nor could "side effects" be
: allowed (Side effects in the programming language sense).

Miller confuses FINDING proofs with REPORTING them.  Just because Prolog
"does not return proof trees" doesn't mean that it "doesn't find proofs".
As a matter of fact some debugging tools _do_ return proof trees, which
doesn't make them any the less Prolog.  Predicate's such as findall/3
and VM/Prolog's call/2 (at least I think that's what they call it) let
you discover how many proofs were found for a goal; intelligent backtracking
would yield different answers.

As they say in the satellite business, there's no such thing as a free
launch.  Prolog strikes a balance between cost and power; it's fast and
stupid rather than slow and smart.