$$\exists R \forall x\_1, \dots, x\_n \big(R(x\_1, \dots, x\_n) \leftrightarrow \phi(x\_1, \dots, x\_n)\big)$$

for any second-order formula φ(x1,...,xn) which does not contain the n-ary relation symbol R. In the *arithmetic* comprehension axiom φ(x1,...,xn) is firstorder.

Generalizing the semantics of SL accordingly in terms of a given set of possible heaps, which does not necessarily contain *all* heaps, we can formulate in SL the following version of the arithmetic comprehension axiom

$$\spadesuit(\forall x, y ((x \hookrightarrow y) \leftrightarrow \phi(x, y)))$$

1 Here we adopt the terminology for second-order logic [V¨a¨a01], where the semantics of *full* second-order logic does not impose any restrictions on the *cardinality* of the interpretation of the predicates/relations, in contrast to *weak* second-order logic which restricts to *finite* interpretations (of the predicates/relations).

which expresses the existence of a heap such that its *graph*, as denoted by the points-to relation →, satisfies the 'pure' first-order formula φ(x, y) (i.e., φ does not involve the separation connectives and the points-to relation). The - modality (formally defined in Sect. 3) expresses the existence of a heap which satisfies the associated formula. Such an instance of the arithmetic comprehension axiom holds if there exists a heap which is characterized by the formula φ(x, y). We cannot generalize this axiom to arbitrary SL formulas because it is not obvious how to avoid contradictions like -(∀x, y((x → y) ↔ ¬(x → y))). Simply requiring that the points-to relation does not occur in φ(x, y) does not work because the separating connectives implicitly refer to it. Therefore, we introduce a new interpretation of SL that restricts the (second-order) quantification to *first-order definable* heaps. For this new interpretation we introduce a *sequent calculus* which is sound and complete. The completeness proof is based on the construction of a model for a *consistent* theory (a theory from which false is not derivable), following [Hen49]. From the completeness proof we further derive that this new interpretation satisfies both compactness and the downward L¨owenheim-Skolem theorem. By the seminal theorem of Lindstr¨om we then infer that this new interpretation is as expressive as first-order logic.

*Related Work.* The model theory of SL has been focused mainly on finite heaps. For example, the computability and complexity results in [CYO01] depend on this assumption. Surprisingly, in [BDL12] the authors show that *weak* SL is as expressive as *weak* second-order logic [Man96], which is a semantics of secondorder logic where quantification is restricted to finite relations. In [DD16] this result is further refined by the restriction to two variables and the separating implication (no separating conjunction) which still is as expressive as weak second-order logic. In [EIP20] the satisfiability problem for SL with k record fields has been studied for finite heaps, but over arbitrary first-order models. A tableaux method for a propositional fragment of SL has been developed in [GM10] which has been proven sound and complete. Extensions to first-order SL are discussed assuming finite heaps. In fact, the tableaux method introduced is based on a labelling mechanism for encoding finite heap structures.

In contrast, when investigating complete proof systems for SL the assumption of the finiteness of heaps has to be dropped, thus allowing for infinite heaps, because, as already observed above, finiteness leads to non-compactness. Our general model theory shows that this generalization of SL, *full* SL, is also non-compact, and therefore does not allow for a finitary sound and complete logic either. Consequently, to obtain such a logic one either has to syntactically restrict SL or further abstract or generalize its semantics. In [DLM21], for example, a sound and complete sequent calculus is described for a quantifier-free subset of SL. On the other hand, examples of further abstractions and generalizations are [HT16] and [Pym02], and both describe a finitary logic which is sound and complete. In [Pym02], models are based on very general preordered commutative monoids and there is no points-to relation. In [HT16], special commutative monoids called *separation algebras* are used to give semantics to the separating connectives. The elements of such separation algebras represent heaps as relations on the underlying (first-order) domain. This allows for a standard set-theoretic interpretation of the points-to relation. However, the semantics of separating conjunction is defined in terms of the abstract monoid, and as such is decoupled from the set-theoretic interpretation of the points-to relation. For example, a first-order specification (using plain conjunction) of an enumeration of the elements of the domain of a (finite) heap *as a set* does not in general correspond with an enumeration using separation conjunction.

A sound and complete axiomatization of the points-to relation in the general context of first-order SL *respecting its standard set-theoretic interpretation* thus remains a main challenge.

Second-order logic allows for a straightforward translation of the (weak or full) semantics of SL, and one can use second-order logic to reason about validity in SL. This approach is followed for example by the IRIS project [JKJ+18] which formalizes the semantics of weak SL in the higher-order logic of Coq [HH14]. By restricting the semantics of the separating connectives to (first-order) definable heaps, our approach instead transforms a *compositional* second-order logical description of the semantics of SL into corresponding rules of a standard firstorder sequent calculus. The resulting calculus allows us to reason, in a natural manner, in first-order logic about the (hierarchical) heap structures generated by the rules for the separating connectives. As such it does not involve the additional tree structures of the so-called *bunched contexts* of the sequent calculi of [HT16] and [Pym02]. Also [Kri08] avoids the use of bunched contexts in a modal sequent calculus for propositional SL, which is proven sound. However it is incomplete because it provides limited support for equational reasoning about the modal contexts (so-called 'worlds') associated with the SL formulas.

*Plan of the Paper.* In the next section we introduce the syntax and semantics of full SL. In Sect. 3 we investigate the expressiveness of full SL. Section 4 introduces a restriction of the semantics to definable heaps. In Sect. 5 we introduce the sequent calculus, and discuss soundness and completeness. Finally, in the conclusion section we wrap up, and discuss some future work.

# **2 Separation Logic**

In this section we introduce the syntax of SL and define its classical semantics with respect to arbitrary first-order models. For an intuitive introduction to separation logic, see [Rey05]. Given a first-order signature of function and predicate symbols2 and a countably infinite set of first-order variables x, y, z, . . ., the first-order terms of this signature are denoted by t, t ,....

We have the following inductive definition of formulas of separation logic.

**Definition 1 (Syntax of SL).** *We define*

p ::= (t1 = t2) | R(t1,...,tn) | (¬p) | (p ∧ q) | ∃x(p) | (p ∗ q) | (p −∗ q)

2 We allow for a countably infinite set of such symbols.

*where* R *is a* n*-ary relation symbol. As a special case we have the binary 'pointsto' relation symbol* → *(also called the weak/loose points-to).*

Let M = (D, I) denote a first-order model, where D denotes the non-empty domain and I provides an interpretation of the function and predicate symbols as functions and relations over D. A valuation s assigns elements of the domain D of M to the first-order variables x, y, z, . . .. We omit the standard inductive definition of the value Is(t) of a term t. Given a model M = (D, I), we denote by M, h, s |= p that p holds in the model M, under the interpretation h ⊆ D ×D of the binary relation symbol →, where h denotes a so-called *heap*, represented as the graph of a *partial function* with *finite domain*.

**Definition 2 (Semantics of SL).** *We have the following main cases.*

*Other cases are the Tarksi-style semantics of classical logic [Yan01, Table 5.2].*

In the above definition we use the set-theoretic operation of *union* of binary relations as sets of pairs. On the other hand, by h1 ⊥ h2 we denote that the *domains* of the relations h1 and h2 are *disjoint*3. As such, we can introduce the strict/tight points-to relation → of SL, defined by M, h, s |= t → t if and only if h = { Is(t), Is(t ) }, as a derived concept: it can be expressed by (t → t ) ∧ ∀x, y((x → y) → (x = t ∧ y = t )). The concept **emp** of the empty relation can also be expressed by ∀x, y(x → y). *Intuitionistic* SL only allows for the weak/loose points-to relation. The strict version cannot be expressed in intuitionistic SL because of its *monotonicity* property that the truth of a formula is preserved by extensions of the domain of the heap [Rey00]. In this article we focus on classical separation logic only.

Let (xi → −) abbreviate ∃y(xi → y). The sentences φn defined by

$$\exists x\_1, \dots, x\_n ((x\_1 \hookrightarrow -) \* \dots \* (x\_n \hookrightarrow -))\ .$$

then state that there exist at least n allocated elements of the underlying domain of the given first-order model. Note that the semantics of the separating conjunction implies that xi = xj for i = j. It is also possible to formulate the same property using propositional conjunction instead of separating conjunction by explicitly stating this fact, that the variables are not aliases. Now collect all φn in a set. Clearly, every finite subset of this set of sentences is satisfied by a finite heap, but that there does not exist a finite heap satisfying all these sentences.

3 The domain of an arbitrary relation R ⊆ D × D is the set d ∈ D for which there exists a d- ∈ D such that d, d- ∈R. Note that for heaps h1 ⊥ h2 is equivalent to h1 ∩ h2 = ∅.

This simple counterexample to compactness provides the basic motivation to study the above semantics of SL extended to unbounded heaps, i.e. heaps which potentially have an infinite domain.

Further, for technical convenience only, we generalize the semantics to arbitrary *binary relations*. For an arbitrary (binary) relation R ⊆ D × D on the underlying domain D of the given first-order model, we define M, R, s |= p as above, where the interpretation of the separating connectives ranges over arbitrary subsets of D × D. In fact, in this generalized semantics, which we call *relational* SL, we can model the restriction to heaps simply by *syntactically* restricting the separating implication to assertions of the form (p ∧ *fun*) −∗ q, where *fun* denotes the assertion ∀x, y, z((x → y ∧ x → z) → y = z). Let p denote the result of restricting syntactically all occurrences of the separating implication in p to heaps (as described above). It follows that the evaluation of p ∧ *fun* is restricted to heaps.

It is worthwhile to observe here that there exists a straightforward formalization of relational SL in second-order logic. For any formula p as defined above we define inductively the second-order formula p(R), where R is a binary relation.

#### **Definition 3 (Logical formalization of relational SL).**

*We have the following main cases.*

*–* (t → t )(R) = R(t, t )*, –* (p ∗ q)(R) = ∃R1, R2(R = R1 R2 ∧ p(R1) ∧ q(R2))*, –* (p −∗ q)(R) = ∀R1, R2((R2 = R1 R ∧ p(R1)) → q(R2))*.*

Here we denote by R = R1 R2, for any binary relation symbols R, R1, R2, the conjunction of the formulas ∀x, y(R(x, y) ↔ (R1(x, y) ∨ R2(x, y))) and ∀x, y, z(¬R1(x, y) ∨ ¬R2(x, z)). We denote by M,s |= φ the standard truth definition of a second-order formula φ, where the evaluation s additionally interprets the second-order variables. Correctness of this translation, that is, M, R, s |= p if and only if M,s[R := R] |= p(R) (where s[R := R] denotes the update of s which assigns to the binary variable R the relation R), can be established by a straightforward induction on p.

#### **3 Model Theory: Compactness and Countability**

To explore the general model theory of SL we introduce the modalities p and p as abbreviations of **true** ∗ (**emp**∧(**true** −∗ p)) and ¬(**true** ∗ ¬p), respectively4. For M = (D, I) we have M, R, s |= p if and only if M, R , s |= p, for *every* R ⊆ D×D. Further, we have M, R, s |= p if and only if M, R , s |= p, for *every* sub-relation R of R (that is, R ⊆ R). By p we denote the formula ¬¬p. It follows that M, R, s |= p if and only if M, R , s |= p, for *some* R ⊆ D × D.

*Characterizing Finite Models.* The above -modality allows to express that the domain D of a model M = (D, I) is finite, by asserting that every injective

4 We note that and are, respectively, and ♦ in [HT16]. However in [HT16] they are introduced not as abbreviations but as *primitive* concepts.

function f : D → D is a surjection: Let *inj* be the conjunction of the formulas *fun* (as defined above), ∀x, y, z((x → z ∧ y → z) → x = y), and ∀x∃y(x → y). We have that M, R, s |= *inj* if and only if R : D → D is injective (note that the domain of R is D because M, R, s |= ∀x∃y(x → y)). And so M, R, s |= (*inj* → ∀x∃y(y → x)) if and only if D is finite. Note that the occurrences of → in the scope of the -modality are universally bounded, and the interpretation of → thus ranges over *all* R ⊆ D × D.

*Characterizing Countable Infinity.* We next show that countability of the underlying domain of a model can be expressed, using the above two modalities. We will be working with chains related by →, and in that sense we speak of a *predecessor* of x, being any y such that (y → x), and *successor* of x, being any y such that (x → y). Let *enum* be the conjunction of the following formulas:

Note that a relation R is well-founded iff *every* (non-empty) sub-relation of R has a minimal element (with respect to that sub-relation). This fact can be expressed by the use of the formula *enum*. Let M, R, s |= *enum*. We show that R encodes an enumeration dn n of D (still we have M = (D, I)). We define the sequence dn n by induction on n: for d0 we take the (unique) minimal element, and for dn+1 we take the unique element d ∈ D such that dn, d ∈R. Note that *inj* implies that every element of D has a unique 'successor' and that dn+1 ∈ {d0,...,dn}. Wellfoundedness ensures that every element of D appears in the enumeration dn n. Because otherwise we can construct an infinite descending chain of elements not appearing in the enumeration dn n (since d0 denotes the unique minimal element with respect to the functional interpretation R of →, it follows that for any d ∈ D which does not appear in the enumeration dn n there exists a d ∈ D which also does not appear in the enumeration dn n and d , d ∈R).

We thus have that M, R, s |= *enum* implies that the domain of M is countably infinite. The formula *enum* further abstracts from the current interpretation of the points-to relation →, so that if the domain of M is countably infinite then M, R, s |= *enum*, for arbitrary R (and s).

The class of uncountable models is characterized by ¬(*enum* ∨ *fin*), where *fin* denotes the above formula which characterizes the class of finite models.

Summarizing, the logic of full SL is neither compact nor does it satisfy the L¨owenheim-Skolem theorem because it can distinguish between countable and uncountable models. Further, we observe that the above expressiveness results do not depend on the interpretation of the points-to relation as an arbitrary relation. That is, these results also hold for the semantics restricted to (infinite) heaps.

5 ∃!xp is an abbreviation of ∃x(p ∧ ∀y(p[y/x] → y = x)), where p[y/x] denotes the substitution of x by y.

Interestingly, since we can express that the points-to relation → is wellfounded (see above), even restricting to the separating conjunction gives rise to non-compactness: given a countably infinite set of individual constants cn, n ≥ 0, let Γ consist of the above formula (**emp**∨ ∃x((x → −)∧ ∀y((y → −) → (y → x))) and the formulas cn+1 → cn, n ≥ 0. Clearly, every finite subset of Γ is satisfiable but Γ itself is not. Note that we do not need to require that all the ci = cj , for every i = j, because in case the formulas cn+1 → cn, n ≥ 0, are satisfied and additionally ci = cj holds, for some i = j, we have a loop in the interpretation of →. Further, restricting SL to separating conjunction also does not satisfy the *upward* L¨owenheim-Skolem theorem, because, as argued above, M, R, s |= *enum* implies (infinite) countability of the domain of M.

*Separation Logic Light.* What about further restricting to *positive* occurrences of the separating conjunction? Since we then can push negation inside, this restriction can be formally defined by the following syntax describing SLL ('separation logic light'):

$$p ::= (\neg) R(t\_1, \ldots, t\_n) \mid (p \lor q) \mid (p \land q) \mid \exists x (p) \mid \forall x (p) \mid (p \* q)$$

Here R denotes either a n-ary relation symbol or the points-to relation →. Thus, in this version of SL, negation can only be applied to atomic formulas. To show that the notion of satisfiability of SLL is compact, we introduce the following first-order translation p@R, where R is a binary predicate different from →, ◦ denotes conjunction/disjunction, and Q denotes the existential/universal quantifier.

$$\begin{array}{ll} (\neg)R(t\_1, \dots, t\_n) \circledast R' = (\neg)R(t\_1, \dots, t\_n) \\ (t \to t') \circledast R &= R(t, t') \\ (p \circ q) \circledast R &= p \circledast R \circ q \circledast R \\ Qx(p) \circledast R &= Qx(p \circledast R) \\ (p \ast q) \circledast R &= R = R\_1 \uplus R\_2 \land p \circledast R\_1 \land q \circledast R\_2 \end{array}$$

The binary relation symbols R1 and R2 are 'fresh'. It follows that p is satisfiable if and only if p@R is satisfiable. More precisely, M, R, s |= p if and only if there exists a (first-order) model M such that M , s |= p@R. Consequently, compactness of first-order logic implies compactness of SLL: Let Γ be an infinite set of formulas of SLL and Γ = {p@R | p ∈ Γ}6, for some binary relation symbol R. If every finite subset of Γ is satisfiable, so is every finite subset of Γ . By the compactness of first-order logic Γ is satisfiable, and so is Γ. Along the same lines it follows that if Γ is satisfiable then there exists a model M = (D, I) such that D is *countable* and M, R, s |= p, for every p ∈ Γ.

Note however that compactness of the satisfiability relation does not imply that the (semantic) consequence relation is compact. In fact, non-compactness of the consequence relation for SLL follows directly from the above argument

6 Note that Γ may require the introduction of an infinite number of fresh (binary) relation symbols. This is however no problem because first-order logic allows for a countably infinite set of function and relation symbols.

involving well-founded relations: Let Γ denote the set formulas cn+1 → cn, n ≥ 0. It follows that Γ |= **true** ∗ (¬**emp** ∧ ∀x((x → −) → ∃y(y → x))). But clearly, there does not exist a finite subset Γ0 of Γ such that Γ0 |= **true** ∗ (¬**emp** ∧ ∀x((x → −) → ∃y(y → x))).

*Some Open Problems.* The question remains whether restricting to separating conjunction satisfies the *downward* L¨owenheim-Skolem theorem. A counterexample to the downward L¨owenheim-Skolem theorem would be the expressibility of uncountable models. This seems to require the p modality (and thus the separating implication).

Another interesting question is whether we can express finiteness of the domain of the current interpretation of the points-to relation, that is, does there exist a formula p in SL such that M, R, s |= p if and only if the domain of the relation R is finite?

A main open problem is a formalization of the relation between full SL and second-order logic. Intuitively, one of the main differences is the *local perspective* of SL, which is determined by the current heap. Remarkably, as already mentioned in the introduction, [BDL12] presents a rather intricate encoding of (dyadic) weak second-order logic into weak SL. Apparently this restriction to finite heaps allows to break the local perspective. Our conjecture however is that full SL is strictly less expressive than (dyadic) second-order logic. To illustrate how subtle this difference may be, consider the following extension of separation logic with a *binding* operator ↓R(p) which binds the binary variable R in the evaluation of p to the current interpretation of the points-to relation. In other words, it corresponds to a bounded (second-order) quantification ∃R((R = →) ∧ p), where, R = → abbreviates the first-order formula ∀x, y(R(x, y) ↔ (x → y)). Alternatively, we can directly define M, R, s |= ↓R(p) if and only if M, R, s[R := R] |= p. This definition thus assumes an extension of the valuation s to (binary) second-order variables. The expressive power of this binding operator lies in that it allows to 'break the spell' of the local perspective since the bound binary variable allows in the local context of the current interpretation of the points-to relation to refer to those 'outer' ones that have generated it (by the separating connectives). This extension of SL allows for a simple, compositional translation of (dyadic) second-order logic. We have the following main case which translates ∃R(φ), where φ a dyadic second-order formula (which is assumed not to contain occurrences of the points-to relation of SL), into the SL formula -(↓R(p)).

#### **4 Separation Logic of Definable Binary Relations**

In this section we restrict the interpretation of the separating connectives to first-order definable binary relations. By φ we now denote a first-order formula which does not contain occurrences of the points-to relation → of SL. We omit the standard inductive truth definition M,s |= φ of a first-order formula φ.

By φ(x1,...,xn) we denote that the free (first-order) variables of φ are among the distinct variables x1,...,xn. A formula φ(x, y) is called a *binary* formula. A binary formula is also simply denoted by φ, omitting its free variables x and y. Given a model M = (D, I), and a first-order formula φ(x, y), we denote by *Rel*M(φ) the relation { s(x), s(y) | M,s |= φ} ⊆ D × D. Note that the evaluation of φ(x, y) only depends on the values of its free variables x and y, that is, M,s |= φ if and only if M,s |= φ, where s(x) = s (x) and s(y) = s (y). By φ(t, t ) we denote the result of replacing in φ(x, y) the variables x and y by t and t , respectively (if necessary renaming bound variables to ensure that the variables of t and t do not become bound).

**Definition 4 (First-order definability).** *Given a model* M = (D, I)*, a relation* R ⊆ D × D *is* first-order definable *if* R = *Rel*M(φ)*, for some binary formula* φ(x, y)*.*

Note that, given a model M = (D, I), I(R) = *Rel*M(R), that is, for any binary relation symbol R its interpretation I(R) is trivially a first-order definable relation. We generalize the definition of R = R1R2 to arbitrary binary formulas: we denote by φ = φ1φ2 that the binary formulas φ1(x, y) and φ2(x, y) represent a partition of the binary formula φ(x, y) which is expressed by the conjunction of ∀x, y(φ(x, y) ↔ (φ1(x, y) ∨ φ2(x, y))) and ∀x, y, z(¬φ1(x, y) ∨ ¬φ2(x, z)). The latter formula, which states that the domains of the binary relations represented by φ1(x, y) and φ1(x, y) are disjoint, we abbreviate by φ1 ⊥ φ2.

In the sequel we denote by M, R, s |= p the *restriction* of the relational semantics of full SL (Definition 2 extended to binary relations) such that instead of quantifying over arbitrary binary relations, the separating connectives involve quantification over first-order definable binary relations. It is worthwhile to observe here that, as for Henkin models of second-order logic [Hen50], the implicit second-order quantification depends on the underlying signature of function and relation symbols. Extending or restricting the signature affects the semantics of formulas of the 'old' signature.

# **5 Sequent Calculus**

To reason about the implicit quantification over definable (binary) relations, we introduce *rooted* assertions of the form p@φ, where φ denotes a binary formula and p is a formula of SL (see Definition 1). We define M,s |= p@φ if and only if M, R, s |= p, where R = *Rel*M(φ). The variables x and y of the binary formula φ(x, y) are thus implicitly bound by the @-operator, that is, M,s |= p@φ if and only if M,s |= p@φ, for any s and s such that s(z) = s (z), for any free variable occurring in p.

Note that the separating connectives are interpreted in terms of relations which are definable by first-order formulas which do not involve the points-to relation →. This allows for the following alternative *predicative* definition7 of the semantics of the separating connectives in rooted assertions (used in both the soundness and completeness proofs). Here ψ ⊥ φ, for the binary formulas ψ(x, y) and φ(x, y), denotes the formula ∀x, y, z(¬ψ(x, y) ∨ ¬φ(x, z)).

7 For a foundational discussion concerning predicativity, see [Cro17].

**Fig. 1.** Sequent calculus. The binary relation symbols R1, R2 and R introduced in the rules **L**∗ and **R**−∗ are 'fresh'. In the points-to rules p denotes a basic formula (which does not contain occurrences of the separating connectives).

#### **Lemma 1.** *We have*

We now develop a calculus for sequents A1,...,An ⇒ B1,...,Bm, where each Ai, i = 1,...,n, and Bj , j = 1,...,m, is constructed from first-order formulas and rooted assertions, which can be further composed using propositional connectives and quantification of first-order variables. This calculus is an extension of standard first-order sequent calculus (including cut), where the standard rules are applicable with respect to top-level propositional connectives and quantifiers. Figure 1 shows the left and right rules for separating conjunction and implication. These rules closely follow the translation in Definition 3 of SL into second-order logic, eliminating the explicit second-order quantification by applying the standard proof rules for second-order quantification (which themselves are straightforward generalizations of the rules for first-order quantification, instantiating the second-order variables by formulas). The binary relation symbols R1, R2 and R introduced in the rules **L**∗ and **R**−∗ are 'fresh' binary relation symbols, that is, they must not appear in the formulas of the conclusion of the rules.

We also have rules which allow classical reasoning under rooted assertions: (p ◦ q)@φ ↔ (p@φ) ◦ (q@φ), where ◦ denotes binary propositional connectives, e.g., conjunction, disjunction, and implication, (¬p)@φ ↔ ¬(p@φ), and (∃xp)@φ ↔ ∃x(p@φ) (and similarly (∀xp)@φ ↔ ∀x(p@φ)). Further, we have ∀x, y(φ ↔ ψ) → (p@φ ↔ p@ψ). It is straightforward to validate these rules, but we omit the details of the semantics M,s |= A, which follows the standard Tarski-style classical semantics, given the semantics of rooted assertions which may appear in the place of atomic formulas.

In the so-called 'points-to' rules of Fig. 1 the formula p does not involve occurrences of the separating connectives. Such a formula of SL we call *basic*. Note that it differs from pure first-order formulas in that basic formulas additionally may involve the points-to relation. For such formulas we denote by p[φ/ →], for any binary formula φ(x, y), the result of replacing every atomic assertion (t → t ) in p by φ(t, t ), which is a pure first-order formula. It follows that M,s |= p[φ/ →] if and only if M, *Rel*M(φ), s |= p, for any basic formula p.

*Example Proofs*

$$\begin{array}{c} \begin{array}{ccc} \Gamma \Rightarrow q@R, R\_1 \bot R\_2 & \Gamma \Rightarrow q@R, p@R\_1 & \Gamma, q@(R\_1 \lor R\_2) \Rightarrow q@R \\ \hline \hline \end{array} & \begin{array}{ccc} \Gamma \Rightarrow R\_1 \Downarrow R\_2, p@R\_1, (p \twoheadrightarrow q)@R\_2 \Rightarrow q@R \\ \hline \end{array} & \begin{array}{ccc} \textbf{L}\_\* & \\ \hline \end{array} \\ \begin{array}{ccc} (p \ast (p \twoheadrightarrow q))@R \Rightarrow q@R \\ \hline \end{array} & \begin{array}{ccc} \left(p \ast (p \twoheadrightarrow q)\right)@R \rightarrow q@R \\ \hline \end{array} \\ \hline \end{array} \end{array} \\ \begin{array}{ccc} \textbf{L}\_\* & \\ \hline \end{array} \\ \end{array}$$

As a first example of the use of the sequent calculus, above we have a derivation of the sequent ⇒ ((p ∗ (p −∗ q)) → q)@R which represents the validity of (p ∗ (p −∗ q)) → q. This derivation essentially consists of an application of the rule **L**∗ followed by an application of the rule **L**−∗. In this derivation Γ denotes the formulas R = R1 R2, p@R1 generated by the application of rule **L**∗. The second premise of the application of the rule **L**−∗ is derivable from an instance of the axiom Γ, A ⇒ A, Δ. Note that ψ (in the **L**−∗ rule) is instantiated with R1. The first and third premise follows from the fact that R = R1 R2 reduces to R1 ⊥ R2 and R = R1 ∪ R2 (that part of the proof is not shown above).

Next we show how to use the calculus in reasoning about the equivalence of weakest preconditions that arise in the practice of verifying the correctness of heap manipulating programs. Let p denote the weakest precondition (u → −)∧(z = 0 u = vv → z) of the heap update [u] := 0 which ensures the postcondition v → z after assigning the value 0 to the location denoted by the variable u (here φbψ abbreviates (b∧φ)∨(¬b∧ψ)) (in [dBHdG23] a dynamic logic extension of SL is introduced which generates this weakest precondition). The standard rule for backwards reasoning in [Rey02] gives the weakest precondition (u → −) ∗ (u → 0 −∗ v → z), which we denote by p . These preconditions are equivalent because both are the weakest.

Surprisingly, a proof of the implication p → p however exceeds the capability of all the automatic SL provers in the benchmark competition for SL [SNPR+19]. In particular, of the automatic provers, only the CVC4-SL tool [RISK16] supports the fragment of SL that includes the separating implication connective. However, from our own experiments with that tool, we found that it produces an incorrect counter-example and reported this as a bug to one of the maintainers of the project (Andrew Reynolds). In fact, the latest version, CVC5-SL, reports the same input as 'unknown', indicating that the tool is incomplete. In the case of (semi) interactive SL provers (such as Iris [JKJ+18], and VerCors [AH21,MRH22] that uses Viper [MSS16] as a back-end) we sought out expertise and collaborated in our search for a tool-supported proof of the above equivalence. Even after personally visiting the Iris team in Nijmegen (lead by Robbert Krebbers) and the VerCors team in Twente (lead by Marieke Huisman), we were unable to guide the tools to produce a proof of p → p. The problem here seems similar to that of [HT16], in that their semantics of separating connectives, which are formalized in terms of abstract monoids, are not compatible with the set-theoretic interpretation of the points-to relation.

In fact, the equivalence between the above two formulas can be expressed in quantifier-free separation logic, for which a complete axiomatization of all valid formulas has been given in [DLM21]. In the sequent calculus we can express the equivalence of p and p in terms of the sequent *fun*(R) ⇒ (p ↔ p )@R. Here R is an arbitrary binary relation symbol used to represent the current interpretation of the points-to relation. We abbreviate ∀x, y, z((R(x, y) ∧ R(x, z)) → y = z) by *fun*(R). A proof of the above sequent amounts to proving the sequents *fun*(R), p @R ⇒ p@R and *fun*(R), p@R ⇒ p @R. Below we present a highlevel proof of the first sequent, abstracting from some basic first-order reasoning in the calculus.

By an application of **L**∗ to derive the sequent *fun*(R), p @R ⇒ p@R it suffices to derive

$$fun(R), R = R\_1 \uplus R\_2, (u \mapsto -) \uplus R\_1, (u \mapsto 0 \twoheadrightarrow v \Longleftrightarrow z) \uplus R\_2 \Rightarrow p \uplus R\_1$$

for some fresh R1 and R2. Let ψ(x, y) denote the binary formula x = u ∧ y = 0. Further, let Γ denote the set of formulas *fun*(R), R = R1 R2,(u → −)@R1. By an application of the rule **L**−∗ it then suffices to prove the following sequents (from Γ ⇒ Δ we can derive Γ ⇒ A, Δ by right-weakening). First we prove Γ ⇒ R2 ∩ ψ = ∅: By the points-to rules the rooted assertion (u → −)@R1 (appearing in Γ) reduces to ∃z(R1(u, z) ∧ ∀x, y(R1(x, y) → x = u ∧ y = z)) (the forall-part of the formula is due to the 'strict' points-to which states that the domain contains u as its only location). Further, R2 ∩ ψ = ∅ logically boils down to ¬∃x, y(R2(x, y) ∧ (x = u ∧ y = 0)), that is, ¬R2(u, 0), which in basic first-order logic follows from ∃zR1(u, z) and the assumptions R = R1 R2 and *fun*(R).

Second, we prove Γ ⇒ (u → 0)@ψ: By the points-to rules (u → 0)@ψ (using the expanded definition φ of u → 0 and the definition of the substitution φ[ψ/ →]) reduces to (u = u)∧(0 = 0)∧∀x, y((x = u ∧ y = 0) → (x = u ∧ y = 0)) which is equivalent to **true**.

420 F. S. de Boer et al.

And, finally, we prove Γ,(v → z)@(R2 ∨ ψ) ⇒ p@R: First note that (again, by the points-to rules)

$$((u \longleftrightarrow -) \land (z = 0 \lhd u = v \rhd v \longleftrightarrow<EMAIL_ADDRESS>
reduces to

$$(\exists z R(u, z)) \land (z = 0 \lhd u = v \rhd R(v, z)))$$

The assertion ∃zR(u, z) clearly follows from the assumptions R = R1 R2 and (u → −)@R1 in Γ. To prove z = 0 u = vR(v, z), we first reduce the assumption (v → z)@(R2 ∨ ψ) to R2(v, z) ∨ (v = u ∧ z = 0). Now, if v = u then ¬R2(v, z), because of the assumptions *fun*(R), R = R1 R2 and (u → −)@R1. So we have that z = 0. Otherwise, we have R2(v, z), and thus R(v, z), because R = R1 R2.

*Soundness and Completeness.* We denote by Γ ⇒ Δ that there exists a proof of the sequent Γ ⇒ Δ. To define |= Γ ⇒ Δ, let σ denote a substitution which assigns to every binary relation symbol R of the sequent Γ ⇒ Δ a binary formula φ. Such a substitution σ simply replaces occurrences of R(t, t ) by φ(t, t ), where σ(R) = φ(x, y). By |= Γ ⇒ Δ we then denote that M,s |= - Γ σ (that is, M,s |= Aσ, for every A ∈ Γ) implies M,s |= Δσ (that is, M,s |= Bσ, for some B ∈ Δ), for every M,s and every substitution σ.

In the soundness proof below we use these substitutions to instantiate the fresh binary relation symbols introduced in the rules **L**∗ and **R**−∗. Note that updating the interpretation of these symbols (as provided by M) would affect the semantics of the separating connectives if binary formulas would refer to these fresh binary relation symbols (note that they are only supposed not to appear in formulas of the conclusion of the rules **L**∗ and **R**−∗).

We generalize the above notions of derivability and validity to possibly infinite Γ: Γ Δ indicates that Γ ⇒ Δ, for some finite Γ ⊆ Γ, and Γ |= Δ indicates that for every substitution σ we have that M,s |= Γ σ (that is, M,s |= Aσ, for every A ∈ Γ) implies M,s |= Bσ, for some B ∈ Δ.

**Theorem 1 (Soundness).** *We have that* Γ ⇒ Δ *implies* |= Γ ⇒ Δ*.*

*Proof.* We prove that the rules for the separating connectives preserve validity. The points-to rules are sound because M, *Rel*M(φ), s |= p if and only if M,s |= p[φ/ →], for any basic formula p (note that p[φ/ →] is a pure first-order formula which does not depend on the heap).

**L**∗: Let M,s |= Γ σ and M,s |= (pσ ∗ qσ)@φσ. We have to show that M,s |= Δσ. By Lemma 1, there exist φ1 and φ2 such that M,s |= (φσ) = φ1 φ2, M,s |= pσ@φ1, and M,s |= qσ@φ2. Let σ = σ[R1, R2 := φ1, φ2]. Since R1 and R2 are fresh and as such do not appear in Γ,(p ∗ q)@φ, it follows that M,s |= Γ σ , where Γ = Γ, φ = R1 R2, p@R1, q@R2. By the validity of the premise we thus obtain that M,s |= Δσ . Since R1 and R2 also do not appear in Δ, we conclude that M,s |= Δσ.

**R**∗: Let M,s |= Γ σ and suppose that M,s |= Δσ. From the validity of the premises it then follows that M,s |= φσ = (φ1 φ2)σ, M,s |= pσ@φ1σ, and M,s |= qσ@φ2σ, By Lemma 1 we conclude M,s |= (pσ ∗ qσ)@φσ.

**L**−∗: Let M,s |= Γ σ and M,s |= (pσ −∗ qσ)@φσ, and suppose that M,s |= Δσ. From the validity of the first two premises it then follows that M,s |= φσ ⊥ ψσ and M,s |= pσ@ψσ. By Lemma 1 again, it follows that M,s |= qσ@(φσ ∨ ψσ). By the validity of the third premise we thus derive that M,s |= Δσ, which a contradicts our assumption.

**R**−∗: Let M,s |= Γ σ and suppose that M,s |= Δσ. We have to show that M,s |= (pσ −∗ qσ)@φσ. Let ψ be such that M,s |= ψ ⊥ (φσ) and M,s |= pσ@ψ. Further, let R be a fresh variable and σ = s[R := ψ]. It follows that M,s |= Γ σ , where Γ = Γ, R ⊥ φ, p@R and M,s |= Δσ . And so we derive from the validity of the premise of the rule that M,s |= qσ@(φσ ∪ ψ). Since ψ was arbitrarily chosen, by Lemma 1 again we conclude that M,s |= (pσ −∗ qσ)@φσ.

As a corollary we obtain that Γ Δ implies Γ |= Δ.

Following the completeness proof of first-order logic as described in [Hen49], it suffices to show that every consistent set of formulas is satisfiable (the socalled 'model existence theorem'). A set of formulas Γ is consistent if Γ ∅. We first show that every consistent set of formulas can be extended to a maximal consistent set. To this end we assume an infinite set of 'fresh' binary relation symbols R that do not appear in Γ. We construct for any consistent set Γ a maximal consistent extension Γ ∞, assuming an enumeration of all formulas A (which also covers all first-order formulas). We define Γ0 = Γ and Γn+1 satisfies the general rule: if Γn, An ∅ then Γn ∪ {An} ⊆ Γn+1, otherwise Γn+1 = Γn. Additionally, in case An is added and An is of the form ∃xA or a rooted assertion (p ∗ q)@φ or ¬(p −∗ q)@φ, we also include corresponding *witnesses* in Γn+1:

– If An is of the form ∃xA we additionally add A(y), where A(y) results from replacing all free occurrences of x in A by the fresh variable y which does not appear in Γn.

Note that A(y) can indeed be added consistently because from Γn, A(y) ∅ we would derive Γn, ∃xA ∅, which contradicts the assumption that Γn, ∃xA ∅.

– If An is of the form (p ∗ q)@φ we additionally add the formulas φ = R1 R2, R1 ⊥ R2, p@R1, and q@R2, where R1 and R2 are fresh (e.g., not appearing in Γn).

Note that these formulas can indeed be added consistently because from Γn, φ = R1R2, R1 ⊥ R2, p@R1, q@R2 ∅ we would derive Γn,(p ∗ q)@φ ∅ (by rule **L**∗).

– If An is of the form ¬(p −∗ q)@φ (which is equivalent to ¬((p −∗ q)@φ)) we additionally add the formulas R ⊥ φ, p@R(x, y), and ¬q@(φ∨ R), where R is fresh (e.g., not appearing in Γn).

Note that these formulas can indeed be added consistently because from Γn, R ⊥ φ, p@R(x, y),¬q@(φ ∨ R) ∅ we would derive Γn (p −∗ q)@φ (by rule **R**−∗), which contradicts the assumption that Γn,¬(p −∗ q)@φ ∅.

We define Γ ∞ = n Γn. By construction Γ ∞ is maximal consistent. Given a maximal consistent set of formulas Γ, let MΓ = (D, I), where D is the set of equivalences classes [t] = {t | t = t ∈ Γ}. For any function symbol f and relation symbol R (excluding the points-to relation →) we define

– I(f)([t1],..., [tn]) = [f(t1,...,tn)], – I(R)([t1],..., [tn]) = **true** if and only if R(t1,...,tn) ∈ Γ.

The above interpretation of the function and relational symbols is welldefined because its definition does not depend on the choice of the representatives (this follows from the equality axioms).

Given a maximal consistent set of formulas Γ and the model MΓ = (D, I), a corresponding valuation s assigns to every variable x an equivalence class [t]. However, in the sequel we will represent such a valuation by a *substitution* s which simply assigns to each variable a term. The value Is(x) of a variable x then is given by the equivalence class [s(x)] of the term s(x).

Given a substitution s, for any term t and formula A (of the sequent calculus) we denote by ts and As the result of replacing every free occurrence of a (firstorder) variable x in t and A by s(x). Note that (p@φ)s = ps@φ, because the meaning of p@φ does not depend on the free variables x and y of the binary formula φ(x, y).

Given a maximal consistent set of formulas Γ and the model MΓ = (D, I), it follows that Is(t)=[ts], for every term t and substitution s.

**Lemma 2.** *Given a maximal consistent set of formulas* Γ *and the model* MΓ = (D, I)*, we have* M,s |= A *if and only if* As ∈ Γ*, for every formula* A *and substitution* s*.*

*Proof.* The proof proceeds by induction on the following well-founded ordering A<B on formulas of the sequent calculus: Let #A = (n, m), where n denotes the number of occurrences of the separating connectives and the @-binding operator of A and m denotes the number of occurrences of the (standard) first-order logical operations of A. Then A<B if #A < #B, where the latter denotes the lexicographical ordering on N × N (w.r.t. the standard 'smaller than' ordering on the natural numbers). We treat the following main cases (for notational convenience M denotes the model MΓ ).

– Let M,s |= A, where A denotes the formula (p ∗ q)@φ. By Lemma 1 there exist φ1 and φ2 such that M,s |= φ = φ1φ2, M,s |= p@φ1 and M,s |= q@φ2. From the induction hypothesis it follows that ps@φ1, qs@φ2, φ = φ1 φ2 ∈ Γ (note that the first-order formula φ = φ1 φ2 does not contain free variables, and thus is not affected by the substitution s). So we derive by rule **R**∗ that Γ (ps ∗ qs)@φ. By maximal consistency of Γ, we then conclude that (ps ∗ qs)@φ ∈ Γ, that is, As ∈ Γ.

On the other hand, let As ∈ Γ. That is, (ps ∗ qs)@φ ∈ Γ. By construction φ = R1 R2, ps@R1, qs@R2 ∈ Γ, for some witnesses R1 and R2. By the induction hypothesis it then follows that M,s |= p@R1 and M,s |= p@R2. Further, the induction hypothesis gives M,s |= φ = R1 R2 (again, note that the formula φ = R1 R2 has no free variables, and thus is not affected by the substitution s). We conclude by Lemma 1 that M,s |= (p ∗ q)@φ.

– Let M,s |= A, where A denotes the formula (p −∗ q)@φ. Suppose As ∈ Γ. By the maximal consistency of Γ, we then have ¬(ps −∗ qs)@φ ∈ Γ. By construction R ⊥ φ, ps@R,¬qs@(φ ∨ R) ∈ Γ, for some witness R, which contradicts M,s |= (p −∗ q)@φ (after application of the induction hypothesis and using Lemma 1 again).

On the other hand, let As ∈ Γ. To show that M,s |= (p −∗ q)@φ, let M,s |= φ ⊥ ψ and M,s |= p@ψ, for some binary formula ψ. By the induction hypothesis we have that φ ⊥ ψ, ps@ψ ∈ Γ. Suppose that qs@(φ∨ψ) ∈ Γ, that is ¬qs@(φ ∨ ψ) ∈ Γ (Γ is maximal consistent), and thus Γ, qs@(φ ∨ ψ) ∅. Applying rule **L**−∗ we then derive Γ,(ps −∗ qs)@φ ∅, which contradicts the consistency of Γ ((ps −∗ qs)@φ ∈ Γ). So we have that qs@(φ∨ψ) ∈ Γ, that is, M,s |= q@(φ ∨ ψ), by the induction hypothesis. Since ψ is chosen arbitrarily, it follows by Lemma 1 that M,s |= (p −∗ q)@φ.

– Let A be a formula p@φ, where p denotes a basic formula. Let R = *Rel*M(φ). We then have M,s |= p@φ iff (by definition) M, R, s |= p iff (straightforward induction on p) M,s |= p[φ/ →] iff (induction hypothesis for p[φ/ →]) ps[φ/ →] ∈ Γ iff (by the points-to rules) ps@φ ∈ Γ. Note that applying the substitution s to p@φ and p[φ/ →] results in ps@φ and ps[φ/ →].

The downward L¨owenheim-Skolem property follows. It should be noted that we cannot remove from the constructed model the binary relation symbols which are introduced as witnesses, as these determine the notion of first-order definability.

# **Theorem 2 (Completeness).** *We have that* Γ |= Δ *implies* Γ Δ*.*

Compactness follows. We thus derive (by Lindstr¨om's theorem [V¨a¨a10]) that this version of SL is as expressive as first-order logic.

#### **6 Conclusion**

We investigated the expressiveness of full SL over arbitrary first-order models. We have shown that restricting the quantification over first-order definable heaps gives rise to a semantic consequence relation that can be captured by a sound and complete extension of the standard sequent calculus for first-order logic.

The main question remains what is the exact relationship between full SL which allows for infinite heaps and second-order logic. In [KR04] a translation is given of general second-order logic in a first-order logic with *spatial conjunction*. Spatial conjunction (as defined in [KR04]) allows to split a global set of *arbitrary* relations. As such it goes beyond the *local* scope of separating conjunction which is restricted to the points-to relation. We conjecture that second-order logic is strictly more expressive than full SL.

**Acknowledgements.** The authors thank the anonymous referees for providing many constructive and useful suggestions for improvement.

## **References**

	- [CK13] Chang, C.C., Keisler, H.J.: Model Theory: Third Edition. Dover Books on Mathematics. Dover Publications (2013)
	- [DD16] Demri, S., Deters, M.: Expressive completeness of separation logic with two variables and no separating conjunction. ACM Trans. Comput. Log. **17**(2), 12 (2016)
	- [DLM21] Demri, S., Lozes, E., Mansutti, A.: A complete axiomatisation for ´ quantifier-free separation logic. Log. Methods Comput. Sci. **17**(3) (2021)
		- [EIP20] Echenim, M., Iosif, R., Peltier, N.: The Bernays-Sch¨onfinkel-Ramsey class of separation logic with uninterpreted predicates. ACM Trans. Comput. Log. **21**(3), 19:1–19:46 (2020)
		- [GM10] Galmiche, D., M´ery, D.: Tableaux and resource graphs for separation logic. J. Log. Comput. **20**(1), 189–231 (2010)
		- [Hen49] Henkin, L.: The completeness of the first-order functional calculus. J. Symb. Log. **14**(3), 159–166 (1949)
		- [Hen50] Henkin, L.: Completeness in the theory of types. J. Symb. Logic **15**(2), 81–91 (1950)
		- [HH14] Huet, G.P., Herbelin, H.: 30 years of research and development around Coq. In: Jagannathan, S., Sewell, P. (eds.) The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, San Diego, CA, USA, 20–21 January 2014, pp. 249– 250. ACM (2014)
		- [HT16] H´ou, Z., Tiu, A.: Completeness for a first-order abstract separation logic. In: Igarashi, A. (ed.) APLAS 2016. LNCS, vol. 10017, pp. 444–463. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47958-3 23
	- [JKJ+18] Jung, R., Krebbers, R., Jourdan, J.-H., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: a modular foundation for higher-order concurrent separation logic. J. Funct. Program. **28** (2018)
		- [KR04] Kuncak, V., Rinard, M.C.: On spatial conjunction as second-order logic. CoRR, cs.LO/0410073 (2004)
	- [V¨a¨a01] V¨a¨an¨anen, J.: Second-order logic and foundations of mathematics. Bull. Symb. Logic **7**(4), 504–520 (2001)
	- [V¨a¨a10] V¨a¨an¨anen, J.: Lindstr¨om's theorem. Universal Logic: An Anthology, pp. 231–236 (2010)
	- [Yan01] Yang, H.: Local reasoning for stateful programs. Ph.D. thesis, University of Illinois at Urbana-Champaign. (Technical Report UIUCDCS-R-2001- 2227) (2001)

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

# **Testing the Satisfiability of Formulas in Separation Logic with Permissions**

Nicolas Peltier(B)

Universit´e Grenoble Alpes, LIG, CNRS, Inria, Grenoble INP, 38000 Grenoble, France<EMAIL_ADDRESS>
**Abstract.** We investigate the satisfiability problem for a fragment of Separation Logic (SL) with inductively defined spatial predicates and permissions. We show that the problem is undecidable in general, but decidable under some restrictions on the rules defining the semantics of the spatial predicates. Furthermore, if the satisfiability of permission formulas can be tested in exponential time for the considered permission model then SL satisfiability is Exptime complete.

# **1 Introduction**

Separation Logic [14,22] (SL) is a dialect of bunched logic [18] that is widely used in verification for reasoning on programs manipulating pointer-based data structures. It constitutes the theoretical basis of several industrial scale automated static program analyzers [1,2,7]. SL formulas describe *heaps*, with atoms asserting that some location (i.e., a memory address) is allocated and refers to some tuple of locations (i.e., a record), combined with a special connective ∗, called *separating conjunction*, which is used to compose heaps. Custom data structures may be described in this setting by using spatial predicates, the semantics of which is defined using *inductive rules*, similar to those used for defining recursive structures in usual programming languages. Such rules allow one to describe heaps of unbounded size with some particular structure such as lists or trees. In this setting, existing work usually focuses on the fragment of SL called *symbolic heaps* (defined as separating conjunctions of SL atoms).

Usually, SL formulas are interpreted in the *standard heap model*, where heaps are defined as partial finite functions mapping locations to tuples of locations and where the separating conjunction ∗ is interpreted as the disjoint union of heaps. Both the satisfiability and entailment problems have been extensively investigated for this heap model. It was proven that the satisfiability problem is Exptime complete [6], whereas the entailment problem is undecidable in general, and 2-Exptime complete provided the inductive rules meet some syntactic conditions [11–13,15] which are general enough to capture usual data structures used in programming. The combination of spatial reasoning with theory reasoning has also been thoroughly investigated, see for instance [16,19–21,23]).

However, richer models exist (see for instance [8]) accounting for additional features of dynamic memory. The automation of reasoning in these models received little attention. One such model that is of practical relevance is *separation logic with permissions* [3,5], where allocated locations are associated with so called *permissions* used to model the ownership of a given heap region (e.g., a process may have read or write permission over some location). The heap composition operator that is used to define the interpretation of the separating conjunction is more complex in this framework than in the above case: non disjoint heaps can be combined if they agree on all the locations on which they are both defined and if the corresponding permissions can be combined (for instance it is natural to assume that read permissions can be freely combined but not write permissions). The framework is thus parameterized by some *permission model* describing which permissions are available and how they can be combined. In [10] algorithms are provided to decide the satisfiability and entailment problems for SL formulas (symbolic heaps) with permissions in the case of lists, i.e., when all allocated locations refer to a single location (i.e., to a record of size 1) and when there is only one spatial predicate lsegp(x, y) denoting a list segment from x to y, with permission p. The provided algorithms are generic w.r.t. the permission model, and it is proven that these problems are in Np and co-Np, respectively, assuming that some oracle exists for testing the satisfiability of permission formulas in the considered model.

In the present paper, we investigate the satisfiability problem for SL formulas with permission defined over arbitrary spatial predicates, with user-defined inductive rules. The goal is to allow for more genericity by tackling custom data structures (such as trees, cyclic lists, doubly linked lists etc.) with arbitrary permissions. The addition of permissions makes satisfiability testing much more difficult: we prove that the problem is undecidable in general, and we devise syntactic conditions on the inductive rules for which the problem is Exptimecomplete. The restrictions are similar – but stronger – to those given in [13] to ensure the decidability of the entailment problem in the standard heap model. In particular, the inductive rules defining the predicate lseg mentioned above fulfill these restrictions1, as well as other usual data structures such as cyclic list, trees etc. (however, doubly linked lists or trees with parent links are not captured). The considered inductive rules use a special connective ◦ (different from ∗) that is interpreted as a disjoint union. As we shall see, this is both more natural for defining data structures (see also [5]) and required for deciding satisfiability.

# **2 Definitions**

*Syntax.* We first briefly review some basic notations. If x and y are finite sequences, then we denote by x.y the concatenation of x and y. We denote by |x| the length of x and by x|i its i-th element (if 1 ≤ i ≤ |x|). If E ⊆ {1,..., |x|} then x|E denotes the set {x|i | i ∈ E}. With a slight abuse of notations, a finite

1 provided the considered lists are not empty.

sequence x is sometimes identified with the set {x|i | i = 1,..., |x|}, for instance, we may write x ∈ (u ∪ v) \ w to state that x occurs in u or v but not in w.

We consider a multisorted framework, with two sorts l (for locations) and p (for permissions). Let Vl and Vp be two countably infinite disjoint sets of *variables* with V def = Vl ∪ Vp, where Vl and Vp denote location variables and permission variables, respectively. The set of *permission terms* Tp denotes the set of terms built inductively as usual on the set of variables Vp and the binary function ⊕ (written in infix notation). A *points-to atom* is an expression of the form x p → (y1,...,yk) with x, y1,...,yk ∈ Vl and p ∈ Tp. An *equational atom* is an expression of the form x y or x  y with either x, y ∈ Vl or x, y ∈ Tp.

We consider two disjoint sets of predicate symbols Pp and P. The set Pp denotes *permission predicates*, where each predicate Pˆ ∈ Pp is associated with a unique arity #(Pˆ). A *permission atom* is an expression of the form Pˆ(p1,...,pn), Pˆ ∈ Pp, n = #(Pˆ) and p1,...,pn ∈ Tp. P is a finite set of *spatial predicate symbols*. Each symbol P ∈ P is associated with a *spatial arity* #l(P) ∈ N and with an *arity* #(P) ∈ N, with #(P) > #l(P) > 0 (#l(P) and #(P) − #l(P) denote the number of arguments of P that are of sort l and p, respectively). A *predicate atom* is an expression of the form P(x1,...,xn, p1,...,pm), with n = #l(P), n + m = #(P), x1,...,xn ∈ Vl and p1,...,pm ∈ Tp. A *spatial atom* is either a points-to atom or a predicate atom.

The set of *formulas* is built inductively as usual on the logical constants emp, and ⊥ and on the set of spatial, equational and permission atoms, using the special connectives ∗ and ◦ and existential quantification on variables of sort l only (existential quantification over variables of type p is not allowed). The connective ∗ is usually called *separating conjunction*, and we call ◦ the *disjoint conjunction* (it is intended to capture the disjoint union of heaps2). Formulas are taken up to associativity and commutativity of the symbols ∗ and ◦, up to the commutativity of ,  and up to prenex form. We denote by |φ| the size of φ. For technical convenience, we assume that the symbols ◦ and ∗ have weight of 1 and 2, respectively, and that all atoms have size 1. For conciseness, a formula ∃x1 ... ∃xn φ will often be written ∃x φ, with x = (x1,...,xn). A *permission formula* is a formula containing no spatial atoms and no equational atom of the form x y or x y with x, y ∈ Vl (note that emp is a permission formula). A formula is *spatial* if all the atoms occurring in it are spatial. A *pure formula* is a formula that contains no spatial atom (it is not necessarily a permission formula, as it may contain equations or disequations between locations) A *symbolic heap* is a formula containing no occurrence of ◦, and a ◦*-formula* is a formula containing no occurrence of ∗.

A variable x is *free* in a formula φ if it occurs in φ outside of the scope of any quantifier binding x. The set of variables (freely) occurring in a term (or formula) φ is denoted by *fv*(φ). A *substitution* is a function mapping every variable in Vl to a variable in Vl and every variable in Vp to a term in Tp.

2 The connective ◦ is called *strong separating conjunction* in [5] and written ∗ (whereas ∗ is written ∗ ). Our notations are mostly consistent with those in [10].

The *domain* of a substitution σ (denoted by *dom*(σ)) is the set of variables x such that σ(x) = x. A substitution of domain {x1,...,xn} with σ(xi) = ti is denoted by {xi ← ti | i = 1,...,n}, or {x ← t}, with x = (x1,...,xn) and t = (t1,...,tn). For all formulas or terms φ, we denote by φσ the formula or term obtained from φ by replacing every free occurrence of a variable x by σ(x).

*Semantics.* Permissions are interpreted in some permission model:

#### **Definition 1 (Adapted from** [10]**).** *A* permission model P *is a triple*

$$(\mathcal{P}\_{\mathfrak{P}}, \oplus \mathfrak{p}, (\hat{P}\_{\mathfrak{P}})\_{\hat{P} \in \mathcal{P}\_{\mathfrak{p}}})$$

*where* PP *is a non empty set, called the set of* permissions*,* ⊕P : P2 P → PP *is a binary partial function that is commutative, associative and cancellative, and* PˆP ⊆ P#(Pˆ) P *, for all* Pˆ ∈ Pp*. If* π, π ∈ PP*, we write* π ≤P π *if* π = π ∨ (∃π ∈ PP π = π ⊕ π)*.*

In what follows, P always denotes a permission model. If π ∈ PP and n ∈ N, we denote by πn the permission π ⊕P ... ⊕P π (n times), note that πn is not necessarily defined and implicitly depends on the considered permission model, which will always be clear from the context. In contrast to [10], we do not assume that a maximal "total" permission 1P exists, we allow instead for arbitrary predicates over permissions (the total permission can be encoded as a unary predicate symbol *T*, with *T*P = {1P}).

*Example 2.* Assume that Pp = ∅. A simple example of permission model is w = ({read, write}, ⊕w, ∅), with read ⊕w read = read and write⊕w π is undefined for all π ∈ {read, write}. Another example (from [4]) is f = (]0, 1], ⊕f, ∅) where ]0, 1] denotes the interval of rational numbers, with π ⊕f π = π +π if π +π ≤ 1 and π ⊕f π is undefined otherwise (f stands for *fractional*).

Let L be a countably infinite set of *locations*. A *store* (for a given permission model P) is a total mapping associating every variable in Vl to an element of L and every variable in Vp to an element of PP. A store can be extended into a partial mapping from Tp to PP inductively defined as follows: s(p1 ⊕ p2) def = s(p1) ⊕P s(p2). Note that the obtained mapping is partial since s(p1) ⊕P s(p2) is not always defined. If x1,...,xn are pairwise distinct variables in Vl and 1,...,n ∈ L, we denote by s{xi ← i | i = 1,...,n} the store s coinciding with s on every variable not occurring in {x1,...,xn} and such that s (xi) = i for all i = 1,...,n.

A *heap* (for a given permission model P) is a partial finite function from L to L∗ × PP. The domain of a heap h is denoted by *dom*(h), and we denote by |h| the finite cardinality of *dom*(h). A heap of domain 1,...,n such that h(i)=(i 1,...,i k*i* , πi) (for all i ∈ {1,...,n}) will be denoted as a set {(i, i 1,...,i k*i* , πi) | i = 1,...,n}. For every heap h we denote by *loc*(h) the set {i | 0 ∈ *dom*(h), h(0)=(1,...,k, π), 0 ≤ i ≤ k}. A heap may be viewed as a directed (labeled) graph: the locations in *loc*(h) are the vertices of the graph and there is a edge from to if h()=(1,...,n, π) and = i for some i ∈ {1,...,n}.

A *subheap* of h is any heap h such that *dom*(h ) ⊆ *dom*(h) and h () = h() for all ∈ *dom*(h ). A p*-weakening* of h (w.r.t. some permission model P) is any heap h such that *dom*(h ) = *dom*(h) and for all ∈ *dom*(h), if h()=(1,...,n, π) then h ()=(1,...,n, π ) with π ≤P π. We write h ≤l h (resp. h ≤p h) if h is a subheap (resp. a p-weakening) of h. The relation ≤ denotes the composition of ≤l and ≤p. We write h ∼ h if h and h only differ by the permissions, i.e., *dom*(h) = *dom*(h ) and for all ∈ *dom*(h), if h ()=(1,...,n, π ) then there exists π such that h()=(1,...,n, π).

*Example 3.* Consider the permission model f defined in Example 2 with L = N. Then

h0 = {(0, 0, 1, 0.1),(1, 0, 0, 0.2)}, h1 = {(0, 0, 1, 0.1)}, h2 = {(0, 0, 1, 0.1),(1, 0, 0, 0.1)} h3 = {(1, 0, 0, 0.1)}

are heaps, and we have, e.g., h0(0) = (0, 1, 0.1) (meaning that the location 0 is allocated and refers to (0, 1), with permission 0.1), h1 ≤l h0, h2 ≤p h0, h3 ≤l h2, and h3 ≤ h0. Moreover, h0 ∼ h2.

Heaps can be composed using the following partial operator. If h1, h2 are heaps, then h1 h2 is defined iff for all ∈ *dom*(h1) ∩ *dom*(h2), we have hi() = (i 1,...,i k*i* , πi) (for all i = 1, 2) where k1 = k2, 1 j = 2 j for all j ∈ {1,...,k1} and π1 ⊕P π2 is defined. Then h1 h2 is defined as follows: if ∈ *dom*(hi) \ *dom*(hj ) with (i, j) ∈ {(1, 2),(2, 1)} then (h1h2)() def = hi(), and if ∈ *dom*(h1)∩*dom*(h2) then (h1 h2)() def = (1 1,...,1 k1 , π1 ⊕P π2).

*Example 4.* Consider the permission model f defined in Example 2, with L = N and the following heaps:

$$\begin{array}{ll} \mathfrak{h}\_0 = \{ (0,0,0.5), (1,0,0.6) \} & \mathfrak{h}\_1 = \{ (0,0,0.5), (1,0,0.2), (2,0.1) \} \\ \mathfrak{h}\_2 = \{ (0,0,0.5), (1,0,0.6) \} & \mathfrak{h}\_3 = \{ (0,0,0.1), (1,0.1) \} \end{array}$$

Then h0 h1 is defined, and we have: h0 h1 = {(0, 0, 1),(1, 0, 0.8),(2, 0.1)}. However, neither h0h2 nor h0h3 is defined (in the former case the permissions of location 1 cannot be combined (as 0.6+0.6 > 1) and in the latter case the location 1 is associated with distinct tuples, (0) and (), respectively.

A *structure* (for a given permission model P) is a pair (s, h) where s is a store and h is a heap for P. It is *injective* if s is injective. A location is *allocated* in a structure (s, h) or in a heap h if ∈ *dom*(h), and a variable x is *allocated* in (s, h) if s(x) ∈ *dom*(h).

The semantics of spatial predicate is defined by inductive rules. A *set of inductive definitions* (SID) is a set of *rules* of the form P(x1,...,xn, y1,...,ym) ⇐ φ where n = #l(P), n+m = #(P), x1,...,xn are pairwise distinct variables in Vl, y1,...,ym are pairwise distinct variables in Vp, and φ is a formula such that *fv*(φ) ⊆ {x1,...,xn, y1,...,ym}. We write P(z1,...,zn, p1,...,pm) ⇐R ψ iff R contains a rule P(x1,...,xn, y1,...,ym) ⇐ φ with ψ = φ{xi ← zi, yj ← pj | i ∈ {1,...,n}, j ∈ {1,...,m}}.

**Definition 5.** *(Semantics) For every permission model* P *and SID* R*, the satisfiability relation* |=P R *is the smallest relation between structures (for* P*) and formulas such that:*

*A structure* (s, h) *such that* (s, h) |=P R φ *is an* (R, P)-model *of* φ*. A formula admitting an* (R, P)*-model is* (R, P)-satisfiable*. Two formulas are* sat-equivalent *(w.r.t.* R*,* P*) if they are both* (R, P)*-satisfiable or both* (R, P)*-unsatisfiable.*

*Example 6.* The formula x u → (y, z) ◦ x u- → (y , z ) is (R, P)-unsatisfiable, as x cannot be allocated in disjoint parts of the heap. x u → (y) ∗ x u- → (y ) ∗ y  y is also (R, P)-unsatisfiable, as x cannot refer to two distinct records, but x u → (y, z) ∗ x u- → (y , z ) admits the model (on the permission model f) (s, h) with s(x) = 0, s(y) = s(y ) = 1, s(z) = s(z ) = 2, s(u)=0.5, s(u )=0.2 and h = {(0, 1, 2, 0.7)}.

Note that there is no logical constant (true): no formula can be satisfied on all heaps. The constant emp is similar to but it states that the heap is empty. For all formulas φ, ψ, we write φ |=P R ψ iff the implication (s, h) |=P R φ =⇒ (s, h) |=P R ψ holds for all structures (s, h), and φ ≡P R ψ iff we have both φ |=P R ψ and ψ |=P R φ. If φ contains no predicate symbols in P, then the truth value of φ in (s, h) does not depend on R. We thus may write (s, h) |=P φ instead of (s, h) |=P R φ. If, moreover, φ is pure, then (s, h) |=P φ holds only if h is empty. We will write s |=P φ to state that (s, ∅) |=P φ. Finally, if φ contains only equalities between variables then its semantics does not depend on R and P thus we write s |= φ to state that (s, ∅) |=P R φ. Note that the semantics of φ1 ◦ φ2 and φ1 ∗ φ2 coincide if φ1 or φ2 is pure, and also coincide with that of the usual standard conjunction if *both* φ1 and φ2 are pure.

*Shorthands.* If x = (x1,...,xn) and y = (y1,...,ym) are sequences of variables in Vl then x y denotes the formula ⊥ if n = m and (x1 y1) ◦ ... ◦(xn yn) otherwise. For every permission term p, we denote by *def* (p) the atom p p. By definition, (s, h) |=P R *def* (p) iff s(p) is defined and h = ∅.

#### **3 h-Regular Systems**

We focus on SIDs of some particular form, defined below.

**Definition 7.** *A rule is* h-regular *if it is of the following form:*

$$P(x, \mathfrak{y}) \Leftarrow \exists u\_1, \ldots, u\_n \left(x \overset{p}{\leftrightarrow} (v\_1, \ldots, v\_k) \circ Q\_1(u\_1, \mathfrak{y}\_1) \ldots \circ Q\_n(u\_n, \mathfrak{y}\_n) \circ \phi\right)$$

*where* {u1,...,un}⊆{v1,...,vk}*,* yi *is a vector of variables*3*,* Qi ∈ P *and* φ *is pure. We assume by* α*-renaming that* x,y *do not occur in* {u1,...,un}*. A SID* R *is* h-regular *if all the rules in* R *are* h*-regular.*

Note that the right-hand side formula contains only the disjoint separation connective ◦ and not the usual separating conjunction ∗. As we will see (Theorem 33) this is crucial for the decidability of the satisfiability problem. However, as already observed in [5], this is also justified from a practical point of view. Assume for instance that we want to define the predicate lseg introduced in [10], denoting a list segment from x to y with some permission z. The following rules can be used4: lseg(x, y, z) ⇐ x z → (y) lseg(x, y, z) ⇐ ∃u (x z → (u) ◦ lseg(u, y, z)). A structure (s, h) satisfies lseg(x, y, z) if h = {(i, i+1, s(z)) | i = 1,...,n} with n > 0, s(x) = 1, s(y) = n+1 and i = j if i = j and i, j ∈ {1,...,n}. This fits in with the definition in [10] (except that n > 0). In contrast, if one uses instead the connective ∗: lseg(x, y, z) ⇐ ∃u (x z → (u) ∗ lseg(u, y, z)), then one could obtain models where the list "loops" on itself an arbitrary number of times, such as, for instance (s, {(s(x), s(x), p))}), with s(y) = s(x) and p = s(z)n, for any n > 0 such that s(z)n is defined. In the former definition, s(y) possibly occurs in {1,...,n}, but each location can only be allocated once.

Intuitively, h-regular sets of inductive rules generate heaps with a regular structure (in the sense that it may be represented by a tree automaton [9]), enriched with some additional edges (referring to the nodes corresponding to the variables passed as parameters to the spatial predicates at some recursive calls). These additional edges may refer to locations corresponding to free variables (e.g. the root of the structure) but also to existential variables (for instance they may refer to the parent node in the tree). h-Regular SID are related to the Pce systems introduced in [13] (for **p**rogressing, **c**onnected and **e**stablished), extended to formulas with permissions, but our conditions are slightly stronger, because we require that every existential variable be allocated at the next recursive call. Note that structures with mixed permissions are allowed, for instance

3 i.e., compound permission terms are not allowed in predicate atoms.

4 As h-regular rules allocate exactly one location, we assume that the segment is non empty, the case of an empty segment must be considered apart.

the rules P(x, z1, z2) ⇐ x z1 → () and P(x, z1, z2) ⇐ ∃u (x z1 → (u) ◦ P(u, z2, z1)) defines a list with permissions alternating between z1 and z2. Rules with compound permission terms in points-to or permission atoms are allowed (such as P(x, y1, y2) ⇐ x y1⊕y2 → () ◦ *def* (y1 ⊕ y1)), but not those with compound permission terms in spatial predicate atoms5 (e.g., P(x, y1, y2) ⇐ x y1 → () ◦ Q(x, y1 ⊕y2) is *not* h-regular).

For every quantifier-free formula φ, we denote by *roots*(φ) the set of variables x (called the *roots of* φ) inductively defined as follows: *roots*(x p → (y1,...,yk)) def = {x}, *roots*(P(x, y1,...,yk)) def = {x}, *roots*(∃y φ) = *roots*(φ)\{y}, *roots*(φ) = ∅ if φ is pure and *roots*(φ1 ∗φ2) = *roots*(φ1 ◦ φ2) = *roots*(φ1)∪*roots*(φ2). By Definition 7, roots are always allocated:

**Proposition 8.** *Let* R *be a* h*-regular SID. If* (s, h) |=P R φ *and* x ∈ *roots*(φ) *then* s(x) ∈ *dom*(h)*. Consequently, every formula of the form* φ1 ◦ φ2 *with roots*(φ1)∩ *roots*(φ2) = ∅ *is* (R, P)*-unsatisfiable.*

The conditions in Definition 7 are actually not sufficient to ensure that the satisfiability problem is decidable:

**Theorem 9.** *If there exist (not necessary distinct) permissions* π1, π2 ∈ PP *such that* π1⊕Pπ2 *is defined, then the* (R, P)*-satisfiability problem is undecidable for* h*-regular SID* R*.*

To ensure decidability, we need to further restrict the way existential variables are passed as parameters during recursive calls. This is the goal of the next definition.

**Definition 10.** *Assume that* R *is* h*-regular. Given two spatial predicates* P *and* Q*, of arities* n *and* m *respectively, we write* P R Q *if* P(x, x1,...,xn−1) ∗ Q(x, y1,...,ym−1) *is* (R, P)*-unsatisfiable*6 *(where* x1,...,xn−1, y1,...,ym−1 *denote pairwise distinct variables of the appropriate sorts). We denote by* γR *the function associating every predicate symbol* P *of spatial arity* n *to a subset of* {2,...,n} *inductively defined as follows: for every rule* P(x1,...,xn, u) ⇐ ∃y1,...,ym φ *in* R*, for every predicate atom* Q(z1,...,zk, uk) *in* φ *with* #l(Q) = k *and for all* i ∈ {2,...,k}*:*

*1.* zi ∈ {y1,...,ym} ⇒ i ∈ γR(Q)*. 2.* zi ∈ {xj | j ∈ γR(P)} =⇒ i ∈ γR(Q)*.*

5 Otherwise the unfolding of spatial predicates could yield terms of arbitrary depth.

6 In practice, as this condition is hard to test, some stronger syntactic condition can be tested instead, for instance one can check that all the formulas φ and φ such that P(x, x1,...,x*n*−1) ⇐R φ and Q(x, y1,...,y*m*−1) ⇐R φ are of the form φ = (x → (u) ◦ ψ) and φ- = (x → (u- ) ◦ ψ- ) with |u| = |u- | (this condition is used in Theorem 33 and for the Exptime-hardness proof in Theorem 32.). More generally, it is sufficient to test that the "shape" of the structures generated by P and Q, up to a certain fixed unfolding depth, are incompatible.

*Let* P *be a subset of* P*, such that: (3)* P ∈ P- =⇒ γR(P) = ∅*; and (4)* P ∈ P- ∧ Q ∈P\P- =⇒ P R Q*. A* h*-regular rule is* ∃-restricted *(w.r.t.* R *and* P-*) if it satisfies the following condition (using the notations of Definition 7):*

*5.* ∀i ∈ {1,...,n} ∀j ∈ {1,...,n} (ui ∈ yj =⇒ Qi ∈ P-)*.*

*A SID* R *is* ∃-restricted *if all the rules in* R *are* ∃*-restricted.*

Conditions 1 and 2 in Definition 10 are meant to ensure that γR(P) denotes the indices of the parameters of P that may (but do not have to) be instantiated by some existential variable introduced during the unfolding of the inductive rules in R (the other parameters may only be instantiated by variables occurring in the initial formula). Condition 1 corresponds to a base case, where an existential variable is passed as a parameter to a predicate symbol, and Condition 2 handles the inductive case, when the variable is carried through recursive calls7. Then, Condition 5 ensures that an existential variable may only be passed as a parameter to a predicate symbol if it is the root of a structure defined by an atom Qi(yi) containing no variables introduced by unfolding (by Condition 3).

*Example 11.* The rules of the predicate lseg are ∃-restricted (with P- = ∅). Indeed, they contain only one existential variable u, which occurs only as the first argument of a predicate. Hence Condition 5 in Definition 10 trivially holds. If R contains no other rule then γR(lseg) = ∅. Note that γR(lseg) depends on the entire set R. For instance, if R contains a rule P(x, y) ⇐ ∃u (x y → (u) ◦ lseg(u, u, y)) then the second argument of lseg may be instantiated by an existential variable hence γR(lseg) = {2}, and the latter rule is not ∃ restricted. On the other hand, if P- = {Q}, then the rules Q(x, y) ⇐ x y → (), R(x, y) ⇐ ∃u, v (x y → (u, v) ◦ lseg(u, v, y) ◦ Q(v, y)) are ∃-restricted, with P- = {Q}. Indeed, the variable u occurs only at the root of a predicate, and the variable v is the root of Q(v, y). Note that lseg(x, y, z) ∗ Q(x, u) and R(x, y) ∗ Q(x, u) are (R, P)-unsatisfiable, thus lseg R Q and R R Q.

Intuitively, the structures generated by ∃-restricted rules are regular treeshaped structures, enriched with two kinds of additional edges: (i) a *bounded* number of *arbitrary* edges (corresponding to free variables, which may be freely passed as arguments to any predicate, thus may be referred to in an arbitrary way); (ii) an *unbounded* number of other edges (corresponding to existential variables) which are only allowed to point to structures that contain no edge of type (ii). Condition 4 ensures that the structures containing only edges of type (i) do not overlap with those containing both kinds of edges. Note that the conditions of Definition 10 always hold if the existential variables occur only

7 For generality, one could assume that all the equalities occurring in the rules are propagated before γR is computed (so that existential variables are eliminated if they are equal to a free variable), but this is not essential for our purposes hence the corresponding formal definitions are omitted.

as roots (with P- = P or P- = ∅). In this case there is no edge of type (ii), i.e., the obtained structures are regular sets of trees with a bounded number of additional edges (for instance trees with pointers to the root, or cyclic lists). Note that doubly linked lists cannot be captured (as they contain an unbounded number of additional edges from every node to the previous one). In the following we devise an algorithm to test the (R, P)-satisfiability of symbolic heaps when R is ∃-restricted.

# **4 A Decision Procedure for Testing Satisfiability**

Before entering into technical details we start with a general overview of the procedure for testing satisfiability (assuming the considered SID is ∃-restricted).

In the next subsections, each of these steps is explained in details.

#### **4.1 Normalization**

We first show that every formula can be transformed into an equivalent formula (that we call *normalized*) in which every allocated variable occurs as a root:

**Definition 12.** *A formula* φ *is* normalized *if it is of the form* ∃x ψ *where* ψ *is quantifier-free and for all spatial atoms* δ *in* ψ*, for all* (R, P)*-models* (s, h) *of* δ *and for all variables* y ∈ *fv*(ψ)*:* s(y) ∈ *dom*(h) ⇐⇒ y ∈ *roots*(ψ)*.*

For instance, lseg(x, y) is not normalized, because y may be allocated (e.g., if s(x) = s(y)) and does not occur in *roots*(lseg(x, y)) = {x}. To enforce this condition, we introduce new predicate symbols (called *derived predicates*), the rules of which can be automatically computed from those of the predicates already occurring in this formula. We first define predicate symbols that ensure that some given variable is not allocated.

**Definition 13.** *For all predicate atoms* P(x, p) *(where* x *and* p *are vectors of location variables and permission terms, respectively) and for all location variables* v*, we denote by* P(x, p)[v] − *any atom of the form* Q(x, v, p)*, where* Q *is a fresh predicate symbol, associated with the rules:*

$$Q(\mathfrak{y}, w, \mathfrak{z}) \Leftarrow \exists \mathfrak{u} \left( Q\_1(\mathfrak{y}\_1, \mathfrak{p}\_1)[w]^- \circ \dots \circ Q\_m(\mathfrak{y}\_m, \mathfrak{p}\_m)[w]^- \circ \phi \circ \mathfrak{y}|\_1 \not\simeq w \right)$$

*for all rules* P(y,z) ⇐ ∃u (Q1(y1, p1) ◦ ... ◦ Qm(ym, pm) ◦ φ) *in* R *(up to AC), where* y,yi *are vectors of location variables,* z*,* pi *are vectors of permission variables, and* φ *contains no predicate atom.*

For instance lseg(x, y, z)[u] − is a predicate atom Q(x, y, u, z) defined by the following rules: {Q(x, y, u, z) ⇐ ∃x (x z → (x ) ◦ Q(x , y, u, z) ◦ x  u), Q(x, y, u, z) ⇐ x z → (y) ◦ x  u}. It denotes a list segment from x to y not allocating u. The following result is straightforward to prove:

**Proposition 14.** *For every* ∃*-restricted SID* R*, the set* R *enriched with the rules associated with the predicate* Q *corresponding to* P(x, p)[v] − *in Definition 13 is* ∃*-restricted, with* γR(Q) = γR(P) *and* Q ∈ P- ⇐⇒ P ∈ P-*.*

Intuitively the structures that satisfy P(x, p)[v] − are exactly those that satisfy P(x, p) and do not allocate v:

**Lemma 15.** *For all* h*-regular SID* R*,* (s, h) |=P R P(x, p)[v] − *iff* (s, h) |=P R P(x, p) *and* s(v) ∈ *dom*(h)*.*

The operator δ → δ[x] − can be applied recursively, e.g., one can consider atoms of the form δ[x] −[y] −, etc. For all predicate atoms δ, we denote by *unalloc*(δ) the set of variables inductively defined as follows: *unalloc*(δ[x] −) def = {x}∪*unalloc*(δ), and *unalloc*(δ) def = ∅ if δ is not of the form δ [x] −. The following proposition is an immediate consequence of Lemma 15:

**Proposition 16.** *If* (s, h) |=P R δ *then* s(x) ∈ *dom*(h)*, for all* x ∈ *unalloc*(δ)*.*

Next, we define predicate symbols allowing one to remove some part of a structure. Intuitively, the expression (φ −−• ψ) will hold exactly in the structures that satisfy ψ when a disjoint structure satisfying φ is added. For instance given the rules tree(x, y) ⇐ ∃x1, x2 x y → (x1, x2) ◦ tree(x1, y) ◦ tree(x2, y) and tree(x, y) ⇐ x y → (), tree(z,y) and tree(x, y) denote binary trees with roots z and x, respectively, and tree(z,y) −−• tree(x, y) denotes a tree of root x with a "hole" at z (the structures satisfying tree(z,y) −−• tree(x, y) are obtained from models of tree(x, y) by removing the part of the heap that corresponds to tree(z,y)). The formula φ −−• ψ is similar to the *strong magic wand* introduced in [17] and to the *context predicates* in [12] and also close in spirit to the separating implication of SL although the semantics are slightly different.

**Definition 17.** *For all finite sequences of predicate atoms* Pi(xi, pi) *(with* i = 0,...,n*), where* xi *and* pi *are vectors of location variables and permission terms, respectively, we denote by* (P1(x1, p1) ◦ ... ◦ Pˆn(xn, pn)) −−• P0(x0, p0) *any atom* P(x, p) *with* x = x0. . . . .xn*,* p = p0. . . . .pn*, and such that* P = P0 *if* n = 0 *and otherwise* P *is a fresh symbol associated with rules of the form*

$$P(\mathfrak{y}, \mathfrak{z}) \Leftarrow \exists \mathfrak{w} \left(\psi\_1 \circ \ldots \circ \psi\_m \circ \phi\right)$$

*for all rules*

$$P\_0(\mathfrak{y}\_0, \mathfrak{z}\_0) \Leftarrow \exists w \left( Q\_1(\mathfrak{u}\_1, \mathfrak{q}\_1) \circ \dots \circ Q\_m(\mathfrak{u}\_m, \mathfrak{q}\_m) \circ \phi \right)$$

*in* R *and for all decompositions* α1 ◦ ... ◦ αm = P1(y1, z1) ◦ ... ◦ Pn(yn, zn) *(up to AC, where the* αi*'s may be empty), where:*

	- *either* αi −−• Qi(ui, qi)*;*
	- *or* yj ui ◦z j qi*, if* αi = Pj (yj , z j ) *and* Pj = Qi*.*

For instance tree(z,y) −−• tree(x, y) denotes an atom P(x, z, y, y) with the rules:

$$\begin{split} P(x,z,y\_{1},y\_{2}) &\Leftarrow \exists x\_{1},x\_{2} \; (x \xhookrightarrow{y\_{1}} (x\_{1},x\_{2}) \diamond P(x\_{1},z,y\_{1},y\_{2}) \circ \mathtt{true}(x\_{2},z,y\_{1})) \\ P(x,z,y\_{1},y\_{2}) &\Leftarrow \exists x\_{1},x\_{2} \; (x \xhookrightarrow{y\_{1}} (x\_{1},x\_{2}) \diamond \mathtt{true}(x\_{1},z,y\_{1}) \diamond P(x\_{2},z,y\_{1},y\_{2})) \\ P(x,z,y\_{1},y\_{2}) &\Leftarrow \exists x\_{1},x\_{2} \; (x \xhookrightarrow{y\_{1}} (x\_{1},x\_{2}) \diamond x\_{1} \simeq z \circ y\_{1} \simeq y\_{2} \circ \mathtt{true}(x\_{2},z,y\_{1})) \\ P(x,z,y\_{1},y\_{2}) &\Leftarrow \exists x\_{1},x\_{2} \; (x \xhookrightarrow{y\_{1}} (x\_{1},x\_{2}) \diamond \mathtt{true}(x\_{1},z,y\_{1}) \diamond x\_{2} \simeq z \circ y\_{1} \simeq y\_{2}) \end{split}$$

For readability, all the expressions of the form emp −−• tree(x2, z,y1) have been replaced by tree(x2, z,y1). Note that the rules are not h-regular, as x1 and x2 do not occur as roots in every rule, but they can easily be transformed into h-regular rules by replacing x1 and x2 by z in the third and fourth rule, respectively (using the equations x1 z and x2 z). The definition can be applied recursively (i.e., P0,...,Pn may be derived predicates). The next proposition is an immediate consequence of Definition 17:

**Proposition 18.** *Let* R *be a* h*-regular SID. The rules associated with any predicate* P *corresponding to an expression* α −−• δ *(Definition 17) are* h*-regular, up to the following equivalence:* ∃x (x y ◦ φ) ≡P R φ{x ← y}*. Moreover, the rules are also* ∃*-restricted, with* γR(P) = γR(P0) *and* P ∈ P- ⇐⇒ P0 ∈ P-*. Finally if* α = emp *then* (α −−• δ) = δ*.*

Note that, however, the implication P ∈ P- ∧ Q ∈ P\P- =⇒ P R Q (Condition 4 in Definition 10) does *not* necessarily hold for derived predicates P, Q. The following lemma states a form of modus ponens, relating the connective ◦ with −−•:

**Lemma 19.** *If* R *is* h*-regular then* P(x, p) ◦((P(x, p) ◦ α) −−• Q(y,q)) |=P R α −−• Q(y,q)*.*

The next lemma states that every predicate atom allocating x can be written as a ◦-formula in which x occurs as a root.

**Lemma 20.** *Assume that* R *is* ∃*-restricted. Let* y,p *be vectors of location variables and permission terms, respectively. If* (s, h) |=P R Q(y,p)*,* s(x) = s(y|1) *and* s(x) ∈ *dom*(h)*, then there exist atoms of the form* P(x, z,q)*,* Pi(xi,yi, qi) *(with* i ∈ {1,...,n}*), where* z ⊆ y ∪ {x1,...,xn}*,* yi ⊆ {y|j | j ∈ γR(Q)}*,* q ⊆ p *and* qi ⊆ p*, such that:* (s, h) |=P R ∃x1,...,xn (β ◦(β −−• Q(y,p)))*, with* β = P(x, z,q) ◦ m i=1Pi(xi,yi, qi)*. Moreover,* Pi ∈ P-*,* {x1,...,xn} ⊆ (x, z)|γR(P ) *and* y ∈ y ∩ z ∧ y ∈ {y|j | j ∈ γR(Q)} =⇒ y ∈ (x, z)|γR(P )*.*

Intuitively, since x is allocated and the rules are h-regular, then necessarily some predicate atom of the form P(x, z,q) must be called at some point during the unfolding of the rules. Using −−•, this predicate can be removed from the call tree of Q(y,p) and lifted at the root level in the formula. The atom P(x, z,q) may contain variables not occurring in Q(y,p) corresponding to existential variables introduced by unfolding. As the rules are ∃-restricted, all such variables xi must themselves appear as the root of some predicate atom Pi(xi,yi, qi) which contains (beside xi) only variables occurring in Q(y,p) (since γR(Pi) = ∅, due to Condition 5 in Definition 10). Again, these atoms can be moved at the root level.

**Definition 21.** *For all atoms* Q(y,p) *we denote by* δ[x] + *the set of formulas of the form* ∃x1,...,xn (β ◦(β −−• Q(y,p))) *as defined in Lemma 20. We also denote by* δ[x] = *the formula:* δ ◦(x y|1)*.*

For every model of δ, δ[x] − holds if x is not allocated in δ, δ[x] = holds if x is equal to the root of δ and δ[x] + holds if x is allocated but is not the root of δ. The following result follows immediately from Lemmata 19 and 20:

**Lemma 22.** *Assume that* R *is* ∃*-restricted. Let* x ∈ Vl*. For every predicate atom* δ *such that* x ∈ *roots*(δ)*, and for all structures* (s, h)*:* (s, h) |=P R δ *iff there exists* ψ ∈ {δ[x] −, δ[x] =} ∪ δ[x] + *such that* (s, h) |=P R ψ*.*

For instance the atom lseg(x, y, z) holds iff one of the formulas lseg(x, y, z) ◦ x y, lseg(x, y, z)[y] − or lseg(y, y, z) ◦(lseg(y, y, z) −−• lseg(x, y, z)) holds. The second formula corresponds to the case where y is not allocated, and the first and third ones correspond to the case where there is a loop on y. By applying repeatedly Lemma 22 on every variable x and atom δ we eventually obtain a disjunction of normalized formulas:

**Lemma 23.** *Let* R *be a* ∃*-restricted SID. There exists an algorithm transforming any symbolic heap* φ *containing no points-to atom into a set of normalized formulas* Ψ *such that for all structures* (s, h)*:* (s, h) |=P R φ *iff there exists* ψ ∈ Ψ *such that* (s, h) |=P R ψ*. Furthermore, every formula in* Ψ *is a (quantified) separating conjunction of* ◦*-formulas.*

# **4.2 Commuting Separating and Disjoint Connections**

The next step consists in showing that – under some particular conditions enforced by the previous transformation – the operator ∗ can be pushed innermost in the formula (below the operator ◦). To this aim, we exploit an essential property of h-regular SIDs, namely that all the locations that occur in the heap of some model of a formula φ but are not allocated correspond to a variable in *fv*(φ). We shall denote by *cut*(L, L , h) the set of locations reachable from L in h, from a path not crossing L :

**Definition 24.** *Let* h *be a heap, let* L, L ⊆ L*. We denote by cut*(L, L , h) *the set of locations inductively defined as follows:* L ⊆ *cut*(L, L , h)*, and if* ∈ *cut*(L, L , h)*,* h( )=(1,...,k, π)*,* i ∈ {1,...,k} *and* i ∈ L *then* i ∈ *cut*(L, L , h)*.*

The following lemma characterizes the domain of the part of the heap satisfying some formula φ:

**Lemma 25.** *Let* R *be a* h*-regular SID and let* φ *be a* ◦*-formula containing no quantifier. Let* s *be a store and let* h, h *be heaps, with* h ≤ h *. Let* V *be a set of variables, with fv*(φ) ⊆ V ∪ *roots*(φ) *and* s(V ) ∩ *dom*(h ) = ∅*. If* (s, h ) |=P R φ *then dom*(h ) = *cut*(s(*roots*(φ)), s(V ), h)*.*

The commutation property, pushing ∗ below ◦, is given by Lemma 26:

**Lemma 26.** *Let* R *be a* h*-regular SID. Let* V ⊆ Vl *and let* φ *be a normalized formula, of the form* φ = φ ◦(∗n i=1(φi ◦ ψi) ∗ ψ )*, where, for all* i ∈ {1,...,n}*, roots*(φi) = V *and* (*roots*(ψi) ∪ *roots*(ψ )) ∩ V = ∅*. Then* φ *is* (R, P)*-satisfiable iff* (φ ◦ ∗n i=1φi) ◦((∗n i=1ψi) ∗ ψ ) *is* (R, P)*-satisfiable.*

Roughly speaking, as *roots*(φi) = V and φi is normalized, it is possible to prove, using the characterization given in Lemma 25, that the parts of the heap that correspond to the formulas φi have all the same domain. This entails that the heaps corresponding to the formulas ψi and φi are disjoint, which permits to prove that ∗n i=1(φi ◦ ψi) can be written (∗n i=1φi) ◦(∗n i=1ψi), yielding the result.

#### **4.3 Merging of Spatial Predicates**

We show that, under some particular conditions, it is possible to replace the separating conjunction of two spatial atoms having the same root by a single spatial atom. The rules defining this atom are obtained by combining the rules of the two initial atoms. More precisely, consider any h-regular SID R and two spatial atoms P(x,y,p) and P (x,y , p ) sharing the same root x, where y,y are vectors of location variables and p and p are vectors of permission terms. We denote by P(x,y,p)-P (x,y , p ) any atom Q(x,y,y , p, p ) where Q is associated with rules of the form:

$$\begin{aligned} Q(v, \mathfrak{w}, \mathfrak{w}', \mathfrak{z}, \mathfrak{z}') &\leftarrow \exists u\_1, \dots, u\_n \quad v \xleftarrow{q} (v\_1, \dots, v\_k) \\ &\circlearrowright\_{i=1}^n (Q\_i(u\_i, \mathfrak{y}\_i, \mathfrak{q}\_i) \nabla Q'\_i(u\_i, \mathfrak{y}'\_i, \mathfrak{q}'\_i)) \circ \phi \circ \phi' \circ \psi \end{aligned}$$

with q def = p ⊕ p , for all pairs of rules of the following forms in R (with the same numbers k and n, and up to α-renaming, so that the rules share the same existential variables):

$$\begin{array}{llll} P(v, \mathfrak{w}, \mathfrak{z}) & \Leftarrow \exists u\_1, \ldots, u\_n & v \stackrel{p}{\mapsto} (v\_1, \ldots, v\_k) \circlearrowright\_{i=1}^n Q\_i(u\_i, \mathfrak{y}\_i, \mathfrak{q}\_i) \circ \phi \\\ P'(v, \mathfrak{w'}, \mathfrak{z'}) & \Leftarrow \exists u\_1, \ldots, u\_n & v \stackrel{p'}{\mapsto} (v'\_1, \ldots, v'\_k) \circlearrowright\_{i=1}^n Q'\_i(u\_i, \mathfrak{y}'\_i, \mathfrak{q}'\_i) \circ \phi' \end{array}$$

where ψ = k i=1(vi v i). Note that all the produced rules are h-regular8.

**Lemma 27.** *Let* R *be a* h*-regular SID. Let* x ∈ Vl *and let* (s, h) *be a structure such that* s(y) ∈ *dom*(h) *holds for all variables* y *such that* s(x) = s(y)*. Then* (s, h) |=P R P(x,y,p)-P (x,y , p ) ⇐⇒ (s, h) |=P R P(x,y,p) ∗ P (x,y , p )*.*

The result crucially depends on the fact that the parts of the heap that correspond to P(x,y,p) and P (x,y , p ) respectively must share the same domain, since otherwise, as R is h-regular, a free variable would be allocated, contradicting the hypothesis. This ensures that the heap can be generated by the above rules.

#### **4.4 Heap Abstractions and Main Result**

As we shall see later, the previous transformations can be used to transform any symbolic heap into a ◦-formula (while preserving satisfiability). The final step is to devise an algorithm to test the satisfiability of ◦-formulas. As it is done in [6] for standard heap models, the algorithm works by constructing relevant abstractions of the models of the predicate atoms. It suffices to keep track of the truth value of the equational atoms, of the allocated variables and of the permission atoms satisfied by the structure.

8 However ∃-restrictedness is not necessarily preserved.

**Definition 28.** *A* heap abstraction *is a tuple* a = (Va, ∼a, Aa, ρa) *where* Va *is a finite set of variables,* ∼a *is an equivalence relation on the variables of sort* l *occurring in* Va*,* Aa *is a subset of* Va∩Vl*, closed under* ∼a *(i.e., for all* x, y ∈ Vl*:* x ∈ Aa ∧ x ∼a y =⇒ y ∈ Aa*), and* ρa *is a permission formula (with variables in* Va*).*

**Definition 29.** *Let* (s, h) *be a structure and let* a = (Va, ∼a, Aa, ρa) *be a heap abstraction. We write* (s, h) |=P a *if all the following conditions are satisfied: (i) For all variables* x, y ∈ Va ∩ Vl*:* x ∼a y ⇐⇒ s(x) = s(y)*; (ii) for all* x ∈ Va ∩ Vl*,* x ∈ Aa ⇐⇒ s(x) ∈ *dom*(h)*; and (iii)* s |=P ρa*.

For all ◦-formulas φ, we define a set of heap abstractions A(φ) by mutual induction as follows. The sets A(φ) are the least sets of heap abstractions satisfying the following properties, for all finite sets of variables9 V ⊇ *fv*(φ) and for all equivalence relations ∼ on V ∩ Vl: (i) if φ = x p → (y1,...,yn) then (V, ∼, {y | y | y ∼ x}, *def* (p)) ∈ A(φ). (ii) if φ = x y (resp. x  y) with x, y ∈ Vl and x ∼ y (resp. x ∼ y) then (V, ∼, ∅, emp) ∈ A(φ); (iii) if φ is a permission formula then (V, ∼, ∅, φ) ∈ A(φ); (iv) if φ = ∃x ψ, (V, ∼, A, ρ) ∈ A(ψ) then (V \ {x}, ∼ , A \ {x}, ρ) ∈ A(φ), where ∼ denotes the restriction of ∼ to the variables distinct from x, i.e., ∼def = {(u, v) | u ∼ v ∧ u, v = x} (note that x cannot occur in ρ, since quantification over permission variables is not allowed); (v) if φ = φ1 ◦ φ2, (V, ∼, Ai, ρi) ∈ A(φi) (for all i = 1, 2) with A1 ∩ A2 = ∅, then (V, ∼, A1∪A2, ρ1 ◦ ρ2) ∈ A(φ); (vi) if φ = P(x, p) and φ ⇐R ξ then A(ξ) ⊆ A(φ).

**Lemma 31.** *A* ◦*-formula* φ *is* (R, P)*-satisfiable iff at least one of the abstractions in* A(φ) *is* P*-satisfiable.*

Putting things together we get the following result:

**Theorem 32.** *If* P*-satisfiability is decidable for permission formulas, then there exists an algorithm that, for every* ∃*-restricted SID, decides whether a given formula* φ *is* (R, P)*-satisfiable. If, moreover,* P*-satisfiability is in* Exptime*, then* (R, P)*-satisfiability is also in* Exptime *(for* ∃*-restricted SID). Finally, for every permission model* P*,* (R, P)*-satisfiability is* Exptime*-hard (for* ∃ *restricted SID).*

# **5 Using Separating Conjunctions Inside Rules**

To end the paper, we wish to point out that the satisfiability problem is undecidable from ∃-restricted SID if the disjoint separation ◦ is replaced by the standard

9 For technical convenience we do not impose any bound on the cardinality of V , hence the set A(φ) is infinite. This simplifies the theoretical definition of the abstraction for disjoint conjunctions. In practice only variables occurring in the initial formula or in the rules need to be considered.

separating connective ∗ in the inductive definitions (see Definition 7). We think that the result is of some theoretical interest, although, as explained above, rules using ◦ are actually more convenient for describing data structures. The notions of ∗-h*-regular* and ∗-∃*-restricted* SID are defined exactly as h-regular SID and ∃-restricted SID (Definitions 7 and 10) except that the symbol ◦ is replaced by ∗ everywhere (for conciseness the formal definitions are omitted).

**Theorem 33.** *Let* P *be any permission model and assume that for every* n ∈ N*, there exists* π ∈ PP *such that* πn *is defined. The* (R, P)*-satisfiability problem is undecidable for* ∗*-*∃*-restricted SID.*

# **6 Conclusion and Future Work**

An algorithm was devised to test the satisfiability of symbolic heaps in Separation Logic with inductively defined predicates and permissions, under some (syntactic) conditions on the inductive rules giving the semantics of the spatial predicates. The algorithm runs in exponential time, provided the satisfiability of permission formulas is in Exptime. In addition, we showed that some natural relaxings of these conditions make the problem undecidable (under some minimal assumptions on the permission model). The next step is to investigate the entailment problem for the considered fragment. The techniques devised in the present paper for transforming symbolic heaps into disjoint conjunctions of atoms should serve as a basis for this purpose, but the extension is not straightforward. Another (much easier) extension that could be of practical relevance is to consider formulas with labels (in the sense of [5]) which allow one to express additional equality conditions on some parts of the structures. In our context, labels would simply yield additional conditions on the decomposition generated during the normalization step: two formulas sharing the same label should be decomposed into formulas with the same set of roots. It could also be interesting to relax some of the conditions on the rules, for instance to allow for existential variables not occurring as roots in the rules. This is required to encode data structures with forward pointers, such as skip lists. It is also unclear whether Condition 4 in Definition 10 is required for decidability. Finally, the decision algorithm could probably be extended to handle arbitrary combinations of disjoint and separating conjunctions.

**Acknowledgments.** This work has been partially funded by the French National Research Agency (ANR-21-CE48-0011)

#### **References**

1. Berdine, J., Calcagno, C., O'Hearn, P.W.: Smallfoot: modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 115–137. Springer, Heidelberg (2006). https://doi.org/10.1007/11804192 6

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

# **First-Order Logics**

# Nested Sequents for Quantified Modal Logics

Tim S. Lyon1(B) and Eugenio Orlandelli2

1 Institute of Artificial Intelligence, TU Dresden, Dresden, Germany<EMAIL_ADDRESS>2 Department of the Arts, University of Bologna, Bologna, Italy<EMAIL_ADDRESS>
Abstract. This paper studies nested sequents for quantified modal logics. In particular, it considers extensions of the propositional modal logics definable by the axioms D, T, B, 4, and 5 with varying, increasing, decreasing, and constant domains. Each calculus is proved to have good structural properties: weakening and contraction are height-preserving admissible and cut is (syntactically) admissible. Each calculus is shown to be equivalent to the corresponding axiomatic system and, thus, to be sound and complete. Finally, it is argued that the calculi are internal i.e., each sequent has a formula interpretation—whenever the existence predicate is expressible in the language.

Keywords: Cut elimination · Nested sequent · Quantified modal logic

# 1 Introduction

Generalisations of Gentzen-style sequent calculi have proven useful for developing cut-free and analytic proof systems for many propositional non-classical logics, including modal and intermediate ones. Among these generalisations are *display calculi* [2], *hypersequents* [1], *labelled calculi* [23,25], and *nested sequents* [5,12]. They often allow one to give constructive proofs of important meta-theoretical properties such as decidability [3], interpolation [9], and automatic countermodel extraction [16]. These systems generalise the structural level of Gentzen-style calculi in different ways in order to express wider classes of logics. In the case of propositional modal logics they can express the structure of various relational models. In particular, nested sequents encode tree-like relational models and labelled calculi encode graph-like models. In contrast to other formalisms (e.g. labelled sequents) nested sequents have the advantage of being internal calculi: each nested sequent has a formula interpretation, and thus, such expressions are not a major departure from the modal language.

Things become more difficult when we add the quantifiers. As is well known [7,10], in quantified modal logics (QMLs) we have *interaction formulas* such as

> CBF := -∀xA ⊃ ∀x-A and BF := ∀x-A ⊃ -∀xA

c The Author(s) 2023

Tim S. Lyon was supported by the European Research Council (ERC) Consolidator Grant 771779 (DeciGUT).

R. Ramanayake and J. Urban (Eds.): TABLEAUX 2023, LNAI 14278, pp. 449–467, 2023. https://doi.org/10.1007/978-3-031-43513-3\_24

whose validity depends on the interrelations between the domains of quantification (Dw) of the different worlds (w) of the model: CBF is valid only if domains are *increasing*—wRv implies Dw ⊆ Dv—and BF is valid only if domains are *decreasing*—wRv implies Dw ⊇ Dv. Axiomatically, CBF is derivable from the interaction of the axioms/rules for modalities and those for the classical quantifiers, and BF is independent from them. However, the situation is radically different for sequent calculi than for axiomatic calculi. The problem is that BF becomes derivable when we add standard sequent rules for the quantifiers to a calculus having separated left and right rules for the modalities—i.e., it is derivable in all generalisations of Gentzen-style calculi mentioned above.

To overcome this issue for nested sequents, we employ a formulation technique motivated by labelled sequent calculi. One way of making CBF and BF independent of the rules for quantifiers within labelled sequent calculi is to extend the language with *domain atoms* of shape y ∈ D(w) whose intended meaning is that 'y belong to the quantificational domain of the label w' [20,25]. In this way, one can restrict the rules for the quantifiers to the terms belonging to the domain of the label under consideration:

$$\frac{w:A(y/x), y \in D(w), w:\forall x A, \varGamma \Rightarrow \Delta}{y \in D(w), w:\forall x A, \varGamma \Rightarrow \Delta} \quad \frac{z \in D(w), \varGamma \Rightarrow \Delta, w:A(z/x)}{\varGamma \Rightarrow \Delta, w:\forall x A} \; \,\_z\text{ fresh}$$

As a consequence, CBF and BF are derivable only if we extend the basic calculus with rules relating the domains of the distinct labels.

In this paper, we study nested sequent calculi for QMLs with varying, increasing, decreasing, and constant domains. Similar to the use of domain atoms in labelled sequents, we will formulate our nested calculi by extending the syntax of sequents with *signatures*—i.e., multisets of terms that restrict the applicability of the rules for the quantifiers at that node of the nested sequent—as was done in [24] to define hypersequents for Gödel-Dummett logic with non-constant domains. In particular, we will use the following rules for the universal quantifier:

$$\frac{\mathcal{S}\{X, y; A(y/x), \forall x A, \varGamma \Rightarrow \Delta\}}{\mathcal{S}\{X, y; \forall x A, \varGamma \Rightarrow \Delta\}}\\_{L\forall} \qquad \frac{\mathcal{S}\{X, z; \varGamma \Rightarrow \Delta, A(z/x)\}}{\mathcal{S}\{X; \varGamma \Rightarrow \Delta, \forall x A\}}\\_{R\forall,\text{ z fresh}}$$

and will add signature structural rules for increasing, decreasing, and constant domains (Table 3).

As a consequence, we will be able to define nested calculi that are equivalent to the labelled calculi considered in [25, Ch. 6] and [20, Ch. 12.1]. We will show that our nested calculi have good structural properties—all rules are height-preserving invertible, weakening and contraction are height-preserving admissible, and cut is syntactically admissible—and that they characterise the quantified extensions of the propositional modal logics in the cube of normal modalities. One advantage of the present approach is that nested sequents with signatures have a formula interpretation given that the language can express the *existence predicate* E. In this paper, we will consider a language with identity so that Ex can be expressed as ∃y(y = x) and it need not be taken as an additional primitive symbol; cf. [7]. Thus, our calculi utilise (nested) sequents as expressive as the modal language, showing that our calculi are syntactically economical.

The rest of the paper is organised as follows: Sect. 2 sketches the QMLs considered in the paper, and Sect. 3 introduces the nested calculi for these logics. Then, Sect. 4 shows that these calculi have good structural properties distinctive of G3-style calculi, including syntactic cut-elimination, and Sect. 5 shows that each calculus is sound and compete with respect to its intended semantics. Finally, Sect. 6 presents some future lines of research.

# 2 Quantified Modal Logics

*-Syntax.* Let *Rel* be a set containing, for each n ∈ N, an at most countable set of n-ary predicates Rn 1 , Rn 2 ,... , and let *Var* be a denumerable set of individual variables. The language L is defined by the following grammar:

$$A ::= \begin{array}{c} R\_i^n(x\_1, \dots, x\_n) \mid x\_1 = x\_2 \mid \perp \mid A \supset A \mid \forall x A \mid \Box A \end{array} \tag{\mathcal{L}}$$