Expressive Logical Combinators for Free

1 Introduction

Modal logics have recently been increasingly used in the analysis of domain specific languages such as XML Schemas [Dal-Zilio et al., 2004; B´arcenas et al., 2011], XPath queries [Genev`es et al., 2007], SPARQL queries [Chekol et al., 2012], and CSS selectors [Genev`es et al., 2012]. They also serve as a formal framework for the analysis of programming languages such as CDuce [Benzaken et al., 2003; Gesbert et al., 2011], XQuery [Boag et al., 2005; Castagna and Xu, 2011], languages for XML access control [Murata et al., 2006; Kolovski et al., 2007] and, more generally, for NoSQL programming languages [Gesbert et al., 2011; Benzaken et al., 2013]. The common goal is to characterize these languages in terms of expressivity and complexity, and to build adapted and effective type-checkers, static analyzers, and compilers.

∗Detailed affiliation of authors: P. Genev`es (CNRS, Laboratoire d'Informatique de Grenoble, Inria, Univ. Grenoble Alpes) and A. Schmitt (Inria, Research Center Rennes - Bretagne Atlantique).

Alan Schmitt∗

Inria, Rennes

Such an approach requires the construction of efficient compilers that translate first-class constructs (such as queries) into logical formulas. Those formulas are then solved for satisfiability using an off-the-shelf satisfiability solver such as the ones found in [Tanabe et al., 2005; Pan et al., 2006; Genev`es et al., 2007; Genev`es et al., 2015a; Tanabe et al., 2008]. A critical aspect is then the size of the obtained logical formula, since it is a factor that affects the combined complexity 1 of the global approach.

We show that a whole class of logical combinators (or "macros") can be used as an intermediate language between the query language and the logical language. Those logical combinators provide an exponential gain in succinctness over the corresponding explicit logical representation, yet preserving the typical exponential time complexity [Tanabe et al., 2005; Pan et al., 2006; Genev`es et al., 2007; Genev`es et al., 2015a; Tanabe et al., 2008] of the logical decision procedure.

This opens the way for solving a wide range of problems such as query satisfiability and query containment in exponential-time, even though their direct formulation into the underlying logic results in an exponential blowup of the formula size, yielding an incorrectly presumed twoexponential time complexity.

Specifically, two essential steps are involved in the reduction of a problem to logical satisfiability: (1) the translation of the initial problem into a logical formula, and (2) the actual satisfiability check of the formula. Traditionally, the complexity of the satisfiability test is stated in terms of the size of the formula, thus every duplication of subformulas during the first step may affect the combined complexity and severely impact the practical applicability of the entire approach. Interestingly, we observe that a common form of µ-calculus sub-formula duplication has a very limited impact on combined complexity in existing implementations, such as [Tanabe et al., 2005; Pan et al., 2006; Genev`es et al., 2015a; Tanabe et al., 2008]. The reason lies in the fact that satisfiability-testing algorithms can operate directly on a Hintikka-set-like representation of formulas, named lean, composed of atomic propositions and modal subformulas. In other terms, the lean can be seen as a succinct but sufficient representation from which the logical satisfiability of the formula can be decided. In this setting, we prove that the time complexity of decision procedures actually depends on the number of distinct atomic propositions and modal subformulas present in the lean. This makes explicit a notion of truth-status sharing for identical sub-formulas not exhibited in the analysis of the time complexity of such algorithms.

1 In the context of problem-solving by reduction to logical satisfiability, combined complexity considers the complexity of the translation of the problem into logic (taking into account any potential blow-up in size induced by the change in representation), composed with the complexity of testing satisfiability of the formula.

We develop this idea in the context of the µ-calculus, whose expressive power subsumes the ones of many modal logics. More specifically we develop this idea using the alternation-free µ-calculus with converse modalities whose models are finite trees, following [Genev`es et al., 2007]. Trees are encoded in binary, without loss of generality, through the "first-child" and "next-sibling" modalities, respectively noted 〈1〉 and 〈2〉 in the manner of [Genev`es et al., 2007].

In this setting, an elegant way of building a µ-calculus formula is to apply a combinator to another formula. For instance, split(X) = 〈1〉X ∧ 〈2〉X is a combinator that generates a formula such that the input formula must hold in both successors of the current node. In the previous example, although X is duplicated, the increase of the size of the lean generated from split(ϕ) when compared to the one generated from ϕ is only a small constant, independent of ϕ.

The paper is organized as follows. We introduce the logical formulas and combinators in §2, state and prove our main result in §3. Finally, we report on practical applications in §4 with experimental results that illustrate that the lean size is indeed a better indicator of the problem's complexity than formula size.

2 Basic Logical Formulas and Combinators

We recall the syntax of the logic of [Genev`es et al., 2007], used to prove properties about finite binary trees. We consider a set AP of atomic propositions, representing the tree node names, which includes a special reserved name σ; a set Var of variables, used in fixpoints; and a set Prog = {1, 2, 1, 2} of programs, to describe navigation in a tree. Program 1 navigates to the first child (left successor), program 2 navigates to the next sibling (right successor), program 1 to the parent (predecessor to the right, if it exists), and program 2 to the previous sibling (predecessor to the left, if it exists). We let a = a for any a ∈ Prog. A logical formula is defined using the following syntax.

• ⊤, ⊥, σ, or ¬σ for all σ ∈ AP \ {σ};
• x for all x ∈ Var;
• ϕ1∨ϕ2 or ϕ1∧ϕ2 where ϕ1 and ϕ2 are logical formulas;
• 〈a〉ϕ or ¬〈a〉⊤ where a ∈ Prog and ϕ is a logical formula;
• µx.ϕ where x ∈ Var and ϕ is a logical formula.

We now give an intuition of the interpretation of formulas in the setting of finite trees: the interpretation of a formula is a set of focused trees, which are finite trees with a selected node. A formula is satisfiable if there exists a tree such that a node of this tree is selected by the formula (i.e., the set of focused trees is not empty). The truth formula ⊤ selects all focused trees, i.e., every node of every tree, whereas ⊥ selects none. The σ formula selects every focused trees whose selected node's name is σ, whereas ¬σ selects the nodes with other names (the node name σ is used to represent names of nodes not occurring in the formula). Formula conjunction and disjunction correspond to set intersection and union, respectively. A formula 〈a〉ϕ selects a node if the node reached following a is selected by formula ϕ. Formula ¬〈a〉⊤ selects a node if there is no node reachable through a. Finally, a fixpoint µx.ϕ is interpreted as the smallest fixpoint (the intersection of every pre-fixpoint).

A formula is closed if every occurrence of a variable x is bound by an enclosing µx. In the following, we only consider formulas that are closed and whose recursion variables are guarded (there is at least one navigation step between a recursion µx and every variable x). Note that since we do not have general negation in formulas (see below), there is no requirement for formulas to be positive (i.e., disallow formulas of the form µx. . . . ¬x): such formulas simply cannot be expressed. Finally, we write ϕ ≺ ψ if ϕ is a sub-formula of ψ, and ϕ ⊀ ψ if it is not.

A combinator F is a formula with zero or more occurrences of a placeholder, written X, possibly negated (¬X). We write F{ϕ/X} for the combinator F where every instance of X has been replaced by the closed formula ϕ. 2 We often write F(X) to make clear the name of the placeholder, and F(ϕ) for F{ϕ/X}.

We consider formulas in negation normal form. The negation of a formula or combinator, written F, is obtained using regular De Morgan's laws extended with the cases of fixpoints: µx.F = µx.F, x = x, X = ¬X, and ¬X = X. Moreover, the negation of a modality is a disjunction:

the modality is false either because there is no node in that direction, or because the node in that direction does not satisfy the sub-formula. Note that, in order to ensure that F = F for every formula, we have a special case when a disjunction is actually the negation of a modality:

Following [Genev`es et al., 2007], the greatest and smallest fixpoint coincide (provided a simple restriction on formulas, namely for cycle-free formulas using sets of finite trees as models, see [Genev`es et al., 2007] for details). Every combinator presented here fulfill this restriction. Nevertheless, this work could also be done in a setting where the smallest and greatest fixpoints differ, and in this case one defines µx.F as νx.F and νx.F as µx.F.

3 Deciding Combined Formulas

The Lean

Following [Pan et al., 2006; Genev`es et al., 2007; Tanabe et al., 2008], we define the lean of F as follows, with LΓ(F)

2 In case of a negated placeholder, we replace ¬X with ϕ, the negation normal form of ϕ (obtained using De Morgan's laws).

defined in Figure 1 (the environment Γ is the set of already unfolded fixpoints). The main difference with the usual approaches is that we close the lean under negation.

Figure 1: Negation Closed Lean

Intuitively, the lean of a formula ϕ is the set of every atomic proposition occurring in ϕ, and every subformula that starts with a modality present in ϕ or in the expansion of the fixpoints of ϕ. In particular, the lean does not directly include disjunctive or conjunctive subformulas. Kozen has shown in [Kozen, 1982] that expanding every fixpoint once is sufficient to generate every subformula that may need to be considered for satisfiability. This single expansion is tracked using the Γ argument in the definition above. Moreover, Kozen has also shown the lean is linear in the size of the formula. We next make this bound more precise.

The Factorization Power of the Lean

We can now state the main theorem of this paper: the lean size is not impacted by the duplication of sub-formulas. We write |S| for the size of a set S.

Theorem 1. Let F be a combinator and ϕ a closed formula. We have the following.

The theorem is a direct consequence of Lemma 9 which is proved below in §3.

We now give some intuition about this result, through a simple example. Recall the split(X) combinator defined as 〈1〉X ∧ 〈2〉X. Since the elements of the lean are either atomic propositions (node names) and modalities, the lean of split(ϕ) includes the lean of ϕ and four new elements: 〈1〉ϕ, 〈1〉ϕ, 〈2〉ϕ, and 〈2〉ϕ. If we now consider split(split(ϕ)), we once again add only four formulas to the lean: 〈1〉split(ϕ), 〈1〉split(ϕ), 〈2〉split(ϕ), and 〈2〉split(ϕ). This linear growth, even though the formula's size increases exponentially, is due to the fact that modalities are considered atomically and are not split up in their components (e.g., 〈1〉 (ϕ ∧ ψ) is not split up into 〈1〉ϕ and 〈1〉 ψ).

Satisfiability-Testing Algorithms based on the Lean

A typical approach to decide the satisfiability of a formula is to first build the lean, as described above, then to use a tableau-based algorithm implemented with BDDs [Tanabe et al., 2005; Pan et al., 2006; Genev`es et al., 2007; Tanabe et al., 2008]. The time complexity of this approach is shown to be exponential in the size of the formula. More precisely, it is exponential in the size of the lean, which is in turn linear in the size of the formula.

The essence of this paper is to show (both in theory and in practice) that the lean may grow much more slowly than the formula when sub-formulas are duplicated. This opens the way for solving a wide range of problems in exponentialtime even though their direct translation into the modal logic is exponential, as illustrated on concrete examples in §4.

Proof of Theorem 1

We define the number of recursive expansions of F or ϕ, written E∅(F), in Figure 2. We use this number to define inductive properties that depend on fixpoints being expanded.

Figure 2: Number of Recursive Expansions

We write (Γ)ϕX as the set of formulas G′ where either G′{ϕ/X} or G′{ϕ/X} is in Γ. We use this set to identify the formulas that were expanded.

Definition 2. Given ϕ, and Γ, we define (Γ)ϕX as follows.

Proof. By induction on F , relying on the fact that x = x.

Proof. By induction on the lexical order of EΓ(F) and the size of F. Base cases are immediate. For conjunction and disjunction, we may apply the induction hypothesis because EΓ(F1) and EΓ(F2) do not increase and the formula size decreases. This is also the case for the modality case.

For the recursion case where x ≺ F, we distinguish three cases (we do not mention the negation µx.F in these cases):

• if µx.F ∈ Γ, then necessarily µx.F ∈ Γ′ and we immediately conclude;
• if µx.F ∈ Γ′ , then we conclude by ∅ ⊆ S for any set S;
• otherwise, we have µx.F in neither set, and we apply the induction hypothesis, as EΓ∪{µx.F}(F{µx.F/x}) is strictly smaller than EΓ(µx.F).

Proof. By an immediate induction on the lexical order of EΓ(G) and the size of G.

Proof. By induction on the lexical order of EΓ(F) and the size of F .

The base cases ⊤, ⊥, x, X, ¬X, σ, ¬σ, ¬ 〈a〉 ⊤, and µx.F there x ⊀ F are immediate.

For F ∧ G, we compute as follows.

The disjunction case is similar.

For the recursion case, if µx.F or µx.F is in Γ, then µx.F or µx.F = µx.F is also in Γ and the result follows. Finally, if neither is in Γ, we compute as follows.

Lemma 8. For all Γ and F, if X ⊀ F, then L(Γ)ϕX (F) = L∅(F ).

Proof. We prove the more general result: for all Γ′ , L(Γ)ϕX ∪Γ′(F) = LΓ′(F) by induction on the lexical order of EΓ′ (F ) and the size of F .

The result is immediate for the base cases, and by induction for the conjunction, disjunction, and modality cases. For the recursion case, if µx.F (or its negation) is in (Γ)ϕX ∪Γ′ , then it must be in Γ′ as X ⊀ F and members of (Γ)ϕX contain X by definition. Thus both sides are equal to ∅. If neither µx.F nor its negation are in (Γ)ϕX ∪Γ′ , we have L(Γ)ϕX ∪Γ′ (µx.F ) = L(Γ)ϕX ∪Γ′∪{µx.F}(F{µx.F/x})

We next apply the induction hypothesis with Γ′ ∪ {µx.F} and F{µx.F/x}, thus we have L(Γ)ϕX ∪Γ′∪{µx.F}(F{µx.F/x}) = LΓ′∪{µx.F}(F{µx.F/x}) = LΓ′ (µx.F ).

We conclude by taking Γ′ = ∅.

Lemma 9. Let F be a formula mentioning X, and ϕ a closed formula. We have L∅(F {ϕ/X}) ⊆ L∅(F ){ϕ/X} ∪ L∅(ϕ).

Proof. We prove the following more general property for any Γ by induction on the lexical order of E(Γ)ϕX (F) and the size of F .

We first deal with every case where X ⊀ F. In this case, X also does not occur in LΓ(F).

Case X. We compute as follows, using Lemma 5 for the

Case ¬X. We compute as follows, using Lemma 5 for the set inclusion, and Lemma 7 to conclude.

Case F ∨G. Identical to the previous case.

Case 〈a〉F. We compute as follows, using Lemma 4 and the induction hypothesis.

Case µx.F with x ≺ F .

If we have µx.F{ϕ/X} ∈ Γ or µx.F{ϕ/X} ∈ Γ then LΓ(µx.F{ϕ/X}) = ∅ and the result is immediate. Otherwise we compute as follows.

ϕ closed

To apply the induction hypothesis, we show that

First, we have µx.F /∈ (Γ)ϕX and µx.F /∈ (Γ)ϕX , since otherwise, we would have µx.F{ϕ/X} ∈ Γ or µx.F{ϕ/X} = µx.F{ϕ/X} ∈ Γ, which we assumed to be false. Thus E(Γ)ϕX (µx.F) = E(Γ)ϕX ∪{µx.F}(F{µx.F/x}) + 1. Next, we have (Γ ∪ {µx.F{ϕ/X}})ϕX = (Γ)ϕX ∪ {µx.F} by definition. Thus we have E(Γ)ϕX (µx.F) = E(Γ∪{µx.F {ϕ/X }})ϕX (F {µx.F/x}) + 1.

We may thus apply the induction hypothesis and continue to compute.

As neither µx.F nor µx.F are in (Γ)ϕX , we have the following equality: L(Γ)ϕX (µx.F) = L(Γ)ϕX ∪{µx.F}(F{µx.F/x}). We may thus conclude the computation as follows.

We complete the proof by taking Γ to be ∅ and remarking that (∅)ϕX = ∅.

4 Applications

We provide an implementation of the proposed system [Genev`es et al., 2015b]. Each example given in this section comes in a boxed version that can directly be used with the implementation [Genev`es et al., 2015b]. Tests are thus reproducible.

We present several examples where advanced properties on the underlying data structure (here a tree) can be formulated using combinators, and for which our result applies. In particular, after an introductory example, we consider numerical constraints on the global number of occurrences, and properties on the sequence of leaves in a tree. This means, for instance, that if one extends a query language (such as XPath) with such kinds of features, then our result applies: problems such as query satisfiability and query containment would not be harder to solve in terms of computational complexity than they already are for the language without the extensions.

A Very Simple Example: Split

The combinator split(X) introduced in Section 3 may generate arbitrary large formulas: for instance, let ϕ = a ∧ 〈1〉 b ∧ 〈2〉µy.c ∨ 〈2〉 y, the formula ψ = split(split(split(ϕ))) uses 8 occurrences of ϕ. To give this formula to the implementation of [Genev`es et al., 2015b], we write it as follows.

phi() = a & <1>b & <2>let $y = c | <2>$y in $y;

split(#x) = <1>#x & <2>#x; split(split(split(phi())))

We then observe that ψ contains 24 atomic propositions, 38 modalities, 15 conjunctions, and 8 disjunctions (including duplicates). The size of the lean is only 19 (14 modalities and 5 atomic propositions 3 Each new split( ) around the formula then only adds two elements to the lean.

The satisfiability check of the above formula is performed in 131ms (milliseconds) with the implementation [Genev`es et al., 2015b], including 5ms for computing the lean and 104ms for computing the tableau. A sample satisfying tree of 33 nodes is also constructed in 39ms.

Document-Order Relation and Global Counting

Extending modal logics with operators for counting occurrences of specific nodes in trees is a notably difficult problem [Lugiez, 2005; Dal-Zilio et al., 2004]. In this example we review how our result applies for a simple form of counting (with respect to constants) in trees.

A very simple example of a combinator is the descendant relation that checks that a node satisfying some formula X is accessible in the subtree by any sequence of forward modalities. It is encoded as follows:

A whole range of combinators to navigate in a tree can be defined in a similar manner. In particular we can encode:

These combinators are easily defined in our logic; as they are very commonly used, they are predefined in [Genev`es et al., 2015b]. They can be used as such to encode the socalled document-order relation ≪. This relation corresponds to the ordering of nodes given by a depth-first tree traversal: x ≪ y iff node y is visited after node x in a depthfirst tree traversal. We define the combinator next(X) = descendant(X) ∨ following(X) with which we can mimic the document-order relation (we write X ∧ next(Y ) for x ≪ y). Notice that this combinator duplicates formulas, since the placeholder X appears twice in its definition.

The document-order relation can be used to express global counting properties in trees. For instance, if we want to encode the so-called concept of a nominal - or more generally the fact that some formula ψ is satisfied by one and only one node in the tree - we can write:

psi() = a & <1>b & <2>let $y = c | <2>$y in $y;

next(#x) = descendant(#x) | following(#x); previous(#x) = preceding(#x) | ancestor(#x); nominal(#x) = #x & ˜previous(#x) & ˜next(#x); nominal(psi())

3 The numbers we report in this paper correspond to the numbers reported by the implementation [Genev`es et al., 2015b].

If we now want to force the existence of at least 4 different tree nodes that satisfy ψ, we can write:

psi() & next(psi() & next(psi() & next(psi())))

The full expansion of the above formula is notably large (if we count duplicates, the formula contains 468 atomic propositions, 871 modalities, 156 conjunctions, and 404 disjunctions). However, the size of its lean is 43 (38 modalities and 5 atomic propositions).

The satisfiability check of the latter formula above is performed in 205ms with the implementation [Genev`es et al., 2015b], including 15ms for computing the lean and 124ms for the tableau. A sample satisfying tree is built in 78ms.

The Tree Frontier

In this example, borrowed from [Afanasiev et al., 2005], one describes constraints on a tree frontier. A tree frontier is the set of leaves (nodes without an outgoing "1" edge) ordered from left to right. A frontier node y is the successor of a frontier node x iff x ≪ y and there is no leaf node in between x and y in the document order. A simple case analysis shows that node y is the successor of a frontier node x in one of three cases:

1. Either x is a leaf with an immediate next sibling which is also a leaf (y);
2. or x is a leaf with an immediate next sibling which is not a leaf, in which case, by navigating downward in its subtree we reach the leftmost leaf (y);
3. or x is a leaf with no next sibling, in which case, by going up to the parent node recursively until we reach a parent node which has a next sibling, then going to this next sibling, and then, from this node, navigating downward in its subtree we reach the leftmost leaf (y).

This yields the following definition of a combinator that captures all the aforementioned cases with the help of a few neatly chosen auxiliary predicates:

nextFrontierNode(Y ) = leaf ∧ upUntilRsibl(ψ)

In this definition, the placeholder Y is to be replaced by a formula that holds at the successor node, and:

Using these combinators, we can now express properties on the tree frontier. For instance, the formula shown on Figure 3 states that the leftmost leaf is labeled "a", and, by further navigation on the tree frontier, we encounter two other leaves labeled "a". If we count duplicates, the corresponding formula

leaf() = ˜<1>T; down_to_first_leaf(#z)= let $x= (leaf() & <0>#z) |<1>$x in $x; up_until_rsibl(#x) = (<2>T & #x) | let $w = <-1>((<2>T & #x) | $w) | <-2>$w in $w; next_frontier_node(#y) = leaf() & up_until_rsibl(<2>down_to_first_leaf(#y)); down_to_first_leaf(a & next_frontier_node(a & next_frontier_node(a)))

contains 7 atomic propositions, 26 modalities, 23 variables, 10 fixpoint binders, 7 negations, 7 conjunctions, and 16 disjunctions. However, the size of the corresponding lean is 22. The lean is only composed of 19 distinct modalities and 3 distinct atomic propositions. Each additional nested call to the combinator ∧ nextFrontierNode(Y ) extends the lean by 6 modalities. However, the corresponding global formula goes from 26 modalities to 58 for the first addition, then it goes to 122 for the second addition. It reaches 32762 modalities for the 10th addition, whereas the corresponding formula is solved for satisfiability in 11052ms (lean size is 82).

The satisfiability check of the formula shown in Figure 3 is performed in 136ms with the implementation [Genev`es et al., 2015b], including 3ms for computing the lean and 109ms for computing the tableau. A sample satisfying tree is built in 18ms.

5 Conclusion

We have presented the concept of logical combinators that avoid exponential increases in combined complexity due to sub-formula duplication. Our main result, of theoretical nature, has very practical consequences and applies for a large class of logical solvers such as the ones found in [Tanabe et al., 2005; Pan et al., 2006; Genev`es et al., 2007; Genev`es et al., 2015a; Tanabe et al., 2008].

We have further illustrated this result in the context of one of these satisfiability solvers [Genev`es et al., 2007; Genev`es et al., 2015a], for which we have presented an indepth analysis. This analysis focuses on the time complexity of lean-based algorithms to decide the satisfiability of a tree logic equipped with inverse programs, nominals, and counting introduced via combinators. The analysis highlights our result by showing that the lean automatically factorizes duplicated sub-formulas even for such advanced features, thus the complexity of the algorithm should not be stated in terms of the size of the initial formula but in terms of the size of the lean. A direct consequence of this observation is that the addition of nominals and a more general form of counting to the initial tree logic has no impact on decidability nor on its precise complexity bound. We have also reported on practical experiments using an implementation.