Chase-rs

An implementation of the chase algorithm in Rust for reasoning engines.

Overview

The chase algorithm is a technique in context of database theory and knowledge representation used for:

• Query answering under tuple-generating dependencies (TGDs)
• Computing universal models
• Datalog with existential rules

This implementation provides a restricted-chase style materialization with active-trigger checks. The default entrypoints use a 10_000 step safeguard and report incomplete results with terminated == false if that limit is reached.

Features

• Core Data Types: Terms, Atoms, Rules, and Instances
• Existential Quantification: Automatic generation of labeled nulls
• Restricted Chase Style: Active-trigger checks for existential rules
• Configurable Step Limit: chase_with_config exposes the step bound
• Fluent API: RuleBuilder for readable rule construction
• Interactive Frontends: REPL, script runner, and a local GUI
• Zero Dependencies: Pure Rust with no external runtime dependencies

See ROADMAP.md for the list of implemented and planned features.

Important

This project is still in early development, so bugs and breaking changes are expected. Please use the issues page to report bugs or request features.

---

Quickstart

Example

use chase_rs::{chase, Atom, Instance, Term};
use chase_rs::chase::rule::RuleBuilder;

// Create initial facts
let instance: Instance = vec![
    Atom::new("Parent", vec![Term::constant("alice"), Term::constant("bob")]),
    Atom::new("Parent", vec![Term::constant("bob"), Term::constant("carol")]),
].into_iter().collect();

// Define rules
// Parent(X, Y) -> Ancestor(X, Y)
let rule1 = RuleBuilder::new()
    .when("Parent", vec![Term::var("X"), Term::var("Y")])
    .then("Ancestor", vec![Term::var("X"), Term::var("Y")])
    .build();

// Ancestor(X, Y), Parent(Y, Z) -> Ancestor(X, Z)
let rule2 = RuleBuilder::new()
    .when("Ancestor", vec![Term::var("X"), Term::var("Y")])
    .when("Parent", vec![Term::var("Y"), Term::var("Z")])
    .then("Ancestor", vec![Term::var("X"), Term::var("Z")])
    .build();

// Run the chase
let result = chase(instance, &[rule1, rule2]);

assert!(result.terminated);
println!("Derived {} facts", result.instance.len());

Use chase_with_config to change the default step bound:

use chase_rs::{Atom, ChaseConfig, Instance, Term, chase_with_config};
use chase_rs::chase::rule::RuleBuilder;

let instance: Instance = vec![Atom::new("P", vec![Term::constant("a")])]
    .into_iter()
    .collect();
let rule = RuleBuilder::new()
    .when("P", vec![Term::var("X")])
    .then("Q", vec![Term::var("X")])
    .build();

let result = chase_with_config(
    instance,
    &[rule],
    ChaseConfig { max_steps: 100 },
);

assert!(result.terminated);

Existential Rules

Rules with head-only variables (existential quantification) automatically generate fresh labeled nulls:

// Every person has an SSN: Person(X) -> HasSSN(X, Y)
let rule = RuleBuilder::new()
    .when("Person", vec![Term::var("X")])
    .then("HasSSN", vec![Term::var("X"), Term::var("Y")]) // Y is existential
    .build();

Frontends

The binary now supports three entrypoints:

# Start the interactive REPL
cargo run -- repl

# Start the local GUI at http://127.0.0.1:7878
cargo run -- gui

# Run a script file
cargo run -- script examples/scripts/ancestor.chase

The REPL and GUI share a minimal command language:

fact Parent(alice, bob).
rule Parent(?X, ?Y) -> Ancestor(?X, ?Y).
run.
query Ancestor(?X, ?Y)?
explain Ancestor(alice, carol)?
show facts
show rules
reset
help

Rules:

• facts and rules end with .
• queries end with ?
• explain ... ? shows one derivation tree per matching answer
• variables are prefixed with ?
• quoted constants are supported, for example "alice smith"

Useful Commands

# Install dependencies
nix develop -c make install-deps

# Run all tests
make test

# Run linter checks
make lint

# Run with optimizations
make build

# Run CLI
make run

---

License

This project is licensed under BSD-3.