DatalogZ
DatalogZ (stylized as Datalogℤ) is an extension of Datalog with integer arithmetic and comparisons. The decision problem of whether or not a given ground atom (fact) is entailed by a DatalogZ program is RE-complete (hence, undecidable), which can be shown by a reduction to diophantine equations.[1]
Syntax
[edit]The syntax of DatalogZ extends that of Datalog with numeric terms, which are integer constants, integer variables, or terms built up from these with addition, subtraction, and multiplication. Furthermore, DatalogZ allows comparison atoms, which are atoms of the form t < s
or t <= s
for numeric terms t
, s
.[2]
Semantics
[edit]This section needs expansion with: a formal treatment of the semantics. You can help by adding to it. (March 2023) |
The semantics of DatalogZ are based on the model-theoretic (Herbrand) semantics of Datalog.[2]
Limit DatalogZ
[edit]The undecidability of entailment of DatalogZ motivates the definition of limit DatalogZ. Limit DatalogZ restricts predicates to a single numeric position, which is marked maximal or minimal. The semantics are based on the model-theoretic (Herbrand) semantics of Datalog. The semantics require that Herbrand interpretations be limit-closed to qualify as models, in the following sense: Given a ground atom of a limit predicate where the last position is a max (resp. min) position, if is in a Herbrand interpretation , then the ground atoms for (resp. ) must also be in for to be limit-closed.[3]
Example
[edit]Given a constant w
, a binary relation edge
that represents the edges of a graph, and a binary relation sp
with the last position of sp
minimal, the following limit DatalogZ program computes the relation sp
, which represents the length of the shortest path from w
to any other node in the graph:
sp(w, 0) :- . sp(y, m + 1) :- sp(x, m), edge(x, y).
See also
[edit]References
[edit]Notes
[edit]- ^ Dantsin, Evgeny; Eiter, Thomas; Gottlob, Georg; Voronkov, Andrei (2001-09-01). "Complexity and expressive power of logic programming". ACM Computing Surveys. 33 (3): 374–425. doi:10.1145/502807.502810. ISSN 0360-0300.. "For example, datalog (which is EXPTIME-complete) with linear arithmetic constraints [...] is undecidable." (Theorem 10.1)
- ^ a b Kaminski et al. 2017, pp. 2.
- ^ Kaminski et al. 2017, pp. 3.
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.