# An Evaluation Algorithm for Datalog with Equality

Martin E. Bidlingmaier

###### Abstract

We describe an evaluation algorithm for _relational Horn logic (RHL)_. RHL
extends Datalog with quantification over sorts, existential quantification in
conclusions and, crucially, the ability to infer _equalities_. These
capabilities allow RHL evaluation to subsume and expand applications of
Datalog and congruence closure algorithms.

We explain how aspects of a fast congruence closure algorithm can be
incorporated into Datalog evaluation to obtain an efficient RHL evaluation
algorithm. We then sketch how Steensgaard’s points-to analysis and type
inference can be implemented using RHL evaluation. RHL and the evaluation
algorithm described here are the foundation of the _Eqlog_ Datalog engine.

##  1 Introduction

Recent work has identified _relational Horn logic_ (RHL) and _partial Horn
logic_ (PHL) as a semantically well-behaved extensions of Datalog
(Bidlingmaier, 2023). This paper describes how the Datalog evaluation
algorithm can be generalized to RHL evaluation.

An RHL theory contains declarations of the following data:

  * •

A set $S$ of _sorts_.

  * •

A set $R$ of _relations_.

  * •

_Arities_ $r:s_{1}\times\dots\times s_{n}$ for all relations $r\in R$.

  * •

A set of _sequents_ (or _rules_ , or _axioms_), each of the form
$\mathcal{F}\implies\mathcal{G}$, where $\mathcal{F}$ and $\mathcal{G}$ are
conjunctions $\phi_{1}\land\dots\land\phi_{n}$ of _atoms_ $\phi_{i}$.

Instead of RHL sequents as above, Datalog engines typically accept rules of
the following form:

$\phi\;\text{:-}\;\phi_{1},\dots,\phi_{n}.$ (1)

The _head_ $\phi$ corresponds to the conclusion of an RHL sequent and consists
of a single atom. The _body_ $\phi_{1},\dots,\phi_{n}$ corresponds to the
premise of an RHL sequent, can contain multiple atoms and is interpreted as
conjunction. The structure of RHL sequents is thus more general at first sight
because the conclusion of an RHL sequents is allowed to be a conjunction of
atoms. However, a single sequent with $n$ conclusion atoms is equivalent to
$n$ sequents, each with a single conclusion atom. Thus, no generality is
gained solely from allowing general conjunctions as conclusions.

Where RHL generalizes Datalog is in what kind of atoms it allows, and how
variables are handled. In Datalog, each atom is of the form
$r(v_{1},\dots,v_{n})$ where $r$ is a relation symbol and the $v_{i}$ are
variables whose sort match the arity of $r$. In addition to such _relation
atoms_ , RHL recognizes also the following types of atoms:

  1. 1.

An _equality atom_

$u\equiv v$ (2)

where $u$ and $v$ have the same sort. We reserve the symbol ${\equiv}$ for RHL
syntax, whereas ${=}$ is used for meta-theoretical equality.

  2. 2.

A _sort quantification_

$v\downarrow$ (3)

where $v$ is a variable with known sort $s$. If the sort of $v$ is not
determined by other atoms in the sequent, we also use the syntax $v:s$ as
synonymous for $v\downarrow$ and the metatheoretical assertion that $v$ has
sort $s$.

If an equality atom $u\equiv v$ occurs in the premise of a sequent, then
matches of the premise are only valid if $u$ and $v$ are interpreted as the
same constant. Thus, equality atoms in a premise can be eliminated by removing
all occurrences of one of the two variables in the sequent by the other
variable.

The semantics of an equality atom $u\equiv v$ in the conclusion of a sequent
are non-trivial, however: Whenever the premise of such a sequent matches such
that $u$ is interpreted as a constant $a$ and $v$ is interpreted as constant
$b$, then we expect the evaluation engine to identify $a$ and $b$ in all
contexts henceforth. For example, the premise of the transitivity axiom
$\mathrm{Le}(u,v)\land\mathrm{Le}(v,w)\implies\mathrm{Le}(u,w)$ should match
tuples $(a,b_{1}),(b_{2},c)\in\mathrm{Le}$ if an equality $b_{1}=b_{2}$ has
been inferred previously.

Partial functions can be encoded in RHL using relations representing the
graphs of partial functions. Thus one identifies partial functions
$f:s_{1}\times\dots\times s_{n}\rightarrow s$ with relations
$f:s_{1}\times\dots s_{n}\times s$ where the first $n$ components of each
entry represent an element in the domain of the function and the last
component represents the value of the function. The _functionality axiom_

$f(v_{1},\dots,v_{n},u)\land f(v_{1},\dots,v_{n},w)\implies u\equiv w$ (4)

enforces that the relation $f$ does indeed correspond to a well-defined
partial function.

Sort quantifications $v:s$ in premises allow matching elements of a given sort
$s$ that do not appear in any relation. In standard Datalog, all variables in
the head of a sequent must also appear in the body. This requirement is
removed in RHL. Variables that only appear in the conclusion are implicitly
existentially quantified. If the premise of a sequent matches, then the
evaluation engine must extend the match to the conclusion by finding an
interpretation of variables that occur only in the conclusion such that the
conclusion holds. If no such extension exists, then the evaluation engine must
create new identifiers to interpret variables that only occur in the
conclusion, and enforce that the atoms of the conclusion hold for this
interpretation. We expect the evaluation engine to output a list of
identifiers of each sort, including those identifiers that were created during
evaluation. An RHL sequent in which all conclusion variables also occur in the
premise is called _surjective_. If an RHL theory contains non-surjective
sequents, then evaluation need not terminate. The Souffle Datalog engine
implements a similar mechanism in the form of its choice construction (Hu et
al., 2021).

The presence of non-surjective sequents can not only lead to non-termination
but also to non-deterministic results, in the sense that the result depends on
the order in which sequents are matched. This is not the case for _strong_ RHL
theories, in which the interpretion of conclusion variables is uniquely
determined once all sequents are satisfied. For example, the RHL theory given
by the functionality sequent (7) and the sequent

$v_{1}:s_{1}\land\dots\land v_{n}:s_{n}\implies f(v_{1},\dots,v_{n},v)$ (5)

is strong, since if the functionality axiom is satisfied, then the
interpretation of the variable $v$ in sequent (5) is uniquely determined.
Unfortunately, it is undecidable whether a given RHL theory is strong.

A further problem with RHL is that functions must be encoded via their graphs.
This leads to excessive verbosity when formulating axioms involving complex
expressions built up from function symbols.

_Partial Horn logic_ (PHL) (Palmgren and Vickers, 2007) is a syntactic layer
on top of RHL that rectifies these shortcomings. In partial Horn logic,
relations must be explicitly declared as predicates or partial functions.
Predicates correspond directly to RHL relations, whereas functions are lowered
into a relation corresponding to the graph of the function and the implicit
functionality axiom (7).

In positions where RHL accepts variables, PHL also allows composite terms

$t\,\text{::=}\,v\mid f(t_{1},\dots,t_{n})$ (6)

which are recursively defined from variables and application of partial
function symbols to terms whose sorts match the function signature. When
lowering PHL to RHL, composite terms $t$ are recursively lowered into a result
variable representing the term $t$ and additional RHL atoms. These additional
atoms are inserted into premise or conclusion of the sequent, depending on
where $t$ appears. To lower a composite term $t=f(t_{1},\dots,t_{n})$, we may
assume that $t=f(v_{1},\dots,v_{n})$ for variables $v_{i}$ by recursively
lowering the arguments $t_{1},\dots,t_{n}$ first. We now choose a fresh
variable $v$ representing $t$ and add the RHL atom $f(v_{1},\dots,v_{n},v)$.
Since lowering a PHL formula reduces nested expressions into a flat sequence
of atoms, the process of lowering PHL to RHL is also called _flattening_.

PHL sequents are _epic_ if all variables in the conclusion are already
introduced in the premise. Note that lowering epic PHL sequents can result in
non-surjective RHL sequents, because lowering composite terms can introduce
fresh variables. Nevertheless, the lowered RHL theory resulting from an epic
PHL theory (i.e. a PHL theory containing epic sequents only) is strong.
Conversely, every strong RHL theory is equivalent to an epic PHL theory; see
Bidlingmaier (2023, Section 4.3) for details. Thus, epic PHL has the same
descriptive strength as strong RHL. On the other hand, checking whether a PHL
sequent is epic is trivial, whereas checking whether an RHL theory is strong
is undecidable. This makes PHL more suitable as human-facing input language to
an evaluation engine compared to RHL.

The _Eqlog_ engine, whose underlying algorithm is described in this paper,
accepts epic PHL as input language. Eqlog lowers a user-provided epic PHL
theory to RHL, which is then transpiled to a Rust module. This is similar to
the Souffle Datalog engine, which transpiles Datalog to C++. In contrast to
Souffle, Eqlog is meant to be used as part of a larger project and not as
standalone tool. Similarly to the _egg_ equality saturation library (Willsey
et al., 2021), Eqlog supports online use-cases in which one alternates
inserting new ground facts into the model and closing the model under PHL
sequents. Refer to the Eqlog project homepage (The Eqlog Authors, ) for
details.

Independently of the work on Eqlog presented in this article, members of the
Egg community have created a very similar tool that combines e-graphs with
Datalog, which will be reported on in an upcoming article.

Outline. In Section 2, we describe a basic algorithm to evaluate RHL, and a
technique to detect termination in many circumstances. Then, in Section 3, we
discuss optimizations of the RHL evaluation algorithm. Finally, in Section 4,
we sketch applications of PHL and RHL evaluation to the implementation of
programming languages. Section 5 concludes.

Acknowledgements. Jakob Botsch Nielsen contributed significantly to previous
versions of the implementation of the Eqlog tool and its application to an
experimental type checker for a dependently typed proof assistant. My own work
on Eqlog and the algorithm presented in this paper commenced during my time as
PhD student at Aarhus University, where I was advised by Bas Spitters and
supported by the Air Force Office and Scientific Research project “Homotopy
Type Theory and Probabilistic Computation”, grant number 12595060.

##  2 RHL Evaluation

In this section, we describe a basic algorithm to evaluate RHL theories. The
input to the evaluation algorithm is a list of RHL sequents and a _relational
structure_ representing ground facts. A relational structure is given by sets
of numerical identifiers for each sort, representing the elements of the sort,
and sets of tuples for each relation. From Section 2.2 onward, we assume that
relational structures contain also union-find data structures for each sort,
representing semantic equality of sort elements.

If RHL evaluation terminates, then we require that the output is a relational
structure that is _weakly free_ with respect to the list of RHL sequents over
the input relational structure (Bidlingmaier, 2023). Intuitively, this means
that the output must satisfy all sequents in the RHL theory, and that it must
be obtained from the input relational structure only from matching sequent
premises and adjoining data corresponding to conclusions.

Weak freeness does not uniquely characterize a relational structure. In
general, the output relational structure depends on the order of matching
premises of RHL sequents. However, if the RHL theory is strong, then the
output relational structure is _(strongly) free_ over the input relational
structure, which determines it uniquely up to unique isomorphism (i.e.
renaming of identifiers). Relevant classes of strong RHL theories are theories
containing surjective sequents only, and theories that are obtained from
lowering epic PHL theories (Bidlingmaier, 2023).

In Section 2.1, we discuss the naive algorithm for Datalog evaluation and
amend it with support for non-surjective sequents and sort quantification, but
not equality. Then, in Section 2.2, we consider a well-known simple congruence
closure algorithm, which we shall understand as a special-purpose algorithm
for evaluation of functionality RHL sequents. The conclusion of functionality
sequents is an equality, which our naive Datalog evaluation algorithm cannot
process. _Union-find data structures_ and _normalization_ are aspects of this
congruence closure algorithm that deal with equalities in particular. We
incorporate these into our naive Datalog algorithm to obtain a naive RHL
evaluation algorithm.

In Section 2.3, we discuss an example where our RHL evaluation algorithm does
not terminate for a non-surjective RHL theory with finite free models. Based
on the example, we show how the evaluation algorithm can be modified to
terminate for this particular example and also a wide range of other RHL
theories.

###  2.1 Naive Datalog evaluation

The naive Datalog algorithm is given by repeating _premise matching_ and
_conclusion application_ phases until a fixed point is reached. The high-level
structure of the algorithm can be expressed in Rust-like pseudo-code as
follows:

⬇

fn datalog(structure, sequents) {

loop {

// 1. Match premises.

let matches = [];

for sequent in sequents {

matches.push(find_matches(structure, sequent.premise));

}

// 2. Apply conclusions.

let has_changed = false;

for (sequent, matches) in sequents.zip(matches) {

for match in matches {

if apply_conclusion(structure, sequent.conclusion, match) {

has_changed = true;

}

}

}

// Terminate if applying conclusions had no effect.

if !changed {

break;

}

}

return structure;

}

find_matches is a subprocedure that returns a list of matches of the given
formula in a relational structure. Each match is given by a mapping from the
set of variables that occur in the formula to elements in the relational
structure. A naive implementation of this function enumerates matches using a
nested loop join. For example, matches of the formula
$\mathrm{Le}(u,v)\land\mathrm{Ge}(w,v)\land\mathrm{Le}(w,x)$ can be enumerated
as follows:

⬇

for (u, v) in structure.rels[Le] {

for (w, v1) in structure.rels[Ge] {

if v1 != v { continue; }

for (w1, x) in structure.rels[Le] {

if w1 != w { continue; }

matches.push({u, v, w, x});

}

}

}

Each relational atom translates into a nested loop over the corresponding
relation in the relational structure, and each sort quantification translates
into a loop over the corresponding list of elements.

apply_conclusion is a subprocedure that inserts data into a relational
structure according to a provided conclusion and a substitution of variables
for elements in the relational structure. It returns a boolean value
indicating whether the operation had an effect, i.e. whether at least some of
the concluded data was not already present in the relational structure. For
surjective sequents without equalities, where every variable in the conclusion
is already bound by a match of the premise, we substitute the variables in
each relation atom and insert the corresponding tuple into the relational
structure.

For non-surjective sequents, we first check if the provided substitution of
premise variables can be extended to interpretations of the conclusion
variables such that the conclusion holds. This can be accomplished using a
version of the find_matches function that takes a list of already fixed
interpretations of some of the variables in the formula. If no such extension
exists, then we adjoin fresh elements to the relational structure to interpret
the unbound conclusion variables and proceed as in the surjective case.

###  2.2 Congruence closure and naive RHL evaluation

RHL equality atoms can be reduced to Datalog by introducing binary equality
relations on each sort representing inferred equality. However, this _setoid
reduction_ (Bidlingmaier, 2023, Section 3.4) typically leads to inefficient
Datalog programs. Semantically, an inferred equality often reduces the size of
the relational structure, since equalities can collapse two previously
distinct tuples in a relation into a single tuple. Instead, the setoid
reduction leads to significant duplication due to congruence axioms, which
assert that all relations must be closed in each argument under inferred
equality. Our goal in this section is to rectify this deficiency: Every
inferred equality should only shrink the relational structure.

Observe that RHL can be used to solve, in particular, the congruence closure
problem: Decide which equalities among a list $t_{1},\dots,t_{n}$ of
expression follow from a list of equalities among subexpressions. This problem
can be encoded in RHL with a theory given by an $(n+1)$-ary relation symbol
$f$ representing the graph of an $n$-ary function symbol that occurs in the
$t_{i}$ and the _functionality axiom_

$f(v_{1},\dots,v_{n},u)\land f(v_{1},\dots,v_{n},w)\implies u\equiv w.$ (7)

One then inserts data corresponding to the $t_{i}$ into a relational
structure, imposes equalities among subexpressions, and closes the structure
under functionality axioms. We may thus understand congruence closure
algorithms as special-purpose evaluation algorithms for functionality RHL
sequents, and try to generalize existing congruence closure algorithms to
general RHL evaluation.

Our inspiration here is the congruence closure algorithm described in Downey
et al. (1980). Consider the following version of their naive algorithm 2.1,
which they attribute to Cocke and Schwartz (1970). The version presented here
is specialized to a single binary function. The input of the algorithm is a
list of triples representing the graph of the function.

⬇

fn congruence_closure(graph) {

uf = UnionFind::new();

loop {

// 1. Match premises.

let eqs = [];

for (x0, x1, x2) in graph {

for (y0, y1, y2) in graph {

if x0 == y0 && x1 == y1 {

eqs.push((x2, y2));

}

}

}

// 2. Apply equalities.

let has_changed = false;

for (lhs, rhs) in eqs {

lhs = uf.find(lhs);

rhs = uf.find(rhs);

if lhs != rhs {

uf.union(lhs, rhs);

has_changed = true;

}

}

// Terminate if nothing has changed.

if !has_changed {

break;

}

// 3. Normalize.

graph0 = [];

for (x0, x1, x2) in graph {

graph0.push(uf.find(x0), uf.find(x1), uf.find(x2));

}

graph = graph0;

}

return uf;

}

Similarly to the Datalog evaluation algorithm of Section 2.1, this congruence
closure algorithm repeats a number of steps until it reaches a fixed point.
Step 1 corresponds to the find_matches function for the premise of the
functionality axiom (7) of a binary function.

Step 2 applies the conclusions $u\equiv v$ for each match that was found in
step 1. The algorithm uses a union-find data structure to represent equality.
A union-find data structure associates a canonical representative to each
equivalence class. Equivalence classes are equal if and only if they have the
same canonical representative.

Union-find data structures support fast find and union operations in near-
constant runtime. The find operation computes the canonical representative in
the equivalence class of a given element. The union operation merges the
equivalence classes of two canonical representatives.

Step 3, which replaces all elements in entries of the graph relation by
canonical representatives, does not have a counterpart in Datalog evaluation.
Because of the use of the union-find data structure, only comparisons among
canonical representatives reflect inferred equality. Note that, instead of the
normalization step, we could also consult the union-find data structure in
step 1 during premise matching when comparing elements. However, a separate
normalization step makes the use of a number of optimizations possible, which
we discuss in Section 3.

By incorporating aspects of the congruence closure algorithm that deal with
equalities into the naive Datalog evaluation algorithm of Section 2.1, we now
obtain our _naive RHL evaluation algorithm_ :

  1. 1.

In addition to sets of elements and relation, relational structures now
contain also union-find data structures for each sort, representing semantic
equality. We maintain the invariant that the relations in the relational
structure contain canonical representatives only before each iteration of the
evaluation algorithm.

  2. 2.

apply_conclusion handles equalities $u\equiv v$ by merging the equivalence
classes of the interpretations of $u$ and $v$ with a call to union.

  3. 3.

Before the end of the loop body, we insert a normalization step, which
replaces each element in a tuple in any relation with its canonical
representative by calling find.

Since relational structures store relations as sets without duplication,
normalization can potentially reduce the number of elements of relations.

The Souffle Datalog engine provides an efficient implementation of equivalence
relations using union-find data structures (Nappa et al., 2019), but it does
not implement normalization.

###  2.3 Detecting termination

If all sequents in the RHL theory to be evaluated are surjective, then the
algorithm we have described in Section 2.2 is guaranteed to terminate. For
non-surjective sequents, however, the (weakly) free model over a finite
structure need not be finite. In these situations, RHL evaluation can thus not
terminate and must instead be aborted after a timeout is exceeded or a desired
property has been inferred. Nevertheless, there are RHL theories for which
free models over finite relational structures are again finite despite the
presence of non-surjective sequents. But even in these situations, the RHL
evaluation algorithm we have discussed so far need not terminate.

Consider, for example, the following PHL theory that axiomatizes pairs of maps
$f:A\rightleftarrows B:g$ such that $g(f(x))=x$ for all $x\in A$:

  1. 1.

$x:A\implies f(x)\downarrow$

  2. 2.

$y:B\implies g(y)\downarrow$

  3. 3.

$y=f(x)\implies g(y)=x$

Axiom 3 is lowered to the RHL axiom $f(x,y)\implies g(y,x)$, which is
surjective. Axioms 1 and 2, however, are non-surjective. Nevertheless, free
models of this theory over finite relational structures are always finite, as
the following construction of free models proves: Given sets $A,B$ and
relations $f\subseteq A\times B,g\subseteq B\times A$, one first identifies
elements within $A$ and $B$ according to the functionality axioms for $f$ and
$g$ and axiom 3. For each element $b\in B$ on which $g$ is not defined, we
then adjoin new elements to $A$ and extend $g$ accordingly to a total function
by axiom 2. Similarly, we then adjoin for each $a\in A$ on which $f$ is not
defined new elements to $B$ and extend $f$ accordingly to a total function by
axiom 1. Now every element in $B$ on which $g$ is not defined is of the form
$g(a)$ for some unique $a\in A$, so by axiom 3, we may extend $g$ to a total
function by setting $g(f(a))=a$. Now $f$ and $g$ are total functions and
$g\circ f$ is the identity function on $A$.

On first thought, we might thus hope RHL evaluation for this theory to
eventually reach a fixed point and terminate. Unfortunately, this is not the
case for the RHL evaluation algorithm described in Section 2.2. Consider the
iterations of evaluation with initial relational structure given by
$A=\\{a_{0}\\}$, $B=\emptyset$ and $f$ and $g$ entirely undefined:

  1. 1.

Axiom 1 matches on $a_{0}\in A$, resulting in a new element $b_{0}\in B$ and
the tuple $(a_{0},b_{0})\in f$.

  2. 2.

Axiom 2 matches on $b_{0}\in B$, and axiom 3 matches on $(a_{0},b_{0})$. The
former results in a new element $a_{1}\in A$ and the tuple $(b_{0},a_{1})\in
g$, while the latter results in the tuple $(b_{0},a_{0})\in g$.

  3. 3.

Axiom 1 matches on $a_{1}\in A$, and the implicit functionality axiom for $g$
matches on $(b_{0},a_{0}),(b_{0},a_{1})$. The former results in a new element
$b_{1}\in B$ and the tuple $(a_{1},b_{1})\in f$, while the latter results in
the equality $a_{0}=a_{1}$.

  4. 4.

Axiom 2 matches on $b_{1}\in B$, and the implicit functionality axiom for $f$
matches on $(a_{0},b_{0}),(a_{1},b_{1})$. The former results in a new element
$a_{2}\in A$ and the tuple $(b_{1},a_{2})\in g$, while the latter results in
the equality $b_{0}=b_{1}$.

  5. 5.

All further iterations alternate between variations of iterations 3 and 4.

What prevents termination for this theory is thus that the evaluation
algorithm matches all sequents at once: Observe that our proof that free
models are finite relies on applying sequents in some particular order. For
this particular theory, non-termination can be prevented by carefully stating
axioms so as to avoid alternating states, for example by replacing axioms 1
and 3 with $x:A\implies g(f(x))=x$.

However, the following variant of the RHL evaluation algorithm described in
Section 2.2 terminates on a wide range of RHL theories, including the theory
above. One splits the top-level evaluation loop into an inner loop responsible
for surjective sequents and an outer loop responsible for non-surjective
sequents. The algorithm thus alternates closing the relational structure under
all surjective sequents (which always terminates) and a single step of
matching and adjoining conclusions of non-surjective sequents. If eventually a
non-surjective step does not change the relational structure, then all
sequents are satisfied and evaluation terminates.

However, I expect there to be theories where termination depends on a
particular order in which non-surjective sequents are applied, and then this
simple approach does not suffice.

##  3 Optimizations

In this section, we consider optimizations of the naive RHL algorithm that we
discussed in Section 2.2. Most of these techniques are adapted from
optimizations that apply to Datalog evaluation, to the congruence closure
problem or to both. Implemented together, these optimizations allow us to
recover the fast congruence closure algorithm due to Downey et al. (1980) as a
special case of RHL evaluation for functionality axioms.

###  3.1 Semi-naive evaluation

Semi-naive evaluation is a common Datalog evaluation optimization. It exploits
the observation that matches of premises that were found in the previous
iteration need not be considered again because conclusions to these matches
have already been adjoined. A match has not been found in a previous iteration
if at least one of the atoms in the premise is matched with new data, i.e.
data was added only in the last iteration. To distinguish old data from new
data, we store for each relation and each sort lists of tuples or elements
that were added in the last iteration. An $n$-fold nested loop that matches
the premise of a sequent can now be replaced with $n$ copies, where in the
$i$th copy the $i$th loop iterates over new data only. For example, the nested
loop described in Section 2.1 enumerating the premise of
$\mathrm{Le}(u,v)\land\mathrm{Ge}(w,v)\land\mathrm{Le}(w,x)$ can be replaced
by the following three nested loops:

⬇

for (u, v) in structure.rels_new[Le] {

for (w, v1) in structure.rels_all[Ge] {

if v1 != v { continue; }

for (w1, x) in structure.rels_all[Le] {

if w1 != w { continue; }

matches.push([u, v, w, x]);

}

}

}

for (u, v) in structure.rels_all[Le] {

for (w, v1) in structure.rels_new[Ge] {

if v1 != v { continue; }

for (w1, x) in structure.rels_all[Le] {

if w1 != w { continue; }

matches.push([u, v, w, x]);

}

}

}

for (u, v) in structure.rels_all[Le] {

for (w, v1) in structure.rels_all[Ge] {

if v1 != v { continue; }

for (w1, x) in structure.rels_new[Le] {

if w1 != w { continue; }

matches.push([u, v, w, x]);

}

}

}

Observe that not only the conclusion application phase but also the
normalization phase can lead to new data: If an element in the tuple of some
relation changes as a result of normalization, then the tuple must be
considered as new tuple.

The optimized congruence closure algorithm described by Downey et al. (1980)
also implements semi-naive evaluation. Their pending list in algorithm 2.4
corresponds to our set of new tuples in the relation representing the graph of
a function.

Semi-naive evaluation is well-suited for online applications, where one
alternates RHL evaluation and ad-hoc manipulation. If this manipulation
consists only of adjoining data, then this data can be adjoined to the same
data structures that hold new data during RHL evaluation. The first iteration
of subsequent RHL evaluation need then only consider matches for this new data
instead of matches in the full relational structure.

###  3.2 Symmetries

Semi-naive matching of the premise of the functionality axiom for a (binary)
function results in two loops:

⬇

for (x0, x1, x2) in structure.rels_new[f] {

for (y0, y1, y2) in structure.rels_all[f] {

...

}

}

for (x0, x1, x2) in structure.rels_all[f] {

for (y0, y1, y2) in structure.rels_new[f] {

...

}

}

On the other hand, the congruence closure algorithm described by Downey et al.
(1980) requires a single loop only. Indeed, the second loop is unnecessary due
to a _symmetry_ in the functionality axiom $f(v_{0},v_{1},u)\land
f(v_{0},v_{1},w)\implies u\equiv w$. The symmetry is given by swapping $u$ and
$w$. This results in a semantically equivalent premise, and swapping the
variable has the same effect as swapping the two premise atoms. In such cases,
it suffices to consider matches where the first of the two atoms is
interpreted with new data. Another example where symmetries can be exploited
is the anti-symmetry axiom $\mathrm{Le}(u,v)\land\mathrm{Le}(v,u)\implies
u\equiv v$.

###  3.3 Indices and occurrence lists

Indices are meant to speed up the nested loops that enumerate matches of
premises. The idea is to replace each inner loop by an efficient sublinear
lookup with fixed projections. For example, matching the premise
$\mathrm{Le}(u,v)\land\mathrm{Le}(v,w)$ of a transitivity axiom can be sped up
with an index on the first projection. One thus maintains a map that allows
fast lookup of all tuples $(v,w)$ for fixed $v$. The premise can then be
enumerated as follows:

⬇

for (u, v) in structure.rels[Le] {

for (_, w) in structure.rels[Le].index[v] {

matches.push((u, v, w));

}

}

Indices are typically realized using variants of ordered search trees or hash
maps. They can be maintained over all iterations, or recreated before and
disposed immediately after the premise matching phase in each iteration.
Recreating indices requires less memory compared to maintaining indices, since
only indices needed to match a single sequent need to be stored in memory at
any time.

Fast Datalog engines often maintain indices over all iterations, which results
in faster execution at the expense of increased memory usage. If indices are
maintained over all iterations, new tuples must also be inserted into indices
during the conclusion application phase. For RHL evaluation, however, index
maintenance is problematic due to the normalization phase, in which elements
in relations are replaced by their canonical representatives if needed. When
using indices, they require normalization, too.

We turn again to the fast congruence closure algorithm described by Downey et
al. (1980, Section 2.4) to implement index normalization efficiently. Their
_signature table_ is a hash map index that speeds up matching premises of
functionality axioms. It is maintained throughout the iterations of the
congruence closure algorithm. Efficient normalization is implemented using
further data structures which we shall refer to as _occurrence lists_. An
occurrence list contains for each equivalence class the expression nodes which
have at least one child in the equivalence class. In the normalization step,
it suffices to normalize those tuples that occur in occurrence lists of
elements that ceased to be canonical representatives.

Occurrence lists can be adapted to RHL evaluation as follows. We associate to
each canonical representative a list of tuples in any relation in which the
canonical representative occurs. Tuples in occurrence lists need not be
normalized.

In the conclusion application phase, we insert tuples also in the occurrence
lists of each element of the inserted tuple. When merging two equivalence
classes, we save the element that ceases to be a canonical representative
along with its occurrence list for use during the following normalization
phase. The occurrence lists of the element that remains a canonical
representative is set to the concatenation of the two original occurrence
lists. Concatenation can be implemented asymptotically efficiently if
occurrence lists are realized as linked lists or rope data structures. In the
normalization phase, we remove each tuple in one of the occurrence lists we
saved earlier, normalize the tuple and reinsert it into each index.

When enforcing an equality during the conclusion phase, the algorithm
described in Downey et al. (1980, Section 2.4) chooses the element that
remains a canonical representative in a way that minimizes the amount of
normalization necessary: Thus, the element with longer occurrence lists should
remain canonical. This applies directly also to occurrence lists in RHL
evaluation.

To avoid normalizing tuples that were inserted in the current iteration, the
conclusion application phase can be split into an _equality application phase_
, where we only consider equalities in conclusions, and a _relation
application phase_ , where we only consider relation atoms. We then normalize
between the equality application phase and the relation application phase.
This has the benefit that new tuples need not be normalized directly after
insertion.

###  3.4 Functional projections

We say that the $i$th projection of a relation $r:s_{1}\times\dots\times
s_{n}$ in an RHL theory is _functional_ if the $i$th projection $x_{i}$ of
each tuple $(x_{1},\dots,x_{n})\in r$ is uniquely determined by the other
components $x_{1},\dots,x_{i-1},x_{i+1},\dots,x_{n}$ of the tuple. More
generally, we can consider a set $I$ of projections which are uniquely
determined by the complementary projections. As the name suggests, the
functionality axiom for an $n$-ary function asserts that the $(n+1)$th
projection of the graph of the function is functional. Another example are
injective functions, where the first $n$ projections of the graph depend
functionally on the $(n+1)$th projection.

When indices are maintained on a relation with a functional projection,
equality constraints can be generated already during insertion into the index
instead of later during the matching phase. For example, if $r$ is an
$(n+1)$-ary relation representing the graph of a function, then an index on
the first $n$ arguments can be maintained to match the premise of the
functionality axiom. Without consideration of functionality of the $(n+1)$th
projection, we expect the index to allow lookups of _lists_ of tuples for
fixed value of the first $n$ projections. Due to the functional dependency, we
can instead enforce that lookups result into at most one tuple. Whenever a
second tuple would be inserted into the index which would violate this
property, then we generate equality constraints according to functional
projections instead. These equalities are then enforced during the next
conclusion application phase.

The _signature table_ hash map in the efficient congruence closure algorithm
described by Downey et al. (1980, Section 2.4) can be understood as an index
with functional projection optimization.

##  4 Applications

In this Section, we discuss two applications of RHL and PHL evaluation to the
implementation of programming languages: Steensgaard’s points-to analysis
(Section 4.1) and type inference (Section 4.2).

###  4.1 Steensgaard’s points-to analysis

Points-to-analysis aims to bound the set of heap objects a variable in a
program can point to. The two well-known approaches are due to Andersen and
Steensgaard. Both algorithms identify heap objects with their allocation
sites, i.e. the program expressions that allocate objects. The Andersen and
Steensgaard analyses thus give an over-approximating answer to the question of
whether a given variable $x$ can point to an object that was allocated in
expression $e$.

Both analyses must consider the case where a variable $x$ is a assigned to a
variable $y$. Andersen-style analysis computes for each variable $x$ a set of
objects $e$ that $x$ can point to such that the following properties hold:

  1. 1.

If there is a statement that assigns an allocating expression $e$ to a
variable $x$, then $x$ can point to $e$.

  2. 2.

If a variable $y$ can take the value of a variable $x$ (e.g. as a result of an
assignment or a function call), and $x$ can point to $e$, then $y$ can point
to $e$.

A minimal implementation of Andersen-style analysis using Datalog populates
input relations $\mathrm{Alloc}(x,e)$ and $\mathrm{Assign}(x,y)$ with data
derived from the program source code. The rules above governing the
$\mathrm{PointsTo}(x,e)$ relation are then encoded in Datalog as follows:

  1. 1.

$\mathrm{Alloc}(x,e)\implies\mathrm{PointsTo}(x,e)$

  2. 2.

$\mathrm{Assign}(x,y)\land\mathrm{PointsTo}(x,e)\implies\mathrm{PointsTo}(y,e)$

To summarize, Andersen’s algorithm enforces _subset constraints_ : If a
variable $y$ can take the value of a variable $x$, either through a function
call or a direct assignment, then the points-to set of $x$ is a subset of the
points-to set of $y$.

Steensgaard’s algorithm is a less precise but typically faster variation of
Andersen’s algorithm. It is based on _equality constraints_. Thus if a
variable $y$ can take the value of a variable $x$, then Andersen’s algorithm
_equates_ the points-to sets of $x$ and $y$. A direct implementation of
Steensgaard’s algorithm maintains a union-find data structure on the variables
of a program, and a mapping that assigns to each canonical representative a
points-to set of heap allocations. The algorithm scans the program source code
and performs the following actions:

  1. 1.

For each statement that assigns an allocation expression $e$ to a variable
$x$, add $e$ to the points-to set of the canonical representative of $x$.

  2. 2.

If a variable $y$ can take the value of a variable $x$, unify the equivalence
classes of $x$ and $y$. The points-to set of the unified equivalence class is
the union of the points-to sets of the classes of $x$ and $y$.

Steensgaard’s algorithm is strictly less precise than Andersen’s, but it
typically requires less memory, since only one points-to set needs to be
maintained for every equivalence class of variables. To encode Steensgaard’s
algorithm in RHL, we can simply replace rule 2 above in Andersen’s analysis
with the rule

$\mathrm{Assign}(x,y)\implies x\equiv y$ (8)

to enforce equality constraints.

###  4.2 Type inference

Type inference (or type reconstruction) is the task of assigning types to
variables and expressions based on their usage in a program fragment. The
constraint-based typing algorithm for the simply typed lambda calculus
described in Pierce (2002, 22.3, 22.4) assigns to each term a separate,
initially unrestricted type variable. It then collects constraints on type
variables according to the usage and definition of the corresponding terms.
This is accomplished by considering typing rules and their inverses. For
example, based on the application typing rule

$\inferrule{k:\sigma\rightarrow\tau s:\sigma}{k\,s:\tau}$ (9)

we infer the following constraints from a term $t_{2}=t_{0}\,t_{1}$:

  1. 1.

If $t_{0}$ has type $S\rightarrow T$, then $t_{1}$ has type $S$.

  2. 2.

Conversely, if $t_{1}$ has type $S$, then $t_{0}$ has type $S\rightarrow T$
for some $T$.

  3. 3.

If $t_{0}$ has type $S\rightarrow T$, then $t_{2}$ has type $T$.

  4. 4.

Conversely, if $t_{2}$ has type $T$, then $t_{0}$ has type $S\rightarrow T$
for some $S$.

The implicit existentials in constraints 2 and 4 generate new type variables
$T$ and $S$, which must be chosen fresh for each instance of the constraint.
In the following unification step, the generated constraints are checked for
compatibility, and if so the most general substitution of type variables is
created that satisfies all the constraints. For example, for the fragment
$x\,y$ for variables $x$ and $y$, the algorithm outputs the substitution
$[T_{0}\mapsto(T_{1}\rightarrow T_{2}),T_{1}\mapsto T_{1},T_{2}\mapsto
T_{2}]$, where $T_{0},T_{1}$ and $T_{2}$ are the type variables initially
assigned to $x,y$ and $x\,y$.

This inference procedure can be implemented in PHL as follows. We introduce
sorts $\mathrm{Tm}$ of terms and $\mathrm{Ty}$ of types. Each $n$-ary type or
term constructor corresponds to an $n$-ary PHL function. For example, function
types are encoded as binary function symbol
$\mathrm{Fun}:\mathrm{Ty}\times\mathrm{Ty}\rightarrow\mathrm{Ty}$ and
application as a function
$\mathrm{Tm}\times\mathrm{Tm}\rightarrow\mathrm{Tm}$. To enforce injectivity
of type constructors, we introduce inverse functions for each parameter of a
type constructor. For function types, we add functions
$\mathrm{Dom}:\mathrm{Ty}\rightarrow\mathrm{Ty}$ and
$\mathrm{Cod}:\mathrm{Ty}\rightarrow\mathrm{Ty}$ and enforce axioms that
$\mathrm{Dom}$ and $\mathrm{Cod}$ are indeed inverses to $\mathrm{Ty}$: Dom(κ)
↓⟹Cod(κ) ↓Cod(κ) ↓⟹Dom(κ) ↓
σ= Dom(κ) ∧τ= Dom(κ) ⟹κ= Fun(σ, τ)
κ= Fun(σ, τ) ⟹Dom(κ) = σ∧Cod(κ) = τ Thus $\mathrm{Dom}$ and $\mathrm{Cod}$ are
defined on the same set of types: Those of the form
$\mathrm{Fun}(\sigma,\tau)$ for types $\sigma$ and $\tau$.

To detect violations of joined injectivity of type constructors, we introduce
a nullary predicate $\bot$ and rules such as Fun(-, -) ≡List(-) ⟹⊥() for every
pair of distinct type constructors, for example function types and list types.
We always arrange $\bot$ to be empty before PHL evaluation, so that $\bot$ is
inhabited after evaluation if and only if a violation of joined injectivity
was inferred.

We encode the typing relation $t:\tau$ as a function
$\mathrm{TmTy}:\mathrm{Tm}\rightarrow\mathrm{Ty}$ instead of a relation
because each term has a unique type. The axiom
$t:\mathrm{Tm}\implies\mathrm{TmTy}(t)\downarrow$ enforces that each term has
a type. During evaluation, this non-surjective rule introduces a fresh
identifier as type of each term if necessary.

Finally, we encode term constructors as PHL functions and add axioms according
to inference rules and their inverses. For example, the typing rule (9) of
function application results in a PHL function
$\mathrm{App}:\mathrm{Tm}\times\mathrm{Tm}\rightarrow\mathrm{Tm}$ and the
following PHL axioms governing it, corresponding to the constraints 1 – 4
above:

  1. 1.

$\mathrm{App}(t_{0},t_{1})\downarrow\land\mathrm{TmTy}(t_{0})=\mathrm{Fun}(\sigma,-)\implies\mathrm{TmTy}(t_{1})=\sigma$

  2. 2.

$\mathrm{App}(t_{0},t_{1})\downarrow\land\mathrm{TmTy}(t_{1})=\sigma\implies\mathrm{Dom}(\mathrm{TmTy}(t_{0}))=\sigma$

  3. 3.

$t_{2}=\mathrm{App}(t_{0},t_{1})\land\mathrm{TmTy}(t_{0})=\mathrm{Fun}(-,\tau)\implies\mathrm{TmTy}(t_{2})=\tau$

  4. 4.

$t_{2}=\mathrm{App}(t_{0},t_{1})\land\mathrm{TmTy}(t_{2})=\tau\implies\mathrm{Cod}(\mathrm{TmTy}(t_{0}))=\tau$

Observe that the conclusions of axioms 2 and 4 assert that domains and
codomains of certain types exist, which together with our axioms for
$\mathrm{Dom}$ and $\mathrm{Cod}$ implies that these types are function types.
If necessary, fresh type identifiers are adjoined during PHL evaluation by the
non-surjective axioms asserting that the $\mathrm{Dom}$ and $\mathrm{Cod}$
functions are defined on the same set of types.

With the PHL theory modeling the type system at hand, the full type inference
algorithm can now be implemented in three steps:

  1. 1.

Populate a relational structure based on the program fragment: We adjoin a
unique term identifier for each term in the program fragment and add entries
in the relations representing graphs of term constructors.

  2. 2.

Close the relational structure under the axioms described above.

  3. 3.

If the $\bot$ relation contains an element, output an error. Otherwise, there
exists for each type identifier $T$ at most one type constructor $\mu$ and an
entry of the form $(T_{1},\dots,T_{n},T)$ with $T$ as last component in the
relation corresponding to $\mu$. Expand each type identifier recursively into
a maximal syntax tree according to such entries. Output the maximal syntax
tree representing $\mathrm{TmTy}(t)$ for each term $t$ in the input program
fragment.

##  5 Conclusion

Using Datalog to implement type checking and inference, as we sketched in
Section 4.2, is not a new idea. For example, the blog post Matsakis  discusses
an implementation of Rust’s trait system using Datalog. One of the issues
raised there is that Rust’s associated types require reasoning about
equalities of types. A similar issue would arise for Haskell’s type families.
The solution proposed in the blog post is to combine Datalog with a
normalization algorithm. RHL’s built-in equality might offer a declarative
alternative to normalization that applies also in situations where no strongly
normalizing rewrite system is available.

Typing rules are typically specified using the notation of natural deduction
(e.g. the application typing rule (9)). Apart from syntactic differences, the
structure of such rules and their semantics correspond almost precisely to
PHL. Indeed, it is generally understood that many type systems can be encoded
as _essentially algebraic theories_ (Adamek and Rosicky, 1994, Chapter 3.D),
which have the same descriptive strength as epic PHL. From this perspective,
program fragments can be identified with elements of the _initial model_ of
the PHL theory axiomatizing the type system, i.e. the free model over the
empty relational structure.

These conceptual connections and the example in Section 4.2 suggest that PHL
and RHL evaluation have the potential to assume a role in the implementation
of programming languages paralleling that of parser generators: Where parser
generators produce parsers from grammars, RHL evaluation engines produce type
checkers from type systems.

## References

  * Adamek and Rosicky (1994) J. Adamek and J. Rosicky.  _Locally Presentable and Accessible Categories_.  Cambridge University Press, mar 1994.  doi: 10.1017/cbo9780511600579.  URL https://doi.org/10.1017/cbo9780511600579.
  * Bidlingmaier (2023) M. E. Bidlingmaier.  Algebraic semantics of Datalog with equality, 2023.  URL https://arxiv.org/abs/2302.03167.
  * Cocke and Schwartz (1970) J. Cocke and J. T. Schwartz.  _Programming Languages and Their Compilers_.  Courant Institute of Mathematical Sciences, New York, 1970.  Preliminary notes, second revised version.
  * Downey et al. (1980) P. J. Downey, R. Sethi, and R. E. Tarjan.  Variations on the common subexpression problem.  _Journal of the ACM_ , 27(4):758–771, oct 1980\.  doi: 10.1145/322217.322228.  URL https://doi.org/10.1145/322217.322228.
  * Hu et al. (2021) X. Hu, J. Karp, D. Zhao, A. Zreika, X. Wu, and B. Scholz.  The choice construct in the Soufflé language.  In _Programming Languages and Systems_ , pages 163–181. Springer International Publishing, 2021.  doi: 10.1007/978-3-030-89051-3˙10.  URL https://doi.org/10.1007/978-3-030-89051-3_10.
  * (6) N. Matsakis.  Lowering Rust traits to logic.  http://smallcultfollowing.com/babysteps/blog/2017/01/26/lowering-rust-traits-to-logic/.  Accessed: 2023-01-30.
  * Nappa et al. (2019) P. Nappa, D. Zhao, P. Subotic, and B. Scholz.  Fast parallel equivalence relations in a Datalog compiler.  In _2019 28th International Conference on Parallel Architectures and Compilation Techniques (PACT)_. IEEE, sep 2019.  doi: 10.1109/pact.2019.00015.  URL https://doi.org/10.1109/pact.2019.00015.
  * Palmgren and Vickers (2007) E. Palmgren and S. Vickers.  Partial Horn logic and cartesian categories.  _Annals of Pure and Applied Logic_ , 145(3):314–353, mar 2007.  doi: 10.1016/j.apal.2006.10.001.  URL https://doi.org/10.1016/j.apal.2006.10.001.
  * Pierce (2002) B. C. Pierce.  _Types and Programming Languages_.  The MIT Press. MIT Press, London, England, jan 2002.
  * (10) The Eqlog Authors.  Eqlog.  https://github.com/eqlog/eqlog.  Accessed: 2023-02-07.
  * Willsey et al. (2021) M. Willsey, C. Nandi, Y. R. Wang, O. Flatt, Z. Tatlock, and P. Panchekha.  Egg: Fast and extensible equality saturation.  _Proc. ACM Program. Lang._ , 5(POPL), jan 2021.  doi: 10.1145/3434304.  URL https://doi.org/10.1145/3434304.