Expand description

An alternative solver based around the SLG algorithm, which implements the well-formed semantics. For an overview of how the solver works, see The On-Demand SLG Solver in the chalk book.

This algorithm is very closed based on the description found in the following paper, which I will refer to in the comments as EWFS:

Efficient Top-Down Computation of Queries Under the Well-founded Semantics (Chen, Swift, and Warren; Journal of Logic Programming ’95)

However, to understand that paper, I would recommend first starting with the following paper, which I will refer to in the comments as NFTD:

A New Formulation of Tabled resolution With Delay (Swift; EPIA ’99)

In addition, I incorporated extensions from the following papers, which I will refer to as SA and RR respectively, that describes how to do introduce approximation when processing subgoals and so forth:

Terminating Evaluation of Logic Programs with Finite Three-Valued Models Riguzzi and Swift; ACM Transactions on Computational Logic 2013 (Introduces “subgoal abstraction”, hence the name SA)

Radial Restraint Grosof and Swift; 2013

Another useful paper that gives a kind of high-level overview of concepts at play is the following, which I will refer to as XSB:

XSB: Extending Prolog with Tabled Logic Programming (Swift and Warren; Theory and Practice of Logic Programming ’10)

While this code is adapted from the algorithms described in those papers, it is not the same. For one thing, the approaches there had to be extended to our context, and in particular to coping with hereditary harrop predicates and our version of unification (which produces subgoals). I believe those to be largely faithful extensions. However, there are some other places where I intentionally diverged from the semantics as described in the papers – e.g. by more aggressively approximating – which I marked them with a comment DIVERGENCE. Those places may want to be evaluated in the future.

Glossary of other terms:

  • WAM: Warren abstract machine, an efficient way to evaluate Prolog programs. See http://wambook.sourceforge.net/.
  • HH: Hereditary harrop predicates. What Chalk deals in. Popularized by Lambda Prolog.

Modules

Defines traits used to embed the chalk-engine in another crate.

derived 🔒
logic 🔒
simplify 🔒
stack 🔒
strand 🔒
table 🔒
tables 🔒

Macros

Structs

An “answer” in the on-demand solver corresponds to a fully solved goal for a particular table (modulo delayed literals). It contains a substitution

The paper describes these as A :- D | G.

A “floundered” subgoal is one that contains unbound existential variables for which it cannot produce a value. The classic example of floundering is a negative subgoal:

Minimums 🔒

The Minimums structure is used to track the dependencies between some item E on the evaluation stack. In particular, it tracks cases where the success of E depends (or may depend) on items deeper in the stack than E (i.e., with lower DFNs).

The “time stamp” is a simple clock that gets incremented each time we encounter a positive answer in processing a particular strand. This is used as an optimization to help us figure out when we may have changed inference variables.

Enums

AnswerMode 🔒

Either A or ~A, where A is a Env |- Goal.