created_at2023-10-21 10:35:19.611276
updated_at2024-04-02 16:54:01.894464
descriptionDatalog with equality
Martin Bidlingmaier (mbid)



# Eqlog 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. ## Example: Semilattices 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: ```eqlog // 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: ```rust // 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](https://github.com/eqlog/eqlog/tree/master/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/inference_test.rs)] - proving facts about categories [[eqlog](https://github.com/eqlog/eqlog/tree/master/eqlog-test/src/lex_category.eqlog)] [[rust](https://github.com/eqlog/eqlog/tree/master/eqlog-test/src/lex_category_test.rs)] ## Integration into rust projects A full sample project can be found in [examples/semilattice](https://github.com/eqlog/eqlog/tree/master/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](https://doc.rust-lang.org/cargo/reference/build-scripts.html) 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!(); ``` Note that a special invocation that specifies the full path is needed for eqlog files in nested subdirectories of `src`. ## Language Each eqlog file consists of a sequence of type, predicate, function and rule declarations. Mathematically, eqlog is a way to specify [essentially algebraic theories](https://ncatlab.org/nlab/show/essentially+algebraic+theory#definition). ### Types Types represent the different carrier sets of models of our theory. They are declared as follows: ```eqlog type ; ``` ### Predicates Predicates are declared as follows: ```eqlog pred (, ..., ); ``` Each predicate has an arity, which is the list of types appearing in the parentheses. ### Functions Functions are declared as follows: ```eqlog func (, ..., ) -> ; ``` 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: ```eqlog func : ; ``` To eqlog, functions are synonymous to *partial* functions; they need not be total. ### Rules Rules are of the form ``` rule { if ; if ; ... if ; then ; then ; ... then ; } ``` where the `` and `` 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: * Atoms of the form `(, ..., )`. Such atoms assert that `, ..., ` must satisfy the `` predicate. * Atoms of the form `!`. Note the exclamation mark. Such atoms assert that `` is defined, i.e. that the involved functions are defined on their arguments. In a `then` clause, `` can be given a name like so: ` := !`. * Atoms of the form ` = `. Such atoms assert that the terms `` and `` are both defined and equal. * Atoms of the form ` : `. Such atoms assert that `` is a variable of type ``. They can only appear in `if` clauses. Except for the ` := ...` 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 !;`. Later `then` statements atoms can then freely use ``. 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); } ``` ## Generated rust interfaces 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 Eqlog type, a Rust type `` of element ids for this type. * 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 rules. * `pub fn close_until(&mut self, condition: impl Fn(&Self) -> bool) -> bool` Close the model under all rules until a condition is satisfied. Returns false if the model could be closed under all rules but the condition still does not hold. * For each type: - `fn new_(&mut self) -> ` Adjoins a new element to the model structure. - `fn equate_(&mut self, lhs: , rhs: )` Enforces the equality `lhs = rhs` in the model structure. - `fn are_equal_(&self, lhs: , rhs: ) -> bool` Returns true if `lhs` and `rhs` represent the same element. - `fn root_(&self, el: ) -> ` Returns the canonical/root element of the equivalence class of an element. * For each predicate: - `fn (&self, arg_1: , ..., arg_n: )` Checks whether the predicate holds on the given arguments. - `fn iter_(&self) -> impl '_ + Iterator>` 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_(&mut self, arg_1: , ..., arg_n: )` Enforces that the predicate holds for the given arguments. * For each function: - `fn (&self, arg_1: , ..., arg_n: ) -> Option<>` Evaluates the function on the given arguments. - `fn iter_(&self) -> impl '_ + Iterator>` 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_(&mut self, arg_1: , ..., arg_n: ) -> ` Enforces that the function is defined on the given arguments, adjoining a new element if necessary. - `fn insert_(&mut self, arg_1: , ..., arg_n: , result: )` 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 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; fn insert_le(&mut self, arg0: El, arg1: El); fn meet(&self, arg0: El, arg1: El) -> Option; fn iter_meet(&self) -> impl '_ + Iterator; fn define_meet(&mut self, arg0: El, arg1: El) -> El; fn insert_meet(&mut self, arg0: El, arg1: El, result: El); } ``` ## Data model and algorithms ### Standard datalog features 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](https://en.wikipedia.org/wiki/Graph_of_a_function). 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](https://en.wikipedia.org/wiki/Fixed_point_(mathematics)) 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](https://en.wikipedia.org/wiki/Join_(SQL)#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. ### Equalities 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](https://en.wikipedia.org/wiki/Disjoint-set_data_structure) 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. ### Non-surjective rules and non-termination 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: ```rust // 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; } } } ``` ## Background For a more thorough explanation of how Eqlog works, have a look at these papers: - *An Evaluation Algorithm for Datalog with Equality* [[Web](https://www.mbid.me/eqlog-algorithm)] [[PDF](https://arxiv.org/pdf/2302.05792.pdf)] - *Algebraic Semantics of Datalog with Equality* [[Web](https://www.mbid.me/eqlog-semantics)] [[PDF](https://arxiv.org/pdf/2302.03167.pdf)] Also have a look at the [egglog project](https://github.com/egraphs-good/egglog) and the corresponding [paper](https://arxiv.org/pdf/2304.04332.pdf). 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.
Commit count: 896

cargo fmt