🚀 go-pugleaf

[Disclaimer:  No, I didn't prompt Feng Yang to post the question! :-)]

In article <1990Nov5.182613.1571@watserv1.waterloo.edu> yfeng@watnow.waterloo.edu (Feng Yang) writes:
>(1) Why does prolog use depth-first, left-to-right search ?  

     There seem to be a few reasons.

o The efficiency considerations you mention.  A breadth-first
  algorithm seems, for many problems, to take up too much extra
  space, and extra time spent switching from goal to goal.

o Depth-first interpreters can be easier to write and make
  efficient.

o Depth-first, left-to-right search has a relatively simple
  execution model which is relatively easy for programmers to
  use when debugging programs.  Debugging a program on a
  breadth-first system seems to involve keeping track of more
  information at one time.

o Another debugging consideration is that with a breadth-first
  interpreter, changes in processor load and/or minor changes
  in the program may affect the order in which solutions are
  returned.  This can be very confusing for debugging purposes.

o The Prolog strategy seems to be "not incomplete enough" for
  many problems to warrant switching to breadth-first.  There
  are certainly examples (such as you give) and problem domains
  in which parallel interpreters are desirable, but these seem
  to be in the minority.

>(2). I would like to know any work on proving two prolog program
>eqivalent (or not), or one program is subset of another.

     You could look at my paper in NACLP'90, "The Logical
Structure of Sequential Prolog".  This gives proof systems for
proving some properties of logic programs.  I don't think those
systems would be very useful for proving equivalences between
programs, but the sequent calculus version of it (forthcoming)
might be.

--
--Jamie.		Original material copyright (c) 1990 by Jamie Andrews;
  jha@lfcs.ed.ac.uk	for distribution only on unmoderated USENET newsgroups.
       "Autumn, to me the most congenial of seasons; the university,
        to me the most congenial of lives"  --Robertson Davies