Algorithmic Aspects of Semiring Provenance for Stratified Datalog

on YouTube ↗28m

" summary

Claim: greatest fixed points of polynomial operators over absorptive semirings with continuity can be computed in polynomial time by iterating n steps, applying an infinite-power operation, then iterating n more steps. Proof uses derivation trees (finite and infinite) plus the absorption property to normalize trees and bound prefixes. Result produces compact circuit representations for stratified Datalog provenance of polynomial size, assuming the infinite-power operation is computable in the target semiring; methods generalize Newton-style semiring techniques and do work on the examples given.

AI-written summary · about

" chapters (8)

1. 0:00Introduction and motivation
2. 1:38Semiring semantics overview
3. 3:46Negation in stratified Datalog
4. 7:40Computing greatest fixpoints
5. 11:36Conditions and derivation trees
6. 15:04Proof of the main result
7. 21:07Circuit representations
8. 25:55Summary and future work

" related talks

• 01h 06mAlgebraic Structures in Logic and Query Evaluation 1Val Tannen · Logic and Algorithms in Database Theory and AI Boot Camp
• 01h 08mAlgebraic Structures in Logic and Query Evaluation 4Dan Suciu · Logic and Algorithms in Database Theory and AI Boot Camp
• 01h 05mAlgebraic Structures in Logic and Query Evaluation 2Val Tannen · Logic and Algorithms in Database Theory and AI Boot Camp
• 01h 02mAlgebraic Structures in Logic and Query Evaluation 3Dan Suciu · Logic and Algorithms in Database Theory and AI Boot Camp
• 36mOptimizing Relational Programs IIRemy Wang · Fine-Grained Complexity, Logic, and Query Evaluation 2023
• 26mDebugging Large-Scale Datalog: A Scalable Provenance Evaluation StrategyDavid Zhao, Bernhard Scholz, Pavle Subotic · POPL 2021
• 05mRelational ProgrammingRemy Wang · 9th Annual Simons Institute Industry Day
• 18mParikh's Theorem Made SymbolicAnthony W. Lin, Matthew Hague, Artur Jez · POPL 2024