View source for DatalogZ

'''DatalogZ''' (stylized as '''{{proper name|Datalog<sub>ℤ</sub>}}''') 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 problem|undecidable]]), which can be shown by a [[Reduction (computability theory)|reduction]] to [[Hilbert's tenth problem|diophantine equations]].<ref>{{Cite journal |last1=Dantsin |first1=Evgeny |last2=Eiter |first2=Thomas |last3=Gottlob |first3=Georg |last4=Voronkov |first4=Andrei |date=2001-09-01 |title=Complexity and expressive power of logic programming |url=https://doi.org/10.1145/502807.502810 |journal=ACM Computing Surveys |volume=33 |issue=3 |pages=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)</ref>

== Syntax ==
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 {{dfni|comparison atoms}}, which are atoms of the form <code>t < s</code> or <code>t <= s</code> for numeric terms <code>t</code>, <code>s</code>.{{sfn|Kaminski|Grau|Kostylev|Motik|2017|pp=2}}

== Semantics ==
{{expand section|date=March 2023|with=a formal treatment of the semantics}}

The semantics of DatalogZ are based on [[Syntax and semantics of logic programming#Semantics|the model-theoretic (Herbrand) semantics of Datalog]].{{sfn|Kaminski|Grau|Kostylev|Motik|2017|pp=2}}

== Limit DatalogZ ==
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 {{dfni|limit-closed}} to qualify as models, in the following sense: Given a ground atom <math>a=r(c_1, \ldots, c_n)</math> of a limit predicate <math>r</math> where the last position is a max (resp. min) position, if <math>a</math> is in a Herbrand interpretation <math>I</math>, then the ground atoms <math>r(c_1,\ldots,k)</math> for <math>k > c_n</math> (resp. <math>k < c_n</math>) must also be in <math>I</math> for <math>I</math> to be limit-closed.{{sfn|Kaminski|Grau|Kostylev|Motik|2017|pp=3}}

=== Example ===
Given a constant <code>w</code>, a binary relation <code>edge</code> that represents the edges of a [[Graph (abstract data type)|graph]], and a binary relation <code>sp</code> with the last position of <code>sp</code> minimal, the following limit DatalogZ program computes the relation <code>sp</code>, which represents the length of the shortest path from <code>w</code> to any other node in the graph:

<syntaxhighlight lang="prolog">
sp(w, 0) :- .
sp(y, m + 1) :- sp(x, m), edge(x, y).
</syntaxhighlight>

== See also ==
* [[Constraint logic programming]]

== References ==
=== Notes ===
{{Reflist}}

=== Sources ===
* {{Cite journal |last1=Grau |first1=Bernardo Cuenca |last2=Horrocks |first2=Ian |last3=Kaminski |first3=Mark |last4=Kostylev |first4=Egor V. |last5=Motik |first5=Boris |date=2020-02-25 |title=Limit Datalog: A Declarative Query Language for Data Analysis |url=https://doi.org/10.1145/3385658.3385660 |journal=ACM SIGMOD Record |volume=48 |issue=4 |pages=6–17 |doi=10.1145/3385658.3385660 |s2cid=211520719 |issn=0163-5808}}
* {{Cite arXiv |last1=Kaminski |first1=Mark |last2=Grau |first2=Bernardo Cuenca |last3=Kostylev |first3=Egor V. |last4=Motik |first4=Boris |last5=Horrocks |first5=Ian |date=2017-11-12 |title=Foundations of Declarative Data Analysis Using Limit Datalog Programs |class=cs.AI |eprint=1705.06927 }}
* {{Cite journal |last1=Kaminski |first1=Mark |last2=Kostylev |first2=Egor V. |last3=Grau |first3=Bernardo Cuenca |last4=Motik |first4=Boris |last5=Horrocks |first5=Ian |date=2021-12-22 |title=The Complexity and Expressive Power of Limit Datalog |url=https://doi.org/10.1145/3495009 |journal=Journal of the ACM |volume=69 |issue=1 |pages=6:1–6:83 |doi=10.1145/3495009 |s2cid=246702614 |issn=0004-5411}}

[[Category:Logic in computer science]]
[[Category:Computer programming]]