The Implementation of Fair Search Rules

Appeared in Volume 7/1, February 1994

Keywords: implementation.

renm@dcs.ed.ac.uk
Renaud Marlet
16th November 1993

A little while ago, I asked for some references on the implementation of fair search rules and WAM-like abstract machines for complete Horn solvers. I also wondered how these things could be related to goal freezing. Here is a summary of the replies and references that I received. Thanks to everybody that replied.

Iterative deepening

[1] discusses some extensions of Prolog, including a "staged depth-first search strategy", which is given a quantitative analysis. The same idea is named "depth-first iterative-deepening" in [2, 3, 4], which have a more Artificial Intelligence flavour, and some quantitative analysis. Roughly, iterative-deepening uses a linear space whereas breadth-first search is exponential; time loss is only a factor b/b-1 where b is the average branching factor.

Computation rule and search rule

Lee Naish (lee@munta.cs.mu.oz.au): The reason no one has a fast implementation is that different computation rules lead to SLD trees of vastly different sizes and finding good fair computation rules is very hard. Take a look at [5]. Note: when/wait/freeze are irrelevant to the search rule.

Or-parallel Prolog

Jacques Chassin de Kergommeaux (chassin@mistral.imag.fr): OR-parallel Prolog systems mix depth-first and breadth-first search. Several OR-parallel Prolog implementations are based on the WAM (see Muse, Aurora, PEPSys, etc.).

Goal freezing

Micha Meier (micha@ecrc.de): If you have an expressive delay system, then, given a program, you can enhance it with delay conditions so that it is fair. But generally this is undecidable.

Frederic Mesnard (fred@iremia.fr): In [6], I show how it is possible to automatically generate freeze declaration from the text of the programs to ensure (depth-first) termination of CLP programs.

Implementation

Micha Meier (micha@ecrc.de): ECLiPSe has an optional DFID (depth-first iterative deepening) search. You can load a library which changes the mode of the compiler so as to generate code that can be executed using DFID. The changes for the WAM were minimal, I think one or two additional instructions to manipulate the depth were necessary.

Since it also has an optional occur check mode, ECLiPSe in fact gives you a complete Horn solver. ECLiPSe documentations can be obtained from:
ftp://ftp.ecrc.de/pub/eclipse/doc

References

1. Stickel, M.E., A Prolog technology theorem prover, New Generation Computing, 1984, No. 2, pp.371-83

2. Richard E. Korf, Iterative-Deepening-A*: An Optimal Admissible Tree Search, Proc. of the Ninth IJCAI, pp.1034-1036, Los Angeles, California, August, 1985

3. Richard E. Korf, Depth-First Iterative-Deepening: An Optimal Admissible Tree Search, Artificial Intelligence, pp.97-109, 1985, Vol.27

4. Mark E. Stickel and W. Mabry Tyson, An Analysis of Consecutively Bounded Depth-First Search with Applications in Automated Deduction, Proc. of the Ninth IJCAI pp.1073-1075, Los Angeles, California, August, 1985

5. Lee Naish, Negation and control in Prolog, LNCS 238, Springer-Verlag, New York, 1986

6. Termination of Constraint Logic Programs, by Means of Approximations, Fred Mesnard, Ph.D. thesis, Universite Paris VI, 1993, January, Written in french.

Abstract:

We first present a class of mappings, called approximations, between constraint LP languages, which allow us to focus on the images Pb in CLP(Bool), and Pq in CLP(Q), of an initial program P.

We study Pb in order to get some knowledge about the state of the variables of a goal once it has been proved.

From Pq, and with the help of a technique due to Sohn and Van Gelder, we bring to light linear terms decreasing at each recursive call.

Then we show how :

we can transform the program P into a logically equivalent program P' that uses freeze declarations to impose a terminating selection rule and;
we can compute, for each predicate p of P, a constraint Cp such that all constraint atoms satisfying Cp will terminate under the standard left-to-right computation rule.

Also thanks to:

Michael Jampel (jampel@cs.city.ac.uk)
Alan Smaill (smaill@dcs.ed.ac.uk)
Jens E Wunderwald (wunderwa@hpradig9.informatik.tu-muenchen.de)

renm@dcs.ed.ac.uk
Renaud Marlet
20th December 1993

I haven't received any more comments since I posted the summary. I successfully used the ECLiPSe system (which is very good), but I didn't find any references in the documentation to the additional WAM instructions that manipulate the depth. However, the als/1 predicate of ECLiPSe prints out an almost readable WAM listing of the generated code, and thus gives some hints about the DFID compilation.