Abstract
Semiring provenance provides a unifying framework for provenance analysis of database queries, logics and games. Initially proposed for positive relational algebra and datalog, featuring least fixed-point computations, it has since been extended to logics with negation.
In this talk, we consider algorithmic problems raised by allowing queries with negations of least fixed points, such as stratified datalog and fixed point logic. Evaluating such queries requires the computation of greatest fixed points; these turn out to be well behaved in the class of absorptive semirings with suitable completeness and continuity assumptions. We show that greatest fixed points can be efficiently computed in these semirings. The proof is based on understanding the fixed-point iteration through derivation trees, inspired by a line of research on Newton's method for commutative semirings.
A second algorithmic issue arises when facts are annotated by polynomials, as the query evaluation can then result in polynomials of exponential size. This problem has been addressed for datalog over absorptive polynomials by using circuit representations. We show that the efficient computation of greatest fixed points can be turned into similar circuit representations for stratified datalog.
Talk based on a RAMiCS'21 paper: https://arxiv.org/pdf/2106.00399.pdf
Closely related papers:
JACM 2010: Newtonian Program Analysis, https://dl.acm.org/doi/10.1145/1857914.1857917
ICDT 2014: Circuits for Datalog Provenance, https://openproceedings.org/ICDT/2014/paper_36.pdf