DatalogZ
DatalogZ (stylized as Datalogℤ) is an extension of Datalog that incorporates integer arithmetic and comparisons. Although the general language is undecidable due to unrestricted numeric operations, structurally constrained fragments provide a unified logical framework for declarative data analysis with strict termination guarantees.
Syntax and Semantics
[edit]The syntax of DatalogZ extends standard Datalog with numeric terms—comprising integers, variables, and functions built with addition, subtraction, and multiplication—and comparison atoms (such as t < s or t <= s). Its semantics build upon model-theoretic Herbrand interpretations evaluated under standard integer arithmetic. Fact entailment is defined via the least fixpoint of a transfinite immediate consequence operator.
Limit DatalogZ
[edit]To address the undecidability of generic DatalogZ, limit DatalogZ restricts intensional predicates to a single maximal or minimal numeric position. Its models are required to be limit-closed: if a max (resp. min) limit fact holds for an integer bound, it implicitly holds for all larger (resp. smaller) bounds.
Limit-Linear Fragment
[edit]Fact entailment remains undecidable in limit DatalogZ if multiplication is completely unrestricted. The limit-linear fragment restores decidability by enforcing a linearity condition: at most one argument in any multiplication operation may contain unguarded (unstratified) numeric variables. This constraint ensures that evaluating rule applicability reduces to an Integer Linear Programming problem, ensuring decidable termination.
Computational Complexity
[edit]The computational properties of limit-linear DatalogZ scale across structural tiers based on its syntactic fragments:
- Positive / Semi-positive: coNEXP-complete (combined complexity) and coNP-complete (data complexity). It captures \(\text{coNP}\) over ordered datasets.
- Stratified Negation: \(\Delta_2^{\text{EXP}}\)-complete (combined complexity) and \(\Delta_2^{\text{P}}\)-complete (data complexity). It captures \(\Delta_2^{\text{P}}\) over ordered datasets.
- Stable / Type-Consistent: EXP-complete (combined complexity) and P-complete (data complexity).
Stable and Type-Consistent Programs
[edit]To satisfy data-intensive database applications, researchers identify a semantic condition called stability. In stable programs, numeric arguments along a cyclic dependency graph cannot diverge infinitely. Because stability is undecidable to check statically, a localized syntactic check called type-consistency is used. Type-consistent programs guarantee tractable, polynomial-time data evaluation matching the bounds of standard Datalog.
Aggregation
[edit]Limit-linear DatalogZ supports native aggregation operators (such as `sum`, `count`, `max`, and `min`) to streamline data analysis tasks. Native aggregation constructs do not increase the core expressive power of the language; any program utilizing aggregates can be polynomially rewritten into an aggregate-free equivalent over ordered datasets using inductive counters.
See also
[edit]References
[edit]Notes
[edit]Sources
[edit]- Grau, Bernardo Cuenca; Horrocks, Ian; Kaminski, Mark; Kostylev, Egor V.; Motik, Boris (2020-02-25). "Limit Datalog: A Declarative Query Language for Data Analysis". ACM SIGMOD Record. 48 (4): 6–17. doi:10.1145/3385658.3385660. ISSN 0163-5808. S2CID 211520719.
- Kaminski, Mark; Grau, Bernardo Cuenca; Kostylev, Egor V.; Motik, Boris; Horrocks, Ian (2017-11-12). "Foundations of Declarative Data Analysis Using Limit Datalog Programs". arXiv:1705.06927 [cs.AI].
- Kaminski, Mark; Kostylev, Egor V.; Grau, Bernardo Cuenca; Motik, Boris; Horrocks, Ian (2021-12-22). "The Complexity and Expressive Power of Limit Datalog". Journal of the ACM. 69 (1): 6:1–6:83. doi:10.1145/3495009. ISSN 0004-5411. S2CID 246702614.