Algebraic Semantics of Datalog with Equality

TL;DR

This paper develops algebraic semantics for extended Datalog languages with equality, introducing a new construction of free models and an implementation of the Eqlog engine.

Contribution

It presents a novel algebraic semantics for RHL and PHL, including a new free model construction and an abstract Datalog evaluation via the small object argument.

Findings

Introduces classifying morphisms for RHL and PHL sequents.

Constructs free and weakly free models using the small object argument.

Implementates the Eqlog Datalog engine for computing free models.

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.