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 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 points-to 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 ad-hoc 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 e-graph, and then close the e-graph under a set of rewrite rules. E-graphs allow sharing nodes that occur as children more than once, so that a large number of expressions can be stored. Furthermore, e-graphs 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 e-graph 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 e-graphs 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 order-theoretic 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 points-to 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 domain-specific 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 better-known 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 orthogonal-reflection 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 better-behaved 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 (semi-naive 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 e-graphs 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 orthogonal-reflection 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 orthogonal-reflection construction for . Thus, the concept of strong morphisms can be used to understand the orthogonal-reflection 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 set-theoretic universe that contains the collection of objects in . All colimits of set-indexed diagrams in exist, while colimits of class-indexed 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 right-cancellation.
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:
  1. .
  2. is closed under coproducts. That is, if is a family of morphisms indexed by some set and for all , then
    is in .
  3. is closed under pushouts. That is, if
    is a pushout square and , then .
  4. is closed under composition of sequences. That is, if
    is a sequence of morphisms with composition , then .

Remark 8.

Standard literature on factorization systems and the closely related small object argument [12] usually considers not only countable sequences of morphisms but also arbitrary transfinite sequences, which are chains of morphisms indexed by an arbitrary ordinal number. In this more general setting, one typically defines a relative -cell complex to be a transfinite composition of pushouts of morphisms in without mention of coproducts.
This more common notion of relative -cell complex satisfies our closure properties 1 -- 4. For 2, one chooses a well-ordering on the indexing set , and then computes the coproduct as composition of a chain indexed by this well-ordering. Conversely, our definition of relative -cell complex is closed under arbitrary transfinite composition if all morphism in have finitely presentable domains and codomains (Definition 14). Thus, whenever the domains and codomains of the morphisms in are finitely presentable, the definition given here and the usual one agree.

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 hom-functor 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:
  1. is a relative -cell complex for all .
  2. 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:

Definition 19.

Let be a relational signature. A relational -structure consists of the following data:
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:
  1. A relation atom , where is a relation symbol and the are variables of sort for all .
  2. A sort quantification atom where is a variable.
  3. 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 meta-theoretical equality. We always assume that meta-theoretical 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:
  1. is a relation atom and .
  2. is a sort quantification atom, without further assumptions.
  3. 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:
  1. If where , then the carriers of are given by distinct elements and a single tuple . The relations for are empty.
  2. If , where has sort , then contains a single element . All other carrier sets and all relations are empty.
  3. 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 .

Proposition 27.

Let be an RHL formula and let be a relational structure. Then there is a bijection between interpretations of in and maps .
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 .

Remark 33.

Let us reflect on the similarities between the proof of Proposition 32 and Datalog evaluation. Note that Datalog is a strict subset of RHL, so we have to specialize Proposition 32 to Datalog theories in order to compare. Thus, we assume that the conclusions of sequents in only contain atoms for variables that occur in the premise (see Section 3.4 for detailed discussion of the fragment of RHL corresponding to Datalog).
Unfolding the small object argument, we see that the reflection of a relational structure into the category of models is given by the colimit of a chain
(2) (2)
of relational structures. The relational structure corresponds to the set of input facts of the Datalog program, and each represents the total set of derived facts after the th iteration of Datalog evaluation. Because contains Datalog sequents only, the transition maps are bijective on carriers. The data of the sequence (2) is thus equivalent to a sequence of inclusions
on the carrier of for all relation symbols , mirroring the monotonically growing relations during Datalog evaluation.
Unfolding our existence proof of the small object argument (Proposition 16) and the universal property of classifying structures (Proposition 27), we see that is obtained from via the following pushout square:
(3) (3)
Here is the set of pairs of sequents and interpretations . Thus the left vertical map corresponds to the set of matches of premises among the facts established after the th iteration of Datalog evaluation. Defining using the pushout square above has the effect of adjoining matches of the conclusion for each match of the premise. Since is a Datalog theory, the conclusions are relation atoms, hence is obtained from by adjoining tuples to relations.

Remark 34.

Semi-naive evaluation is an optimized version of Datalog evaluation, where we consider only matches of premises at the th stage that have not been present already in the th stage. This does not change the result of Datalog evaluation since conclusions of matches that have been found in a previous iteration have already been adjoined. In terms of the small object argument, this optimization can be understood as a more economic choice of the set : In diagram (3), we can replace by the set of interpretations that do not factor via .

Remark 35.

Still, there are properties of Datalog evaluation that Proposition 32 does not entirely capture. First, the result of Datalog evaluation is determined uniquely via fixed point semantics, whereas Proposition 32 guarantees uniqueness (up to ismorphism) only in the case of strong theories. Since classifying morphisms of Datalog sequents are epic, all Datalog theories are strong (Proposition 4). Thus, Proposition 32 does indeed determine the result of Datalog computation uniquely. However, not all strong theories are Datalog theories or even contain epimorphisms only. For example, Proposition 5 allows extending every RHL theory to a strong theory. A syntactic characterization of strong RHL theories is the main purpose of Section 4, where we discuss partial Horn logic.
A second feature of Datalog evaluation we have not discussed is that it always terminates: Since Datalog evaluation monotonically increases the size of relations on a fixed carrier, it reaches a fixed point after a finite number of iterations. This is not generally true for RHL theories, since the carrier sets change during evaluation. We can, however, prove termination for surjective theories, which subsume and generalize Datalog theories (Corollary 42). In general, it is undecidable whether evaluating a given RHL theory terminates on some input.

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 well-defined) 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.
  1. is injective if is an injective function for all sorts .
  2. is surjective if is a surjective function for all sorts .

Proposition 38.

Let be a morphism of relational structures.
  1. is injective if and only if is a monomorphism in .
  2. 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.
  1. is injective if the conclusion does not contain an equality atom.
  2. 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:
  1. The classifying morphisms of injective RHL sequents are precisely the injections of finite relational structures.
  2. 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 non-empty 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.
  1. is a Datalog sequent if all atoms in are of the form and all variables in the conclusion of also occur in the premise.
  2. 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.
  3. 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:
  1. The classifying morphisms of Datalog sequents are precisely the injective surjective morphisms of finite relational structures that do not contain unbound variables.
  2. The classifying morphisms of Datalog sequents with sort quantification are precisely the injective surjective morphisms of finite relational structures.
  3. 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 .

Definition 48.

The setoid transformation of an RHL theory defined on a signature is a Datalog with choice theory defined on a relational signature as follows. The signature extends by a relation symbol for each sort . The sequents of are given as follows:
  1. For each sort , sequents asserting that is an equivalence relation:
  2. For each relation , a sequent asserting that the equivalence relations behave as congruences with respect to :
  3. For each sequent in , the sequent which is obtained from by replacing each equality atom with the atom , where is the sort of and .
The category of setoid models is given by the models of , where we consider morphisms of setoid models as equal if are equal as setoid morphisms for all sorts .

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 well-defined, 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. 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 well-defined.
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
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 .

Remark 51.

Proposition 49 shows that RHL can be reduced to Datalog with minor extensions. In practice, however, using the resulting Datalog programs to compute free models is often unfeasible even for small inputs.
One issue is that storing the equivalence relations naively requires quadratic memory with respect to the size of equivalence classes. This problem can be largely addressed by using a union-find data structure, which only requires linear memory. Union-find data structures are available in the Souffle Datalog engine [4].
A more significant issue are the congruence axioms 2, which result in an exponential increase in memory requirements with respect to the arity of relations. Every equality inferred during evaluation can significantly increase the total size of the relational structure in the next stage. Semantically, however, every inferred equality should in fact reduce the size of the relational structure at the next stage. The Eqlog engine, which evaluates RHL theories directly, takes advantage of this observation by maintaining a union-find data structure on each sort to keep track of a canonical representative for each equivalence class. The relations then contain entries only for these canonical representatives. An inferred equality results in a merge of two equivalence classes, with one of the canonical representatives ceasing to be representative. Eqlog then canonicalizes all tuples by replacing each occurrence of the old representative with the new representative. Since relations are stored without duplicates, this often results in a decrease in the size of the relations, so that later stages can be computed faster.

Remark 52.

The following alternative sparse setoid transformation of an RHL theory can result in a more efficient Datalog program. The signature of the sparse setoid transformation is the same as in the standard setoid transformation (Definition 48), so contains additional equivalence relations for all sorts . As before, contains the equivalence relation axioms 1. However, the congruence axioms 2 are omitted.
Instead, we modify the premise of each sequent in so that the different occurrences of a variable can be interpreted by distinct but equivalent elements. As before, we replace equality atoms by atoms in premise and conclusion. Next, for each variable that occurs times in the premise , we choose a list of variables of the same sort, where are fresh. We now replace the th occurrence of in with , and add the atoms for all to .
The transformed premises have the following property: If is a relational -structure that satisfies the equivalence relation axioms and is the relational structure over that furthermore satisfies the congruence axioms, then maps are in bijection to maps up to setoid morphism equality. From this it follows that Corollary 50 holds also for the sparse transformation .
The sparse transformation avoids duplication in many cases, but data that can be inferred twice for distinct but equivalent elements is still duplicated. Furthermore, the transformed premises can be more computationally expensive to match because all elements in an equivalence class must be considered for every occurrence of a variable in the original premise .

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 user-defined 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 non-epic sequents. Note that there exist PHL theories containing non-epic 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 non-epic 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 non-empty. 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:
  1. If is a variable of sort , then is a term of sort .
  2. 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:
  1. In each type of atom, also composite terms of the same sort are allowed in place of only variables.
  2. 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.
  3. 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 well-defined on :
Note that the right-hand side might not be defined; in this case also the left-hand 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 .

Remark 60.

There are some differences between our notion of partial Horn logic and the notion introduced by [5]:
  1. In [5], the notation is a meta-theoretic abbreviation for self-equality atoms .
  2. In [5], sequents are annotated with a context, i.e. a set of variables. Sequents may only refer to variables listed in the context. Interpretations of the premise of the sequent must always also interpret variables in the context. A sequent with context as in [5] is thus semantically equivalent to our PHL sequent .
  3. Our notion of sequent allows variables in the conclusion that do not occur in the premise (or context). According to our semantics, we may think of such variables as implicitly existentially quantified: A sequent is satisfied if for every interpretation of the premise, there exists a suitable extension of the interpretation to the conclusion. This does not have a counterpart in the PHL considered in [5].
1 and 2 are minor syntactic differences, but 3 increases the descriptive strength of PHL non-trivially. We later consider epic PHL (Section 4.3), where all variables in the conclusion must also occur in the premise. Apart from 1 and 2 and above, our notion of epic PHL agrees with PHL as defined in [5].

Definition 61.

Let be a term. The flattening of consists of an RHL formula and a result variable . Flattening is defined recursively as follows:
  1. If is a variable, then is the empty conjunction and .
  2. 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:
  1. If is a predicate atom, then
  2. If is a term assertion atom, then
  3. 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.

Remark 62.

The flattening of a composite term involves the choice of a ``fresh'' variable . This notion can be made precise as follows: The flattening operations take as additional parameter a sequence of variables such that the variables do not occur in the syntactic objects that should be flattened. Choosing a ``fresh'' variable now means that we set , and for all further flattening operations we pass the sequence .
This means that a term that appears twice in the same formula will be flattened twice with different choices of fresh variables. For example, if is a binary function symbol and are variables, then the flattening of the PHL formula
is the RHL formula
where .

Proposition 63.

Let be an algebraic structure.
  1. 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 .
  2. 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.
  3. Let be a PHL sequent. Then satisfies if and only if it satisfies the RHL sequent .
Proof. By construction.

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 .

Proposition 65.

Let be a PHL formula and let be an algebraic structure. Then there is a bijection between interpretations of in and maps .
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:
  1. , where .
  2. , where .
  3. , 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:
  1. Every variable occurs in if and only if it occurs in .
  2. 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.
  1. An algebraic structure satisfies if and only if is a total function.
  2. 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.
  1. is a monomorphism in if and only if it is injective.
  2. 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:
  1. , where is a predicate symbol and .
  2. , where is a function symbol, and is a fresh variable.
  3. , where .
  4. , 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.

Remark 84.

There appears to be no simple analogue to Proposition 82 that classifies PHL sequents corresponding to monomorphisms of algebraic structures. One possible notion of monic PHL sequent one might consider are PHL sequents in which the conclusion does not contain equality atoms. Indeed, the classifying morphisms of such sequents are monic. But not every monomorphism of finite algebraic structures can be described as classifying morphism of such sequents.
For example, consider a signature given by a single sort and a nullary function symbol , and the inclusion of algebraic structures given by singleton carriers and . The RHL sequent corresponding to this inclusion is . But since is a function symbol, is not a valid PHL atom. Indeed, unflattening yields the PHL sequent , which would not be monic per our proposed definition.
To rectify this, we might then try to change the definition of PHL so that relation atoms are valid also in case is a function symbol. But now with the notion of monic PHL sequent considered above, not all classifying morphisms of monic PHL sequents would be monomorphisms, for example for the sequent .

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 :
  1. The sequent , where is obtained from by replacing each variable in that does not occur in with .
  2. The sequents
    for all variables in that do not occur in .
  3. 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
(5) (5)
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 well-defined 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

  1. The Choice Construct in the {Souffl{\'{e}}} Language. Programming Languages and Systems, pages 163–181, 2021.
  2. Points-to analysis in almost linear time. Proceedings of the 23rd {ACM} {SIGPLAN}-{SIGACT} symposium on Principles of programming languages - {POPL} {\textquotesingle}96, 1996.
  3. Variations on the Common Subexpression Problem. Journal of the {ACM}, 27(4):758–771, 1980.
  4. Fast Parallel Equivalence Relations in a {Datalog} Compiler. 2019 28th International Conference on Parallel Architectures and Compilation Techniques ({PACT}), 2019.
  5. Partial {Horn} logic and cartesian categories. Annals of Pure and Applied Logic, 145(3):314–353, 2007.
  6. Locally Presentable and Accessible Categories. 1994.
  7. From {Datalog} to {Flix}: a declarative language for fixed points on lattices. {ACM} {SIGPLAN} Notices, 51(6):194–208, 2016.
  8. Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. {ACM} {SIGPLAN} Notices, 39(6):131–144, 2004.
  9. Strictly declarative specification of sophisticated points-to analyses. Proceeding of the 24th {ACM} {SIGPLAN} conference on Object oriented programming systems languages and applications - {OOPSLA} 09, 2009.
  10. What you always wanted to know about {Datalog} (and never dared to ask)., 1(1):146–166, 1989.
  11. Martin E. Bidlingmaier. An Evaluation Algorithm for {Datalog} with Equality. 2023.
  12. Mark Hovey. Model categories., (63), 2007.
  13. Benjamin C. Pierce. Types and Programming Languages. The MIT Press, 2002.
  14. 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.