ExDatalog.Validator.Stratification (ExDatalog v0.2.0)

Copy Markdown View Source

Stratification checks for ExDatalog programs.

A Datalog program with negation must be stratifiable — there must be no cycle in the dependency graph that contains a negative edge. If such a cycle exists, evaluation order is ambiguous and the program is rejected.

This module:

  1. Builds a dependency graph from the program's rules.
  2. Computes strongly connected components (SCCs) using Tarjan's algorithm.
  3. Checks that no SCC contains a negative edge.
  4. Assigns a stratum to each relation.

Summary

Types

edge()
graph()
scc()

Functions

assign_strata(program)

Assigns strata to all relations in the program.

check(program)

Checks whether the program has unstratifiable negation.

Types

edge()

@type edge() :: {String.t(), :positive | :negative}

graph()

@type graph() :: %{required(String.t()) => [edge()]}

scc()

@type scc() :: [String.t()]

Functions

assign_strata(program)

@spec assign_strata(ExDatalog.Program.t()) :: %{
  required(String.t()) => non_neg_integer()
}

Assigns strata to all relations in the program.

Returns a map from relation name to stratum number (0-based). Every declared relation is included — relations that appear only in facts (not in any rule) are assigned stratum 0. Only valid for programs that pass check/1.

check(program)

@spec check(ExDatalog.Program.t()) :: :ok | {:error, [ExDatalog.Validator.Error.t()]}

Checks whether the program has unstratifiable negation.

Returns :ok if all SCCs are stratifiable, or {:error, errors} listing every SCC that contains a negative edge.