A Formal Comparison between Datalog-based Languages for Stream Reasoning
(extended version)

Nicola Leone 1Department of Mathematics and Computer Science, University of Calabria, Rende, Italy
, 1name.surname@unical.it Marco Manna 1Department of Mathematics and Computer Science, University of Calabria, Rende, Italy
, 1name.surname@unical.it Maria Concetta Morelli 2Department of Mathematics and Computer Science, University of Calabria, Rende, Italy
2maria.morelli@unical.it Simona Perri 1Department of Mathematics and Computer Science, University of Calabria, Rende, Italy
, 1name.surname@unical.it

Abstract

The paper investigates the relative expressiveness of two logic-based languages for reasoning over streams, namely LARS Programs — the language of the Logic-based framework for Analytic Reasoning over Streams called LARS — and LDSR — the language of the recent extension of the $I$ -DLV system for stream reasoning called I-DLV-sr. Although these two languages build over Datalog, they do differ both in syntax and semantics. To reconcile their expressive capabilities for stream reasoning, we define a comparison framework that allows us to show that, without any restrictions, the two languages are incomparable and to identify fragments of each language that can be expressed via the other one.

Keywords:

Stream Reasoning, Datalog, Knowledge Representation and Reasoning, Relative Expressiveness

\tocauthor

Nicola Leone, Marco Manna, Maria Concetta Morelli, Simona Perri

1 Introduction

Stream Reasoning (SR) DBLP:journals/datasci/DellAglioVHB17 is a recently emerged research area that consists in the application of inference techniques to heterogeneous and highly dynamic streaming data. Stream reasoning capabilities are nowadays a key requirement for deploying effective applications in several real-world domains, such as IoT, Smart Cities, Emergency Management. Different SR approaches have been proposed in contexts such as Complex Event Processing, Semantic Web and Knowledge Representation and Reasoning (KRR) DBLP:journals/ijsc/BarbieriBCVG10; hoeksema2011high; DBLP:conf/lpnmr/PhamAM19; DBLP:conf/semweb/PhuocDPH11. In the KRR research field, the Answer Set Programming (ASP) declarative formalism DBLP:journals/cacm/BrewkaET11; DBLP:conf/ijcai/GebserLMPRS18 has been acknowledged as a particularly attractive basis for SR DBLP:journals/datasci/DellAglioVHB17 and a number of SR solutions relying on ASP have been recently proposed beck2018lars; bazoobandi2017expressive; beck2018ticker; eiter2019distributed; DBLP:conf/bigdataconf/RenCNX18; DBLP:conf/rr/MileoAPH13; DBLP:conf/lpnmr/PhamAM19; DBLP:conf/ai/DoLL11; DBLP:conf/lpnmr/GebserGKS11; DBLP:journals/tplp/CalimeriMMMPZ21. Among these, I-DLV-sr DBLP:journals/tplp/CalimeriMMMPZ21 is a SR system that efficiently scale over real-world application domains thanks to a proper integration of the well-established stream processor Apache Flink carbone2015apache and the incremental ASP reasoner $I$ $^{2}$ -DLV DBLP:journals/tplp/IanniPZ20. Its input language, called LDSR (the Language of $I$ -DLV for Stream Reasoning) inherits the highly declarative nature and ease of use from ASP, while being extended with new constructs that are relevant for practical SR scenarios.

Although LDSR enjoys valuable knowledge modelling capabilities together with an efficient and effective reasoner, it would be desirable to formally investigate its expressive power. This is exactly the mission of the present paper. To this aim, the prime objective is to compare LDSR with one of the most famous and well-studied formalisms for reasoning over streams that goes under the name of LARS Programs (the language of LARS), where LARS is the Logic-based framework for Analytic Reasoning over Streams beck2018lars. More precisely, the paper investigates the relative expressiveness of LDSR and LARS Programs. Despite the fact that these languages build over Datalog and represent the information via sets of ASP ground predicate atoms associated with different time points, unfortunately they overall differ both in syntax and semantics. In particular, LDSR associates information that is true at every time point with standard ASP facts, whereas LARS Programs involve background atoms whose truth is not directly associated with all the time points. Moreover, given an input stream, LDSR returns a single set of information related to the most recent time point (streaming model), whereas LARS Programs associate, for each different time point of the stream, another stream called answer stream at that time point.

To reconcile the expressive capabilities for stream reasoning of LDSR and LARS Programs, we first define a comparison framework that allows to understand in which cases, starting from the same input stream, both languages may produce the same output. Inside this framework, we identify three output profiles —called atomic, bound, and full— that fix the form of the output stream. Without any restriction on the two languages, the paper shows that they are incomparable under all the output profiles. Eventually, for each output profile, the paper isolates large fragments of each of the two languages that can be expressed via the other one.

2 Preliminaries

We assume to have finite sets $V$ , $C$ , $P$ and $U$ consisting of variables, constants, predicate names and $t i m e$ $v a r i a b l e s$ respectively; we constrain $V$ and $C$ to be disjoint. A term is either a variable in $V$ or a constant in $C$ . A predicate atom has the form $p (t_{1}, \dots, t_{n})$ , where $p \in P$ is a predicate name, $t_{1}, \dots, t_{n}$ are terms and $n \geq 0$ is the arity of the predicate atom; a predicate atom $p ()$ of arity $0$ can be also denoted by $p$ . A predicate atom is ground if none of its terms is a variable. We denote by $G$ the set of all ground predicate atoms constructible from predicate names in $P$ and constants in $C$ . We divide the set of predicates $P$ into two disjoint subsets, namely the extensional predicates $P^{ε}$ and the intensional predicates $P^{I}$ . Extensional predicates are further partitioned into $P_{B}^{ε}$ for background data and $P_{S}^{ε}$ for data streams. The mentioned partitions are analogously defined for ground atoms $G^{I}$ , $G_{B}^{ε}$ and $G_{S}^{ε}$ . In what follows we will introduce different types of constructs peculiar to the two languages considered in this paper. In both, given a set of constructs $C$ , we will denote by $p r e d (C)$ the set of predicates appearing in $C$ .

A stream $Σ$ is a sequence of sets of ground predicate atoms $⟨ S_{0}, \dots, S_{n} ⟩$ such that for $0 \leq i \leq n$ , $S_{i} \subseteq G$ . Each natural number $i$ is called time point. A ground predicate atom $a \in S_{i}$ is true at the $i$ -th time point. Given a value $m \in N$ s.t. $0 \leq m \leq n$ , we define the restriction of $Σ$ to $m$ the stream $⟨ S_{0}, \dots, S_{m} ⟩$ denoted with $Σ_{|_{m}}$ . Moreover, let $F \subseteq P$ we indicate with $Σ_{|_{F}}$ the stream $⟨ S_{0}^{'}, \dots, S_{n}^{'} ⟩$ with $S_{i}^{'} = ⋃_{{a \in S_{i} | p r e d (a) \in F}} a$ for each $i \in {0, \dots, n}$ . A subset of a stream $Σ = ⟨ S_{0}, \dots, S_{n} ⟩$ is a stream $Σ^{'} = ⟨ S_{0}^{'}, \dots, S_{n}^{'} ⟩$ such that $S_{i}^{'} = \emptyset$ for each $i \notin t (Σ^{'})$ where $t (Σ^{'})$ is a subset of consecutive numbers of the set ${0, \dots, n}$ and for each $i \in t (Σ^{'})$ $S_{i}^{'} \subseteq S_{i}$ . For a stream $Σ = ⟨ S_{0}, \dots, S_{n} ⟩$ , a backward observation identifies ground predicate atoms that are true at some time points preceding the $n$ -th time point. More formally, given a stream $Σ = ⟨ S_{0}, \dots, S_{n} ⟩$ and a set of numbers $D$ $\subset N$ , we define the backward observation of $Σ$ w.r.t. $D$ as the family of sets ${S_{i} | i = n - d with d \in D \land i \geq 0}$ , and we denote it as $O (Σ, D)$ . Given $w \in N$ , a backward observation of $Σ$ w.r.t. ${0, \dots, w}$ is called window.

2.1 Lars syntax and semantics

A window function is a function $f_{w}$ that returns, given a stream $Σ$ and a time point $t \in {1, . . ., n}$ , a substream of $Σ$ . We consider only time-based window functions, which select all the atoms appearing in the last $w$ time points, to which a window is trivially associated according to the definition above. Given a predicate atom $a$ , a term $t \in N \cup U$ and a window function $f_{w}$ , formulas $α$ are defined by the following grammar:

α ::= a | \neg α | α \land α | α \lor α | α \to α | ⋄ α | □ α | @_{t} α | ⊞^{f_{w}} α | ▹ α .

A LARS program P is a set of rules of the form $α \leftarrow β_{1}, \dots, β_{n}$ , where $α, β_{1}, \dots, β_{n}$ are formulas. Given a rule $r$ , we call $α$ the head of $r$ , denoted with $H (r)$ , and we call the conjunction $β_{1} \land \dots \land β_{n}$ the body of $r$ , denoted with $B (r)$ . A ground formula can be satisfied at a time point $t$ in a $s t r u c t u r e$ that is a triple $M = (Σ, W, B)$ where $Σ$ is a stream, $W$ is a set of window functions and $B \subseteq G_{B}^{ε}$ . Let $Σ^{'} \subseteq Σ$ , we start defining the entailment relation $⊩$ between $(M, Σ^{'}, t)$ and formulas:

$M, Σ^{'}, t ⊩ a$ iff $a \in S_{t}$ or $a \in B$
$M, Σ^{'}, t ⊩ \neg α$ iff $M, t ⊮ α$
$M, Σ^{'}, t ⊩ α \land β$ iff $M, t ⊩ α$ and $M, t ⊩ β$
$M, Σ^{'}, t ⊩ α \lor β$ iff $M, t ⊩ α$ or $M, t ⊩ β$
$M, Σ^{'}, t ⊩ α \to β$ iff $M, t ⊮ α$ or $M, t ⊩ β$
$M, Σ^{'}, t ⊩ ⋄ α$ iff $M, Σ^{'}, t ⊩ α$ for some $t^{'} \in t (Σ^{'})$
$M, Σ^{'}, t ⊩ □ α$ iff $M, Σ^{'}, t ⊩ α$ for all $t^{'} \in t (Σ^{'})$ ,
$M, Σ^{'}, t ⊩ @_{t^{'}} α$ iff $M, Σ^{'}, t^{'} ⊩ α$ and $t^{'}$ $\in t (Σ^{'})$ ,
$M, Σ^{'}, t ⊩ ⊞^{f_{w}} α$ , iff $M, Σ^{''}, t ⊩ α$ where $Σ^{''} = f_{w} (Σ^{'}, t),$
$M, Σ^{'}, t ⊩ ▹ α$ iff $M, Σ, t ⊩ α$ .

The structure $M = (Σ, W, B)$ satisfies $α$ at time $t$ ( $M, t ⊨ α)$ if $M, Σ^{'}, t ⊩ α$ . Given a ground LARS program $P$ , a stream $Σ$ and a structure $M$ we say that: $(i)$ $M$ is a model of rule $r \in P$ for $I$ at time $t$ , denoted $M, t ⊨ r$ , if $M, t ⊨ B (r) \to H (r)$ ; $(i i)$ $M$ is a model of $P$ for $I$ at time $t$ , denoted $M, t ⊨ P$ , if $M, t ⊨ r$ for all rules $r \in P$ ; $(i i i)$ $M$ is a minimal model, if no model $M^{'} = (Σ^{'}, W, B)$ of $P$ for $I$ at time $t$ exists such that $Σ^{'} \subset Σ$ and $t (Σ) = t (Σ^{'})$ ; and $(i v)$ The reduct of a program $P$ with respect to $M$ at time $t$ is defined by $P^{M, t} = {r \in P | M, t ⊨ B (r)}$ . Fixed an input stream $I$ , contains only atoms belong to $G_{S}^{ε}$ , we call $i n t e r p r e t a t i o n s t r e a m$ $f o r I$ any stream $Σ$ such that all atoms that occur in $Σ$ but not in $I$ have intensional predicates. An interpretation stream $Σ$ for a stream $I$ is an $a n s w e r s t r e a m$ of a program $P f o r I a t t$ , if $M = (Σ, W, B)$ is a $\subseteq$ -minimal model of the reduct $P^{M, t}$ for $I$ at time $t$ . The semantics of the non-ground programs is given by the answer streams of according groundings, obtained by replacing variables with constants from $C$ , respectively time points from $t (Σ)$ , in all possible ways. We consider LARS programs with a single answer stream for each time point, denoted with ${LARS}_{D}$ , and we indicate the single answer stream of $P$ for $I$ at $t$ with $A S (P, I, t)$ .

2.2 Ldsr syntax and semantics

Given a predicate atom $a$ , a term $c \in C \cap N^{+}$ , a counting term $t \in (C \cap N^{+}) \cup V$ , and a finite non-empty set $D = {d_{1}, \dots, d_{m}} \subset N$ , we define three types of streaming atoms:

a a t l e a s t c i n {d_{1}, \dots, d_{m}} | a a l w a y s i n {d_{1}, \dots, d_{m}} | a c o u n t t i n {d_{1}, \dots, d_{m}}

In particular, if $D$ is of the form ${0, . . ., w}$ , then this set can be alternatively written as $[w]$ inside streaming atoms; also we may write $a$ in place of $a a t l e a s t 1 i n [0]$ . A streaming atom $α$ (resp., $n o t α$ ) is said to be a positive streaming literal (resp., negative streaming literal), where $n o t$ denotes negation as failure. A streaming literal is said to be harmless if it has form $a a t l e a s t c i n D$ or $a a l w a y s i n$ $D$ ; otherwise, it is said to be non-harmless. A streaming literal is said to be ground if none of its terms is a variable.

A rule is a formula of form $(1) a\,: {-}l1,…,lb.$ or $(2) #tempa\,: {-}l1,…,lb.$ , where $a$ is a predicate atom, $b \geq 0$ and $l_{1}, \dots, l_{b}$ represent a conjunction of literals (streaming literals or other literals defined in the ASP-Core-2 standard DBLP:journals/tplp/CalimeriFGIKKLM20).

For a rule $r$ , we say that the head of $r$ is the set $H (r) = {a}$ , whereas the set $B (r) = {l_{1}, \dots, l_{b}}$ is referred to as the body of $r$ . A rule $r$ is safe if all variables in $H (r)$ or in a negative streaming literal of $B (r)$ also appear in a positive streaming literal of $B (r)$ .

A program $P$ is a finite set of safe rules. We denote with ${f o r m}_{(1)} (P)$ the set of rules of $P$ of form (1) and with ${f o r m}_{(2)} (P)$ the set of rules of $P$ of form (2).

A program $P$ is stratified if there is a partition of disjoint sets of rules $P = Π_{1} \cup \dots \cup Π_{k}$ (called strata) such that for $i \in {1, \dots, k}$ both these conditions hold: ( $i$ ) for each harmless literal in the body of a rule in $Π_{i}$ with predicate $p$ , ${r \in P | H (r) =$ ${p (t_{1}, \dots, t_{n})}} \subseteq ⋃_{j = 1}^{i} Π_{j}$ ; ( $i i$ ) for each non-harmless literal in the body of a rule in $Π_{i}$ with predicate $p$ , ${r \in P | H (r) =$ ${p (t_{1}, \dots, t_{n})}} \subseteq ⋃_{j = 1}^{i - 1} Π_{j}$ . We call $Π_{1}, \dots, Π_{k}$ a stratification for $P$ and $P$ is stratified by $Π_{1}, \dots, Π_{k}$ . An LDSR program is a program being also stratified.

A backward observation allows to define the truth of a ground streaming literal at a given time point. Given a stream $Σ = ⟨ S_{0}, \dots, S_{n} ⟩$ , $D = {d_{1}, \dots, d_{m}} \subset N$ , $c \in C ∖ {0}$ and the backward observation $O (Σ, D)$ , Table 1 reports when $Σ$ entails a ground streaming atom $α$ (denoted $Σ ⊨ α$ ) or its negation ( $Σ ⊨ n o t α$ ). If $Σ ⊨ α$ ( $Σ ⊨ n o t α$ ) we say that $α$ is true (false) at time point $n$ .

$α$	$Σ ⊨ α$	$Σ ⊨ n o t α$
$a a t l e a s t c i n {d_{1}, \dots, d_{m}}$	$\| {A \in O (Σ, D) : a \in A} \| \geq c$	$\| {A \in O (Σ, D) : a \in A} \| < c$
$a a l w a y s i n {d_{1}, \dots, d_{m}}$	$\forall A \in O (Σ, D), a \in A$	$\exists A \in O (Σ, D) : a \notin A$
$a c o u n t c i n {d_{1}, \dots, d_{m}}$	$\| {A \in O (Σ, D) : a \in A} \| = c$	$\| {A \in O (Σ, D) : a \in A} \| \neq c$

Table 1: Entailment of ground streaming literals.

To make a comparison between ${LARS}_{D}$ and LDSR, we defined also for LDSR a model-theoretic semantics that can be shown to be equivalent to the operational semantics originally defined. Moreover, besides the concept of streaming model for LDSR, we defined the concept of answer stream.

Consider an LDSR program $P$ . Given a rule $r \in P$ , the ground instantiation $G r (r)$ of $r$ denotes the set of rules obtained by applying all possible substitutions $σ$ from the variables in $r$ to elements of $C$ . In particular, to the counting terms are applied only constants belong to $C \cap N^{+}$ . Similarly, the ground instantiation $G r (P)$ of $P$ is the set $⋃_{r \in P} G r (r)$ . Given a ground rule $r \in P$ , a stream $Σ = ⟨ S_{0}, \dots, S_{n} ⟩$ and a stream $Σ^{'} = ⟨ S_{0}^{'}, \dots, S_{n}^{'} ⟩$ such that $Σ \subseteq Σ^{'}$ , we say that $Σ^{'}$ is a model of $r$ for $Σ$ , denoted $Σ^{'} ⊨ r$ , if $Σ^{'} ⊨ H (r)$ when $Σ^{'} ⊨ B (r)$ . We say that $Σ^{'}$ is a model of $P$ for $Σ$ , denoted $Σ^{'} ⊨ P$ , if $Σ^{'} ⊨ r$ for all rules $r \in G r (P)$ . Moreover, $Σ^{'}$ is a minimal model, if no model $Ω$ of $P$ exists such that $Ω \subset Σ^{'}$ and $t (Ω) = t (Σ^{'})$ . Let $Σ^{'}$ be a model of $P$ for $Σ$ , an atom $a \in S_{n}^{'}$ is temporary in $Σ^{'}$ if $a \notin S_{n}$ and there exists no rule $r \in {f o r m}_{(1)} (P)$ such that $Σ^{'} ⊨ B (r)$ and $Σ^{'} ⊨ H (r)$ . Accordingly, let $T (S_{n}^{'})$ be the set of all temporary atoms in $S_{n}^{'}$ , the stream $⟨ S_{0}^{'}, \dots, S_{n}^{'} ∖ T (S_{n}^{'}) ⟩$ is called the permanent part of $Σ^{'}$ . Eventually, the reduct of $P$ w.r.t. $Σ^{'}$ , denoted by $P^{Σ^{'}}$ , consists of the rules $r \in G r (P)$ such that $Σ^{'} ⊨ B (r)$ .

Definition 1

Given an LDSR program $P$ , a stream $Σ = ⟨ S_{0}, \dots, S_{n} ⟩$ and a stream $Σ^{'} = ⟨ S_{0}^{'}, \dots, S_{n}^{'} ⟩$ such that $Σ \subseteq Σ^{'}$ , $Σ^{'}$ is called answer stream and $S_{n}^{'}$ streaming model of $P$ for $Σ$ if: $(1)$ if $n > 0$ , $⟨ S_{0}^{'} ⟩$ is the permanent part of the minimal model $M$ of the reduct $P^{M}$ for the stream $⟨ S_{0} ⟩$ ; $(2)$ if $n > 0$ , for all $i \in 1, \dots, n - 1$ , $Σ_{| i}^{'}$ is the permanent part of the minimal model $M$ of the reduct $P^{M}$ for the stream $⟨ S_{0}^{'}, \dots, S_{i - 1}^{'}, S_{i} ⟩$ ; and $(3)$ $Σ^{'}$ is a minimal model of the reduct $P^{Σ^{'}}$ for the stream $⟨ S_{0}^{'}, \dots, S_{n - 1}^{'}, S_{n} ⟩$ .

Note that, differently from LARS, for which the information associated with each time point is entirely derived at the time point of evaluation, for LDSR, each time point $t$ in the answer stream is associated with the information derived when the time point $t$ has been evaluated. In other words, the answer stream for LDSR is obtained by collecting the results of the previous time points and integrating them with the result of the time point of evaluation.

3 Framework

In this section, we present the framework that has been designed for comparing the languages ${LARS}_{D}$ and LDSR. The comparison focuses on different parts of the answer stream. In particular, given an input stream $S = ⟨ S_{0}, \dots, S_{n} ⟩$ , when referring to an evaluation time point $t \leq n$ , one could compare the answer streams only at $t$ , or in all the time points up to $t$ or also in all time points up to $n$ . To this aim, we define three types of streams. Given $n \in N$ and $t \in {0, \dots, n}$ , we say that a stream $S = ⟨ S_{0}, \dots, S_{n} ⟩$ is of $t y p e$ $t - a t o m i c$ if $S_{i} = \emptyset$ for each $i \in {0, \dots, n} ∖ {t}$ ; $t - b o u n d$ if $S_{i} = \emptyset$ for each $i \in {t + 1, \dots, n}$ ; and $t - f u l l$ if $S_{i}$ may be nonempty for each $i \in {0, \dots, n}$ .

Consider a language $L \in {LDSR, {LARS}_{D}}$ , an input stream $I = ⟨ I_{0}, \dots, I_{n} ⟩$ , a set of ground predicate atoms $B \subseteq G_{B}^{ε}$ and a program $P \in L$ , we call $(I, B, P)$ an $L -$ tuple. According to the three types of streams, for a $L -$ tuple and for each time point $t \in {0, \dots, n}$ , we now define three types of output streams for each language $L$ .

Given a $LDSR - t u p l e$ $(I, B, P)$ and a time point $t \in {0, \dots, n}$ , we define:

$t - a t o m i c (I, B, P) = ⟨ O_{0}, \dots, O_{n} ⟩$ where $O_{i} = \emptyset$ for $i \neq t$ and $O_{t}$ is the streaming model of $P \cup {b . | b \in B}$ on $I_{|_{t}} = ⟨ I_{0}, \dots, I_{t} ⟩$ .
$t - b o u n d (I, B, P) = ⟨ O_{0}, \dots, O_{n} ⟩$ , where $⟨ O_{0}, \dots, O_{t} ⟩$ is the answer stream of $P \cup {b . | b \in B}$ for $I_{|_{t}} = ⟨ I_{0}, \dots, I_{t} ⟩$ and $O_{i} = \emptyset$ for $t < i \leq n$ .
$t - f u l l (I, B, P) = ⟨ O_{0}, \dots, O_{n} ⟩$ where $⟨ O_{0}, \dots, O_{t} ⟩$ is the answer stream of $P \cup {b . | b \in B}$ for $I_{|_{t}} = ⟨ I_{0}, \dots, I_{t} ⟩$ and $O_{i} = I_{i} \cup B$ for $t < i \leq n$ .

Analogously, given a ${LARS}_{D} - t u p l e$ $(I, B, P)$ and a time point $t \in {0, \dots, n}$ , and the answer stream $A S (P, I, t) = ⟨ A_{0}, \dots, A_{n} ⟩$ , we define:

$t - a t o m i c (I, B, P) = ⟨ O_{0}, \dots, O_{n} ⟩$ where $O_{i} = \emptyset$ for $i \neq t$ and $O_{t} = A_{t} \cup B$ .
$t - b o u n d (I, B, P) = ⟨ O_{0}, \dots, O_{n} ⟩$ , where $O_{i} = A_{i} \cup B$ for $0 \leq i \leq t$ and $O_{i} = \emptyset$ for $t < i \leq n$ .
$t - f u l l (I, B, P) = ⟨ O_{0}, \dots, O_{n} ⟩$ where $O_{i} = A_{i} \cup B$ for $0 \leq i \leq n$ .

We now define when a fragment of a language can be expressed in the other one in our framework. In particular, we differentiate expressible fragments from strictly expressible fragments. Given a stream form $ϕ \in {a t o m i c, b o u n d, f u l l}$ ,and $L_{1}, L_{2} \in {LDSR$ , ${LARS}_{D}}$ with $L_{1} \neq L_{2}$ , a fragment $F \subset L_{1}$ is $ϕ - e x p r e s s i b l e$ via $L_{2}$ if there exists a mapping $ρ : F \to L_{2}$ such that, for each $F$ -tuple $(I, B, P)$ and for each time point of evaluation $t \in {0, \dots, n}$ , it holds that $t - ϕ (I, B, P) = t - ϕ (I, B, ρ (P))_{|_{p r e d (P \cup I \cup B)}}$ ; moreover, $F$ is $s t r i c t l y ϕ - e x p r e s s i b l e$ via $L_{2}$ if $t - ϕ (I, B, P) = t - ϕ (I, B, ρ (P))$ . Basically, for the non strict expressiveness, a translation into the other language is possible but it can involve the addition of auxiliary predicates, while for the strict one, there is a translation that does not require auxiliary predicates and thus for which the outputs coincide without the need of any filtering.

We are now ready to compare the two languages. The first result of the comparison is that, without any restrictions, the two languages are incomparable. The following two propositions describe the results. The ideas behind the formal demonstrations, which are instead reported in appendix 0.B, are also introduced.

Proposition 1

${LARS}_{D}$ is not $a t o m i c - e x p r e s s i b l e$ via LDSR.

To see this, consider the simple ${LARS}_{D}$ program $P_{1}$ = ${@_{T - 1} a \leftarrow @_{T} c .}$ . This program, that expresses that the presence of an atom $c$ in a time point infers the presence of an atom $a$ in the previous time point, is not expressible in LDSR since in its semantic the information associated at every time point are relative only to the information received and inferred up to it.

Proposition 2

LDSR is not $a t o m i c - e x p r e s s i b l e$ via ${LARS}_{D}$ .

To prove this result, consider the following LDSR program $P2={a(Y)\,: {-}a(X),b(X,Y).}$ where the predicate $a$ belongs to the input predicates $P_{S}^{ε}$ . The program $P_{2}$ is not expressible in ${LARS}_{D}$ since its semantics avoids to infer ground atoms over input predicates.

Since $t - a t o m i c (I, B, P) \neq t - a t o m i c (I, B, ρ (P))$ implies $t - ϕ (I, B, P) = t - ϕ (I, B, ρ (P))$ holds for $ϕ \in {b o u n d, f u l l}$ , Proposition 1 and 2 imply the following result.

Theorem 3.1

${LARS}_{D}$ and LDSR are incomparable under each of the three stream forms.

Given the incomparability of the languages, we introduced some restrictions to identify fragments of a language expressible in the other. Up to now, we identified seven fragments that are described in detail in sections 3.1 and 3.2. Here, we briefly discuss their relations and expressiveness (see Fig. 3 and Tables 3 and 3). In particular, Table 3 presents the fragments of ${LARS}_{D}$ $F_{1}$ , $F_{2}$ and $F_{3}$ . All of them are strictly expressible via LDSR. $F_{1}$ is the largest identified fragment and it is atomic-expressible; $F_{2}$ is obtained from $F_{1}$ by imposing some restriction and it is bound-expressible, while $F_{3}$ is obtained by further restricting $F_{2}$ , and allows for achieving full-expressivity.

Table 2:

{LARS}_{D}

to LDSR

$ϕ$	strictly	not strictly
$a t o m i c$	$F_{1}$	$F_{1}$
$b o u n d$	$F_{2}$	$F_{2}$
$f u l l$	$F_{3}$	$F_{3}$

Table 3: LDSR to

{LARS}_{D}

$ϕ$	strictly	not strictly
$a t o m i c$	$F_{6} \cup F_{7}$	$F_{4}$
$b o u n d$	$F_{6} \cup F_{7}$	$F_{4}$
$f u l l$	$F_{6}$	$F_{5}$

As for LDSR, Table 3 summarizes its identified fragments $F_{4}$ , $F_{5}$ , $F_{6}$ and $F_{7}$ . The largest fragment is $F_{4}$ , which is bound-expressible via ${LARS}_{D}$ ; the fragment $F_{5}$ , that restricts $F_{4}$ , allows full expressiveness; the other two fragments allows for strictly expressiveness: $F_{6}$ further restricts $F_{5}$ , and it is full-expressible, while $F_{7}$ is obtained by imposing restrictions on $F_{4}$ and is bound-expressible.

3.1 ${LARS}_{D}$ to Ldsr

Here we present the identified fragments of ${LARS}_{D}$ . We consider two types of rules:

(I) □ (a \leftarrow β_{1} \land \dots \land β_{b}) and (I I) a \leftarrow β_{1}, \dots, β_{b}

where $a$ is an intensional predicate atom and $β_{i} \in {⊞^{m} ◊ p, ⊞^{m} □ p, p, ⊞^{0} @_{T} ⊤ \land @_{T - K} p, \neg ⊞^{m} ◊ p, \neg ⊞^{m} □ p, \neg p, \neg (⊞^{0} @_{T} ⊤ \land @_{T - K} p) | p$ is a predicate atom, $T \in U$ and $m \in N}$ for $i \in {1, \dots, b}$ . For a rule of type $(I)$ , we denote as $c o n s (r)$ the consequent ${a}$ of the implication, and with $p r e m (r)$ the set of formulas ${β_{1}, \dots, β_{b}}$ in the premise; moreover, for a rule of type $(I I)$ , we denote with $h e a d (r)$ the atom ${a}$ and with $b o d y (r)$ the set of formulas ${β_{1}, \dots, β_{b}}$ . Let $P$ be a ${LARS}_{D}$ program, we denote with $t y p e_{I} (P)$ the set of rules of $P$ of type $(I)$ and with $t y p e_{I I} (P)$ the set of rules of $P$ of type $(I I)$ .
We say that a predicate $p$ is $m a r k e d$ if there are two rules $r \in t y p e_{I} (P)$ and $r^{'} \in t y p e_{I I} (P)$ with $p = p r e d (c o n s (r))$ , $h \in p r e d (p r e m (r))$ and $h = p r e d (h e a d (r^{'}))$ . The set of marked predicates of a program $P$ is denoted with $M (P)$ .

Consider a ${LARS}_{D}$ program $P$ containing rules of type $(I)$ and $(I I)$ only. Let $P_{1} = t y p e_{I} (P)$ and $P_{2} = t y p e_{I I} (P)$ . We define the graph $G (P) = ⟨ N, A ⟩$ , where: $(1)$ $N = (\cup_{r \in P_{1}} p r e d (c o n s (r)))$ $\cup$ $(\cup_{r \in P_{2}} p r e d (h e a d (r)))$ ; $(2)$ $(q, p, ‘ ‘$ + $") \in A$ if there exists a rule $r \in P_{1}$ with $p r e d (c o n s (r)) = p$ and $q \in p r e d (p r e m (r))$ occurring in a formula without negation or if there exists a rule $r^{'} \in P_{2}$ with $p r e d (h e a d (r^{'})) = p$ and $q \in p r e d (b o d y (r^{'}))$ occurring in a formula without negation; and $(3)$ $(q, p, ‘ ‘$ - $") \in A$ if there exists a rule $r \in P_{1}$ with $p r e d (c o n s (r)) = p$ and $q \in p r e m (r)$ occurs in a formula with negation or if there exists a rule $r^{'} \in P_{2}$ with $p r e d (h e a d (r^{'})) = p$ and $q \in p r e d (b o d y (r^{'}))$ occurring in a formula with negation.

Definition 2

Fragment $F_{1}$ of ${LARS}_{D}$ collects all the programs $P$ that meet the next conditions: $(i)$ $P = t y p e_{I} (P) \cup t y p e_{I I} (P)$ ; $(i i)$ $\cup_{r \in t y p e_{I} (P)} p r e d (p r e m (r)) \cap M (P) = \emptyset$ ; $(i i i)$ $\cup_{r \in t y p e_{I I} (P)} p r e d (b o d y (r)) \cap M (P) = \emptyset$ ; $(i v)$ no cycle in $G (P)$ contains an arc labeled with “-”.

Roughly, $F_{1}$ contains only programs that are stratified w.r.t negation, featuring only rules of types (I) and (II), where no marked predicate appears in premises and in bodies.

Proposition 3

$F_{1}$ is strictly atomic-expressible via LDSR.

Indeed, it can be shown that there is a mapping $ρ_{1} : F_{1} \to LDSR$ such that for each $F_{1} - t u p l e$ $(I, B, P)$ and for each time point of evaluation $t \in {0, \dots, n}$ , it holds that $t - a t o m i c (I, B, P) = t - a t o m i c (I, B, ρ_{1} (P))$ . In particular, given a program $P \in F_{1}$ , the LDSR program $ρ_{1} (P)$ is obtained by replacing:

each rule $□ (a \leftarrow β_{1}, \dots, β_{m}$ ) of type $(I)$ with the LDSR rule $a\,: {-}f(β1),…,f(βm)$ of form $(1)$
each rule $a \leftarrow β_{1}, \dots, β_{m}$ of type $(I I)$ with the LDSR rule $#tempa\,: {-}f(β1),…,f(βm)$ of form $(2)$

where $f$ associates each ${LARS}_{D}$ formula in the $F_{1}$ fragment with a LDSR streaming atom as reported below:

$f (⊞^{m} ◊ p) = p i n [m]$ .
$f (⊞^{m} □ p) = p a l w a y s i n [m]$ .
$f (p) = p$ .
$f (⊞^{0} @_{T} ⊤ \land @_{T - K} p) = p i n {k}$ .
$f (\neg β) = n o t f (β)$ where $β$ is a formula.

Intuitively, the idea of the mapping $ρ_{1}$ is that ${LARS}_{D}$ rules of type $(I)$ that must be evaluated at each time point are associated with $L D R S$ rules of form (1) and ${LARS}_{D}$ rules of type $(I I)$ that infer information only at the evaluation time point $t$ are associate with LDSR rules of form (2) which are evaluated at each time point but the derivations of the time points preceding $t$ have been forgotten via the $# t e m p$ operator. Moreover, we impose the restrictions $(i i)$ and $(i i i)$ for defining $F_{1}$ in order to achieve atomic-expressiveness; indeed, they ensure that, if in LDSR a permanent information is derived relying on a temporary information, this is not used to derive other information.

Now, we define the fragment $F_{2}$ that imposes an additional restriction w.r.t to $F_{1}$ , and the fragment $F_{3}$ that further restricts $F_{2}$ .

Definition 3

The fragment $F_{2}$ of ${LARS}_{D}$ is the subset of the programs of $F_{1}$ that meet the condition $(⋃_{r \in t y p e_{I I} (P)} p r e d (h e a d (r))) \cap ((⋃_{r \in t y p e_{I} (P)} p r e d (p r e m (r)) = \emptyset$ .

Proposition 4

$F_{2}$ is strictly bound-expressible via LDSR.

It can be shown that for the mapping $ρ_{2} = {ρ_{1}}_{|_{F_{2}}}$ , it holds that for each $F_{2} - t u p l e$ $(I, B, P)$ and for each time point of evaluation $t \in {0, \dots, n}$ , $t - b o u n d (I, B, P) = t - b o u n d (I, B, ρ_{2} (P))$ . Basically, the additional condition for fragment $F_{2}$ avoids that a temporary information associated to a time point can generate a permanent information.

We now show an example of a program belonging to fragment $F_{2}$ and its image with respect to the function $ρ_{2}$ . The example is taken from one of the tasks of the “model and solve” Stream Reasoning Hackathon 2021 DBLP:conf/esws/SchneiderALDP22. The task concerns urban traffic management. Traffic is observed from a top-down, third-person perspective, and vehicle movement flows in a given road network coded as Datalog facts are considered. We want to identify the vehicles that appear or disappear in the network. It is then necessary to note vehicles that were absent at the previous time point and are now present and vice versa. A rule of type $(I)$ is used to evaluate the presence of vehicles at the current and previous time points; then the obtained information is used in a rule of type $(I I)$ that detects the appearance or disappearance of a vehicle at the evaluation time point. This task can be modelled via the following program $P$ in $F_{2}$ :

□ (i n N e t w o r k (V e h) \leftarrow o n L a n e (V e h, X, Y)) . a p p e a r s (V e h) \leftarrow o n L a n e (V e h, X, Y), \neg ⊞^{0} @_{T} ⊤ \land @_{T - 1} i n N e t w o r k (V e h) . d i s a p p e a r s (V e h) \leftarrow ⊞^{0} @_{T} ⊤ \land @_{T - 1} i n N e t w o r k (V e h), \neg i n N e t w o r k (V e h) .

The corresponding LDSR program, image of the $ρ_{2}$ function, is:

inNetwork(Veh)\,: {-}onLane(Veh,X,Y).   #tempappears(Veh)\,: {-}onLane(Veh,X,Y),not inNetwork(Veh)in{1}.#tempdisappears(Veh)\,: {-}onLane(Veh,X,Y)in{1},not inNetwork(Veh).

Definition 4

The fragment $F_{3}$ of ${LARS}_{D}$ is the subset of the programs of $F_{2}$ that meet the condition $P = t y p e_{I I} (P)$ .

Proposition 5

$F_{3}$ is strictly full-expressible via LDSR.

Similarly to $F_{2}$ , it can be shown that, considering the mapping $ρ_{3} = {ρ_{1}}_{|_{F_{3}}}$ , it holds that that for each $F_{3} - t u p l e$ $(I, B, P)$ and for each time point of evaluation $t \in {0, \dots, n}$ , $t - f u l l (I, B, P) = t - f u l l (I, B, ρ_{3} (P))$ . Intuitively, since in LDSR the evaluation of a program with respect to a time point $t$ can not add information in the output stream at time points that are subsequent to $t$ , to achieve full expressiveness, we impose the restriction to rules of type type $(I I)$ in ${LARS}_{D}$ as these are evaluated only at $t$ and do not change the output in the subsequent time points.

3.2 Ldsr to ${LARS}_{D}$

Here we present the identified fragments of LDSR along with their expressiveness. While, for the fragments of ${LARS}_{D}$ we obtained strict expressiveness and each rule in ${LARS}_{D}$ has been translated into exactly one rule in LDSR, for the fragments of LDSR, the translation, in general, needs auxiliary atoms and additional rules to simulate the behavior of rules of the form (2) and of some streaming and aggregates atoms.

The largest identified fragment is $F_{4}$ that is defined as follows.

Definition 5

The fragment $F_{4}$ is the subset of the LDSR programs $P$ that meet the condition $⋃_{r \in P} p r e d (H (r)) \subset P^{I}$ .

Basically, $F_{4}$ is obtained from LDSR by simply imposing that no extensional predicate appears in the head of a rule.

Proposition 6

$F_{4}$ is bound-expressible via ${LARS}_{D}$ .

It can be shown that there is a mapping $ρ_{4} : F_{4} \to {LARS}_{D}$ such that for each $F_{4} - t u p l e$ $(I, B, P)$ and for each $t \in {0, \dots, n}$ , $t - b o u n d (I, B, P) = t - b o u n d (I, B, ρ_{4} (P))_{|_{p r e d (P \cup I \cup B)}}$ . First, we note that, in general, each streaming atom in $F_{4}$ has to properly translated into a ${LARS}_{D}$ formula; moreover a special rewriting, requiring additional rules, has to be performed for streaming atoms of the form $a c o u n t v i n {d_{1}, \dots, d_{m}}$ , where $v$ is a variable in $C$ and for all the aggregate atoms. Thus, without going into details, the mapping $ρ_{4}$ relies on a function $g$ that associates each streaming atom (but those of form $a c o u n t v i n {d_{1}, \dots, d_{m}}$ ) with a ${LARS}_{D}$ formula that expresses the condition that must be satisfied in the stream for the streaming atom to be true; moreover, if $α$ is an aggregate atom or a streaming atom of the form $a c o u n t v i n {d_{1}, \dots, d_{m}}$ , $g$ associates it with a formula containing auxiliary atoms defined via an additional set of rules $C_{α}$ that are needed to simulate its semantics. For the sake of the presentation, the function $g$ and the set of additional rules $C_{α}$ are reported in appendix 0.A.1

Furthermore, given a program $P \in F_{4}$ , the mapping $ρ_{4}$ has to replace each rule $r$ in $P$ with one or more ${LARS}_{D}$ rules. In sum, the program $ρ_{4} (P)$ is obtained by:

replacing each rule $a\,: {-}β1,…,βm$ of form (1) with the ${LARS}_{D}$ rule
$□ (a \leftarrow ⊞^{0} @_{T} ⊤ \land g (β_{1}) \land \dots \land g (β_{m}))$ .
for each rule $#tempa\,: {-}β1,…,βm$ of form (2),
- replacing it with the ${LARS}_{D}$ rule $a \leftarrow ⊞^{0} @_{T} ⊤, g (β_{1}), \dots, g (β_{m})$
- adding the rule $□ (a t e m p \leftarrow ⊞^{0} @_{T} ⊤ \land g (β_{1}) \land \dots \land g (β_{m}))$ .
adding for each streaming atom $α$ of the form $a c o u n t v i n {d_{1}, \dots, d_{m}}$ , where $v$ is a variable in $C$ or aggregates atom, a set of rules $C_{α}$ .

Basically, the mapping $ρ_{4}$ manages the interaction between the two forms of rules, simulating, at an evaluation time point $t$ , the temporary derivations obtained in the previous time points and evaluating their effect on the permanent derivations that will be part of the output. This is mainly obtained by creating and handling a copy of each rule of the form (2) where the suffix “temp” is added to the head predicate. Moreover, since the streaming atoms in LDSR are evaluated according to the backward observation, we need to identify the reference time point in which the $L A R S$ formulas representing the conditions expressed by the streaming atoms have to checked. To do this, we use the formula $⊞^{0} @_{T} ⊤$ that evaluates the tautology within a window of size 0 and thus, it holds in the rule instance where the variable $T$ corresponds to the reference time point.

We are now ready to define the fragment $F_{5}$ that is obtained from $F_{4}$ by avoiding rules of form (1).

Definition 6

The fragment $F_{5}$ of LDSR is the subset of the programs of $F_{4}$ that meet the condition $P = {f o r m}_{2} (P)$ .

Proposition 7

$F_{5}$ is $f u l l - e x p r e s s i b l e$ via ${LARS}_{D}$ .

To see this, consider, the mapping $ρ_{5} : F_{5} \to {LARS}_{D}$ such that, for each program $P \in F_{5}$ , $ρ_{5} (P)$ is obtained by:

replacing each rule $#tempa\,: {-}β1,…,βm$ of form (2) , with the ${LARS}_{D}$ rule
$a \leftarrow ⊞^{0} @_{T} ⊤, g^{'} (β_{1}), \dots, g^{'} (β_{m})$ .
adding for each streaming atom $α$ of the form $a c o u n t v i n {d_{1}, \dots, d_{m}}$ , where $v$ is a variable in $C$ or aggregates atom, a set of rules $C_{α}$ .

It can be shown that $ρ_{5}$ is such that for each $F_{5} - t u p l e$ $(I, B, P)$ and for each $t \in {0, \dots, n}$ , $t - f u l l (I, B, P) = t - f u l l (I, B, ρ_{5} (P))_{|_{p r e d (P \cup I \cup B)}}$ . Roughly, similarly to $ρ_{4}$ , $ρ_{5}$ relies on a function $g^{'}$ for rewriting body atoms and adds auxiliary rules for handling aggregate atoms or a streaming atoms of the form $a c o u n t v i n {d_{1}, \dots, d_{m}}$ (more details on this are reported in Appendix in0.A.2); however the translation for the fragment $F_{5}$ is simpler than the one for $F_{4}$ , as it is sufficient to associate each rule of form (2) with a ${LARS}_{D}$ rule of type (II). Indeed, since rules of form (1) are not allowed, there is no need to consider the information that can be derived in a permanent way through them. The condition defining the fragment $F_{5}$ ensures the full expressiveness: since a program in this fragment features only rules of form (2), and its translation only rules of type (II), their evaluation at each time point $t$ can derive information only at $t$ , while leaving unchanged the output in the other time points.

The fragment $F_{6}$ restrict $F_{5}$ to reach strict full expressiveness.

Definition 7

The fragment $F_{6}$ of LDSR is the subset of the programs of $F_{5}$ in which streaming atoms of the form $a c o u n t v i n {d_{1}, \dots, d_{m}}$ where $v \in V$ and aggregate atoms are not allowed in rule bodies.

Proposition 8

$F_{6}$ is strictly full-expressible via ${LARS}_{D}$ .

It can be shown that for the mapping $ρ_{6} = {ρ_{5}}_{|_{F_{6}}}$ , it holds that for each $F_{6} - t u p l e$ $(I, B, P)$ and for each $t \in {0, \dots, n}$ , $t - f u l l (I, B, P) = t - f u l l (I, B, ρ_{6} (P))$ . Since no atoms involving the addition of auxiliary predicates are considered, $F_{6}$ is strictly expressible.

The last considered fragment $F_{7}$ still features strict expressiveness, but of bound type, as, differently from $F_{6}$ , it allows also rules of form (1) to some extent.

Definition 8

The fragment $F_{7}$ of LDSR is the subset of the programs of $F_{4}$ that meet the following conditions: $(i)$ $(\cup_{r \in {f o r m}_{2} (P)} (p r e d (B (r))) \cap (\cup_{r \in f o r m_{2} (P)} (p r e d (H (r))) = \emptyset$ $(i i)$ streaming atoms of the form $a c o u n t v i n {d_{1}, \dots, d_{m}}$ where $v \in V$ and aggregate atoms are not allowed in rule bodies.

Proposition 9

$F_{7}$ is strictly bound-expressible via ${LARS}_{D}$ .

It can be shown that there is a mapping $ρ_{7} : F_{7} \to {LARS}_{D}$ such that for each $F_{7} - t u p l e$ $(I, B, P)$ and for each $t \in {0, \dots, n}$ , $t - b o u n d (I, B, P) = t - b o u n d (I, B, ρ_{7} (P))$ . To see this, consider, the mapping $ρ_{7} : F_{7} \to {LARS}_{D}$ such that, for each program $P \in F_{7}$ , $ρ_{7} (P)$ is obtained by:

replacing each rule $#tempa\,: {-}β1,…,βm$ of form (2) with the ${LARS}_{D}$ rule
$a \leftarrow ⊞^{0} @_{T} ⊤, g^{'} (β_{1}), \dots, g^{'} (β_{m})$ .
replacing each rule $a\,: {-}β1,…,βm$ of form (1) with the ${LARS}_{D}$ rule
$□ (a \leftarrow ⊞^{0} @_{T} ⊤ \land g^{''} (β_{1}) \land \dots \land g^{''} (β_{m}))$ .

The mapping relies on the same function $g^{'}$ as $ρ_{5}$ for the rules of form (2). In addition, for the rule of form (1), a different function $g^{''}$ is used to associate the body streaming atoms with $L A R S$ formulas based on the following definition.

Definition 9

Given an atom $a (t_{1}, \dots, t_{n})$ and a LDSR rule $r$ with $H (r) = a (t_{1}^{'}, \dots, t_{n}^{'})$ we call definition of $a (t_{1}, \dots, t_{n})$ in $r$ , denoted with $d_{r} (a (t_{1}, \dots, t_{n}))$ , the conjunction $⋀_{{β \in B (r)}} β ⋀_{1 \leq i \leq n} t_{i} = t_{i}^{'}$ . Given an LDSR program $P$ the definition of $a (t_{1}, \dots, t_{n})$ in $P$ is $d_{P} (a (t_{1}, \dots, t_{n})) = a (t_{1}, \dots, t_{n}) \lor (⋁_{{r \in P | p r e d (H (r)) = a}} d_{r} (a (t_{1}, \dots, t_{n})))$ .

This definition identifies, for each predicate $a$ in the head of a rule of form (2), a $L A R S$ formula relying only on permanent information that can be used in the $L A R S$ translation in place of $a$ . Further details on the translation and the $g^{''}$ functions are reported in Appendix 0.A.3. We note here that the strict expressiveness of this fragment is obtained since the translation of the allowed streaming atoms does not require the use of additional atoms, and condition $(i i)$ simplifies the rewriting of the rules of form $(2)$ w.r.t what fragment $F_{4}$ . Indeed, in this case, it is not necessary to add the rules used by $ρ_{4}$ such as $□ (a t e m p \leftarrow ⊞^{0} @_{T} ⊤ \land g (β_{1}) \land \dots \land g (β_{m}))$ that required additional auxiliary atoms.

Consider, for example, the LDSR program $P^{'}$ that could be used for monitoring irregularity in a subway station monitoring system. Three minutes are expected to elapse between the arrival of one train and the next, so the program records an irregularity when one train passes and another has already passed in one of the previous two minutes:

P′={irregular \,: {-}train_pass,train_passatleast1in{1,2}.}

The program belongs to the $F_{7}$ fragment, and the corresponding ${LARS}_{D}$ program with respect to the $ρ_{7}$ function is as follows:

ρ7(P′)={□(irregular←⊞0@T⊤∧(@T1train_pass∧T1=T−0)∧(@T2train_pass∧((T2=T−1)∨(T2=T−2))).}

4 Conclusion

This work presents a formal comparison about the relative expressiveness of the two languages LDSR and LARS. The main contribution of the work is twofold: $(i)$ we propose a suitable framework to compare the two languages, which exhibit different syntax and semantics. and $(i i)$ for each language, we identify a number of fragments that can be expressed by the other one, showing possible rewritings. In order to compare the semantics of the two languages, we first provided an alternative equivalent model-theoretic definition of the semantics of LDSR, instead of the operational one originally provided. Moreover, we defined the concept of answer stream also for LDSR, as an extension of the streaming model. The framework allowed us for focusing the comparison on different forms of the output stream (atomic, bound, full) and on the nature of the rewriting that could forbid or admit the addition of auxiliary predicates (strict or not strict expressiveness, respectively). For each given form of output and type of rewriting, we studied how to build fragments of a language that could meet the desired expressiveness. To do this, we considered the semantics behind each construct or combination of constructs that can occur in the rules and the effect of interactions between the different rules. The fragments $F_{1}, . . ., F_{7}$ are the largest we identified so far, but, of course, these could be further enlarged and new ones could be possibly found; this will be the subject of future works.

5 Acknowledgments

This work has been partially supported by the project “MAP4ID - Multipurpose Analytics Platform 4 Industrial Data”, N. F/190138/01-03/X44 and by the Italian MIUR Ministry and the Presidency of the Council of Ministers under the project “Declarative Reasoning over Streams” under the “PRIN” 2017 call (CUP $H 24 I 17000080001$ , project 2017M9C25L_001).

References

Appendix 0.A Details on the translation from Ldsr to ${LARS}_{D}$

We introduce a function $σ$ that associates any streaming atoms with a $L A R S$ formula. Function $σ$ will be used to present $g$ , $g^{'}$ and $g^{''}$ and works as follows:

By applying $σ$ over $a a t l e a s t c i n {d_{1}, . . ., d_{m}}$ we obtain:

$(⋀ i \in C @_{T_{i}} a) \land ⎛ ⎜ ⎝ ⋀ i, j \in C s.t. i < j (T_{i} \neq T_{j}) ⎞ ⎟ ⎠ \land (⋀ i \in C (⋁ j \in M (T_{i} = T - d_{j})))$

where $C = {1, . . ., c}$ , $M = {1, . . ., m}$ and $T_{1}, . . ., T_{n}$ are fresh variables.
By applying $σ$ over $a a l w a y s i n {d_{1}, \dots, d_{m}}$ we obtain:

$(⋀ i \in M @_{T_{i}} a) \land ⎛ ⎜ ⎝ ⋀ i, j \in M s.t. i < j (T_{i} \neq T_{j}) ⎞ ⎟ ⎠ \land (⋀ i \in M (⋁ j \in M (T_{i} = T - d_{j})))$

where $M = {1, . . ., m}$ and $T_{1}, . . ., T_{n}$ are fresh variables.
By applying $σ$ over $a c o u n t c i n {d_{1}, \dots, d_{m}}$ with $c \in C \cap N^{+}$ we obtain:

$(⋀ i \in C @_{T_{i}} a) \land ⎛ ⎜ ⎝ ⋀ i, j \in C s.t. i < j (T_{i} \neq T_{j}) ⎞ ⎟ ⎠ \land (⋀ i \in C (⋁ j \in M (T_{i} = T - d_{j}))) \land \neg (@_{T_{c + 1}} a \land (⋀ i \in C (T_{c + 1} \neq T_{i})) \land (⋁ j \in M (T_{c + 1} = T - d_{j})))$

where $C = {1, . . ., c}$ , $M = {1, . . ., m}$ and $T_{1}, . . ., T_{n}$ are fresh variables.
By applying $σ$ over $a c o u n t v i n {d_{1}, \dots, d_{m}}$ with $v \in V$ we obtain the predicate atom $c o u n t (b, t_{1}, \dots, t_{n}, d_{1}, \dots, d_{m}, V)$ .

Basically, the function $σ$ returns a LARS formula that is true when the corresponding LDSR streaming atom is true. The formula identifies the time points related to the backward observation of a stream w.r.t the set ${d_{1}, . . ., d_{m}}$ for which the condition defined by the streaming atom holds.

0.a.1 The function $g$

We present the function $g$ , used by $ρ_{4}$ . In particular, $g$ associates each streaming atom (but those of form $a c o u n t v i n {d_{1}, \dots, d_{m}}$ ) with a ${LARS}_{D}$ formula that expresses the condition that must be satisfied in the stream for the streaming atom to be true; it has to consider also the temporary information possibly present in the previous time point when the streaming atom was evaluated. The presence of these information in the stream is simulated with the auxiliary atoms with suffix “temp”.

$g (a a t l e a s t 1 i n {d_{1}, \dots, d_{m}}) =$

$a t e m p \lor σ (a a t l e a s t 1 i n {d_{1}, \dots, d_{m}} ∖ {0}) .$
Let $c > 1$ , $g (a a t l e a s t c i n {d_{1}, \dots, d_{m}}) =$

$(a t e m p \land σ (a a t l e a s t c - 1 i n {d_{1}, \dots, d_{m}} ∖ {0})) \lor$

$σ (a a t l e a s t c i n {d_{1}, \dots, d_{m}} ∖ {0})) .$
$g (a a l w a y s i n {d_{1}, \dots, d_{m}}) =$

${\begin{matrix} a t e m p \land σ (a a l w a y s i n {d_{1}, \dots, d_{m}} ∖ {0} & if 0 \in {d_{1}, \dots, d_{m}} σ (a a l w a y s i n {d_{1}, \dots, d_{m}}) & otherwise \end{matrix}$
$g (a c o u n t 1 i n {d_{1}, \dots, d_{m}}) =$

$a t e m p \lor (\neg a t e m p \land σ (a c o u n t 1 i n {d_{1}, \dots, d_{m}} ∖ {0})) .$
Let $c > 1$ , $g (a c o u n t c i n {d_{1}, \dots, d_{m}}) =$

$(a t e m p \land σ (a c o u n t c - 1 i n {d_{1}, \dots, d_{m}} ∖ {0})) \lor σ (a c o u n t c i n {d_{1}, \dots, d_{m}} ∖ {0}) .$

Moreover, if $α$ is a streaming atom of the form $a c o u n t v i n {d_{1}, \dots, d_{m}}$ or an aggregate atom, $g$ associates it with a formula containing auxiliary atoms defined via an additional set of rules $C_{α}$ that are needed to simulate its semantics. Let $C \in V$ , $g (a c o u n t C i n {d_{1}, \dots, d_{m}}) =$

(a t e m p \land σ (a c o u n t C_{1} i n {d_{1}, \dots, d_{m}} ∖ {0}) \land (C_{1} + 1 = C) \lor

(\neg a t e m p \land σ (a c o u n t C i n {d_{1}, \dots, d_{m}} ∖ {0}))

The set of rules $C_{α}$ defining $α = b (t_{1}, \dots, t_{n}) c o u n t v i n {d_{1}, \dots, d_{m}}$ where $v \in V$ are the following $m + 1$ rules:

$p r e s e n t (b, t_{1}, \dots, t_{n}, d_{1}, \dots, d_{m}, c) \leftarrow σ (b (t_{1}, \dots, t_{n}) a t l e a s t c i n {d_{1}, \dots, d_{m}})$ for $c \in 1, . . ., m$
$c o u n t (p, t_{1}, \dots, t_{n}, d_{1}, \dots, d_{m}, C) \leftarrow p r e s e n t (b, t_{1}, \dots, t_{n}, d_{1}, \dots, d_{m}, C), \neg p r e s e n t (b, t_{1}, \dots, t_{n}, d_{1}, \dots, d_{m}, C + 1)$ .

First, $m$ rules are needed, where each one verifies if atoms of type $b (t_{1}, \dots, t_{n})$ occur $1, 2, . . .,$ or $m$ times. Eventually, a rule is needed to verify the exact number of occurrences. Similar approaches are used for the translation of the aggregate atoms.
Eventually, $g (n o t α) = \neg g (α)$ for each positive literal $α$ .

0.a.2 The function $g^{'}$

We present the function $g^{'}$ , used by $ρ_{5}$ . In particular, $g^{'}$ associates each streaming atom (but those of form $a c o u n t v i n {d_{1}, \dots, d_{m}}$ ) with a ${LARS}_{D}$ formula that expresses the condition that must be satisfied in the stream for the streaming atom to be true.

$g^{'} (a a t l e a s t c i n {d_{1}, \dots, d_{m}}) = σ (a a t l e a s t c i n {d_{1}, \dots, d_{m}})$ .
$g^{'} (a a l w a y s i n {d_{1}, \dots, d_{m}}) = σ (a a l w a y s i n {d_{1}, \dots, d_{m}})$ .
$g^{'} (a c o u n t k i n {d_{1}, \dots, d_{m}}) = σ (a c o u n t k i n {d_{1}, \dots, d_{m}})$ if $k \in N^{+}$ .

Moreover, if $α$ is a streaming atom of the form $a c o u n t v i n {d_{1}, \dots, d_{m}}$ or an aggregate atom, $g^{'}$ associates it with a formula containing auxiliary atoms defined via an additional set of rules $C_{α}$ that are needed to simulate its semantics. Let $v \in V$ , $g^{'} (b (t_{1}, \dots, t_{n}) c o u n t v i n {d_{1}, \dots, d_{m}}) = c o u n t (b, t_{1}, \dots, t_{n}, d_{1}, \dots, d_{m}, V)$ . The set of rules $C_{α}$ defining $σ (α)$ for $α = b (t_{1}, \dots, t_{n}) c o u n t v i n {d_{1}, \dots, d_{m}}$ where $v \in V$ are the following $m + 1$ rules:

$p r e s e n t (b, t_{1}, \dots, t_{n}, d_{1}, \dots, d_{m}, c) \leftarrow σ (b (t_{1}, \dots, t_{n}) a t l e a s t c i n {d_{1}, \dots, d_{m}})$ for $c \in 1, . . ., m$
$c o u n t (b, t_{1}, \dots, t_{n}, d_{1}, \dots, d_{m}, C) \leftarrow p r e s e n t (b, t_{1}, \dots, t_{n}, d_{1}, \dots, d_{m}, C), \neg p r e s e n t (b, t_{1}, \dots, t_{n}, d_{1}, \dots, d_{m}, C + 1)$ .

Eventually, $g^{'} (n o t α) = \neg g^{'} (α)$ for each positive literal $α$ .

0.a.3 The function $g^{''}$

We present the function $g^{''}$ , used by $ρ_{7}$ . In particular, $g^{''}$ associates each streaming atom (but those of form $a c o u n t v i n {d_{1}, \dots, d_{m}}$ ) with a ${LARS}_{D}$ formula that expresses the condition that must be satisfied in the stream for the streaming atom to be true; it has to consider the temporary information possibly present in a time point $t$ when $t$ was the evaluation time point and thus the streaming atom was evaluated. It is possible to verify the presence of an atom $a$ at the time of a previous evaluation also if was derived by a rule of form (2): since in the body of any rule of form (2) are only present atoms deriving from the input stream o from rules of form (1), we can know if an atom was derived considering its derivation $d_{P} (a)$ . We assume that the program rules do not share variables.

$σ (a \lor b) = σ (a) \lor σ (b)$ .
$σ (a \land b) = σ (a) \land σ (b)$ .
$σ (n o t α) = \neg σ (α)$
$g^{^{''}} (a a t l e a s t 1 i n {d_{1}, \dots, d_{m}}) =$

$σ (d_{P} (a)) \lor σ (a a t l e a s t 1 i n {d_{1}, \dots, d_{m}} ∖ {0})$
Let $c > 1$ , $g^{''} (a a t l e a s t c i n {d_{1}, \dots, d_{m}}) =$

$(g (d_{P} (a) \land g (a a t l e a s t c - 1 i n {d_{1}, \dots, d_{m}} ∖ {0})) \lor$

$g (a a t l e a s t c i n {d_{1}, \dots, d_{m}} ∖ {0}))$
$g^{''} (a a l w a y s i n {d_{1}, \dots, d_{m}}) =$

${\begin{matrix} σ (d_{P} (a)) \land σ (a a l w a y s i n {d_{1}, \dots, d_{m}} ∖ {0} & if 0 \in {d_{1}, \dots, d_{m}} σ (a a l w a y s i n {d_{1}, \dots, d_{m}}) & otherwise \end{matrix}$
$g^{''} (a c o u n t 1 i n {d_{1}, \dots, d_{m}}) =$

$σ (d_{P} (a)) \lor (\neg σ (d_{P} (a)) \land σ (a c o u n t 1 i n {d_{1}, \dots, d_{m}} ∖ {0})) .$
Let $c > 1$ , $g^{''} (a c o u n t c i n {d_{1}, \dots, d_{m}}) =$

$σ (d_{P} (a)) \land σ (a c o u n t c - 1 i n {d_{1}, \dots, d_{m}} ∖ {0})) \lor σ (a c o u n t c i n {d_{1}, \dots, d_{m}} ∖ {0})) .$

Eventually, $g^{''} (n o t α) = \neg g^{''} (α)$ for each positive literal $α$ .

Appendix 0.B Proofs

0.b.1 Statement and Proof of Lemma 1

Lemma 1

Let $P$ be a LDSR program, $I = ⟨ I_{0}, \dots, I_{n} ⟩$ an input stream and $t \in {1, \dots, n}$ , for all set of ground predicate atoms $B \subset G$ and for all $I^{'} = ⟨ I_{0}^{'}, \dots, I_{n}^{'} ⟩$ with $I_{i} = I_{i}^{'}$ for $i = 0, \dots, t$ , we have that $t - b o u n d (I, B, P) = t - b o u n d (I^{'}, B, P)$ .

Let $t - b o u n d (I, B, P) = O = ⟨ O_{0}, \dots, O_{n} ⟩$ and $t - b o u n d (I^{'}, B, P) = O^{'} = ⟨ O_{0}^{'}, \dots, O_{n}^{'} ⟩$ , for definition of answer stream:

$⟨ O_{0} ⟩$ is the permanent part of a minimal model $M$ of the reduct ${P^{+}}^{M}$ for the stream $⟨ I_{0} ⟩$ and $⟨ O_{0}^{'} ⟩$ is the permanent part of a minimal model $M$ of the reduct ${P^{+}}^{M}$ for the stream $⟨ I_{0}^{'} ⟩$ . Since $I_{0} = I_{0}^{'}$ we have that $O_{0} = O_{0}^{'}$ ;
for all $i \in 1, \dots, t - 1$ , $O_{| i}$ is the permanent part of a minimal model $M$ of the reduct ${P^{+}}^{M}$ for the stream $⟨ O_{0}, \dots, O_{i - 1}, I_{i} ⟩$ . Since $I_{i} = I_{i}^{'}$ , we have that $O_{| i} = O_{| i}^{'}$ .
$O_{| t}$ is a minimal model of the reduct ${P^{+}}^{O_{| t}}$ for the stream $⟨ O_{0}, \dots, O_{t - 1}, I_{t} ⟩$ . Since $I_{t} = I_{t}^{'}$ , we have that $O_{| t} = O_{| t}^{'}$ .

Finally, for definition $O_{i} = O_{i}^{'} = \emptyset$ for $t < i \leq n$ .

0.b.2 Proof of Proposition 1

Let $P$ be the LARS program ${@_{T - 1} a \leftarrow @_{T} c}$ .

Let $T = {0, \dots, n}$ and $0 < τ < n$ . Let $C \subseteq T ∖ {0}$ any subset of T such that $τ + 1 \in C$ and $i \in C \to i - 1 \notin C$ . Let $A = {i - 1 | i \in C}$ . Let $I = ⟨ I_{0}, I_{1}, \dots, I_{n} ⟩$ a stream such that:
$I_{i} = {\begin{matrix} \emptyset & if i \notin C {c} & if i \in C \end{matrix}$

Let $O = ⟨ O_{0}, O_{1}, \dots, O_{n} ⟩ \in A S (P, I, τ)$ . Observe that:

$O_{i} = {a}$ if $i \in A$
$O_{i} = {c}$ if $i \in C$
$O_{i} = \emptyset$ if $i \notin (A \cup C)$

Assume, by contradiction, that there exists a mapping $ρ : L A R S \to LDSR$ such that, for each $I$ and $B$ and for each time point of evaluation $t \in {0, \dots, n}$ , it holds that $t - a t o m i c (I, B, P) = t - a t o m i c (I, B, ρ (P))_{|_{p r e d (P \cup I \cup B)}}$ . Let $B = \emptyset$ and $I^{'} = ⟨ I_{0}^{'}, I_{1}^{'}, \dots, I_{n}^{'} ⟩$ a stream such that:
$I_{i}^{'} = {\begin{matrix} I_{i} & if i \neq τ + 1 \emptyset & if i = τ + 1 \end{matrix}$

Let $ρ (P) = ¯ P$ and $O^{'} = ⟨ O_{0}^{'}, O_{1}^{'}, \dots, O_{n}^{'} ⟩ \in A S (P, I^{'}, τ)$ , we have that $O_{τ} = a$ and $O_{τ}^{'} = \emptyset$ .
Since for the Lemma 1 $τ - b o u n d (I, B, ¯ P)_{|_{τ}} = τ - b o u n d (I^{'}, B, ¯ P)_{|_{τ}}$ , we have that
$τ - a t o m i c (I^{'}, B, P) \neq τ - a t o m i c (I^{'}, B, ¯ P)$ .

0.b.3 Proof of Proposition 2

Let $P$ be the LDSR program ${a(Y)\,: {-}a(X),b(X,Y).}$ Let $T = {0, \dots, n}$ and $τ > 0 \in T$ . Let $I = ⟨ I_{0}, I_{1}, \dots, I_{n} ⟩$ a stream with $I_{i} = {a (1), b (1, 2)}$ for $i \in {0, \dots, n}$ . Assume, by contradiction, that there exists a mapping $ρ : LDSR \to L A R S$ such that, for each $I$ and $B$ and for each time point of evaluation $t \in {0, \dots, n}$ , it holds that $t - a t o m i c (I, B, P) = t - a t o m i c (I, B, ρ (P))_{|_{p r e d (P \cup I \cup B)}}$ .

Let $B = \emptyset$ , $ρ (P) = ¯ P$ and $τ - a t o m i c (I, B, P) = τ - a t o m i c (I, B, ¯ P) = ⟨ O_{0}, O_{1}, \dots, O_{n} ⟩$ , we have that $O_{τ} = {a (1), a (2), b (1, 2)}$ .
For definition, let $A = ⟨ A_{0}, \dots, A_{n} ⟩ \in A S (P, I, t)$ , we have that $O_{τ} = A_{τ} \cup B$ , but $A$ is an interpretation stream for $I$ , so all atoms that occur in $A$ but not in $I$ must have intensional predicates but the atom $a (2)$ has predicate $a$ with $a \in P_{S}^{ε}$ .

A Formal Comparison between Datalog-based Languages for Stream Reasoning (extended version)