Crate datalog_structural_model 

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.

Serialization and checked loading

All public semantic data supports Serde directly, including symbols, nested terms, expressions, aggregates, rules, programs, profiles and diagnostics. JSON and Postcard are exercised; the model does not use a JSON intermediate. Symbols serialize as exact text. Cached hashes and allocation identity are rebuilt through the symbol constructors and never appear in serialized data.

Program::try_new and Rule::try_new validate checked construction. Their Serde inputs use those same paths: unsafe variables, invalid Skolem placement, excessive term nesting and cycles through negation fail on input. Standalone Term and GroundTerm decoding checks context-free structure; rule position and variable binding still require program validation. Raw public fields remain available for authoring invalid source descriptions and reporting their errors; those descriptions cannot bypass checked loading into executable programs. Unknown semantic fields and enum variants are rejected.

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

let atom = Atom {
    predicate: PredicateSymbol::new("person"),
    terms: vec![Term::Constant(ConstantSymbol::new("alice"))],
};
let program = Program::try_new(vec![Rule::positive(atom, vec![])])?;
let profile = DatalogProfile::positive();
program.validate_for(&profile)?;
let bytes = postcard::to_allocvec(&program)?;
let loaded: Program = postcard::from_bytes(&bytes)?;
loaded.validate_for(&profile)?;
assert_eq!(program, loaded);

Stratification results serialize as reports. Recompute stratification from the validated program when scheduling execution; loading a report does not certify an executable plan. Serde encodings are neither canonical hashes nor RDF concrete syntaxes. Callers own decoding resource budgets; this crate owns structural and program-safety validation. The supported triple-term nesting depth remains MAX_TRIPLE_TERM_NESTING.

Explicit Datalog language profiles

DatalogProfile::positive() describes positive flat Datalog without extension operators. DatalogProfile::stratified() adds stratified negation. Custom profiles pair an explicit DatalogCapabilities set with an equality validation regime.

Program::required_capabilities() inspects the entire program, including nested bindings, filters, triple terms, Skolem terms and aggregate inner bodies. Filter, binding and aggregate requirements identify exact operations, rather than broad “supports expressions” flags. Program::validate_for rejects unsupported features with a typed missing-capability set, and retains the existing rejection of negation/aggregation under equality rewriting.

A capability declaration describes a contract, not proof of engine support. DatalogCapabilities::all_model_features() lists what the IR can represent; an engine must independently declare and test what it implements. Forward and backward execution remain separate from the language profile.

RDFS, OWL 2 RL/RDF, Horst and vendor-compatible entailment presets belong in RDF reasoning rule packages. They can consume this model without adding OWL or backend dependencies to the generic Datalog layer. This crate does not yet provide those RDF rules or enable new inference modes in Python packages.

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.

DatalogCapabilities

Language feature set. This describes a contract; it does not certify an engine.

DatalogProfile

Explicit language features and equality regime selected for a program. This is neither an RDF entailment profile nor an execution strategy.

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.

UnsupportedCapabilities

Features required by the program and absent from the selected profile.

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.

BindingKind

An operation represented by BindExpr, independent of evaluator support.

BuiltinFilter

Built-in filter expression.

DatalogFeature

A language feature required by a rule program. Positive flat atoms require no extension capabilities.

EqualityMode

Equality-reasoning mode under which a Datalog program is validated.

FilterKind

An operation represented by BuiltinFilter, independent of evaluator support.

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.

ProfileCheckError

An invalid program or an explicitly unsupported language feature.

ProgramValidationError

Program validation failures.

StratificationError

Stratification failure.

Term

Datalog term (variable, constant, quoted-triple term, or SKOLEM(name, args...) function call).

TermShapeError

Invalid term structure, independent of variable binding or rule position.

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.