Module Datalogl.Make

Functor building a Datalog implementation for the given constant type.

Parameters

Signature

type constant = Constant.t

Constant type see Datalogl.CONSTANT.

Datalog Expressions

module Variable : sig ... end

A Datalog variable is a placeholder for arbirtary constants.

module Term : sig ... end

A Datalog term is either a Variable.t or a constant.

module Atom : sig ... end

A Datalog atom is a predicate symbol with a list of terms of type Term.t.

module Literal : sig ... end

A literal is a positive or negative Atom.t.

module Clause : sig ... end

A clause are expressions that allow us to deduce facts from other facts.

Datalog Program

module Program : sig ... end

A Datalog program is a set of clauses (Clause.t).

Database

module Tuple : sig ... end
module Database : sig ... end

Evaluation

type query = Atom.t
val query : database:Database.t -> program:Program.t -> query -> Tuple.Set.t Lwt.t

Incremental Evaulation

The state of a Datalog evaluation can be reused for multiple queries or for re-querying the database after new tuples have been added. When reusing the state a considerably smaller amount of work is necessary.

type state

State of a Datalog evaluation.

val init : Program.t -> state

init program Returns the initial state for evaluations with the Datalog program program.

val query_with_state : database:Database.t -> state:state -> query -> (state * Tuple.Set.t) Lwt.t

query_with_state ~database ~state query returns the set of answer tuples for query (see also query) as well as the updated state.

The set of answer tuples for a query is monotonically increasing with the updated state.

The database must also be monotonically increasing (tuples can not be deleted from the database). When new tuples are added to the database, they will be considered for answers to the query. But if tuples are removed from the databse the returned answer might contain tuples that are no longer valid with respect to the program and database.