Crate datalog_structural_model

Expand description

§datalog-structural-model

Typed Datalog rule programs, validation, and stratification analysis.

datalog-structural-model is the finite rule-program layer between a rule authoring or compiler front-end and an evaluator. It models predicates, variables, terms, atoms, rules, filters, bindings, and aggregates, then validates safety and computes predicate strata for programs with negation.

It does not read input data, execute rules, retain a fact store, or collect solutions. Evaluation engines can consume a validated Program while keeping facts and derived results in their own asynchronous, backpressured, and spill-capable data paths.

§A small rule program

use datalog_structural_model::{
    Atom,
    ConstantSymbol,
    Literal,
    PredicateSymbol,
    Program,
    Rule,
    Term,
    VariableSymbol,
};

let person = PredicateSymbol::new("person");
let ancestor = PredicateSymbol::new("ancestor");
let x = VariableSymbol::new("x");
let y = VariableSymbol::new("y");
let z = VariableSymbol::new("z");

let parent_xy = Atom {
    predicate: PredicateSymbol::new("parent"),
    terms: vec![Term::Variable(x.clone()), Term::Variable(y.clone())],
};
let ancestor_yz = Atom {
    predicate: ancestor.clone(),
    terms: vec![Term::Variable(y), Term::Variable(z.clone())],
};
let ancestor_xz = Atom {
    predicate: ancestor,
    terms: vec![Term::Variable(x), Term::Variable(z)],
};

let program = Program {
    rules: vec![Rule::new(
        ancestor_xz,
        vec![Literal::Positive(parent_xy), Literal::Positive(ancestor_yz)],
    )],
};

program.validate().expect("the rule is safe and stratifiable");
assert_eq!(person.as_str(), "person");
assert_eq!(ConstantSymbol::new("example").as_str(), "example");

The rule model is deliberately separate from execution. A caller may build a program in memory because a rule program is a finite description, but the facts matched by that program are not part of this crate and must not be materialized here.

§Validation and stratification

Program::validate checks range restriction, variable safety, supported expression structure, and the absence of cycles through negation. A valid program can be passed to a forward or backward evaluator. Program::stratify exposes the calculated strata when an evaluator needs to schedule them.

The dependency graph uses strongly connected components and preserves the distinction between positive and negative dependencies. A recursive positive cycle is valid; a cycle that contains a negated dependency is rejected.

§Scope

This crate contains rule-program data structures and pure validation only. It does not provide a parser or CST for a Datalog source language, and it does not define an execution runtime. Those are separate layers so that parsers can stream source tokens and evaluators can stream facts and results without turning this IR crate into an in-memory data engine.

§License

Licensed under either of:

Apache License, Version 2.0 (LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0)
MIT license (LICENSE-MIT or https://opensource.org/licenses/MIT)

at your option. Typed Datalog rule programs and stratification analysis.

Structs§

AggregateBody: An aggregation sub-query inside a rule body.
Atom: Datalog atom: predicate(term_1, ..., term_n).
ConstantSymbol: Constant symbol used in Datalog terms.
GroundAtom: Ground form of an Atom — the value form with no variables anywhere in the argument tree. Used inside GroundTerm::TripleTerm so quoted-triple facts can be stored alongside flat facts in a fact set (TT1).
PredicateSymbol: Predicate symbol in a Datalog atom.
Program: Datalog program as an ordered set of rules.
Rule: Datalog rule: head :- body_1, ..., body_n.
Stratification: Stratification of a Datalog¬ program.
Stratum: A single stratum — the set of predicates defined together.
VariableSymbol: Variable symbol used in Datalog terms.

Enums§

Aggregator: SQL/SPARQL aggregator vocabulary supported in rule bodies.
BindExpr: Expression carried by a Literal::Bind body literal.
BuiltinFilter: Built-in filter expression.
EqualityMode: Equality-reasoning mode under which a Datalog program is validated.
GroundTerm: Ground term — the value form of a Term with all variables substituted. Used as the cell type inside tuples so an evaluator can store both flat constant-only facts and quoted-triple facts (TT1).
Literal: Datalog body literal — a positive or negated atom, a built-in filter expression, or a built-in BIND(expr AS ?var) form.
ProgramValidationError: Program validation failures.
StratificationError: Stratification failure.
Term: Datalog term (variable, constant, quoted-triple term, or SKOLEM(name, args...) function call).

Constants§

MAX_TRIPLE_TERM_NESTING: Maximum allowed nesting depth for Term::TripleTerm variants. Programs whose triple-term nesting exceeds this limit are rejected at Program::validate time.