Crates.io | eqlog-runtime |
lib.rs | eqlog-runtime |
version | 0.7.0 |
source | src |
created_at | 2022-08-14 10:45:48.990692 |
updated_at | 2024-04-03 22:05:15.657962 |
description | Datalog with equality |
homepage | |
repository | https://github.com/eqlog/eqlog/ |
max_upload_size | |
id | 645351 |
size | 24,556 |
An extension of datalog with function symbols and equality. Combines datalog with congruence closure. Compiles to specialized rust code that easily integrates into rust projects.
Semilattices are partial orders (i.e. sets equipped with reflexive, transitive and antisymmetric relations) with binary meets. They can be formalized in the following eqlog theory:
// semilattice.eqlog
// The carrier set.
type El;
// The less-equal relation.
pred le: El * El;
// The less-equal relation is reflexive.
rule reflexivity {
if x: El;
then le(x, x);
}
// The less-equal relation is transitive.
rule transitivity {
if le(x, y);
if le(y, z);
then le(x, z);
}
// The less-equal relation is antisymmetric.
rule antisymmetry {
if le(x, y);
if le(y, x);
then x = y;
}
// A function assigning binary meets, i.e. binary greatest lower bound.
func meet(El, El) -> El;
// The meet function is total, i.e. defined for all elements x, y.
rule totality {
if x: El;
if y: El;
then meet(x, y)!;
}
// The meet is a lower bound.
rule lower_bound {
if m = meet(x, y);
then le(m, x);
then le(m, y);
}
// The meet is the greatest lower bound.
rule greatest_lower_bound {
if le(z, x);
if le(z, y);
if m = meet(x, y);
then le(z, m);
}
Eqlog translates this eqlog file to a rust module that allows computations on models of the semilattice theory, i.e. semilattices. For example, we can verify that the meet function in a semilattice is associative:
// main.rs
use eqlog_runtime::eqlog_mod;
eqlog_mod!(semilattice);
use crate::semilattice::*;
fn main() {
// Create an empty semilattice structure and add three elements to it.
let mut sl = Semilattice::new();
let x = sl.new_el();
let y = sl.new_el();
let z = sl.new_el();
// Close the semilattice structure by matching atoms in if statements of rules
// and adding then atoms until we reach a fixed point.
sl.close();
// sl satisfies all semilattice rules now.
// Evaluate the left-associated meet xy_z = (x /\ y) /\ z.
let xy = sl.meet(x, y).unwrap();
let xy_z = sl.meet(xy, z).unwrap();
// Evaluate the right-associated meet x_yz = x /\ (y /\ z).
let yz = sl.meet(y, z).unwrap();
let x_yz = sl.meet(x, yz).unwrap();
// Check that the two elements are equal.
if sl.are_equal_el(xy_z, x_yz) {
println!("Meet is associative.");
} else {
println!("Meet is not associative.");
}
}
The eqlog-test/src contains more examples:
A full sample project can be found in examples/semilattice.
Eqlog consists of the compiler crate eqlog
, which is only needed during build, and the runtime crate eqlog-runtime
.
We can specify them as dependencies in Cargo.toml
by adding the following lines:
[dependencies]
eqlog-runtime = "0"
[build-dependencies]
eqlog = "0"
In order for our rust code to integrate with the code generated by eqlog, we need to run eqlog before building the crate itself.
This can be accomplished by adding the following build.rs
file next to Cargo.toml
in the package root directory:
fn main() {
eqlog::process_root();
}
Cargo automatically executes the build.rs
file before building.
eqlog::process_root()
searches for files under the src
directory and generates a rust module for each .eqlog
file.
To declare the rust module generated from an eqlog file, we use the eqlog_mod!
macro:
use eqlog_runtime::eqlog_mod;
eqlog_mod!(<filename without extension>);
Note that a special invocation that specifies the full path is needed for eqlog files in nested subdirectories of src
.
Each eqlog file consists of a sequence of type, predicate, function and rule declarations. Mathematically, eqlog is a way to specify essentially algebraic theories.
Types represent the different carrier sets of models of our theory. They are declared as follows:
type <TypeName>;
Predicates are declared as follows:
pred <PredName>(<Type_1>, ..., <Type_n>);
Each predicate has an arity, which is the list of types appearing in the parentheses.
Functions are declared as follows:
func <FuncName>(<ArgType_1>, ..., <ArgType_n>) -> <ResultType>;
Each function has a domain, which is the list of types appearing before the arrow, and a codomain type after the arrow.
A function with empty domain is a constant. Constants are declared as follows:
func <ConstantName> : <Type>;
To eqlog, functions are synonymous to partial functions; they need not be total.
Rules are of the form
rule <name> {
if <Premise_1>;
if <Premise_2>;
...
if <Premise_m>;
then <Conclusion_1>;
then <Conclusion_2>;
...
then <Conclusion_n>;
}
where the <Premise_i>
and <Conclusion_j>
are atoms.
Most atoms contain terms.
A term is either a variable or an application of a function symbol to terms.
Variables that are used only once should be replaced with a wildcard _
.
Eqlog supports the following atoms:
<PredName>(<arg_1>, ..., <arg_n>)
.
Such atoms assert that <arg_1>, ..., <arg_n>
must satisfy the <PredName>
predicate.<term>!
.
Note the exclamation mark.
Such atoms assert that <term>
is defined, i.e. that the involved functions are defined on their arguments.
In a then
clause, <term>
can be given a name like so:
<var_name> := <term>!
.<tm_1> = <tm_2>
.
Such atoms assert that the terms <tm_1>
and <tm_2>
are both defined and equal.<var_name> : <TypeName>
.
Such atoms assert that <var_name>
is a variable of type <TypeName>
.
They can only appear in if
clauses.Except for the <var> := ...
form of the exclamation mark operator, no additional variables may be introduced in then statements.
Every term appearing in a then
statement of a rule must be equal to a term appearing in an earlier if
statement.
The only way to circumvent this restriction is to add a statement of the form then <tm>!;
.
Later then
statements atoms can then freely use <tm>
.
For example, consider the following invalid and valid rules for the semilattice theory above:
// Invalid: Cannot infer type of x.
rule {
if x = x;
then x = x;
}
// Valid (but nonsensical):
rule {
if x: El;
then x = x;
}
// Invalid: x and y are not introduced in an `if` statement.
rule {
then meet(x, y)!;
}
// Valid:
rule {
if x: El;
if y: El;
then meet(x, y)!;
}
// Invalid: meet(x, y) is not equal to a term occurring earlier.
rule {
if le(z, x);
if le(z, y);
then le(z, meet(x, y));
}
// Valid: Assert that meet(x, y) exists in a then statement.
rule {
if le(z, x);
if le(z, y);
then meet(x, y)!
then le(z, meet(x, y));
}
// Valid: Suppose that meet(x, y) exists in if statement.
rule {
if le(z, x);
if le(z, y);
if meet(x, y)!;
then le(z, meet(x, y));
}
// Invalid: Both Meet(x, y) and Meet(y, x) do not occur earlier.
rule {
if x: El;
if y: El;
then meet(x, y);
then meet(y, x);
}
// Valid: the term on the left-hand side of the equation is introduced
// in an if statement.
rule {
if meet(x, y)!;
then meet(x, y);
then meet(y, x);
}
// Valid: the term on the right-hand side of the equation is introduced
// earlier in a then statement.
rule {
if x: El;
if y: El;
then meet(x, y)!;
then meet(y, x) = meet(x, y);
}
// Invalid: meet(x, y) is not equal to a term that occurs earlier.
rule {
if u = meet(x, meet(y, z))!;
then meet(meet(x, y), z) = u;
}
// Valid: All of u, Meet(x, y) and z are introduced in an if statement.
rule {
if u = meet(x, meet(y, z))!;
if meet(x, y)!;
then u = meet(meet(x, y), z);
}
Eqlog translates each .eqlog
to an .rs
file.
The rust file must be declared inside a module of the src
directory (e.g. lib.rs
or main.rs
) using the eqlog_runtime::eqlog_mod!
macro.
Eqlog generates documented rust code. To build and view this documentation, run
cargo doc --document-private-items --open
The public API of the generated rust module consists of the following symbols:
<TypeName>
of element ids for this type.semi_group.eqlog
, this would be SemiGroup
.The model structure has the following member functions:
fn new() -> Self
fn close(&mut self)
pub fn close_until(&mut self, condition: impl Fn(&Self) -> bool) -> bool
fn new_<sort_name>(&mut self) -> <TypeName>
fn equate_<sort_name>(&mut self, lhs: <TypeName>, rhs: <TypeName>)
lhs = rhs
in the model structure.fn are_equal_<sort_name>(&self, lhs: <TypeName>, rhs: <TypeName>) -> bool
lhs
and rhs
represent the same element.fn root_<sort_name>(&self, el: <TypeName>) -> <TypeName>
fn <pred_name>(&self, arg_1: <Type_1>, ..., arg_n: <Type_n>)
fn iter_<pred_name>(&self) -> impl '_ + Iterator<Item = <arity>>
fn insert_<pred_name>(&mut self, arg_1: <Type_1>, ..., arg_n: <Type_n>)
fn <func_name>(&self, arg_1: <Type_1>, ..., arg_n: <Type_n>) -> Option<<ResultType>>
fn iter_<func_name>(&self) -> impl '_ + Iterator<Item = <arity>>
fn define_<func_name>(&mut self, arg_1: <Type_1>, ..., arg_n: <Type_n>) -> <ResultType>
fn insert_<func_name>(&mut self, arg_1: <Type_1>, ..., arg_n: <Type_n>, result: <ResultType>)
For example, these are the public declarations of the rust module generated from the semilattice theory:
struct El;
struct Semilattice;
impl Semilattice {
fn new() -> Self;
fn close(&mut self);
fn close_until(&mut self, condition: impl Fn(&Self) -> bool) -> bool;
fn new_el(&mut self) -> El;
fn equate_el(&mut self, lhs: El, rhs: El);
fn are_equal_el(&self, lhs: El, rhs: El) -> bool;
fn root_el(&self, el: El) -> El;
fn le(&self, arg0: El, arg1: El) -> bool;
fn iter_le(&self) -> impl '_ + Iterator<Item = (El, El)>;
fn insert_le(&mut self, arg0: El, arg1: El);
fn meet(&self, arg0: El, arg1: El) -> Option<El>;
fn iter_meet(&self) -> impl '_ + Iterator<Item = (El, El, El)>;
fn define_meet(&mut self, arg0: El, arg1: El) -> El;
fn insert_meet(&mut self, arg0: El, arg1: El, result: El);
}
The theory model structures generated by eqlog can be thought of as in-memory SQL databases, with schema given by type, predicate and function declarations.
Elements of a given type are simple integer ids, and the model structure maintains a list of valid ids for each type.
Every predicate p
is represented as a table whose rows are the tuples of elements for which the predicate holds.
Functions are represented as graphs.
For example, if f
is a function in one argument, then the internal table for f
will consist of rows of the form (x, f(x))
.
The close
function repeatedly enumerates all matches of if statements in rules and adjoins data corresponding to the then statements in the rule to the model.
Eventually, a fixed point is reached (unless the theory contains non-surjective rules, see below) and the algorithm stops.
For example, for the transitivity axiom
rule {
if le(x, y);
if le(y, z);
then le(x, z);
}
the close function enumerates all rows (x, y_0)
and (y_1, z)
in the Le
table such that y_0 = y_1
, and then adds the row (x, z)
to Le
.
Eventually, the Le
table will already contain all the new rows (x, z)
we find, which means that we have reached the fixed point and can stop:
The le
predicate is transitive now.
The enumeration of instances of if statements is known as (inner) join in SQL terminology.
SQL databases speed up inner joins using indices, and eqlog automatically selects and maintains indices to speed up the joins required to enumerate the rules listed in the eqlog file.
In each iteration, it is not necessary to enumerate if statements that were already enumerated in the previous iteration.
This optimization is known as semi-naive evaluation, and is again something that eqlog uses to speed up the close
function.
In addition to the standard datalog features discussed so far, eqlog supports equalities in then
statements.
One example is the antisymmetry axiom of partial orders:
rule {
if le(x, y);
if le(y, x);
then x = y;
}
Another source of equality in then
statements are the implicit functionality axioms for functions:
For functions f
, if we find both (x_1, ..., x_n, y)
and (x1, , ..., x_n, z)
in the graph of f
, then we must derive y = z
.
If we denote the graph of f
by g_f
, then the implicit functionality axiom can be stated as follows:
rule {
if g_f(x_1, ..., x_n, y);
if g_f(x_1, ..., x_n, z);
then y = z;
}
Note, however, that graphs of functions cannot be referred to directly in eqlog files.
To account for derived equalities, eqlog model structures maintain union-find data structures for each type.
When an equality x = y
is derived during a call to close
, eqlog merges the equivalence classes of x
and y
.
To speed up computation of the joins required when matching if statements, eqlog maintains indices for each table. However, these indices can only be used if element ids can be compared for equality directly instead of consulting a union find data structure. Eqlog thus maintains the invariant that all predicate and function graph tables contain canonical type elements only, i.e. only elements whose ids are root nodes with respect to the corresponding union find data structure.
This invariant is temporarily violated when eqlog merges the equivalence class of some element x
into that of an element y
.
To restore the invariant, eqlog removes all rows from tables that contain x
, replaces x
by the new root id y
, and inserts the rows again.
To speed up this process, eqlog maintains a list for each root id that contains all rows in which the root id appears.
Recall that eqlog rules need to be surjective unless the exclamation mark operator !
is used:
Every element in a then statement must be equal to some element in an if statement.
Closing model structures under surjective rules does not increase the number of elements in the model, which guarantees that the close
function eventually terminates.
If there are non-surjective rules, then this is not guaranteed. Consider the following eqlog theory that formalizes natural numbers:
type N;
zero: N;
succ: N -> N;
rule {
then Zero()!;
}
rule {
if n: N;
then Succ(n)!;
}
Closing the empty model structure will first add an element zero
to the model, then the element succ(zero)
, then succ(succ(zero))
and so forth.
However, the presence of non-surjective rules does not necessarily mean that the close function must run indefinitely.
For example, the semilattice theory contains the non-surjective rule
rule {
if x: El;
if y : El;
then meet(x, y)!;
}
but close
nevertheless terminates.
If a theory contains non-surjective rules, the generated close
function will consist of nested close loops:
The outer loop is responsible for non-surjective rules, and the inner loop is responsible for surjective rules.
In pseudo-code, the close
function looks a bit like this:
// Match `if` statements in a rule and change the model such that the
// corresponding `then` statements holds. Returns true if the model was
// changed, i.e. if new facts were concluded.
fn adjoin_conclusions(ax: Axiom) -> bool {
...
}
fn close() {
loop {
loop {
let model_changed = surjective_rules.iter().any(adjoin_conclusion);
if !model_changed {
break;
}
}
let model_changed = non_surjective_rules.iter().any(adjoin_conclusion);
if !model_changed {
break;
}
}
}
For a more thorough explanation of how Eqlog works, have a look at these papers:
Also have a look at the egglog project and the corresponding paper. Even though its surface language looks a bit different, Egglog is based on very similar ideas as those underlying Eqlog, and can be used for many of the same applications.