[−][src]Module razor_chase::chase

Provides a framework and interfaces to various components that are used for implementing the Chase. It also implements entrypoints for running the Chase.

Background

Razor implements a variant of the Chase algorithm to construct models for first-order theories with equality. The Chase operates on geometric theories, theories that contain a syntactic variation of first-order formulae which we refer to as the Geometric Normal Form (GNF). Formulae in GNF have the following shape:

A₁ ∧ ... ∧ A_m → (∃ x₁₁, ..., x_1j₁ . A₁₁ ∧ ... ∧ A_1n₁)

    ∨ (∃ x₂₁, ..., x_2j₂ . A₂₁ ∧ ... ∧ A_2n₂)
    ∨ ...
    ∨ (∃ x_i1, ..., x_{ij_i} . A_i1 ∧ ... ∧ A_{in_i})

where A_ks are (positive) atomic formulae (possibly including equality) and free variables are assumed to be universally qualified over the entire formula.

In the context of a run of the Chase, we refer to formulae in the their GNF as sequents. The premise (left side) and the consequence (right side) of the implication are respectively said to be the body and the head of the sequent.

Satisfiability of Geometric Theories

It turns out that every first-order theory can be transformed to a geometric theory that is equisatisfiable to the original theory via standard syntactic manipulation. In fact, for every model N of the original theory, there exists a model M of the geometric theory such that there is a homomorphism from M to N. This is an important result that enables Razor to utilize the Chase to construct homomorphically minimal models of a given first-order theory.

In the context of a model-finding application, the models that the Chase produces are desirable since they contain minimum amount of information, thus they induce minimal distraction. As a direct consequence of semi-decidability of satisfiability in first-order logic (see Gödel's incompleteness theorems), satisfiability of geometric theories is semi-decidable as well.

Note: A comprehensive discussion on the properties of the models that are constructed by the Chase is out of the scope of this document.

The Chase

Given a geometric theory and starting with an empty model, a run of Chase consists of repeated applications of chase-steps by which the model is augmented with necessary pieces of information until there is a contradiction or the model satisfies the theory. Within Razor's implementation, instances of any type that implements ModelTrait can serve as a first-order model. Also, inspired by Steven Vickers, we refer to the units of information that augment models as observations.

Chase Step

Given a geometric theory and an existing model, a chase-step proceeds as follows:

A sequent from the theory is selected to be evaluated against the model. Razor uses an instance of StrategyTrait to select the sequent.
The selected sequent is evaluated against the model: given an assignment from the free variables of the sequent to the elements of the model, if the body of the sequent is true and its head is not true in the model, new observations are added to the model to make the sequent's head true. Instances of any type that implements EvaluatorTrait may be used to evaluate the sequent in the model.

2.1. If the sequent is headless, meaning its consequence is falsehood (an empty disjunction), the Chase fails on the given model.

2.2. If the head of the sequent contains more than one disjunct (with at least one non-trivial disjunction), the Chase branches and satisfies each disjunct independently on clones of the model. Razor uses instances of SchedulerTrait to schedule various branches of the Chase for future Chase steps.

2.3. If no sequent can be found such that its body and head are respectively true and false in the model, the model already satisfies the theory and will be returned as an output of the Chase.

Termination

As a result of semi-decidability of geometric theories, it can be shown if a geometric theory is unsatisfiable, a run of the Chase on the theory always terminates, although it may take a very very long time. However, when the theory is satisfiable, a run of the Chase may not terminate, producing infinitely large models and/or infinitely many models that satisfy the theory. Nevertheless, in practice, Razor can bound the size of models created by the Chase to guarantee termination. Razor uses instances of types that implement BounderTrait to implement various strategies to cap the size of search space for models.

Implementation

The primary motivation for implementing Razor is to study the Chase and improve its performance for practical applications. The flexible (but somehow complex) design of Razor allows for experimenting with various data structures to represent models and sequents, evaluating sequents in models using a variety of algorithms, testing different ideas for scheduling branches of the Chase and devising various strategies for selecting sequents. Also, because of theoretical and non-theoretical consequences of non-termination of the Chase, Razor is going to explore a variety of ideas for limiting the search space by bounding the size of models:

Interesting combinations of these various options are constantly benchmarked and the configuration with the best average performance is used by the Rusty Razor application.

Modules

bounder	Implements various bounders for bounding the size of models, generated by the Chase.
impl	Contains all implementations of models, sequents and evaluators.
scheduler	Implements various schedulers for scheduling branches of the Chase.
strategy	Implements various strategies for selecting sequents in a chase-step.

Structs

E	Is a symbol to represent elements of first-order models. An element is identified by an index.
EvaluateResult	Is result of evaluating a model in a chase-step.
Rel	Relations are semantic counterparts of predicates and are used to store `Fact`s in models.

Enums

Observation

Represents positive units of information by which Models are constructed. Once a Model is augmented by an observation, the observation remains true in the model.

Traits

BounderTrait	Bounder is the trait of algorithms for bounding the size of models generated by the Chase.
EvaluatorTrait	Is the trait of algorithms that evaluate an implementation of SequentTrait in an implementation of ModelTrait within a chase-step.
ModelTrait	Is the trait for various implementations of first-order models that are constructed by the Chase.
SchedulerTrait	Is the trait of algorithms for scheduling various branches of the Chase. A branch of the Chase is represented with a model together with a strategy for scheduling sequents to be evaluated in the model.
SequentTrait	Is the trait for types that represents a geometric sequent in the context of an implementation of the Chase.
StrategyTrait	Strategy is the trait of algorithms for choosing sequents in the context of an implementation of the Chase. Strategy instances provide the next sequent to be evaluated by the Chase.
WitnessTermTrait	Is the trait for special kind of variable-free terms that are used to witness existence of model elements. These terms are used as provenance information for models to describe why elements exist or facts are true in models.

Functions

chase_all	Given a `scheduler`, an `evaluator` and possibly a `bounder`, runs an implementation independent run of the Chase and returns all resulting models. The return value is empty if the theory is not satisfiable.
chase_step	Given a `scheduler`, an `evaluator`, possibly a `bounder` and a `consumer` closure, runs an implementation independent chase-step. Satisfying models of the theory that are produced by the `chase-step` will be consumed by the `consumer`. In contrast, `incomplete_consumer` (if provided) consumes incomplete non-models of the theory that are rejected by the bounder.