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: ```rust // semilattice.eqlog
// The carrier set. Sort El; // The less-equal relation. Pred Le: El * El;
// Reflexivity. Axiom x: El => Le(x, x); // Transitivity. Axiom Le(x, y) & Le(y, z) => Le(x, z); // Antisymmetry. Axiom Le(x, y) & Le(y, x) => 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. Axiom x: El & y: El => Meet(x, y)!; // The meet is a lower bound. Axiom m = Meet(x, y) => Le(m, x) & Le(m, y); // All lower bounds are smaller or equal to the meet. Axiom Le(z, x) & Le(z, y) & m = Meet(x, y) => 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: ```rust // main.rs
use eqlogruntime::eqlogmod; 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.newel(); let y = sl.newel(); let z = sl.new_el();
// Close the semilattice structure by matching premises of axioms and
// adding conclusions until we reach a fixed point.
sl.close();
// sl satisfies all semilattice axioms 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: - type inference [[eqlog](https://github.com/eqlog/eqlog/tree/master/eqlog-test/src/inference.eqlog)] [[rust](https://github.com/eqlog/eqlog/tree/master/eqlog-test/src/inferencetest.rs)] - proving facts about categories [[eqlog](https://github.com/eqlog/eqlog/tree/master/eqlog-test/src/lexcategory.eqlog)] [[rust](https://github.com/eqlog/eqlog/tree/master/eqlog-test/src/lexcategorytest.rs)]
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:
```toml
[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:
rust
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:
rust
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 sort, predicate, function and axiom declarations. Mathematically, eqlog is a way to specify essentially algebraic theories.
Sorts represent the different carrier sets of models of our theory.
They are declared as follows:
rust
Sort <SortName>;
The name of a sort must be UpperCamelCase.
Predicates are declared as follows:
rust
Pred <PredName> : <Sort_1> * ... * <Sort_n>;
Each predicate has an arity, which is the list of sorts separated by an asterisk appearing after the colon.
All sorts appearing in the arity must be declared prior to the predicate.
Predicate names must be UpperCamelCase.
Functions are declared as follows:
rust
Func <FuncName> : <ArgSort_1> * ... * <ArgSort_n> -> <ResultSort>;
Each function has a domain, which is the list of sorts appearing before the arrow, and a codomain sort after the arrow.
All sorts appearing in the domain and the codomain must be declared prior to the function.
Function names must be UpperCamelCase.
A function with empty domain is a constant.
Constants are declared as follows:
rust
Func <ConstantName> : <Sort>;
To eqlog, functions are synonymous to partial functions; they need not be total.
The simplest but most general type of axiom is the implication.
Implications are of the form
rust
Axiom <Premise> => <Conclusion>;
where <Premise> and <Conclusion> are conjunctions of atoms.
Most atoms contain terms.
A term is either a variable or an application of a function symbol to terms.
Variables names must be lower_snake_case.
Variables that are used only once should be replaced with a wildcard _.
Eqlog supports the following atoms:
* Atoms of the form <PredName>(<arg_1>, ..., <arg_n>).
Such atoms assert that <arg_1>, ..., <arg_n> must satisfy the <PredName> predicate.
* Atoms of the form <term>!.
Note the exclamation mark.
Such atoms assert that <term> is defined, i.e. that the involved functions are defined on their arguments.
* Atoms of the form <tm_1> = <tm_2>.
Such atoms assert that the terms <tm_1> and <tm_2> are both defined and equal.
* Atoms of the form <var_name> : <SortName>.
Such atoms assert that <var_name> is a variable of type <SortName>.
They can only appear in premises.
Every variable occuring in an implication must be used at least once in the premise.
Thus no additional variables may be introduced in the conclusion.
Furthermore, unless the exclamation mark operator ! is used, implications must be surjective:
Every term appearing in the conclusion of an implication must be equal to a term appearing in the premise or earlier in the conclusion.
The only way to circumvent this restriction is to add an atom of the form <tm>! in the conclusion.
Later atoms can then freely use <tm>.
For example, consider the following invalid and valid axioms for the semilattice theory above: ```rust // Invalid: Cannot infer sort of x. Axiom x = x => x = x; // Valid (but nonsensical): Axiom x: El => x = x;
// Invalid: x and y are not used in the (empty) premise. Axiom Meet(x, y)!; // Valid: Axiom x: El & y: El => Meet(x, y)!;
// Invalid: Meet(x, y) is not equal to a term occuring earlier. Axiom Le(z, x) & Le(z, y) => Le(z, Meet(x, y)); // Valid: Assert that Meet(x, y) exists as part of conclusion. Axiom Le(z, x) & Le(z, y) => Meet(x, y)! & Le(z, Meet(x, y)); // Valid: Suppose that Meet(x, y) exists in premise. Axiom Le(z, x) & Le(z, y) & Meet(x, y)! => Le(z, Meet(x, y));
// Invalid: Both Meet(x, y) and Meet(y, x) do not occur earlier. Axiom x: El & y: El => Meet(x, y) = Meet(y, x); // Valid: the term on the left-hand side of the equation is introduced // in the premise. Axiom Meet(x, y)! => Meet(x, y) = Meet(y, x); // Valid: the term on the right-hand side of the equation is introduced // earlier in the conclusion. Axiom x: El & y : El => Meet(x, y)! & Meet(y, x) = Meet(x, y);
// Invalid: Meet(x, y) is not equal to a term that occurs earlier. Axiom u = Meet(x, Meet(y, z))! => Meet(Meet(x, y), z) = u; // Valid: All of u, Meet(x, y) and z are introduced in the premise. Axiom u = Meet(x, Meet(y, z))! & Meet(x, y)! => u = Meet(Meet(x, y), z); ```
Reductions are syntactic sugar for implication axioms.
A reduction has the form
rust
Axiom <from> ~> <to>;
where <from> and <to> are terms of the same sort and <from> must not be a variable.
A reduction axiom has the following meaning:
If all subterms of <from> are defined and <to> is defined, then also <from> is defined and equals <to>.
Accordingly, if <from> = <Func>(<arg_1>, ..., <arg_n>), then the reduction desugars to the implication
rust
Axiom <arg_1>! & ... & <arg_n>! & <to>! => <from> = <to>;
The order of the from and to terms can be confusing at first, but consider that algorithms involving reduction usually work top-down, whereas eqlog evaluates bottom-up.
Eqlog also supports the following symmetric form
rust
Axiom <lhs> <~> <rhs>;
which desugars to the two reductions
rust
Axiom <lhs> ~> <rhs>;
Axiom <rhs> ~> <lhs>;
Both reductions and symmetric reductions can be made conditional on a premise:
rust
Axiom <atom_1> & ... & <atom_n> => <lhs> ~> <rhs>;
Axiom <atom_1> & ... & <atom_n> => <lhs> <~> <rhs>;
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
sh
cargo doc --document-private-items --open
The public API of the generated rust module consists of the following symbols:
* For each sort, a type <SortName> of element ids for this sort.
* The model structure.
Its name is derived by converting the file name to upper camel case.
For example, for semi_group.eqlog, this would be SemiGroup.
The model structure has the following member functions:
* fn new() -> Self
Creates an empty model structure.
* fn close(&mut self)
Close the model under all axioms.
* pub fn close_until(&mut self, condition: impl Fn(&Self) -> bool) -> bool
Close the model under all axioms until a condition is satisfied.
Returns false if the model could be closed under all axioms but the condition still does not hold.
* For each sort:
- fn new_<sort_name>(&mut self) -> <SortName>
Adjoins a new element to the model structure.
- fn equate_<sort_name>(&mut self, lhs: <SortName>, rhs: <SortName>)
Enforces the equality lhs = rhs in the model structure.
- fn are_equal_<sort_name>(&self, lhs: <SortName>, rhs: <SortName>) -> bool
Returns true if lhs and rhs represent the same element.
- fn root_<sort_name>(&self, el: <SortName>) -> <SortName>
Returns the canonical/root element of the equivalence class of an element.
* For each predicate:
- fn <pred_name>(&self, arg_1: <Sort_1>, ..., arg_n: <Sort_n>)
Checks whether the predicate holds on the given arguments.
- fn iter_<pred_name>(&self) -> impl '_ + Iterator<Item = <arity>>
Returns an iterator over tuples satisfying the predicate.
The item type yielded by the iterator is a tuple type determined by the arity.
- fn insert_<pred_name>(&mut self, arg_1: <Sort_1>, ..., arg_n: <Sort_n>)
Enforces that the predicate holds for the given arguments.
* For each function:
- fn <func_name>(&self, arg_1: <Sort_1>, ..., arg_n: <Sort_n>) -> Option<<ResultSort>>
Evaluates the function on the given arguments.
- fn iter_<func_name>(&self) -> impl '_ + Iterator<Item = <arity>>
Returns an iterator over tuples in the graph of the function.
The item type yielded by the iterator is a tuple type determined by the arity.
- fn define_<func_name>(&mut self, arg_1: <Sort_1>, ..., arg_n: <Sort_n>) -> <ResultSort>
Enforces that the function is defined on the given arguments, adjoining a new element if necessary.
- fn insert_<func_name>(&mut self, arg_1: <Sort_1>, ..., arg_n: <Sort_n>, result: <ResultSort>)
Insert a tuple into the graph of the function.
For example, these are the public declarations of the rust module generated from the semilattice theory: ```rust 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 newel(&mut self) -> El; fn equateel(&mut self, lhs: El, rhs: El); fn areequalel(&self, lhs: El, rhs: El) -> bool; fn root_el(&self, el: El) -> El;
fn le(&self, arg0: El, arg1: El) -> bool;
fn iterle(&self) -> impl ' + Iterator fn meet(&self, arg0: El, arg1: El) -> Option The theory model structures generated by eqlog can be thought of as in-memory SQL databases, with schema given by sort, predicate and function declarations.
Elements of a given sort are simple integer ids, and the model structure maintains a list of valid ids for each sort.
Every predicate The The enumeration of instances of premises 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 axioms listed in the eqlog file.
In each iteration, it is not necessary to enumerate premises 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 In addition to the standard datalog features discussed so far, eqlog supports equalities in conclusions.
One example is the antisymmetry axiom of partial orders:
To account for derived equalities, eqlog model structures maintain union-find data structures for each sort.
When an equality To speed up computation of the joins required when matching axiom premises, 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 sort 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 Recall that eqlog axioms need to be surjective unless the exclamation mark operator If there are non-surjective axioms, then this is not guaranteed.
Consider the following eqlog theory that formalizes natural numbers:
```
Sort N;
Zero: N;
Succ: N -> N; Axiom Zero()!;
Axiom n: N => Succ(n)!;
If a theory contains non-surjective axioms, the generated fn close() {
loop {
loop {
let modelchanged = surjectiveaxioms.iter().any(adjoinconclusion);
if !modelchanged {
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.Data model and algorithms
Standard datalog features
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)).close function repeatedly enumerates all instances of premises of axioms and adjoins their conclusion to the model.
Eventually, a fixed point is reached (unless the theory contains non-surjective axioms, see below) and the algorithm stops.
For example, for the transitivity axiom
rust
Axiom Le(x, y) & Le(y, z) => Le(x, z);
the 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.close function.Equalities
rust
Axiom Le(x, y) & Le(y, x) => x = y;
Another source of equality in conclusions 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:
rust
Axiom G_F(x_1, ..., x_n, y) & G_F(x_1, ..., x_n, z) => y = z
Note, however, that graphs of functions cannot be referred to directly in eqlog files.x = y is derived during a call to close, eqlog merges the equivalence classes of x and y.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.Non-surjective axioms and non-termination
! is used:
Every element in the conclusion must be equal to some element in the premise.
Closing model structures under surjective axioms does not increase the number of elements in the model, which guarantees that the close function eventually terminates.
Closing the empty model structure will first add an element `Zero` to the model, then the element `Succ(N)`, then `Succ(Succ(N))` and so forth.
However, the presence of non-surjective axioms does not necessarily mean that the close function must run indefinitely.
For example, the semilattice theory contains the non-surjective axiom
rust
Axiom x: El & y : El => Meet(x, y)!;
``
butclose` nevertheless terminates.close function will consist of nested close loops:
The outer loop is responsible for non-surjective axioms, and the inner loop is responsible for surjective axioms.
In pseudo-code, the close function looks a bit like this:
```rust
// Match axiom premise and change the model such that the conclusion holds.
// Returns true if the model was changed, i.e. if not all conclusions were
// already true.
fn adjoin_conclusions(ax: Axiom) -> bool {
...
}let model_changed = non_surjective_axioms.iter().any(adjoin_conclusion);
if !model_changed {
break;
}
Background