A Non-Deterministic Multiset Query Language

In a data-centric approach to business process modelling (see, e.g., [1, 2]), specification of data transformation during case execution is an integral part of the business process model. This new paradigm requires new tools and formalisms for effective specification, simulation and validation. Task-centric models are commonly formalized using Petri nets (see, e.g., [3, 4]). Adapting Petri net-based formalizations to data-centric models is, however, problematic: While simple transformations on data can be represented directly within a coloured Petri net, Petri nets lack facilities for complex data processing and querying. Even so, there exists a large amound of literature (see e.g., [5, 6, 7]) devoted to enriching Petri nets with with data processing capabilities and automated verification of their properties. Recent paper [8] introduced DB-Nets — an attempt to integrate coloured Petri nets with relational databases. The use of two separate formalisms complicates verification and simulation (though it corresponds to actual implementations of BPM systems). In the following paper [9] a subset of database operations was implemented inside coloured Petri nets with name creation and transition priorities.

Conditional term rewriting [10] was proposed as an alternative (if less popular) generic framework for specification of dynamic systems [11]. It subsumes a variety of Petri nets [12] and their simulation is one of popular applications of the term rewriting system Maude [13, 14]). More precisely, it is well known (see e.g., [12]) that coloured Petri nets can be implemented by multiset rewriting systems, and, conversely, rewriting systems which rewrite multisets of terms representing colour tokens can be interpreted as Petri nets: just identify places with colour tokens, and each rewriting rule of the form

with a transition with input arcs from $a_{1}$, $a_{2}$, $\ldots$, $a_{n}$ and output arcs to $b_{1}$, $b_{2}$, $\ldots$, $b_{m}$. Other constructs, such as inhibitor arcs can be easily implemented with conditional rewriting rules. Rewriting systems are more general than Petri Nets since they are not limited to rewriting multisets (on the other hand, Petri nets are much better supported by tools and programming libraries). However, rewriting systems still share with Petri nets the limitation and inconvenience of not directly supporting bulk, complex operations on data which involve some kinds of quantification. For example, suppose that the state of a data driven business process related to e-commerce is represented by a multiset of terms. In particular, terms of the form $\text{\tt item}(p,c)$ denote the presence of a product $p$ in the basket of a customer $c$. Suppose now that $c$ cancels the case, and so we need to remove all $c$’s items from the multiset. Describing removal of a single (nondeterministically chosen) item is easy with the rule $\text{\tt item}(c,x)\Rightarrow\emptyset$ where $x$ is a variable, but specifiying in a rewriting system (or a Petri net) that all of them need to be removed before the next business step is more complex (though clearly possible) and would require auxilliary tokens and conditional rewrite rules corresponding to inhibitor arcs in a Petri net preventing other transitions as long as there are still some $c$’s items present in the rewritten multiset. Thus, a high-level query language adding quantifier constructs on top of conventional rewriting system or a Petri net is clearly desirable, particularly if rewriting systems or Petri nets are to become convenient formalisms to model data driven business processes.

In this paper we present an expressive multiset query and update language $\mathcal{Q}_{\Sigma,\mathcal{D}}$, designed to be executable in a term rewriting system, useful for a unified and somewhat “Petri nettish” formalization of data-centric business processes. The connection with Petri nets is admittedly tenuous and follows from the fact that the language acts on data represented as multisets of terms which could be viewed as tokens (see the discussion above). Since this language specifies changes to data, instead of being a reimplementation of relational calculus, it contains linear-like features fitting a term rewriting implementation. Most remarkably, $\mathcal{Q}_{\Sigma,\mathcal{D}}$ is non-deterministic — the result of a query or update is not, in general, uniquely determined by the database. This permits modelling user choices, just like in the case of Petri nets. $\mathcal{Q}_{\Sigma,\mathcal{D}}$ consists of three sublanguages, parametrized with respect to a signature $\Sigma$ and $\Sigma$-algebra of facts $\mathcal{D}$:

1. 1.

   Language $\mathcal{Q}_{\Sigma,\mathcal{D}}^{\mathbf{cnd}}$ of conditions (Boolean queries) which can be used independently as constraints, or as components of queries in $\mathcal{Q}_{\Sigma,\mathcal{D}}^{\mathbf{qry}}$ and $\mathcal{Q}_{\Sigma,\mathcal{D}}^{\mathbf{dml}}$.

2. 2.

   Data manipulation language$\mathcal{Q}_{\Sigma,\mathcal{D}}^{\mathbf{dml}}$. A DML query $Q$ in $\mathcal{Q}_{\Sigma,\mathcal{D}}^{\mathbf{dml}}$ defines new facts to be added to the database. Some of the old facts used in constructing the new ones may be deleted.

3. 3.

   Language $\mathcal{Q}_{\Sigma,\mathcal{D}}^{\mathbf{qry}}$ of queries which only return facts but do not change the database. Both syntax, and to some extent semantics of $\mathcal{Q}_{\Sigma,\mathcal{D}}^{\mathbf{qry}}$ is a restriction of syntax and semantics of $\mathcal{Q}_{\Sigma,\mathcal{D}}^{\mathbf{dml}}$.

A query $Q$ in $\mathcal{Q}_{\Sigma,\mathcal{D}}^{\alpha}$, $\alpha\in\{\mathbf{cnd},\mathbf{qry},\mathbf{dml}\}$, is given semantics by assignment of a rewriting system $\mathcal{R}_{\Sigma,\mathcal{D}}^{\alpha}(Q)$. To evaluate $Q$ in a database $F$ we start with an initial term $\mathrm{I}_{Q}(F)$. A normal form of $\mathrm{I}_{Q}(F)$ wraps a result of $Q$’s evaluation: a Boolean value indicating validity of a condition, a query answer or a new database resulting from execution of a DML query. As remarked above, while $\mathcal{R}_{\Sigma,\mathcal{D}}^{\alpha}(Q)$ is always terminating (i.e., there are no infinite execution paths, so we always do get some result from evaluating $Q$), it is not confluent (i.e., divergent execution paths may not eventually converge) in general, hence we may get distinct results depending on nondeterministic choices. We identify syntactic constraints on queries in each of the sublanguages which ensure confluence for the rewriting system, and hence determinism for the results of the query. $\mathcal{Q}_{\Sigma,\mathcal{D}}$ shares with the language introduced in [15] a non-standard approach to variable binding. The approach avoids problems with capture-free substitutions without dispensing with explicit variables, but at the price of non-compositionality: The surrounding context may determine whether a variable in a subterm is free or bound in this subterm. $\mathcal{Q}_{\Sigma,\mathcal{D}}^{\mathbf{dml}}$ supports introduction of fresh values to the database, which is used, e.g., to generate identifiers for newly created artifacts or to simulate user input (cf. [7]).

Since queries in $\mathcal{Q}_{\Sigma,\mathcal{D}}$ are converted to a term rewriting system, verification of a business process specified as a set of DML queries (see Section 7) can be assisted with symbolic reachability analysis techniques based on narrowing (see e.g., [16]) . We plan to expand on this idea in future research. Note that our results in this article regarding the confluence of the rewriting systems to which a particular subclass of queries compiles to, may be relevant for narrowing (see e.g., [17, 18], c.f. [19]). E.g., narrowing a confluent system may provide a more efficient search procedure than in the case of a non-confluent one.

Our queries are evaluated against, or act on, finite multisets of facts. Duplicate facts can be genuinely useful and removing them is computationally expensive. If necessary, duplicates can be removed explicitly or, better, one can ensure that no duplicates are introduced in the first place by judicious choice of DML operations. In fact, SQL is a multiset query language as well, hence by using multisets we are closer to the actual relational database practice than formal systems based on sets.

$\mathcal{Q}_{\Sigma,\mathcal{D}}$ is parametrized with respect to a signature of facts $\Sigma$ and a $\Sigma$-algebra of facts $\mathcal{D}$. $\Sigma_{S}$ must contain sorts Fact and Bool for facts and Booleans, respectively. All constructors for facts are contained in $\Sigma_{F}$. Facts are reifications of predicate instances. A typical fact has the form $f(a_{1},\ldots,a_{n})$, where $f:s_{1}\ldots s_{n}\rightarrow\text{\tt Fact}$ is a fact constructor. $\mathcal{D}$ defines all the data types used in facts and is specifiable in terms of directed equations and equational attributes. $\mathcal{D}$ must define Boolean connectives and Boolean-valued equality $\_=\_:s\;s\rightarrow\text{\tt Bool}$ for all $s\in\Sigma_{S,K}$. We assume that all ground terms of sort Bool simplify to either t or f. This is non-trivial: Define a function $f:\text{\tt Nat}\rightarrow\text{\tt Bool}$ with a single equation $f(0)=\text{\bf t}$. Then $f(1)$ is fully reduced and distinct from both t and f.

Multisets of facts. The signature of multisets extends $\Sigma_{S}$ with sorts (Ne)FSet of finite (non-empty) multisets of facts. The subsort ordering is given by $\text{\tt Fact}<\text{\tt NeFSet}<\text{\tt FSet}$. In particular, each fact is a non-empty multiset of facts. Finite multisets of facts are constructed with an associative and commutative binary operator $\_\circ\_:\text{\tt FSet}\;\text{\tt FSet}\rightarrow\text{\tt FSet}$ (cf. [38]) with identity element $\emptyset:\rightarrow\text{\tt FSet}$. Operator $\_\circ\_$ is subsort overloaded with the additional declaration $\_\circ\_:\text{\tt FSet}\;\text{\tt NeFSet}\rightarrow\text{\tt NeFSet}$. Thus, a multiset constructed from a multiset and a non-empty multiset is non-empty.

Freshness and nominal sorts. Support for creation of fresh values is a common requirement (cf. [7]): Identifiers for new objects must not belong to the present nor any past active domain of the database. To understand why reusing identifiers from past domains is bad consider situation where a new business object is created with the identifier of a previously deleted one. In this case the attempt to verify if the deleted object is present in the final database may yield an incorrect affirmative answer. We support creation of fresh values of nominal sorts only. Usually this suffices, and freshness for non-nominal data types is problematic (cf. [39]). A sort $s$ is nominal (relative to $\Sigma$-algebra $\mathcal{D}$) if values of this sort have no non-trivial algebraic or relational structure beside equality. In particular, for nominal $s$, $s^{\prime}\leq s\leq s^{\prime\prime}$ if and only if $s^{\prime}=s=s^{\prime\prime}$. To create values of each nominal sort $s$ we have constructor $\imath^{s}_{\_}:\text{\tt Nat}\rightarrow s$ which belongs neither to $\Sigma$ nor to the signature of $\mathcal{Q}_{\Sigma,\mathcal{D}}$.

Constructing values of nominal sorts from natural numbers simplifies creation of fresh values: to ensure freshness one can construct the new value with the smallest natural number which was not used so far. To keep track of those “smallest unused naturals”, and to make retrieval of fresh values similar to retrieval of data we use fresh facts of sort $\text{\tt Fact}^{\mathbf{n}}$ unrelated to Fact. For each nominal sort $s$ we have a single-argument constructor of the form $C_{s}:s\rightarrow\text{\tt Fact}^{\mathbf{n}}$ which wraps value $\imath^{s}_{n}$ such that for all $m\geq n$, $\imath^{s}_{m}$ was never used before. When fresh value of sort $s$ is requested, we return $\imath^{s}_{n}$ and update the fresh fact to $C_{s}(\imath^{s}_{n+1})$. Fresh facts are combined into (non-empty) multisets of sort (Ne)$\text{\tt FSet}^{\mathbf{n}}$ using commutative and associative operator $\_\circ\_:\text{\tt FSet}^{\mathbf{n}}\;\text{\tt FSet}^{\mathbf{n}}\rightarrow\text{\tt FSet}^{\mathbf{n}}$ with identity $\emptyset:\rightarrow\text{\tt FSet}^{\mathbf{n}}$. To facilitate bulk updates of fresh facts needed in the semantics of DML queries, we define the following function:

Patterns. Quantifiers in $\mathcal{Q}_{\Sigma,\mathcal{D}}$ quantify over patterns (of sort Pat) containing non-ground multisets of facts and fresh facts marked by modalities, which control retention of matched facts (i.e., whether upon matching they are removed temporarily, permanently, or not at all from the database), and syntactically wrap fresh facts (i.e., fresh facts can appear in the pattern only inside specialized modality). Patterns can be preserving (of sort $\text{\tt Pat}^{p}$), semi-terminating (of sort $\text{\tt Pat}^{\text{\it st}}$), terminating (of sort $\text{\tt Pat}^{t}$), terminating and preserving (of sort $\text{\tt Pat}^{\text{\it tp}}$), or neither. The subsort relation is defined by $\text{\tt Pat}^{\text{\it tp}}<\text{\tt Pat}^{t}<\text{\tt Pat}^{\text{\it st}}<\text{\tt Pat}$ and $\text{\tt Pat}^{\text{\it tp}}<\text{\tt Pat}^{p}<\text{\tt Pat}$. Patterns are constructed with modalities

and associative and commutative, subsort overloaded operator:

Thus, a terminating (resp. a semi-terminating) pattern has to contain at least one fact wrapped with $[\_]_{?}$ (resp. with either $[\_]_{?}$ or $[\_]_{0}$). A terminating and preserving pattern consists of facts marked only with $[\_]_{!}$ or $[\_]_{?}$, and it contains at least one fact wrapped with $[\_]_{?}$. Directed equalities $[F_{1}]_{m}\circ[F_{2}]_{m}=[F_{1}\circ F_{2}]_{m}$, where $m\in\{!,?,0,\mathbf{n}\}$, and $F_{1}$, $F_{2}$ are non-empty multisets of (fresh) facts guarantee that fully reduced patterns have facts gathered in groups of the same modality.

The informal meaning of modalities is as follows: Facts matched by those marked by $[\_]_{?}$ can be considered at most once during quantifier evaluation, but they are not removed from the database. Facts marked by $[\_]_{0}$ are removed from the database when matched, but they are returned if the computation branch this matching leads to is unsuccessful. Thus, the presence of facts marked by $[\_]_{0}$ in the pattern may not guarantee termination, unless one can prove that the formula under quantifier is always successful. Facts marked by $[\_]_{!}$ are always retained in the database, and $[\_]_{\mathbf{n}}$ wraps fresh facts.

This section introduces the three sublanguages of $\mathcal{Q}_{\Sigma,\mathcal{D}}$, their syntax and informal semantics. Formal semantics based on conditional term rewriting is provided in the subsequent sections.

Semantics of a sentence $\phi$ in $\mathcal{Q}_{\Sigma,\mathcal{D}}^{\mathbf{cnd}}$ is given by the rewriting system $\mathcal{R}_{\Sigma,\mathcal{D}}^{\mathbf{cnd}}(\phi)$. Terms rewritten by $\mathcal{R}_{\Sigma,\mathcal{D}}^{\mathbf{cnd}}(\phi)$ are of the form $\{F,S\}^{c}$, where $\{\_,\_\}^{c}:\text{\tt FSet}\;\text{\tt Stk}^{c}\rightarrow\text{\tt State}^{c}$, $F$ is the database of facts on which $\phi$ is checked, and $S$ is a stack of sort $\text{\tt Stk}^{c}$ implementing structural recursion. Normal forms, constructed with $\mathfrak{s}:\text{\tt Bool}\rightarrow\text{\tt State}^{c}$, encapsulate the result of $\phi$’s evaluation. Sort $\text{\tt State}^{c}$ of terms holding the full state of evaluation must be distinct from all the other sorts and it must not have any super- or sub-sort relation to other sorts. This guarantees that there are no constructors accepting terms of sort $\text{\tt State}^{c}$ as arguments. Consequently, if all rewrite rules have terms of this sort on the left-hand side, then no subterms can be rewritten, i.e., the defined rewriting system is top-level. Terms of sort $\text{\tt Stk}^{c}$ are built from frames of sort $\text{\tt Frm}^{c}$, where $\text{\tt Frm}^{c}<\text{\tt Stk}^{c}$, using an associative binary operator $\_\_:\text{\tt Stk}^{c}\;\text{\tt Stk}^{c}\rightarrow\text{\tt Stk}^{c}$ with identity $\emptyset$. Most constructors of frames are indexed by subconditions $\psi$ of $\phi$, and lists of distinct variable names $\vec{v}:=v_{1},\ldots,v_{n}$ of respective sorts $s_{1},\ldots,s_{n}$ ($\vec{v}$ can be of any length, even be empty, as long as $\{\vec{v}\}\subseteq\mathit{Var}(\phi)$ and it contains free variables of $\psi$):

As $\vec{v}$ can be empty, the above signature templates include $[]^{|c}_{\psi},[]^{|c,\downarrow}_{\psi}:\rightarrow\text{\tt Frm}^{c}$ and $[\_|]^{|c}_{\psi}:\text{\tt FSet}\rightarrow\text{\tt Frm}^{c}$. $\mathfrak{r}(B)$ encapsulates the result of evaluation of a subcondition. Frame ${\neg}$ negates the result of the next frame on the stack. Frames of the form $[\vec{a}]^{\vec{v}|c}_{\psi}$, $[\vec{a}]^{\vec{v}|c,\downarrow}_{\psi}$, or $[F^{\prime}|\vec{a}]^{\vec{v}|c}_{\psi}$ are called $(\psi,\sigma)$-frames, where $\sigma:=\{\vec{a}/\vec{v}\}$ is the current substitution. They are related to evaluation of $\sigma(\psi)$. Marked frames $[\vec{a}]^{\vec{v}|c,\downarrow}_{\psi}$ occur in evaluation of disjunctions $\_\vee\_$. Iterator frames $[F^{\prime}|\vec{a}]^{\vec{v}|c}_{\exists P\mathbin{.}\psi}$ represent iterative evaluation of quantifiers. Multiset $F^{\prime}$, called iterator state, contains facts available for matching with $P_{!}\circ P_{?}$. Given a database $F$, to evaluate sentence $\phi$ we rewrite a state term $\mathrm{I}_{\phi}(F):=\{F,[]^{|c}_{\phi}\}$ until a normal form $\mathfrak{s}(B)$ is reached. If $B$ then $\phi$ is satisfied in $F$.

Now we present rule schemata for $\mathcal{R}_{\Sigma,\mathcal{D}}^{\mathbf{cnd}}(\phi)$ instantiated for a given formula $\phi$ in $\mathcal{Q}_{\Sigma,\mathcal{D}}$. It is important to distinguish between object variables substituted when applying actual rules, and metavariables used to define rule templates. Below, $F,F^{\prime}:\text{\tt FSet}$, $S:\text{\tt Stk}^{c}$, and $B:\text{\tt Bool}$ are object variables. We also denote by $\vec{v}:=v_{1},\ldots,v_{n}$ and $\vec{w}=w_{1},\ldots,w_{m}$ sequences of object variables in $\mathit{Var}(\phi)$. Metavariables, $\psi$, $\psi_{1}$, and $\psi_{2}$ stand for arbitrary subconditions of $\phi$, metavariable $\mathcal{B}$ stands for Boolean subterms of $\phi$. Metavariable $P$ stands for arbitrary patterns in $\phi$, and $P_{!}$ and $P_{?}$ denote multisets of facts in the instance of pattern $P$ marked by respective modalities (see Remark 2.3).

Constant $\bot$ evaluates to f, and $\{\mathcal{B}\}$ evaluates to $\sigma(\mathcal{B})$, where $\sigma$ is the current substitution of variables $\vec{v}$ ($\sigma(\mathcal{B})$ is ground since $\{\vec{v}\}$ contains all free variables (i.e., all variables) of $\mathcal{B}$, hence, by assumption, it simplifies to either f or t):

To evaluate $\sigma(\neg\psi)$, we “unfold” by replacing the $(\neg\psi,\sigma)$-frame with $\neg$ and $(\psi,\sigma)$-frame. When $\sigma(\psi)$ is evaluated we “fold” by negating the result:

To evaluate disjunction $\psi_{1}\vee\psi_{2}$ we create two frames corresponding to the disjuncts. If $\psi_{2}$ evaluates to t, the frame marked by $\downarrow$ is dropped (disjunctions are short circuited). If $\psi_{2}$ evaluates to f, the frame corresponding to $\psi_{1}$ drops $\downarrow$ and is evaluated normally.