Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Size Bound-Adorned Datalog

Christian Fattebert, Zhekai Jiang, Christoph Koch, Reinhard Pichler, Qichen Wang

Abstract

We introduce EDB-bounded datalog, a framework for deriving upper bounds on intermediate result sizes and the asymptotic complexity of recursive queries in datalog. We present an algorithm that, given an arbitrary datalog program, constructs an EDB-bounded datalog program in which every rule is adorned with a (non-recursive) conjunctive query that subsumes the result of the rule, thus acting as an upper bound. From such adornments, we define a notion of width based on (integral or fractional) edge-cover widths. Through the adornments and the width measure, we obtain, for every IDB predicate, worst-case upper bounds on their sizes, which are polynomial in the input data size, given a fixed program structure. Furthermore, with these size bounds, we also derive fixed-parameter tractable, output-sensitive asymptotic complexity bounds for evaluating the entire program. Additionally, by adapting our framework, we obtain a semi-decision procedure for datalog boundedness that efficiently rewrites most practical bounded programs into non-recursive equivalent programs.

Size Bound-Adorned Datalog

Abstract

We introduce EDB-bounded datalog, a framework for deriving upper bounds on intermediate result sizes and the asymptotic complexity of recursive queries in datalog. We present an algorithm that, given an arbitrary datalog program, constructs an EDB-bounded datalog program in which every rule is adorned with a (non-recursive) conjunctive query that subsumes the result of the rule, thus acting as an upper bound. From such adornments, we define a notion of width based on (integral or fractional) edge-cover widths. Through the adornments and the width measure, we obtain, for every IDB predicate, worst-case upper bounds on their sizes, which are polynomial in the input data size, given a fixed program structure. Furthermore, with these size bounds, we also derive fixed-parameter tractable, output-sensitive asymptotic complexity bounds for evaluating the entire program. Additionally, by adapting our framework, we obtain a semi-decision procedure for datalog boundedness that efficiently rewrites most practical bounded programs into non-recursive equivalent programs.
Paper Structure (34 sections, 25 theorems, 50 equations, 1 figure, 1 algorithm)

This paper contains 34 sections, 25 theorems, 50 equations, 1 figure, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Datalog
  4. Unification
  5. Proof trees
  6. Derived atoms
  7. EDB-Adorned and EDB-Bounded Datalog Programs
  8. Basic Definitions
  9. Construction of EDB-Bounded Datalog Programs
  10. Algorithm to Construct EDB-Bounded Programs
  11. Base case
  12. Adornment propagation
  13. Membership checking
  14. Requirement of Simultaneous Unifiers in \ref{['alg:adornment']}
  15. Equivalence of EDB-Bounded Programs Produced by \ref{['alg:adornment']}
  16. ...and 19 more sections

Key Result

proposition 1

For any adornment relaxation function $g$ and safe datalog rule $\rho$ with only EDB atoms in the body, $g(\rho)$ subsumes $\rho$.

Figures (1)

  • Figure 1: Example of one generalized proof tree for transitive closure

Theorems & Definitions (62)

  • definition 1: EDB-adorned atom
  • definition 2: EDB-adorned datalog rule
  • definition 3: EDB-bounded rule
  • definition 4: EDB-bounded program
  • definition 5: adornment relaxation function
  • proposition 1
  • definition 6: membership checking function
  • definition 7: equivalent EDB-bounded program
  • theorem 1
  • proof
  • ...and 52 more