Algebraic Semantics of Datalog with Equality
Abstract
We discuss the syntax and semantics of relational Horn logic (RHL) and partial Horn logic (PHL).
RHL is an extension of the Datalog programming language that allows introducing and equating variables in conclusions.
PHL is a syntactic extension of RHL by partial functions and one of the many equivalent notions of essentially algebraic theory.
Our main contribution is a new construction of free models.
We associate to RHL and PHL sequents classifying morphisms, which enable us to characterize logical satisfaction using lifting properties.
We then obtain free and weakly free models using the small object argument.
The small object argument can be understood as an abstract generalization of Datalog evaluation.
It underpins the implementation of the Eqlog Datalog engine, which computes free models of PHL theories.
1 Introduction
Datalog [
10] is a programming language for logical inference from Horn clauses.
Abstracting from concrete syntax, a Datalog program consists of the following declarations:

A set of
sort symbols .

A set of
relation symbols and their
arities .

A set of
sequents (or
rules, or
axioms) of the form
where
is a sortcompatible list of variables for each
, and each variable in the conclusion also appears in the premise.
A
fact is an expression of the form
where each
is a constant symbol of the appropriate sort.
Given a Datalog program and a set of input facts, a
Datalog engine computes the set of facts that can be derived from the input facts by repeated application of sequents.
A typical example of a problem that can be solved using Datalog is the computation of the transitive closure of a (directed) graph.
Graphs are given by a binary relation
of edges among a sort
of vertices.
The only axiom of transitive graphs is the transitivity axiom
A set of input facts for this Datalog program is given by a set of expressions
where
are constant symbols.
We identify such data with the data of a graph with vertices
and edges
.
Every finite graph in which every vertex appears in some edge arises in this way, so we conflate such graphs and sets of facts.
(Standard Datalog does not support constants that do not appear in a fact.)
Given the Datalog program for transitive graphs and a corresponding set of facts, a Datalog engine enumerates all matches of the premise of the transitivity axiom, i.e. all substitutions
such that the substituted conjuncts of the premise,
and
, are in the set of input facts.
For each such substitution, the Datalog engine then adds the substitution
of the conclusion to the set of facts.
This process is repeated until the set of facts does not increase anymore; that is, until a fixed point has been reached.
This final set of facts now corresponds to a transitive graph.
Datalog has seen renewed interest in recent years for the implementation of program analysis tasks [
9,
8,
7] such as pointsto analysis.
One encodes abstract syntax trees derived from the program source code as relations, on which one then runs Datalog programs.
The advantage of this approach over more adhoc methods is that implementation time can be reduced significantly, and that different analyses can be integrated seamlessly.
Equality saturation has garnered interest as a program optimization technique in recent years [
14].
The idea is to insert expressions that should be optimized into an egraph, and then close the egraph under a set of rewrite rules.
Egraphs allow sharing nodes that occur as children more than once, so that a large number of expressions can be stored.
Furthermore, egraphs can be efficiently closed under congruence, i.e. equivalence can be propagated from subexpressions to their parents.
After a suitable number of rewrite rules have been applied and the egraph has been closed under congruence, one selects a suitable equivalent expression from the equivalence class of the expression one is interested in according to a cost function.
Crucially, equality saturation makes considerations about the order of rewrites unnecessary.
In this paper, we study languages and corresponding semantics that combine and subsume both Datalog and the applications of egraphs outlined above.
To that end, we extend Datalog by
equality, that is, the ability of enforce an equality
in the conclusion of a sequent.
One example is the ordertheoretic antisymmetry axiom
which is not valid Datalog due to the equality atom
, but allowed in our extension.
If during evaluation of RHL an equality among constants
and
is inferred, we expect the system to conflate
and
in all contexts henceforth.
In other words, inferred equality should behave as congruence with respect to relations.
For example, the premise
of the transitivity axiom should match
if the equality
has been inferred earlier.
In addition to a set of derived facts, we also expect evaluation to yield an equivalence relation on each sort, representing inferred equalities.
Relational Horn logic extends Datalog further by sort quantification, i.e. variables matching any element of a sort, and by variables that only occur in a conclusion.
We interpret the latter as existentially quantified:
If the premise of a sequent matches and the conclusion contains a variable that is not bound in the premise, then we expect the Datalog engine to create new identifiers of the given sort if necessary to ensure that the conclusion holds.
Partial Horn logic, originally due to [
5], is a layer of syntactic sugar on top RHL, i.e. a purely syntactic extension with the same descriptive power.
PHL adds function symbols
, which desugar into relations
representing the graph of the function and the functionality axiom
In positions where RHL expects variables (e.g. arguments of predicates or in equations), PHL allows also composed terms.
A composed term is desugared into a fresh variable corresponding to the result of applying the function and an assertion about the graph of the function.
These features enable the implementation of algorithms in PHL for which Datalog unsuitable, for example congruence closure [
3], Steensgaard's pointsto analysis [
2] and type inference [
13, 22.3, 22.4].
In each case, evaluation of the PHL theory encoding the problem domain yields the same algorithm as the standard domainspecific algorithm.
However, the present paper focuses on the semantics of PHL and RHL, whereas an evaluation algorithm and the applications above are presented in [
11].
Partial Horn logic is one of the equivalent notions of
essentially algebraic theory [
6, Chapter 3.D].
Essentially algebraic theories generalize the betterknown algebraic theories of universal algebra by allowing functions to be partial.
Crucially, the
free model theorem of universal algebra continues to hold also for essentially algebraic theories.
Free models are the basis of our semantics of PHL evaluation.
We show that free models can be computed using the
small object argument, which we shall come to understand as an abstract generalization of Datalog evaluation.
In brief, the relation of free models and Datalog evaluation can be understood for the transitivity Datalog program outlined above as follows.
We have seen that input data for this Datalog program represent certain graphs
, while output data represent transitive graphs
.
The two graphs
and
share the same set of vertices
, which is the set of constant symbols that appear in the set of input facts.
Intuitively,
arises from
by adding data that must exist due to the transitivity axiom but no more.
Let us rephrase the relation between
and
using category theory.
Denote by
the category of graphs:
A morphism
between graphs is a map
that preserves the edge relation.
Thus if
, then we must have
.
The requirement that the output graph
arises from the input
solely by application of the transitivity sequent can now be summarized as follows:
Proposition 1.
Let
be the output graph generated from evaluating the transitivity Datalog program on a finite input graph
.
Then
is the free transitive graph over
.
Proof.
First we must exhibit a canonical graph morphism
.
As
and
share the same set of vertices, we choose
simply as identity map on
.
Note that the identity on
is indeed a graph morphism
because
.
Now we must show that for all graph morphisms
where
is a transitive graph, there exists a unique graph morphism
such that the following triangle commutes:
Because
is the identity map, it suffices to show that
also defines a graph morphisms
; uniqueness of
follows from surjectivity of
.
Recall that
arises from repeatedly matching the premise of the transitivity axiom and adjoining its conclusion.
Thus there is a finite chain
where for each
there exist
such that
(1)
(1)
By induction, it suffices to show for all
that
is a graph morphism
assuming that
is a graph morphisms
.
Choose
such that
and
(1) is satisfied.
Because
is a graph morphism
, we have
.
Because
is transitive, it follows that
.
Thus
preserves the edge
and hence constitutes a graph morphism
.
Denote by
the full subcategory of
given by the transitive graphs.
The inclusion functor
has a left adjoint, a
reflector, which is given by assigning a graph to its transitive hull.
Thus Proposition
1 shows that the transitivity Datalog program computes the reflector.
Our primary goal in this paper is to explore and extend a semantics of PHL along these lines.
Outline and Contributions.
In Section
2, we review the
small object argument [
12, Theorem 2.1.14] as a method of computing weak reflections into subcategories of injective objects.
We introduce
strong classes of morphisms, for which the small object argument specializes to the
orthogonalreflection construction [
6, Chapter 1.C] and produces a reflection into orthogonal subcategories.
In Section
3, we introduce
relational Horn logic (RHL).
RHL extends Datalog with sort quantification, with variables that occur only in the conclusion, and with equations.
Input data of Datalog programs generalize to finite
relational structures, and output data generalize to
models, i.e. relational structures that satisfy all sequents.
Our poof of the existence of free or weakly free models associates to each RHL sequent a classifying morphism of relational structures.
Satisfaction of the sequent can be characterized as lifting property against the classifying morphism.
The small object argument now shows the existence of weakly free models.
From this perspective, we may thus understand the small object argument as an abstract formulation of Datalog evaluation.
In Section
4, we extend RHL by function symbols to obtain
partial Horn logic (PHL).
By identifying each function symbol with a relation symbol representing its graph and adding a functionality axiom, every PHL theory gives rise to a relational Horn logic theory with equivalent semantics.
For
epic PHL theories, where all variables must be introduced in the premise of a sequent, the associated RHL theory is strong.
Conversely, we show that the semantics of every strong RHL theory can be recovered as semantics of an epic PHL theory.
This justifies the usage of epic PHL as an equally powerful but syntactically betterbehaved language compared to strong RHL.
The results of this paper serve as semantics of
Eqlog, a Datalog engine that computes free models of epic PHL theories.
Eqlog's algorithm is based on an efficient implementation of the small object argument that combines optimized Datalog evaluation (seminaive evaluation and indices) with techniques used in congruence closure algorithms.
The present paper focuses on the semantics of PHL and RHL, whereas the evaluation algorithm employed by Eqlog is presented in [
11].
Independently of Eqlog and the work presented there, members of the Egg [
14] community have recently created the
Egglog tool, which combines Datalog with egraphs and is based on very similar ideas as those of Eqlog.
2 The Small Object Argument
This section is a review of the small object argument, which we shall in later sections come to understand as an abstract description of Datalog evaluation.
The concepts we discuss here are not new and are in fact widely known among homotopy theorists; see for example [
12] for a standard exposition.
A minor innovation is our consideration of
strong sets:
Sets of morphisms for which injectivity coincides with orthogonality.
For strong sets, the small object argument yields a reflection into the orthogonal subcategory where in general we would obtain only a weak reflection into the injective subcategory.
The
orthogonalreflection construction [
6, Chapter 1.C] produces a reflection into the orthogonal subcategory for arbitrary sets of morphisms
.
We show that every set of morphism
can be extended to a strong set
such that
and
induce the same orthogonality class.
The small object argument for
now specializes to the orthogonalreflection construction for
.
Thus, the concept of strong morphisms can be used to understand the orthogonalreflection construction as a specialized variation of the small object argument.
Fix a cocomplete locally small category
for the remainder of this section.
We reserve the word
set for a small set, while
class refers to a set in a larger settheoretic universe that contains the collection of objects in
.
All colimits of setindexed diagrams in
exist, while colimits of classindexed diagrams need not exist.
Definition 2.
Let
be a morphism and let
be an object.
We write
and say that
is
injective to
if for all maps
there exists a map
such that
commutes.
If furthermore
is unique for all
, then we write
and say that
is
orthogonal to
.
If
is a class of morphisms, then we write
if
for all
, and
if
for all
.
The full subcategories given by the injective and orthogonal objects, respectively, are denoted by
and
.
We call
the
injectivity class of
and
the
orthogonality class of
.
Definition 3.
A class
of morphisms is called
strong if
.
One of the main sources of strong sets is the following proposition:
Proposition 4.
Let
be a class of epimorphisms.
Then
is strong.
Proof.
This follows immediately from rightcancellation.
Another source of strong sets is the following proposition.
It lets us reduce questions about orthogonality classes to strong injectivity classes.
Proposition 5.
Let
be a class of morphisms.
Then there exists a superclass
such that
is strong and
.
If
is a set, then
can be chosen as set.
Proof.
Let
be a morphism in
.
Then for each object
, the data of a single map
and two maps
such that
commutes for
is in bijective correspondence to a map
.
Let
be the canonical map that collapses the two copies of
into one.
Then
if and only if there exists a map
such that
commutes.
The map
is an epimorphism.
Thus if
exists, then it exists uniquely, and
.
It follows that
is orthogonal to
if and only if
is injective to both
and
.
The desired class
can thus be defined by
.
Definition 6.
A
sequence of morphisms is a diagram of the form
for a countable set
of morphisms.
The
(infinite) composition of a sequence of morphisms
is the canonical map
to the colimit of the sequence.
Note that the composition of a sequence of morphisms is uniquely determined only up to a choice of colimit.
Definition 7.
Let
be a class of morphisms.
The class
of
relative cell complexes is the least class of morphisms such that the following closure properties hold:

.

is closed under coproducts.
That is, if
is a family of morphisms indexed by some set
and
for all
, then
is in
.

is closed under pushouts.
That is, if
is a pushout square and
, then
.

is closed under composition of sequences.
That is, if
is a sequence of morphisms
with composition
, then
.
Proposition 9.
Let
be a class of morphisms.
Define classes of morphisms
as follows:
Then
.
Proof.
Coproducts, pushouts and compositions of sequences are all defined via colimits.
Because colimits commute with colimits,
is closed under coproducts, pushouts and compositions of sequences.
It follows that
, hence
.
Proposition 10.
Let
be a class of morphisms.
Then
and
.
Proof.
If
is an inclusion of classes of morphisms, then in general
and
.
This proves the inclusions
.
Conversely, it suffices to show for
that the class
satisfies the closure properties
1 
4 of Definition
7, and similarly for orthogonality.
This is routine.
For example, closure under pushouts can be proved as follows.
Let
be injective to
, let
be a pushout of
, and let
be an arbitrary morphism.
The lift
can then be obtained from a lift
and the universal property of the pushout as depicted in the following commuting diagram:
If the lift
is unique, then also
is unique by uniqueness of the morphism induced by the universal property of the pushout.
Definition 11.
Let
be a full subcategory.
A
weak reflection of an object
into
is a map
such that
and every map
with
factors via
.
If the factorization is unique for all
, then
is a
reflection.
A
(weak) reflector consists of a functor
and a natural transformation
such that
is a (weak) reflection for all
.
The subcategory
is
(weakly) reflective in
if there exists a (weak) reflector.
Proposition 12.
Let
be a class of morphisms.
Let
be a relative
cell complex, and let
be a map with
.
Then there is a map
such that
.
If furthermore
is strong, then
is unique.
Proof.
This follows from the fact that the class of morphisms
for which the proposition holds satisfies properties
1 
4 of Definition
7.
Proposition 13.
Let
be a class of morphisms.
Let
be a relative
cell complex such that
.
Then
is a weak reflection into
.
If
is strong, then
is a reflection.
Proof.
By Proposition
12.
Definition 14.
An object
is
finitely presentable if the homfunctor
preserves filtered colimits.
Proposition 15 (Small Object Argument: Property).
Let
be a class of morphisms with finitely presentable domains and codomains.
Let
be a sequence in
such that the following holds:

is a relative
cell complex for all
.

For all
in
,
and maps
, there exists a map a map
for some
such that
commutes.
Then the infinite composition
of the
is a weak reflection into
.
If
is strong, then
is a reflection.
Proof.
Because
is closed under infinite composition, the map
is a relative
cell complex.
Thus by Proposition
13, it suffices to show that
is in
.
Let
be in
and let
.
Because
is finitely presentable, there exists
and
such that
factors as
.
By assumption
2, there exist
and
that commutes with
,
and
.
Thus if we define
as composition
, then
.
Proposition 16 (Small Object Argument: Existence).
Let
be a set of morphism with finitely presentable domains and codomains, and let
be an object.
Then there exists a sequence
satisfying the conditions of Proposition
15.
In particular,
is a (weakly) reflective subcategory of
.
Proof.
It suffices to construct a relative
cell complexes
such that for every
in
and
, there exists a commuting diagram
We then obtain the desired sequence by induction.
Let
be the set of pairs
, where
is a morphism in
and
.
Note that
is a set because
is a set and
is a set for all
.
Now let
be the map defined by the following pushout diagram:
Here the top map is the coproduct
, and the left vertical map
is induced by the universal property of coproducts.
Proposition 17.
Let
be a strong set of morphisms, and let
.
Denote by
the reflection of
into
.
Then the following equations among injectivity and orthogonality classes hold:
Proof.
Let
be orthogonal (equivalently: injective) to
.
Then there is a bijective correspondence between solutions to the following lifting problems:
Here
is an arbitrary map, and
is induced from
by the universal property of
and
being orthogonal to
.
3 Relational Horn Logic
Relational Horn Logic (RHL) is a superset of Datalog.
Most notably, RHL allows equations, and in particular equations in conclusions.
Our semantics of RHL are based on
relational structures, which we introduce in Section
3.1.
In Section
3.2, we then consider syntax and semantics of RHL.
We show that RHL models can be characterized using lifting properties against
classifying morphisms.
This enables us to apply the small object argument to prove the existence of (weakly) free models, in close analogy to Datalog evaluation.
In Section
3.3, we prove a completeness result for the descriptive power of RHL:
Every finitary injectivity class of relational structures can be obtained as semantics of an RHL theory.
In Section
3.4, we identify in detail the subset of RHL that corresponds to Datalog.
We then explain how the computation of free RHL models can be reduced to evaluation of Datalog with minor extensions via the
setoid transformation.
3.1 Relational Structures
Definition 18.
A
relational signature is given by the following data:

A set
of
sort symbols.

A set
of
relation symbols.

A map that assigns to each relation symbol
an
arity
of sort symbols
for
.
Definition 19.
Let
be a relational signature.
A
relational structure consists of the following data:

For each sort symbol
, a
carrier set .

For each relation symbol
with arity
, a relation
.
A
morphism of relational structures consists of functions
for
that are compatible with the relations
and
for all
.
That is, we require that if
for some relation symbol
, then
.
The category of relational structures is denoted by
.
When no confusion can arise, we suppress sort annotations.
Thus if
is a relational structure, then we write
to mean that
for some
.
Similarly, if
is a morphism of relational structures and
, then we often denote the image of
under
by
instead of
.
If the signature
is clear from context, we abbreviate
as
.
There is an evident forgetful functor
to the
ary product of the category of sets, which is given by discarding the relations.
When we mention the
carrier sets of a relational structure, we mean the result of applying this forgetful functor.
Proposition 20.
Let
and
be relational signatures such that
extends
, in the sense that
and
and
assign the same arities to relation symbols
.
Then the evident forgetful functor
has both a left adjoint and a right adjoint.
Both adjoints are sections to the forgetful functor, that is, both composites
are identity functors.
Proof.
Let
be a relational
structure.
Let
and let
be in
.
The left adjoint extends
to a relational
structure
by
and
.
The right adjoint extends
to a relational
structure
such that
is a singleton set and
.
Proposition 21.
Let
be a relational signature.
Then
is complete and cocomplete, and the forgetful functor
preserves limits and colimits.
Proof.
Limit and colimit preservation follows from Proposition
20, since the forgetful functor is induced by the extension of signatures
.
Limits commute with other limits and in particular products.
Thus, limits of relational structures can be constructed as limits of carriers endowed with the limits of relation sets.
The construction of colimits is more involved because products do not generally commute with quotients.
Let
be a diagram of relational structures.
We define the carrier sets of our candidate colimit structure
by the colimit of carrier sets.
That is,
for all
.
We obtain evident maps
for all objects
in
and
.
Let
be a relation symbol.
Then we define
as union over the images of the
.
Thus,
where
.
Definition 22.
Let
be a relational signature.
A relational
structure
is
finite if
that is, if all the
and
are finite and almost always empty.
Proposition 23.
Let
be a relational signature.
Then a relational
structure is finite if and only if it is a finitely presentable object in
.
Proof.
Let
be a finite relational structure and let
be a map to a filtered colimit.
Then the image of each element
is represented by some element
.
Since
contains only finitely many elements and
is directed, we may assume that
is constant over all
.
For each tuple
for some
we have that
.
Since there are only finitely many
, we may again increase
so that
.
Now
factors via
.
Conversely, if a relational structure
is not finite, then there exists a strictly increasing sequence of relational substructures
such that
.
Then the canonical map
does not factor via any
, so
is not finitely presentable.
3.2 Syntax and Semantics
Fix a relational signature
.
We assume a countable supply of variable symbols
, each annotated with a sort
.
Definition 24.
An
RHL atom is an expression of one of the following forms:

A
relation atom , where
is a relation symbol and the
are variables of sort
for all
.

A
sort quantification atom where
is a variable.

An
equality atom , where
and
are variables of the same sort.
An
RHL formula is a finite conjunction
of RHL atoms
.
An
RHL sequent is an implication
of RHL formulas
.
An
RHL theory is a set of RHL sequents.
Observe that, since we assume that each variable has an intrinsically associated sort, annotating sort quantification atoms
with a sort
would be redundant.
We reserve the
symbol for RHL syntax, while the
symbol is used for metatheoretical equality.
We always assume that metatheoretical equality binds weaker than RHL connectives, so that
states that
is equal to the syntactic object
, and
states that
is equal to the sequent
.
Definition 25.
Let
be a relational structure.
An
interpretation of a set of variables in
is a map
that assigns to each variable
of sort
an element
.
An
interpretation of an RHL atom in
is an interpretation
of the variables occurring in
such that one of the following conditions holds:

is a relation atom and
.

is a sort quantification atom, without further assumptions.

is an equality atom and
.
An
interpretation of an RHL formula in
is an interpretation of the variables occurring in
that restricts to an interpretation of
for each
.
A relational structure
satisfies an RHL sequent
if each interpretation of
in
can be extended to an interpretation of
in
.
A
model of a theory
is a relational structure that satisfies all sequents in
.
The
category of models is the full subcategory of relational structures given by the models of
.
Definition 26.
We associate to each RHL atom
a
classifying relational structure and a
generic interpretation of
in
as follows:

If
where
, then the carriers of
are given by distinct elements
and a single tuple
.
The relations
for
are empty.

If
, where
has sort
, then
contains a single element
.
All other carrier sets and all relations are empty.

If
, where
and
have sort
, then
contains a single element
.
All other carrier sets and all relations are empty.
Let
be an RHL formula.
The
classifying relational structure of
is the quotient
where
is the relation given by
for all
and variables
occurring in both
and
, and the generic interpretation
is the amalgamation of the interpretations
.
Proof.
If
, then
is an interpretation of
in
.
Conversely, let
for RHL atoms
.
Then every interpretation
of
restricts to an interpretation of
for each
.
The carrier sets of
are defined using the variables of
, which defines an evident map
.
Since the restrictions of
to the variables in each
agree on variables that occur simultaneously in two atoms, the individual maps
glue to a map
.
Definition 28.
Let
be an RHL sequent.
The
classifying morphism of
is the map
that is induced by the canonical interpretation of
in
.
Proposition 29.
Let
be an RHL sequent and let
be a relational structure.
Then
satisfies
if and only if
is injective to
.
Proof.
Let
.
By Proposition
27, interpretations
of the premise
correspond to maps
, and interpretations
of
correspond to maps
.
The map
is given by restriction of the generic interpretation of
in
to the variables occurring in
.
It follows that
commutes if and only if
is a restriction of
.
Proposition 30.
Let
and
be RHL formulas.
Then
Proof.
By the universal property of classifying relational structures.
Definition 31.
An RHL theory
is
strong if
is strong.
Proposition 32.
Let
be an RHL theory.
Then
is a weakly reflective category.
If
is strong, then
is a reflective subcategory.
Proof.
By application of the small object argument (Propositions
15 and
16) to
.
3.3 Completeness Results
In this section, we study the descriptive strength of RHL.
We show that every morphism of finite relational structures can be described as classifying morphism of an RHL sequent (Proposition
36).
We then define identify subsets of RHL corresponding to injections and surjections of finite relational structures.
Finally, we show that the sequence resulting from application of the small object argument applied to surjective RHL sequents reaches a fixed point after a finite number of steps (Corollary
42).
This generalizes the fact that evaluation of Datalog programs always terminates.
Proposition 36.
Let
be an RHL sequent.
Then the classifying morphism
is a morphism of finite relational structures.
Conversely, for every morphism
of finite relational structures, there exists an RHL sequent
such that
and
are isomorphic, in the sense that there exists a commutative square of the form
Proof.
Since RHL formulas are finite, it follows from construction that classifying relational structures are finite.
Conversely, let
be a morphism of finite relational structures.
Choose distinct variables
of sort
for every sort
and element
.
The RHL formulas
are finite (and hence welldefined) because
is finite.
The formula
encodes the carrier sets of
, and
encodes the relations.
Thus if
, then
.
Let
be a fresh variable for each sort
and element
that is not in the image of
.
For arbitrary elements
, we let
for some fixed choice of
such that
if such an element
exists, and
otherwise.
Set
and let
.
Then
has the universal property of the classifying morphism of
, hence
.
Definition 37.
Let
be a map of relational structures.

is
injective if
is an injective function for all sorts
.

is
surjective if
is a surjective function for all sorts
.
Proposition 38.
Let
be a morphism of relational structures.

is injective if and only if
is a monomorphism in
.

is surjective if and only if
is an epimorphism in
.
Proof.
1.
In general, a morphism
in a complete category
is a monomorphism if and only if
is a pullback square.
Because the carrier functor, i.e. forgetful functor from relational structures to
indexed families of sets preserves limits, it follows that it preserves monomorphisms.
Thus, every monomorphism of relational structures is injective.
The same forgetful functor is faithful, hence reflects monomorphisms, so every injective morphism of relational structures is a monomorphism.
2.
Analogously to
1, since the carrier functor also preserves colimits.
Definition 39.
Let
be an RHL sequent.

is
injective if the conclusion
does not contain an equality atom.

is
surjective if every variable in the conclusion
also occurs in the premise
.
Proposition 40.
The classifying morphisms of RHL sequents with the properties of Definition
39 can be characterized up to isomorphism as follows:

The classifying morphisms of injective RHL sequents are precisely the injections of finite relational structures.

The classifying morphisms of surjective RHL sequents are precisely the surjections of finite relational structures.
Proof.
The verification that the classifying morphisms of the sequents in question have the desired properties can be reduced to sequents of the form
where
is an RHL atom by Proposition
30, and then follows by case distinction on
.
Conversely, the construction of sequents
with the respective property given a morphism
such that
is analogous to the proof of Proposition
36.
In both cases, the atoms in the conclusion
that violate the condition on the sequent are redundant because of the assumed property of
:
If
is injective, then
is a conjunction of equality atoms of the form
and hence can be omitted.
If
is surjective, then
is empty, so the case
for some
that is not in the image of
does not occur.
Proposition 41.
Let
be a finite set of epimorphisms of finite relational structures.
Let
be any sequence of maps of relational structures satisfying the conditions of Proposition
15 such that furthermore
is finite.
Then the sequence is eventually stationary, in the sense that
is an isomorphism for all sufficiently large
.
Proof.
Since all maps in
are surjective and colimits of relational structures commute with colimits on carrier sets, it follows that all maps in
are surjective.
Thus the cardinality of the carriers of the
decreases monotonically with
.
Since
is finite, the carriers
are empty for almost all sorts
.
Eventually, the sum of the cardinalities of the carriers of
must thus become stable, say after
.
Without loss of generality, we may assume that
is the identity map on carriers for
.
Let
.
Then for all
, we have that
and the latter is a finite set.
Thus, eventually
is stationary.
Even when
is infinite, we have
for all
and almost all
, since only finitely many relations are nonempty in any of the involved relational structures (
or a domain or codomain of a map in
).
For sufficiently large
and all
we thus have
for all
and hence
.
Corollary 42.
Let
be an RHL theory containing only surjective sequents.
Then the reflection of a finite relational structure into
is a finite relational structure.
3.4 Datalog and Relational Horn Logic
In this section, we study the subset of RHL that corresponds to Datalog.
We show that RHL can be reduced to Datalog with choice by way of the setoid transformation.
Definition 43.
Let
be an RHL sequent.

is a
Datalog sequent if all atoms in
are of the form
and all variables in the conclusion of
also occur in the premise.

is a
Datalog sequent with sort quantification if all atoms in
are of the form
or
, and all variables in the conclusion of
also occur in the premise.

is a
Datalog sequent with choice if all atoms in
are of the form
or
.
Note that in standard Datalog, usually only sequents with a single atom as conclusion are allowed.
However, our generalized Datalog sequents
1 have the same descriptive power as standard Datalog, since a single sequent with
conclusions can equivalently be replaced by
sequents with single conclusions.
The name
Datalog with choice in
3 alludes to the choice construct in Souffle [
1] with similar semantics.
Definition 44.
An element
in a relational structure is
unbound if it does not appear in any tuple
for all
.
Proposition 45.
The classifying morphisms of Datalog sequents can be characterized up to isomorphism as follows:

The classifying morphisms of Datalog sequents are precisely the injective surjective morphisms of finite relational structures that do not contain unbound variables.

The classifying morphisms of Datalog sequents with sort quantification are precisely the injective surjective morphisms of finite relational structures.

The classifying morphisms of Datalog sequents with choice are precisely the injective surjective morphisms of finite relational structures.
Proof.
Analogously to the proofs of Propositions
36 and
40.
Definition 46.
A
setoid consists of a set
and an equivalence relation
on
.
A morphism
is a map of underlying sets that respects the equivalence relations.
Two morphisms
of setoids are equal if
for all
.
The category of setoids is denoted by
.
Proposition 47.
The categories
and
are equivalent.
An equivalence is given by the quotient functor
and the diagonal functor
.
Proposition 49.
Let
be an RHL theory.
Then
and
are equivalent categories.
An equivalence is given as follows.
The functor
extends a relational
structure
to a relational
structure
on the same carrier by
for all sorts
.
The functor
assigns to a setoid model
the relational
structure with carriers
and relations
.
Proof.
We must first verify that
and
are welldefined, i.e., that the relational structures in their images are indeed models of the respective theories.
This is clear for
.
Let
for
.
Let
be a formula for the signature
and let
be an interpretation of
in
.
Since the carriers of
are defined as quotients of the carriers of
, every interpretation
of
in
lifts to an interpretation
of the same set of variables in
, so that we have
for all variables
.
Note that
is an interpretation of the set of variables of
, but not always of the formula
.
Let
be the formula obtained from
by replacing every equality atom
by the atom
, where
is the sort of
and
.
We claim that
is an interpretation of
in
.
To show this, it suffices to consider the case where
is an atom.

If
, then
, so
.
Thus
and
are in the same equivalence class, that is,
.

If
for some relation symbol
, then
.
By definition of
, there exist
such that
and
.
Thus
, so we have
for all
.
Since
satisfies the congruence sequents
2,
is closed under equivalence in each argument, hence
.

The case
is trivial.
Conversely, every interpretation
of
in
descends to an interpretation of
of
in
by setting
.
Now, let
be a sequent in
, and let
be an interpretation of
in
.
We have just shown that
lifts to an interpretation of
in
.
Because
satisfies
, we can extend
to an interpretation
of
in
, and then
descends to an interpretation of
in
that extends
.
Thus
is welldefined.
The composition
is equivalent to the identity functor since a quotient by the diagonal does not change the original set.
As for
, note that there is a canonical map
for all setoid models
.
The restriction
of
to a setoid carrier
is an isomorphism of setoids for all sorts
, with inverses
given by a choice of representative in each equivalence class.
Since the relations of
are closed under equivalence in each argument, it follows that
is a morphism of relational structures.
Thus
and
are isomorphisms.
Corollary 50.
Let
be an RHL theory with setoid transformation
.
Then the reflection
can be computed as composite
where

is the functors that extends relational
structures
to relational
structures with empty relations
,

is the free
model functor, and

is one half of the equivalence constructed in Proposition
49.
Proof.
and
are left adjoints and
is an equivalence.
The composite of the respective right adjoints is the inclusion
, so the composite of the
is the reflection into
.
4 Partial Horn Logic
Partial Horn logic is one of the many equivalent notions of essentially algebraic theory.
It was initially defined by Palmgren and Vickers [
5], who proved its equivalence to essentially algebraic theories.
Here we shall understand PHL as a syntactic extension, as
syntactic sugar, over RHL.
Observe that it cannot be read off from the individual sequents whether or not an RHL theory is strong or not.
Instead, one has to consider the interplay between the different sequents of the theory.
As a result, it is computationally undecidable whether or not a given RHL theory is strong.
Our application for the semantics developed in this paper are tools that allow computations based on the small object argument.
Such tools compute (fragments of) free models of userdefined theories that encode problem domains.
It is highly desirable that these theories are strong, since otherwise the result of the computation is not uniquely determined.
As strong RHL theories are difficult to recognize for both humans and computers, we argue that RHL is not directly suitable as an input theory language for this purpose.
What is needed, then, is a language with the same descriptive power as RHL, but where an easily recognizable subset allows axiomatizing all strong theories.
PHL is indeed such a language:
Proposition
85 shows that every strong RHL theory is equivalent to a PHL theory containing
epic sequents only.
PHL sequents are epic if no new variables are introduced in the conclusion, which is a criterion that can be easily checked separately for each sequent without regard for the theory the sequent appears in.
If tools wish to allow only strong theories, they can accept PHL as input language but reject nonepic sequents.
Note that there exist PHL theories containing nonepic sequents which are nevertheless strong, but such theories can be equivalently axiomatized as epic PHL theories.
Thus, no generality is lost compared to general strong theories when rejecting nonepic PHL theories.
4.1 Algebraic Structures
Definition 53.
An
algebraic signature is a relational signature
equipped with a partition
of the set of relation symbol into disjoint sets
of
predicate symbols and
of
function symbols such that the arity of every function symbol is nonempty.
If
is a function symbol, then we write
if the arity of
as a relation symbol is
.
Definition 54.
An
algebraic structure is a relational
structure
such that
is the graph of a partial function for all
.
Thus if
and
, then
.
We use
to denote the unique element
such that
, and we write
to denote that such an element
exists.
A
morphism of algebraic structures is a morphism of underlying relational structures.
The
category of algebraic structures is denoted by
.
If the algebraic signature
is clear from context, we abbreviate
as
.
Proposition 55.
Let
be a relational structure.
Then
is an algebraic structure if and only if it satisfies the RHL sequent
(4)
(4)
for each function symbol
.
Corollary 56.
The category of algebraic structures is a reflective subcategory of the category of relational structures.
The reflections
of relational structures
into
are surjections.
Proof.
That every reflection is surjective follows from the small object argument and the fact that the classifying morphisms of functionality axioms
(4) are epimorphisms of relational structures, hence so are all coproducts, pushouts and (infinite) compositions thereof.
We denote the free algebraic structure functor by
.
Corollary 57.
The category of algebraic structures is complete and cocomplete.
Proof.
This follows from general facts about reflective subcatgories:
They are stable under limits, and colimits are computed by reflecting colimits of the ambient category.
4.2 Syntax and Semantics
Fix an algebraic signature
.
Definition 58.
The set of
terms and a sort assigned to each term is given by the following recursive definition:

If
is a variable of sort
, then
is a term of sort
.

If
is a function symbol and
are terms such that
has sort
for all
, then
is a term of sort
.
PHL atoms, PHL formulas and PHL sequents are defined as in Definition
24, but with three changes:

In each type of atom, also composite terms of the same sort are allowed in place of only variables.

A PHL atom
is valid only if
is a predicate symbol, but not if
is a function symbol.
We refer to such atoms as
predicate atoms.

An atom of the form
is called a
term assertion atom, whereas
sort quantification atom is reserved for atoms of the form
with
a variable.
Definition 59.
Let
be an algebraic structure.
An
interpretation of a term in
is an interpretation
of the variables occurring in
such that the following recursive extension of
to composite terms is welldefined on
:
Note that the righthand side might not be defined; in this case also the lefthand side is undefined.
An
interpretation of a PHL atom in
is defined analogously to the interpretation of an RHL atom, but with the additional condition that the interpretation is defined on all (possibly composite) terms occurring in the atom.
An
interpretation of a PHL formula is an interpretation of the variables occurring in
that restricts to an interpretation of
for each
.
An algebraic structure
satisfies a PHL sequent
if each interpretation of
in
can be extended to an interpretation of
in
.
Definition 61.
Let
be a term.
The
flattening of
consists of an RHL formula
and a result variable
.
Flattening is defined recursively as follows:

If
is a variable, then
is the empty conjunction and
.

If
, then
where
is a fresh variable.
Let
be a PHL atom.
The flattening
is an RHL formula which is defined depending on the type of
as follows:

If
is a predicate atom, then

If
is a term assertion atom, then

If
is an equality atom, then
The flattening of a PHL formula is the conjunction of the flattenings of each atom making up the formula.
The flattening of a PHL sequent is the RHL sequent given by flattening premise and conclusion.
Proposition 63.
Let
be an algebraic structure.

Let
be a term and let
be an interpretation of the variables of
in
.
Then
can be extended to the term
if and only if
can be extended to an interpretation of the RHL formula
.
In either case, if an extension
exists, then it exists uniquely, and
.

Let
be a PHL atom and let
be an interpretation of the variables of
in
.
Then
is an interpretation of
if and only if
can be extended to an interpretation
of the RHL formula
.
If
exists, then it exists uniquely.

Let
be a PHL sequent.
Then
satisfies
if and only if it satisfies the RHL sequent
.
Definition 64.
We associate to each PHL formula
the following
classifying algebraic structure:
The composition of the generic interpretation
in
with the reflection into
induces an interpretation of
in
, which then restricts to an interpretation
of
in
.
We call
the
generic interpretation of
.
Proof.
This follows by combining Proposition
63, Proposition
65 and the universal property of the free algebraic structure functor.
Definition 66.
Let
be a PHL sequent.
The
classifying morphism of
is the morphism
of classifying algebraic structures that is induced by the canonical interpretation of
in
.
Proposition 67.
Let
be a PHL sequent and let
be an algebraic structure.
Then
satisfies
if and only if
is injective to
.
Proof.
Analogous to the proof of Proposition
29.
Proposition 68.
Let
be a PHL theory.
Denote the functionality sequent
(4) for function symbols
by
.
Then
is equivalent to the following injectivity classes:

, where
.

, where
.

, where
.
Here
in the definition of
denotes the classifying morphism of the PHL sequent
, which is a morphism of algebraic structures, hence in particular a morphism of relational structures.
denotes the classifying morphism of the RHL sequent
.
In particular,
is a weakly reflective subcategory of both
and
.
If any one of
or
are strong, then all of them are strong, and
is a reflective subcategory of
and
.
Proof.
1 follows from Proposition
65, and then
2 and
3 follow from Proposition
17.
Proposition 69.
Let
be an RHL formula.
Then there exists a PHL formula
with the following properties:

Every variable occurs in
if and only if it occurs in
.

Let
be an interpretation of the variables of
in an algebraic structure
.
Then
is an interpretation of the PHL formula
if and only if it is an interpretation of the RHL formula
.
Proof.
Replace every relation atom of the form
for some function symbol
with the PHL atom
.
Proposition 70.
Let
and
be PHL formulas.
Then
Proof.
This follows from the universal property of classifying morphisms.
4.3 Completeness Results
In this section, we study the descriptive strength of PHL.
As with RHL and relational structures, every map of finite algebraic structures can be described as classifying morphism of a PHL sequent (Proposition
71).
We classify epimorphisms of algebraic structures and show that epimorphisms of finite algebraic structures correspond to
epic PHL sequents, where variables cannot be introduced in the conclusion (Proposition
82).
Finally, we show that every strong RHL theory is semantically equivalent to an epic PHL theory (Proposition
85).
Proposition 71.
Let
be a PHL sequent.
Then the classifying morphism
is a morphism of finite algebraic structures.
Conversely, for every morphism
of finite algebraic structures, there exists a PHL sequent
such that
and
are isomorphic.
Proof.
By Propositions
36 and
69.
Definition 72.
Let
be a function symbol.
The
totality sequent is given by
We denote by
the set of classifying morphisms of totality sequents.
Proposition 73.
Let
be a function symbol.

An algebraic structure
satisfies
if and only if
is a total function.

is an epimorphism of algebraic structures.
Definition 74.
Let
be a map of algebraic structures.
We say that
is
total over Y (with respect to
) if and only if for all function symbols
and elements
, if
is defined, then
is defined.
Proposition 75.
Let
be a map of algebraic structures.
Then there exists a factorization
such that
is a relative
cell complex and
is total over
.
Moreover, the triple
is uniquely determined by
up to unique isomorphism.
Proof.
Consider the set
of all triples
of function symbols
and pairs of morphisms
and
making up commuting triangles
is a set of epimorphisms in the slice category
.
It follows that
is strong, so
is a reflective subcategory of
.
Partial algebras over
are total over
if and only if they are injective to
.
It follows that a triple
with
a relative
complex and
relatively total exists and is unique up to unique isomorphism.
It remains to show that
is a relative
cell complex.
By definition, the class of relative
cell complexes is obtained from
by closure under certain classes of colimits.
The forgetful functor
preserves colimits and maps
into
.
From this it follows that the image of a relative
cell complex in
is a relative
complex.
In particular,
is a relative
cell complex.
Definition 76.
Let
be a map of algebraic structures.
We call the unique factorization
as in Proposition
75 the
relative totalization of
.
Proposition 77.
Let
be a map of algebraic structures such that
is total over
.
Then
is an epimorphism in
if and only if it is surjective.
Proof.
Since
is a subcategory of
, every morphism in
which is an epimorphism in
is also an epimorphism in
.
Thus, every surjective morphism of algebraic structures is an epimorphism.
Conversely, suppose that
is an epimorphism of algebraic structures such that
is total over
.
Let
be the image factorization of
in
.
Thus,
for all sorts
, and
for all relations
.
Since
is an algebraic structure, the relational substructure
is an algebraic structure.
Because
is relatively total over
, also
is relatively total over
.
Since
is surjective if and only if
is surjective (that is, a bijection on carriers), we may henceforth assume that
is injective.
Now consider the pushout
in
.
There are inclusions
and
corresponding to the two components of
such that
, and inclusions
.
We have
for all sorts
, but note that the analogous equation does not necessarily hold for relations.
We claim that
is an algebraic structure.
Thus let
be a function symbol, and let
such that
and
.
We need to show that
.
If
or
this follows from the fact that
is an algebraic structure.
We may thus (by symmetry) assume that
and
.
Because the first
projections of
and
agree, we have
, hence
for
.
Because
is total over the
with respect to the inclusions
, we have
for some
.
It follows that
and
, hence
.
As in every cocomplete category,
is an epimorphism of algebraic structures if and only if the two maps
to the pushout of algebraic structures agree.
But we have just shown that
, so also the two maps
agree.
Thus
is an epimorphism in
, hence surjective.
Proposition 78.
Let
be a map of algebraic structures.

is a monomorphism in
if and only if it is injective.

Let
be the relative totalization of
.
Then
is an epimorphism in
if and only if
is a surjection.
Proof.
1.
In general, morphisms in reflective subcategories are monic if and only if they are monic as morphisms in the ambient category.
2.
Every morphism in
is an epimorphism.
Since epimorphisms are stable under pushouts and infinite compositions, every relative
cell complex and in particular
is an epimorphism.
Thus
is an epimorphism in
if and only if
is an epimorphism in
.
We conclude with Proposition
77.
Definition 79.
A PHL sequent
is
epic if every variable in the conclusion
also occurs in the premise
.
Proposition 80.
Let
be a PHL formula.
Let
for RHL atoms
.
Let
for some
and let
Then
has one of the following forms:

, where
is a predicate symbol and
.

, where
is a function symbol,
and
is a fresh variable.

, where
.

, where
.
Proof.
Follows inductively from the definition of flattening; see also Remark
62.
Proposition 81.
The classifying morphisms of epic PHL sequents are, up to isomorphism, closed under composition.
Proof.
Let
and
be epic PHL sequents and suppose that there exists an isomorphism
.
It suffices to show that
is isomorphic to the classifying morphism of an epic PHL sequent of the form
, since then
by Proposition
70.
Every variable
in
corresponds to some term
in
under
.
More precisely, the canonical interpretation of
and the inverse of
determine an element
, and then
is the canonical interpretation
of some term
that occurs in
.
Let
be the formula that is obtained from
by replacing every variable
by a corresponding term
in
.
Observe that we assumed
to be an epic sequent, so every variable in
also occurs in
.
Thus,
is epic.
By induction over the number of atoms in
, we find an interpretation of
in
that is compatible with
, and vice versa there is an interpretation of
in
that is compatible with
.
These interpretations then induce a commutative square
as desired.
Proposition 82.
The classifying morphisms of epic PHL sequents are, up to isomorphism, precisely the epimorphisms of finite algebraic structures.
Proof.
Let
be the flattening of an epic PHL sequent
.
Then
is the classifying morphism of
.
We need to show that
is an epimorphism.
Since epimorphisms are stable under composition, we may assume that
is a single RHL atom of one of the types listed in Proposition
80 where
is the set of variables occurring in
.
If
is an atom of type
1,
3 or
4, then the morphism
of relational structures is surjective.
Because the free algebraic structure functor preserves epimorphisms, this implies that
is an epimorphism in
.
In case
2,
is a pushout of
in
.
Since
is an epimorphism in
and pushouts preserve epimorphisms, it follows that also in this case
is an epimorphism.
Now suppose that
is an epimorphism of finite algebraic structures.
Let
be the relative totalization of
over
.
Since
is a relative
cell complex, there exists by Proposition
9 a sequence of pushout squares
for a totality sequent
for all
such that
is the infinite composition of the
.
Note that, a priori, Proposition
9 implies only that
is a pushout of a
coproduct of totality sequents.
However, finiteness of
and
implies inductively that these coproducts can be chosen to be finite, and then a single pushout of a finite coproduct can equivalently be written as a finite composition of pushouts.
We claim that
for all
and a sequence of epic PHL sequents
.
To verify this, choose first a PHL formula
such that
.
A formula
with this property exists by Proposition
71 because the identity on
is a map of finite algebraic structures.
The map
corresponds to elements
, and these elements are the interpretations of terms
that occur in
.
Now
Let
for
.
Because
is finite, the chain
is eventually stationary, say for
, and then
.
is an epimorphism, hence
is a surjection by Proposition
78, hence also
is a surjection.
Thus
for some surjective RHL sequent
.
Note that the PHL sequent
is epic because the RHL sequent
is surjective.
We have thus decomposed
into a composition
in which each map is isomorphic to the classifying morphism of an epic PHL sequent
.
Thus by Proposition
81,
for some epic PHL sequent
.
Corollary 83.
Let
be an epic PHL theory, i.e. a PHL theory comprised of epic sequents only.
Then
is a reflective subcategory of both
and
.
Proof.
By combining Proposition
68 with Proposition
82.
Proposition 85.
Let
be a relational signature and let
be an RHL theory for
.
Then there exists an algebraic signature
on the same set of sorts
such that
and an epic PHL theory
for
such that the forgetful functor
restricts to an equivalence
.
In particular, if
is strong, then
.
Proof.
Observe that a relational
structure is orthogonal to a classifying morphism
of an RHL sequent
if every interpretation of the premise
extends
uniquely to an interpretion of
.
Our strategy is to add function symbols for each variable in a conclusion of a sequent in
that does not occur in the premise.
We then add axioms enforcing that each conclusion variable can be obtained by application of the corresponding function symbol to the variables in the premise and vice versa.
Because evaluation of partial functions yields a unique result, this enforces that the interpretion of conclusion variables is uniquely determined by the interpretation of premise variables.
In detail, our set of function symbols
is given by
Let
be in
.
Let
be an enumeration of the variables in
with sorts
.
Let
be a variable in
that does not occur in
, and let
be the sort of
.
Then the signature of
is given by
.
Note that each relation symbol in
corresponds to a predicate symbol in
.
We thus implicitly coerce RHL sequents for
to PHL sequents for
(without invoking
).
Let
be the set containing the following PHL sequents, for all
in
:

The sequent
, where
is obtained from
by replacing each variable
in
that does not occur in
with
.

The sequents
for all variables
in
that do not occur in
.

The sequent
where
ranges over the variables in
that do not occur in
.
Clearly all PHL sequents in
are epic.
Let
be the forgetful functor.
We first show that if
, then
for every sequent
.
Let
be the enumeration of variables in
that we chose in the definition of the signature of the function symbols
.
Let
be an interpretation of
in
.
As mentioned earlier, we implicitly treat
also as a PHL sequent for the signature
, and under this identification we can view
as an interpretation of the PHL sequent
in the algebraic structure
.
Because
satisfies sequent
1, it follows that
is also an interpretation of
in
.
By definition of
, it follows that we obtain an interpretation
of
by setting
if
occurs in
and
if
does not occur in
.
Thus
satisfies the sequent
.
Two interpretations of
in
that agree on the variables in
agree also on the variables that occur in
because of sequent
3.
Next we construct a model
given
such that
for
.
Set
for all sorts
and
for
.
Let
be in
, and let
be the enumeration of the variables in
that we chose earlier.
Then we set
whenever
is an interpretation of
in
.
Since
is orthogonal to
, two interpretations of
are equal as soon as the interpretations agree on the variables
of
.
Thus, equation
(5) yields welldefined partial functions
.
By construction,
satisfies sequent
1 and the sequents
2.
Satisfaction of sequent
3 follows again from uniqueness of the interpretation of conclusion variables.
The assignment
is functorial.
Indeed, let
be a map in
with
and
orthogonal to
for
, and let
for
.
We need to show that the action of
on carrier sets is also a morphism
, i.e. that it preserves partial functions.
This follows from the definition of the partial functions
(5) because if
is an interpretation of
in
, then
is an interpretation of
in
.
Clearly
is the identity functor.
If
, then the partial functions of
satisfy equation
(5).
Thus,
is the identity functor.
Bibliography

The Choice Construct in the {Souffl{\'{e}}} Language. Programming Languages and Systems, pages 163–181, 2021.

Pointsto analysis in almost linear time. Proceedings of the 23rd {ACM} {SIGPLAN}{SIGACT} symposium on Principles of programming languages  {POPL} {\textquotesingle}96, 1996.

Variations on the Common Subexpression Problem. Journal of the {ACM}, 27(4):758–771, 1980.

Fast Parallel Equivalence Relations in a {Datalog} Compiler. 2019 28th International Conference on Parallel Architectures and Compilation Techniques ({PACT}), 2019.

Partial {Horn} logic and cartesian categories. Annals of Pure and Applied Logic, 145(3):314–353, 2007.

Locally Presentable and Accessible Categories. 1994.

From {Datalog} to {Flix}: a declarative language for fixed points on lattices. {ACM} {SIGPLAN} Notices, 51(6):194–208, 2016.

Cloningbased contextsensitive pointer alias analysis using binary decision diagrams. {ACM} {SIGPLAN} Notices, 39(6):131–144, 2004.

Strictly declarative specification of sophisticated pointsto analyses. Proceeding of the 24th {ACM} {SIGPLAN} conference on Object oriented programming systems languages and applications  {OOPSLA} 09, 2009.

What you always wanted to know about {Datalog} (and never dared to ask)., 1(1):146–166, 1989.

Martin E. Bidlingmaier. An Evaluation Algorithm for {Datalog} with Equality. 2023.

Mark Hovey. Model categories., (63), 2007.

Benjamin C. Pierce. Types and Programming Languages. The MIT Press, 2002.

Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock and Pavel Panchekha. {Egg}: Fast and Extensible Equality Saturation. Proc. ACM Program. Lang., 5(POPL), 2021.