[][src]Crate chalk_engine

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 rustc guide.

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-formed 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 dieverged 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:

Modules

context

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

derived
fallible
forest
hh
logic
simplify
stack
strand
table
tables

Structs

DelayedLiteralSet

A set of delayed literals.

DelayedLiteralSets
DepthFirstNumber

The DepthFirstNumber (DFN) is a sequential number assigned to each goal when it is first encountered. The naming (taken from EWFS) refers to the idea that this number tracks the index of when we encounter the goal during a depth-first traversal of the proof tree.

ExClause

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

FlounderedSubgoal

A "floundered" subgoal is one that contains unbound existential variables for which it cannot produce a value. The classic example of flounding 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).

SimplifiedAnswer
SimplifiedAnswers
StackIndex
TableIndex
TimeStamp

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

DelayedLiteral
InnerDelayedLiteralSets
Literal

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

Functions

maybe_grow_stack

Because we recurse so deeply, we rely on stacker to avoid overflowing the stack.