Rémi Brochenin

Stéphane Demri

Etienne Lozes

On the Almighty Wand 1

Keywords: separation logic, second-order logic, expressive power, complexity

We investigate decidability, complexity and expressive power issues for (firstorder) separation logic with one record field (herein called SL) and its fragments. SL can specify properties about the memory heap of programs with singly-linked lists. Separation logic with two record fields is known to be undecidable by reduction of finite satisfiability for classical predicate logic with one binary relation. Surprisingly, we show that second-order logic is as expressive as SL and as a by-product we get undecidability of SL. This is refined by showing that SL without the separating conjunction is as expressive as SL, whence undecidable too. As a consequence, in SL the separating implication (also known as the magic wand) can simulate the separating conjunction. By contrast, we establish that SL without the magic wand is decidable, and we prove a non-elementary complexity by reduction from satisfiability for the first-order theory over finite words. This result is extended with a bounded use of the magic wand that appears in Hoare-style rules. As a generalisation, it is shown that kSL, the separation logic over heaps with k ≥ 1 record fields, is equivalent to kSO, the second-order logic over heaps with k record fields.

Introduction

Separation logic. Programming languages with pointer variables seldom have mechanisms to detect errors. An inappropriate management of memory is the source of numerous bugs and security holes such as buffer overflow attacks, null pointer dereferences or memory leaks. Prominent logics for analysing such pointer programs include separation logic [START_REF] Reynolds | Separation logic: a logic for shared mutable data structures[END_REF], pointer assertion logic PAL [START_REF] Jensen | Automatic verification of pointer programs using monadic second-order logic[END_REF], TVLA [START_REF] Lev-Ami | TVLA: A system for implementing static analyses[END_REF], alias logic [START_REF] Bozga | On logics of aliasing[END_REF], BI (Bunched Implication) [START_REF] Ishtiaq | BI as an assertion language for mutable data structures[END_REF] and LRP (logic of reachable patterns) [START_REF] Yorsh | A logic of reachable patterns in linked data structures[END_REF] to quote a few examples. Separation logic (SL) is an assertion language used in Hoare-like proof systems [START_REF] Reynolds | Separation logic: a logic for shared mutable data structures[END_REF] that are dedicated to verify programs manipulating heaps. Any procedure mechanizing the proof search requires subroutines that check satisfiability of formulae from the assertion language. The main concern of the paper is to analyze the expressive power of the assertion language and the decidability of its satisfiabily problem. Recall that separation logic contains a structural separation connective and its adjoint (the separating implication -- * , also known as the magic wand). Concise and modular proofs can be derived using these connectives, since they can express properties such as non-aliasing and disjoint concurrency. In this perspective, the models of separation logic are pairs made of a store (variable valuation) and a memory heap (partial function with finite domain) that are understood as memory states.

Magic wand and lists. The complexity of the satisfiability, the model-checking, the validity or the entailment problems for several fragments of separation logic have been intensively studied since the early days of separation logic until quite recently [START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF][START_REF] Calcagno | Computability and complexity results for a spatial assertion language[END_REF][START_REF] Reynolds | Separation logic: a logic for shared mutable data structures[END_REF][START_REF] Brochenin | Reasoning about sequences of memory states[END_REF][START_REF] Cook | Tractable reasoning in a fragment of separation logic[END_REF]. The magic wand connective makes any of these problems quite difficult to decide (note that these problems are often equivalent in presence of magic wand). The expressive power of -- * is increased by the first-order quantification: SL with magic wand is known to be equivalent to a classical propositional logic [START_REF] Lozes | Separation logic preserves the expressive power of classical logic[END_REF] if first-order quantifiers are disabled, whereas no adjunct elimination occurs in SL with first-order quantifiers [START_REF] Dawar | Adjunct elimination through games in static ambient logic[END_REF][START_REF] Lozes | Elimination of spatial connectives in static spatial logics[END_REF]. The same gap exists with respect to decidability: SL without first-order quantifiers is decidable, but it becomes undecidable if first-order quantifiers are taken into account [START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF]. These known results however crucially relies on the memory model addressing cells with two record fields (undecidability of SL in [START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF] is by reduction to the first-order theory of a finite binary relation). But, despite the predominance of the list-manipulating programs in the case studies of separation logic, the minimality and complexity of SL with magic wand is not known for memory models with only one record field.

Second-order logic. A natural question about separation logic is how it compares with weak second-order logic (SO) and its fragments. This is a very natural question for at least three reasons. Firstly, separating conjunction and its adjoint are essentially second-order connectives (see also a similar concern on graphs with spatial logics [START_REF] Dawar | Expressiveness and complexity of graph logic[END_REF]), which clearly makes SL be a fragment of SO. Secondly, many properties on heaps require second-order logic, for instance to express recursive predicates, or list and tree properties. Thirdly, SO is known to be a sufficiently expressive assertion language for ensuring the completeness of the Hoare-Floyd logic, and better understanding the relationship between SL and SO could serve to derive the completeness of the proof system of SL.

A first exploration of the relationships between SL and SO can be found in [START_REF] Kuncak | On spatial conjunction as second-order logic[END_REF], but Kunczak and Rinard considered a separation logic for arbitrary first-order structures, and not the standard, finite, functional heap model of SL. The expressivity of SL with magic wand for lists is thus also an open question.

Our contributions. In this paper, we address simultaneously the decidability, complexity, expressive power, and minimality of first-order separation logic with one selector (record field) with and without magic wand.

We show that first-order separation logic with one selector (called herein SL) is as expressive as second-order logic over the class of memory states. As a by product, we get that even in presence of a unique selector, firstorder separation logic is undecidable (solving an open problem stated in [START_REF] Galmiche | Tableaux and resource graphs for separation logic[END_REF]). This is refined by showing that SL without the separating conjunction is as expressive as SL, whence undecidable too. Our proof also shows that the two formalisms have the same conciseness modulo logarithmic-space translations. As a consequence, SL is not a minimal logic, as the magic wand can simulate the separating conjunction, but it does not have the adjunct elimination. Moreover, these results generalize to non-linear recursive data structures: kSL, the separation logic over heaps with k ≥ 1 record fields, is equivalent to kSO, the second-order logic over heaps with k record fields. Note that we use the loose version of points-to and as far as we can judge, our results are dependent on using the loose points-to. We did not investigate in details which of our results can be adapted to the tight points-to.

The correspondence between first-order separation logic with one selector and weak second-order logic over the class of memory states is particularly interesting from a logical point of view. Indeed, it shows that separating operators are sufficient to express weak second-order quantification; actually we even show that the magic wand suffices. There are well-known examples of standard logics that are shown equivalent to standard other formalisms, such that temporal logics. The celebrated Kamp's theorem states that the the popular linear-time temporal logic LTL is as expressive as first-order logic [START_REF] Kamp | Tense logic and the theory of linear order[END_REF]; here LTL has only the strict until and since operators. This result is refined in [START_REF] Etessami | First-order logic with two variables and unary temporal logic[END_REF] where it is shown that unary LTL is as expressive as firstorder logic restricted to two individual variables. Similarly, the automatabased approach for formal verification stems from the famous result showing the equivalence between monadic second-order logic and Büchi automata as far as definability of languages of infinite words are concerned [START_REF] Büchi | On a decision method in restricted second-order arithmetic[END_REF]. In this paper, our pivot logic is weak second-order logic over the class of memory states.

We also establish that SL without the magic wand is decidable, but with a non-elementary complexity (this lower bound is obtained by reduction from satisfiability for the first-order theory over finite words [START_REF] Stockmeyer | The complexity of decision problems in automata theory and logic[END_REF], and holds already with three variables). Decidability is shown by reduction to weak monadic second-order theory of one unary (total) function that is shown decidable in [START_REF] Rabin | Decidability of second-order theories and automata on infinite trees[END_REF]. It is worth noting that even though the first-order theory of one unary function is known to be not elementary recursive [START_REF] Börger | The Classical Decision Problem[END_REF], we cannot take advantage of this result since in our models the domain of the unary function is necessarily finite and finiteness cannot be expressed in most first-order dialects. As a by-product, we obtain that the entailment problem considered in [START_REF] Berdine | A decidable fragment of separation logic[END_REF] for a fragment of separation logic with one selector is decidable. We also establish that decidability can be obtained with a restricted use of the magic wand as it occurs in Hoare-like proof systems involving separation logic.

Related work. The closest works to ours are certainly the recent ones on the decidability of separation logic for lists with data [START_REF] Bansal | Beyond shapes: Lists with ordered data[END_REF] and the work on the comparison of the expressive power of monadic second-order logic and the spatial logic for graphs [START_REF] Antonopoulos | Separating graph logic from MSO[END_REF]. Although the questions solved in these works do not overlap the results presented herein, these works adopt a point of view quite similar to the one of this paper and give a more complete picture of the topic. More detailed comments are given in related sections of this paper.

The magic wand is rarely considered by the litterature on SL, which our result may explain from the complexity point of view. The magic wand is however often behind the scene in recent developments of SL. For instance, the bi-abduction problem [START_REF] Gorogiannis | The complexity of abduction for separated heap abstractions[END_REF] can be seen as a specialized version of the satisfiability problem for SL with magic wand. As a parallel to this work, results stating either the absence of adjunct elimination or the undecidability of satisfiability for logics including a form of magic wand have been independently established for boolean BI [START_REF] Larchey-Wendling | The Undecidability of Boolean BI through Phase Semantics[END_REF], propositional SL [START_REF] Brotherston | Undecidability of propositional separation logic and its neighbours[END_REF], or context logic [START_REF] Calcagno | Context logic as modal logic: completeness and parametric inexpressivity[END_REF]. The main difference with our work is that the models of these logics include formal propositional variables that can be used to axiomatize the models in any desired way, whereas we are sticking to the heap model.

As seen previously, heap properties are formalized in various logical languages [START_REF] Jensen | Automatic verification of pointer programs using monadic second-order logic[END_REF][START_REF] Lev-Ami | TVLA: A system for implementing static analyses[END_REF][START_REF] Reynolds | Separation logic: a logic for shared mutable data structures[END_REF][START_REF] Bozga | On logics of aliasing[END_REF][START_REF] Yorsh | A logic of reachable patterns in linked data structures[END_REF] and separation logic is just one prominent example of these logics. However, in this paper we focus on expressive power and decidability issues rather than on verification techniques. Verification methods and logics for verifying programs with singly-linked lists can be found for instance in [START_REF] Berdine | A decidable fragment of separation logic[END_REF][START_REF] Bouajjani | Verifying programs with dynamic 1-selector-linked structured in regular modelchecking[END_REF][START_REF] Ranise | A theory of singly-linked lists and its extensible decision procedure[END_REF]. From another perspective, the relationships between logics on graphs with separating features and second-order logic can be found in [START_REF] Dawar | Expressiveness and complexity of graph logic[END_REF]. Finally, we would like to mention that sabotage modal logics (SML) considered in [START_REF] Van Benthem | An essay on sabotage and obstruction[END_REF][START_REF] Löding | Model checking and satisfiability for sabotage modal logic[END_REF] have also the ability to modify the model under evaluation by using new logical connectives. So far, we are not aware of any work relating separation logic and SML.

Plan of the paper. In Section 2, we present the different logical formalisms used in the paper (separation logic SL and weak second-order logic SO), examples for properties that can be expressed in such languages and a translation from SL into SO. In Section 3, we show that SL restricted to the separating conjunction is decidable with non-elementary complexity. The complexity lower bound is by reduction from the first-order theory over finite words and decidability is obtained by a logarithmic-space reduction into weak monadic second-order theory for one unary function. In Section 4, we extend this decidability result with a restricted use of the magic wand. Section 5 contains many technical contributions about the expressive power of SL, in particular we show how to express arithmetical constraints about the memory heap. These results are essential to show in Section 6 that SO and SL are equivalent in terms of expressivity. This is refined by showing that SL restricted to the magic wand (called herein SL(-- * )) is also as expressive as SO (and SL). In Section 7, we show how the equivalence between separation logic and second-order logic can be extended to memory cells with k > 1 record fields. Section 8 contains concluding remarks and open problems for further investigation.

This paper is a completed version of [START_REF] Brochenin | On the almighty wand[END_REF].

Preliminaries

In this section, we recall the definition of first-order separation logic with one selector (record field), called herein SL, and second-order logic over the same class of structures (called herein SO). We introduce the concept of being at least as expressive as another fragment, and provide examples of properties that can be expressed in our formalisms. This section ends by presenting a quite straightforward encoding of SL into fragments of SO over structures with one unary function.

Separation Logic and Second-Order Logic

Memory states. Memory states are models for all the logical formalisms we consider herein. They represent the states of the memory for programs manipulating lists. Let Loc be a countably infinite set of locations ranged over by l, l , . . . that represents the set of addresses. A memory state is composed of a pair made of a store and a heap. Let Var be a countably infinite set of (first-order) variables x, y, z, . . . . A memory state (also called a model in the rest of the document) is a pair (s, h) such that • s is a variable valuation of the form s : Var→Loc (store),

• h is a partial function h : Loc Loc with finite domain (heap). We write dom(h) to denote its domain and ran(h) to denote its range.

Given a finite set X of variables (for instance occurring in a given formula), we can assume that a model is finite by restricting the domain of the store to X. The variables in Var can be viewed as programming variables, the domain of h as the set of addresses of allocated cells, and h(l) as the value held by the cell at the address l. We write S to denote the set of stores, and H to denote the set of heaps. A heap h with domain {l 1 , . . . , l n } is sometimes represented by the set of memory cells {l 1 → h(l 1 ), . . . , l n → h(l n )}. Two heaps h 1 , h 2 are said to be disjoint, noted h 1 ⊥h 2 , if their domains are disjoint; when this holds, we write h 1 * h 2 to denote the disjoint union h 1 h 2 . Given a memory state (s, h) and a location l we write l to denote the cardinal of the set {l ∈ Loc : h(l ) = l} (number of predecessors of the location l in (s, h)).

A location l is a descendant [resp. strict descendant] of l if there is n ≥ 0 [resp. n > 0] such that h n (l) = l (h n (l)
is not always defined). In the rest of the paper, we assume that Loc = Val = N, the value nil can be encoded by an individual variable in the first-order language.

Formulae in SL and SO. Formulae of first-order separation logic with one selector SL are defined by the grammar below:

φ := ¬φ | φ ∧ φ | ∃x φ | x → y | x = y | φ * φ | φ -- * φ
The connective * is called separating conjunction whereas the adjoint operator -- * , the separating implication, is usually called the magic wand. We will make use of standard notations for the derived connectives ∀, ∨, ⇒, ⇔. We write FV(φ) to denote the set of free variables occurring in φ.

We write SL( * ) [resp. SL(-- * )] to denote the restriction of SL without the magic wand [resp. without the separating conjunction].

In order to define formulae in SO, we consider a family VAR = (VAR i ) i≥0 of second-order variables, denoted by P, Q, R, . . . that will be interpreted as finite relations over Loc. Each variable in VAR i is interpreted as an i-ary relation. An environment E is an interpretation of the second-order variables such that for every P ∈ VAR i , E(P) is a finite subset of Loc i . Since we require finiteness of models, the version of second-order logics we shall consider is usually called weak.

Formulae of (weak) second-order logic SO are defined by the grammar below:

φ := ¬φ | φ ∧ φ | ∃x φ | x → y | x = y | ∃P φ | Q(x 1 , . . . , x n )
where P, Q are second-order variables and Q ∈ VAR n . We write MSO [resp. DSO] to denote the restriction of SO to second-order variables in VAR 1 [resp. VAR 2 ]. As usual, a sentence is defined as a formula with no free occurrence of second-order variables. Let us mention that the equality x = y could be also encoded as by Leibnitz formula ∀P.(P(x) ⇔ P(y)).

Satisfaction relations for SL and SO. The logics SL and SO share the same class of models, namely the set of memory states. The satisfaction relation for SO is defined below with argument an environment E (below

P ∈ VAR n ). (s, h), E |= ∃P φ iff there is a finite subset R of Loc n , such that (s, h), E[P → R] |= φ (s, h), E |= P(x 1 , • • • , x n ) iff (s(x 1 ), . . . , s(x n )) ∈ E(P) (s, h), E |= ¬φ iff not (s, h), E |= φ (s, h), E |= φ ∧ ψ iff (s, h), E |= φ and (s, h), E |= ψ (s, h), E |= ∃x φ iff there is l ∈ Loc such that (s[x → l], h), E |= φ (s, h), E |= x → y iff h(s(x)) = s(y) (s, h), E |= x = y iff s(x) = s(y)
As usual, when φ is a sentence, we write (s, h) |= φ to denote (s, h), E |= φ for any environment E since E has no influence on the satisfaction of φ. The satisfaction relation for SL is defined without any environment (or equivalently with no influence of the environment). The clauses that are specific to SL are the following ones:

(s, h) |= φ 1 * φ 2 iff there are two heaps h 1 , h 2 such that h = h 1 * h 2 , (s, h 1 ) |= φ 1 and (s, h 2 ) |= φ 2 (s, h) |= φ 1 -- * φ 2 iff for all heaps h ⊥h, if (s, h ) |= φ 1 then (s, h * h) |= φ 2 .
Consequently, -- * is a universal modality whereas * has an existential flavour.

Validity and satisfiability problems are defined in the usual way. The connective -- * is the adjunct of * , meaning that

(φ * ψ) ⇒ ϕ is valid iff φ ⇒ (ψ -- * ϕ) is valid.
Observe that * and -- * are not interdefinable since typically the formula ((φ * ψ) ⇒ ϕ) ⇔ (φ ⇒ (ψ -- * ϕ)) is not valid. This shall be strengthened in the sequel by establishing that SL( * ) is decidable whereas SL(-- * ) is not.

Septraction. We also introduce a slight variant of the dual connective for the magic wand, also called the septraction: φ -- * ¬ ψ is defined as the formula

¬((φ) -- * (¬(ψ))). It is easy to check that (s, h) |= φ 1 -- * ¬ φ 2 iff there is h ⊥ h such that (s, h ) |= φ 1 and (s, h * h ) |= φ 2 .
Septraction is nothing else than an existential version of magic wand. Hence, the septraction operator is quite natural since it states the existence of a disjoint heap satisfying a formula and for which the addition to the original heap satisfies another formula.

Adding the constant null. The current version of SL does not contain the constant null interpreted by nil such that any h is undefined for the value nil. Any formula φ possibly with the constant null can be easily translated into a formula φ of SL such that φ is satisfiable iff φ is satisfiable. Indeed, φ can be defined as ∃ null (¬∃z null → z) ∧ φ, where null is understood as a distinguished variable. In the sequel, we might use the constant null without further notice.

Here are some lemmas that shall be used in the sequel.

Lemma 2.1 Let (s, h) be a model, E be an environment, and ψ be a formula in DSO. Let l, l be locations such that

• l / ∈ dom(h) ∪ ran(h). • l / ∈ dom(h) ∪ ran(h) ∪ {s(x) : x ∈ FV(ψ)}.
• l is not in the finite graph of E(P) for any second-order variable P occurring in ψ.

Then (s[l ← l ], h), E[l ← l ] |= ψ iff (s, h), E |= ψ.
In the above statement, s[l ← l ] [resp. E[l ← l ]] denotes the store obtained from s [resp. the environment obtained from E] by replacing every occurrence of l by l (in the range). Its proof is by simple induction on the structure of ψ.

Lemma 2.2 For all s, h, E, s , ψ, if s | FV(ψ) = s | FV(ψ) , then (s, h), E |= ψ iff (s , h), E |= ψ.
The proof of Lemma 2.2 is also by an easy verification.

Let F and F be two fragments of SL or SO. We say that F is at least as expressive as F (written F F ) whenever for every sentence φ ∈ F, there is φ ∈ F such that for every model (s, h), we have (s, h) |= φ iff (s, h) |= φ . We write F ≡ F if F F and F F. A translation from F to F is a computable function t : F → F such that for every sentence φ ∈ F, for every model (s, h), we have (s, h) |= φ iff (s, h) |= t(φ).

Arithmetical constraints. Observe that SL does not contain explicitly arithmetical constraints as in [START_REF] Klaedtke | Monadic second-order logics with cardinalities[END_REF][START_REF] Magill | Arithmetic strengthening for shape analysis[END_REF][START_REF] Bozga | Quantitative separation logic and programs with lists[END_REF]. However, in Section 5 we show how to compare number of predecessors. Similar developments can be performed to compare lengths of lists but this will come as a corollary of the equivalence between SL and SO.

Another model with data. A more realistic approach to model lists consists in considering two selectors. However, SL behaves as separation logic with two selectors for which one selector is never used (separation with one selector can only speak about the structure and not about data values). Indeed, we already know that an unrestricted use of the two selectors leads to undecidability. In the paper, we show that even SL satisfiability/validity is already undecidable. It is open how to refer to data values while preserving the decidable results for SL fragments. Possible directions consist either in imposing syntactic restrictions (like the guarded fragment for classical predicate logic) or in forbidding a direct access to data values but allowing predicates of the form "there is a list from x to y with increasing data values", see e.g. [START_REF] Bansal | Beyond shapes: Lists with ordered data[END_REF].

A Selection of Properties

We present below a series of properties that can be expressed in SL( * ).

• The value of x is in the domain of the heap: alloc (x) ∃y x → y.

• The domain of the heap is restricted to the value of x, and maps it to that of y: x → y x → y ∧ ¬∃y (y = x ∧ alloc (y)).

• The domain of the heap is empty: emp ¬∃x alloc (x).

Predecessors and special nodes. A predecessor of the variable x in the model (s, h) is a location l such that h(l) = s(x). There are formulae in SL( * ), namely x ≥ n and x = n, such that x ≥ n [resp. x = n] holds true exactly in models such that x has at least n predecessors [resp. exactly n predecessors]. For instance, x ≥ n can be defined in the following ways:

n times (∃y y → x) * • • • * (∃y y → x) * or ∃x 1 , . . . , x n i =j x i = x j ∧ n i=1 x i → x
It is worth noting that the first formula has a unique additional variable y but n occurrences of * whereas the second formula has no separating connectives but n additional variables.

Reachability and list predicates. Reachability in a graph is a standard property that can be expressed in monadic second-order logic. In separation logic, very often a built-in predicate for lists is added, sometimes noted ls(x, y).

Adapting some technique used in the graph logics [START_REF] Dawar | Expressiveness and complexity of graph logic[END_REF], we show below how this very predicate can be expressed in SL( * ) as well as the reachability predicate x→ * y.

A cyclic list in a model (s, h) is a non-empty finite sequence l 1 , . . . , l n (n ≥ 1) of locations such that h(l n ) = l 1 and for every i ∈ {1, . . . , n -1}, h(l i ) = l i+1 . A model (s, h) is a list segment between x and y if there are locations l 1 , . . . , l n (n ≥ 2) such that s(x) = l 1 , s(y) = l n , l 1 = l n , dom(h) = {l 1 , . . . , l n-1 }, and for every i ∈ {1, . . . , n -1}, h(l i ) = l i+1 . Consider the formula below

x -→ + y x = 0 ∧ alloc (x) ∧ y = 1 ∧ ¬alloc (y) ∧∀z z = y ⇒ ( z = 1 ⇒ alloc (z)) ∧∀z z ≤ 1 Lemma 2.3 Let (s, h) be a model. (s, h) |= x -→
+ y iff h is undefined for s(y) and there are unique heaps h 1 , h 2 such that h 1 * h 2 = h, (s, h 1 ) is a list segment between x and y and (s, h 2 ) can be decomposed uniquely as a (finite) collection of cyclic lists.

Proof A location l is shared whenever l ≥ 2. A location l is initial [resp. final] whenever l ∈ dom(h) \ ran(h) [resp. l ∈ ran(h) \ dom(h)]. It is easy to show that (s, h) x -→ + y if and only if • s(x) is initial, • s(y) is final,
• s(y) is the only final location,

• h has no shared location.

It is easy to check that if h is of the form h 1 * h 2 having the properties stated in Lemma 2.3, then it satisfies the formula x -→ + y, which shows one implication. Let us prove the other implication.

Assume (s, h) x -→ + y. Since dom(h) is finite, the set of descendants of s(x) forms either a cyclic list, or a lasso (a list segment followed by a cycle) or a list ended by a final location. Since there are no shared locations, there is no lasso; and since s(x) is initial, it does not belong to a cyclic list. So s(x) has a descendant that is final. It can only be s(y), so h contains a list segment from s(x) to s(y). To end the proof, we must show that the rest of the heap contains cyclic lists only. This is equivalent to say that no location different from s(x) is initial. The proof is ad absurdum. Suppose that l is an initial location distinct from s(x). Then by the same reasoning as for s(x), we have s(y) is a descendant of l, so two distinct paths reach s(y), which contradicts the absence of shared locations. Now, we can introduce additional formulae (in SL( * )) that are useful in the sequel.

ls(x, y)

x -→

+ y ∧ ¬(x -→ + y * ¬emp) x → + y * ls(x, y) x→ * y x = y ∨ x → + y
These formulae express the properties below. Proof For all variables P, Q, R in VAR 2 , let us define the SO formulae below with free occurrences of P, Q, R:

• init(P)
∀x, y xPy⇔x →y,

• heap(P) ∀x, y, z xPy ∧ xPz ⇒ y = z (functionality),

• P = Q * R ∀x, y (xPy⇔(xQy ∨ xRy)) ∧ ¬(xQy ∧ xRy).
Let φ be a formula in SL and P be a variable in VAR 2 . One can show that for every model (s, h), we have (s, h) |= φ iff (s, h) |= ∃P init(P) ∧ t P (φ) where t P (•) is inductively defined as follows (t P (•) is homomorphic for Boolean connectives and first-order quantification):

t P (x →y) xPy t P (ψ * ϕ) ∃Q, Q P = Q * Q ∧ t Q (ψ) ∧ t Q (ϕ) t P (ψ -- * ϕ) ∀Q((∃Q heap(Q ) ∧ Q = Q * P) ∧ heap(Q) ∧ t Q (ψ)) ⇒ (∃Q heap(Q ) ∧ Q = Q * P ∧ t Q (ϕ))
In the above clauses, the second-order variables Q and Q are fresh.

Proposition 2.6 There is a logarithmic-space translation from SO to DSO (hence SO DSO).

Proof We use the standard graphical representation of a multigraph: a tuple (l 1 , . . . , l n ) is represented by n edges (l 1 , l), . . . , (l n , l) for some location l. To each variable P in VAR n , we associate n distinct variables P 1 , . . . , P n in VAR 2 . Let us define the map t, homomorphic for Boolean connectives and first-order quantification, such that t preserves the semantics:

t(∃P ψ) ∃P 1 , . . . , P n t(ψ) t(P(x 1 , . . . , x n )) ∃y n i=1 P i (x i , y).
Correctness of the translation makes an essential use of the fact that in SO, the second-order quantification is over finite sets of locations. Indeed, let R 1 , . . . , R n be n finite binary relations and R be a finite n-ary relation (over Loc). We say that (R 1 , . . . , R n ) corresponds to R whenever for all

(l 1 , . . . , l n ) ∈ Loc n , (l 1 , . . . , l n ) ∈ R iff there is l ∈ Loc such that for 1 ≤ k ≤ n, (l k , l) ∈ R k .
We have the following properties:

1. For all finite binary relations R 1 , . . . , R n , there is a finite n-ary relation

R such that (R 1 , . . . , R n ) corresponds to R. 2. Reciprocally, for every finite n-ary relation R, there are n finite binary relations R 1 , . . . , R n such that (R 1 , . . . , R n ) corresponds to R.
Sections 5 and 6 are devoted to prove that DSO SL(-- * ). We will obtain that SL(-- * ), SL, DSO and SO have the same expressive power (via logspace translations). Consequently, this implies undecidability of the validity problem for any of these logics by the undecidability of classical predicate logic with one binary relation [START_REF] Trakhtenbrot | The impossibility of an algorithm for the decision problem for finite models[END_REF]. By contrast, we prove below that SL( * ) is decidable.

On the Complexity of SL( * )

In this section, we show that SL( * ) satisfiability is decidable but with nonelementary recursive complexity (by reduction from the first-order theory of finite words). Lemma 3.1 MSO satisfiability is decidable. Proof The weak monadic second-order theory of unary functions is the theory over structures of the form (D, f, =) where D is a countable domain, f is a unary function, and = is equality. This theory is decidable, see e.g. [START_REF] Börger | The Classical Decision Problem[END_REF]Corollary 7.2.11]. Since in such a logical language it is possible to express that D is infinite and to simulate that f is a partial function with finite domain (use a monadic predicate symbol to be interpreted as the finite domain of f ), one can specify that (D, f, =) augmented with a first-order valuation is isomorphic to a heap. Based on these elementary facts, we define a translation t P (.), computable in logarithmic space, such that a MSO sentence φ is satisfiable iff

infinity (¬∃P ∀x P(x)) ∧∃P t P (φ)
is satisfiable in the weak monadic second-order theory of one unary function, where t P (•) is defined as follows:

t P (x → y) P(x) ∧ f (x) = y t P (x = y) x = y t P (Q(x)) Q(x)
t Q is homomorphic for the Boolean connectives and for quantifications.

∃P (∀x P(x)⇔ (∃y x → y)) ∧ t P (φ)
is satisfiable where t P (•) is defined as in the proof of Lemma 3.1 with the following clauses:

• t P (x →y) P(x) ∧ x →y, • t P (x = y) x = y, • t P (φ * ψ) ∃Q, Q P = Q Q ∧ t Q (φ) ∧ t Q (ψ) where P = Q Q is an abbreviation for ∀x (P(x)⇔(Q(x) ∨ Q (x))) ∧ ¬(Q(x) ∧ Q (x)).
t Q is homomorphic for the Boolean connectives and for first-order quantification.

As conjectured in [START_REF] Brochenin | On the almighty wand[END_REF], recently it has been shown that MSO is strictly more expressive than SL( * ) [START_REF] Antonopoulos | Separating graph logic from MSO[END_REF].

Corollary 3.3 SL( * ) satisfiability is decidable.
In order to show that satisfiability in SL( * ) is not elementary recursive, we explain below how to encode finite words as memory states. Let Σ = {a 1 , . . . , a n } be a finite alphabet. A finite word w = a i 1 • a i 2 • • • a im is usually represented as the first-order structure ({1, . . . , m}, <, (P a ) a∈Σ ) where P a is the set of positions labelled by the letter a. Similarly, the word w can be represented as a memory state (s w , h w ) in which • x beg → + x end holds true and, x beg and x end are distinguished variables marking respectively, the beginning and the end of the encoding of w (they do not encode any of its letters),

• the list segment induced from the satisfaction of x beg → + x end has exactly m + 2 locations, and any location l of position j ∈ {2, . . . , m + 1} in the list segment (hence excluding s w (x beg ) and s w (x end )) has exactly i j-1 predecessors. Since s w (x beg ) and s w (x end ) do not encode any position in w, there is no constraint on them.

In Figure 1, we present a memory state encoding the finite word a 1 a 2 a 3 a 1 . Throughout the paper, a memory state (s, h) is encoded as a graph representing the heap such that there is an edge from l to l iff h(l) = l . Locations are represented by letters l (representing themselves), variables x (representing s(x)) or a joker location (representing an unspecified location different from all the other locations present in the graph). Although the graph of h is fully specified, we may omit irrelevant variables in the representation of (s, h). In Figure 1, note that each position of the word corresponds to a unique location in the memory state. For instance, the location l 4 has one predecessor encoding the fact that the fourth letter in the word is precisely the first letter a 1 . The location l 3 has 3 predecessors encoding that fact that the third letter of the word is precisely the third letter a 3 .

Similarly, any memory state (s, h) containing a list segment between x beg and x end and such that any location on the list segment that is different from s(x beg ) and s(x end ) has at most card(Σ) predecessors corresponds to a unique finite word with the above encoding. In this direction, the memory state may contain other dummy locations but they are irrelevant for the representation of the finite word. Moreover, a memory state can encode only one word since x beg and x end are end-markers. x beg l 2 l 3 l 4

x end Proposition 3.4 SL( * ) is not elementary recursive (even its restriction with 5 variables).

Proof Satisfiability of the first-order theory of finite words [START_REF] Stockmeyer | The complexity of decision problems in automata theory and logic[END_REF] is not elementary recursive (this result holds already with three variables). Let us reduce this problem to satisfiability in SL( * ). Let ψ word be the formula specifying a word model:

(x beg → + x end ) ∧ (∀x ((x beg → + x) ∧ (x → + x end )) ⇒ x ≤ card(Σ))
It is then easy to show that given a first-order formula φ over the signature (<, (P a ) a∈Σ ), φ is satisfiable over finite words iff ψ word ∧ t(φ) is satisfiable in SL( * ) where t is defined as follows:

t(x < y) (x → + y) t(∀x ψ) ∀x. ((x beg → + x) ∧ (x → + x end )) ⇒ t(ψ) t(P a i (x)) x = i.
The translation t is homomorphic for Boolean connectives and remember that x = i is a shortcut for a formula in SL( * ) of size O(i) (see Section 2.2). Similarly, x → + y and x ≤ card(Σ) belongs to SL( * ) (see Section 2.2). One can check that if φ contains at most three variables, then ψ word ∧t(φ) contains at most five variables.

As a corollary of Corollary 3.3, we obtain an alternative decidability proof of the entailment problem for the fragment of SL considered in [START_REF] Berdine | A decidable fragment of separation logic[END_REF]. We have established decidability for a fragment of SL larger than the one considered in [START_REF] Berdine | A decidable fragment of separation logic[END_REF] (for which the entailment problem is shown to be in conp) but of higher complexity.

It is probable that the number of variables can be reduced further while preserving non-elementarity, but it is not very essential at this point, for instance by identifying the limits of the words by unique patterns instead of distinguished variables.

A Decidable Fragment of SL with a Restricted Use of -- *

In Section 3, we have seen that SL( * ) satisfiability is decidable whereas satisfiability for full SL will be shown to be undecidable. However, SL( * ) is certainly not the largest decidable fragment of SL. In this section, we investigate another decidable extension of SL( * ) thanks to a restricted use of the magic wand; quantification over disjoint heaps is done only for heaps whose domain has cardinality smaller than some fixed n (details will follow). Since the forthcoming extension is closed under negation, this also corresponds to a restricted use of the operator -- * ¬ .

A Restricted

(s, h) |= φ 1 n -- * ¬ φ 2 iff there is h ⊥ h such that card(dom(h )) ≤ n, (s, h ) |= φ 1 and (s, h * h ) |= φ 2 .
SL( * + n -- * ¬ ) allows to encode the restricted use of the magic wand in the Hoare-like proof systems as in the backward-reasoning form rule (MUBR) recalled below, see also [START_REF] Reynolds | Separation logic: a logic for shared mutable data structures[END_REF]:

{(∃z x → z) * ((x → y) -- * φ)} [x] := y {φ} It is easy to show that (x → y) -- * φ is equivalent to ¬((x → y) 1 -- * ¬ ¬φ).
Typically, whenever the left argument of a formula with outermost connective -- * has only models of bounded size, this trick can be applied again. Let us push a bit further this idea.

Bounding the Cardinal of Heap Domains

Let SL -( * ) be the fragment of SL( * ) defined by the grammar below and whose formulae are also interpreted over memory states:

φ ::=⊥ | x → y | size ≤ k | size = k | φ * φ | φ ∨ φ | φ ∧ φ | ∃ x φ
where k ∈ N. Since SL -( * ) is not closed under negation, it makes sense to consider both size ≤ k and size = k. Anyhow, we shall show that size ≤ k can be expressed differently. The satisfaction relation is defined as for SL with the obvious following update:

(s, h) |= size ≤ k iff card(dom(h)) ≤ k. Observe that size = k with k ≥ 1 is also equivalent to the formula below (in SL -( * )): ∃ x 1 , . . . , x k ((∃ y x 1 → y) * • • • * (∃ y x k → y)) Let | φ | denote the size of a formula φ in SL -( * )
with the natural numbers encoded with a unary representation. In order to establish the above lemma, it is sufficient to observe that

Lemma 4.1 For any φ ∈ SL -( * ), if (s, h) |= φ then card(dom(h)) ≤ | φ |.
φ -- * ψ is equivalent to ¬(φ | φ | -- * ¬ ¬ψ) whenever φ ∈ SL -( * ) and ψ ∈ SL.

Symbolic Disjoint Heaps

In order to show decidability for SL( * + n -- * ¬ ), we define a reduction into SL( * ). The translation is based on a simple observation: since a formula with outermost connective n -- * ¬ requires the existence of a disjoint heap whose domain size is at most n, this new heap can be encoded by a set of pairs of variables of cardinality n. Hence, a heap of size at most n disjoint from (s, h) can be represented symbolically by a set C = {(y 1 , z 1 ), . . . , (y n , z n )} such that {s(y 1 ), . . . , s(y n )} ∩ dom(h) = ∅ and s(y i ) = s(y j ) implies s(z i ) = s(z j ), naturally encoding the heap h(C) = {s(y i ) → s(z i ) : s(y i ) = nil, 1 ≤ i ≤ n} assuming that nil is a distinguished value represented by some dedicated variable null. This is the only place in the paper where nil shall be used and as usual we require that nil cannot belong to the domain of heaps (see Section 2.1). The set C = {(y 1 , z 1 ), . . . , (y n , z n )} represents a heap with at most n memory cells, even though C contains exactly n pairs. However, whenever s(y i ) = nil, the pair (y i , z i ) does not encode any new memory cell. In terms of formulae, (y i , z i ) encodes a memory cell iff y i = null holds true. This shall be intensively used in forthcoming formulae.

Let us provide now the formal definitions. A symbolic disjoint heap C for the memory state (s, h) is a finite set of pairs of variables {(y 1 , z 1 ), . . . , (y n , z n )} such that

• {s(y 1 ), . . . , s(y n )} ∩ dom(h) = ∅. • For 1 ≤ i, j ≤ n, s(y i ) = s(y j ) implies s(z i ) = s(z j ).
The heap represented by C, written h(C), is defined by h(C)

def = {s(y i ) → s(z i ) : s(y i ) = nil, 1 ≤ i ≤ n}. Observe that card(dom(h(C))) ≤ n and h(C) ⊥ h. C is said to be of length n.
Lemma 4.3 Given a memory state (s, h) and h such that h ⊥ h and card(dom(h )) ≤ n, there exists a symbolic disjoint heap C of length n such that h = h(C) and s may differ from s at most for the variables occurring in C.

The proof is by an easy verification by symbolically representing h with new variables, whence the store s .

Below we introduce simple formulae useful to separate a symbolic disjoint heap or to extend a symbolic disjoint heap by another symbolic disjoint heap. Given

C = {(y 1 , z 1 ), . . . , (y n , z n )}, C 0 = {(y 0 1 , z 0 1 ), . . . , (y 0 n , z 0 n 0 )} and C 1 = {(y 1 1 , z 1 1 ), . . . , (y 1 n , z 1 n 1 )}, we write C = C 0 * C 1 to denote the conjunction of the formulae below: • h(C) is included in h(C 0 ) ∪ h(C 1 ): 1≤i≤n ( 1≤i≤n 0 y 0 j = y i ) ∨ ( 1≤i≤n 1 y 1 j = y i ) • h(C 0 ) ∪ h(C 1 ) is included in h(C): 1≤i≤n 0 y 0 j = null ⇒ 1≤i≤n y i = y 0 j ∧ 1≤i≤n 1 y 1 j = null ⇒ 1≤i≤n y i = y 1 j • h(C 0 ) and h(C 1 ) encode a function: 1≤j,j ≤n 0 (y 0 j = y 0 j ⇒ z 0 j = z 0 j ) ∧ 1≤j,j ≤n 1 (y 1 j = y 1 j ⇒ z 1 j = z 1 j )
• h(C 0 ) and h(C 1 ) are disjoint:

1≤i≤n 0 1≤i≤n 1 ((y 0 j = null) ∨ (y 1 j = null)) ⇒ (y 0 j = y 1 j )
We provide a few lemmas whose easy proofs are omitted. However, they will be helpful to prove correctness in Section 4.4.

Lemma 4.4 Let C be a symbolic disjoint heap of length n for (s, h) and C 0 = {(y 0 1 , z 0 1 ), . . . , (y 0 n , z 0 n 0 )} and C 1 = {(y 1 1 , z 1 1 ), . . . , (y 1 n , z 1 n 1 )} be symbolic disjoint heaps whose variables do not occur in C. Let s be a store that may differ from s at most for the variables occurring in C 0 and C 1 . Assume moreover that (s , h)

|= C = C 0 * C 1 . Then, h(C 0 ) and h(C 1 ) are symbolic disjoint heaps for (s , h), h(C 0 ) ⊥ h(C 1 ) and h(C 0 ) * h(C 1 ) = h(C).
Again, the proof is by easy verification and we can also get a converse property.

Lemma 4.5 Let C be a symbolic disjoint heap of length n for (s, h). Let h 0 * h 1 = h(C). There exist symbolic disjoint heaps C 0 and C 1 for (s , h) such that variables in C, C 0 and C 1 are mutually disjoint, s may differ from s at most for the variables occurring in

C 0 and C 1 , h 0 = h(C 0 ), h 1 = h(C 1 ) and (s , h) |= C = C 0 * C 1 .
Let us now consider the corresponding lemmas to build disjoint heaps. Lemma 4.6 Let C 0 be a symbolic disjoint heap for (s, h), C and C 1 be symbolic disjoint heaps whose variables do not occur in C 0 , and such that (s , h) |= C = C 0 * C 1 , where s may differ from s at most for the variables occurring in C and C 1 . Then, C and C 1 are symbolic disjoint heaps for (s , h).

We can also get a converse property. Lemma 4.7 Let C 0 be a symbolic disjoint heap for (s, h) and, h be disjoint from h * h(C 0 ) and the cardinal of its domain is less than n. There exists a symbolic disjoint heap C 1 of length n for (s, h)

such that h = h(C 1 ), h * h(C 0 ) = h(C 0 ∪ C 1 ) and (s , h) |= (C 0 ∪ C 1 ) = C 0 * C 1 (
s may differ from s at most for the variables occurring in C 1 ).

The Translation

The recursive translation function is of the form t(ψ, C, F ) where ψ is a subformula to be translated, C has the format of some symbolic disjoint heap and F ∈ {0, 1} is a flag that specifies whether ψ is evaluated under h(C)

(F = 0) or under h * h(C) (F = 1).
Before defining the recursive map t, let us mention that a formula φ is translated into t(φ, ∅, 1).

• t(x = x , C, F ) = x = x . • t(x → x , C, 1) = (x → x ) ∨ t(x → x , C, 0). • t(x → x , C, 0) = (y,z)∈C (y = null ∧ y = x ∧ z = x ).
• t is homomorphic for Boolean connectives and first-order quantification (up to renaming quantified variables to avoid capturing variables of C).

• t(ψ 0 -- * ¬ ψ , C, F ) = t(ψ, ∅, 0) ∧ t(ψ , C, F ) • t(ψ n -- * ¬ ψ , C, F ) for n ≥ 1 is equal to ∃v (C ∪ C ) = C * C ∧ t(ψ, C , 0) ∧ t(ψ , C ∪ C , F ) ∧ (y,z)∈C ¬alloc (y)
where v is a sequence of n pairs of fresh variables from the symbolic disjoint heap C .

• t(ψ * ψ , C, F ) with C of length n is equal to ∃v (t(ψ, C 0 , F ) * t(ψ , C 1 , F )) ∧ C = C 0 * C 1
where v is a sequence of 2n pairs of fresh variables from the symbolic disjoint heaps C 0 and C 1 of length n.

Even though in the worst-case there is an exponential number of ways to divide a heap into two disjoint heaps, our translation remains in polynomial time. The soundness of the translation is guaranteed by the lemma below whose proof is by structural induction and uses the previous lemmas.

Lemma 4.8 Let C be a symbolic disjoint heap for (s, h). For all formulae

ψ in SL( * + n -- * ¬ ), we have • (s, h(C)) |= ψ iff (s, h) |= t(ψ, C, 0), and
• (s, h * h(C)) |= ψ iff (s, h) |= t(ψ, C, 1).
Proof The proof is by structural induction on ψ. The induction hypothesis is of the following form: for every ψ whose size is strictly smaller than the size of ψ, if C be a symbolic disjoint heap for (s , h ), then we have

(1) (s , h(C )) |= ψ iff (s , h ) |= t(ψ , C , 0), and (2)
(s , h * h(C )) |= ψ iff (s , h ) |= t(ψ , C , 1).
The base case for atomic formulae is by an easy verification as well as the cases in the induction step for Boolean connectives and first-order quantification.

We treat below the case ψ = ψ 1 * ψ 2 , the case ψ = ψ 1 n -- * ¬ ψ 2 can be treated analogously using Lemmas 4.6 and 4.7.

Suppose (s, h(C)) |= ψ 1 * ψ 2 . There exist h 1 and h 2 such that h 1 * h 2 = h(C), (s, h 1 ) |= ψ 1 and (s, h 2 ) |= ψ 2 . By Lemma 4.5, there exist symbolic disjoint heaps C 1 and C 2 (with fresh variables) for (s , h) such that s may differ from s at most for the variables occurring in

C 1 ∪C 2 , h 1 = h(C 1 ) and h 2 = h(C 2 ). Since each C i is a disjoint symbolic heap for (s , h i ), by the induction hypothesis, (s , h) |= t(ψ 1 , C 1 , 0) and (s , h) |= t(ψ 2 , C 2 , 0). Moreover, (s , h) |= C = C 1 * C 2 (observe that satisfaction of C = C 1 * C 2 depends only on the store). Hence, (s, h) |= ∃v (t(ψ 1 , C 1 , 0) * t(ψ 2 , C 2 , 0)) ∧ C = C 1 * C 2
where v is the sequence of variables from C 1 and C 2 . Consequently, we have

(s, h) |= t(ψ 1 * ψ 2 , C, 0). Similarly, suppose (s, h * h(C)) |= ψ 1 * ψ 2 . There exist h 1 , h 2 , h 1 and h 2 such that h 1 * h 2 = h(C), h 1 * h 2 = h, (s, h 1 * h 1 ) |= ψ 1 , (s, h 2 * h 2 ) |= ψ 2 .
By Lemma 4.5, there exist symbolic disjoint heaps C 1 and C 2 (with fresh variables) for (s , h) such that s may differ from s at most for the variables occurring in C 1 , C 2 , h 1 = h(C 1 ) and h 2 = h(C 2 ). Since each C i is a symbolic disjoint heap for (s , h i ), by the induction hypothesis,

(s , h 1 * h(C 1 )) |= t(ψ 1 , C 1 , 1) and (s , h 2 * h(C 2 )) |= t(ψ 2 , C 2 , 1). Moreover, (s , h) |= C = C 1 * C 2 . Hence, (s, h) |= ∃v (t(ψ 1 , C 1 , 1) * t(ψ 2 , C 2 , 1)) ∧ C = C 1 * C 2 So, (s, h) |= t(ψ 1 * ψ 2 , C, 1). Now suppose (s, h) |= t(ψ 1 * ψ 2 , C, 0), that is (s, h) |= ∃v (t(ψ, C 0 , F ) * t(ψ , C 1 , F )) ∧ C = C 0 * C 1
where v corresponds to the sequence of variables from the fresh symbolic disjoint heaps C 0 and C 1 . Hence there exists a store s that may differ from s at most for the variables occurring in v such that

(s , h) |= (t(ψ 1 , C 0 , 0) * t(ψ 2 , C 1 , 0)) ∧ C = C 0 * C 1
By the induction hypothesis, (s , h(C This leads to the main result of this section. Proof (II) is a consequence of (I) by using the decidability of SL( * ) satisfiability (see Section 3). (I) By Lemma 4.8, for every memory state (s, h), we have (s, h * h(∅)) |= ψ iff (s, h) |= t(ψ, ∅, 1) where t(ψ, ∅, 1) is an SL( * ) formula and ∅ denotes the empty symbolic disjoint heap. Moreover, we have seen that t(ψ, ∅, 1) can be built in polynomial-time assuming that the natural numbers are represented with a unary encoding in ψ. Since h * h(∅) is equal to h, the formulae ψ and t(ψ, ∅, 1) hold true at the same memory states.

We then obtain the following interesting corollary. Corollary 4.10 Satisfiability for SL restricted to formulae such that the left argument of any -- * -formula belongs to SL -( * ) is decidable.

Expressing Advanced Arithmetical Constraints in SL(-- * )

In this section, we show how SL(-- * ) can be used to express cardinality constraints on finite sets of locations that are defined by logical predicates. Given a formula φ(x) with free variable x and a model (s, h), we write φ to denote the number of locations l such that (s[x → l], h) |= φ(x). As a consequence of SL ≡ SO, for all formulae φ(x) and ψ(x) from either SL or SO, there is a formula that can capture a constraint of the form φ < ψ. However, in order to show SL ≡ SO, we shall need to establish this expressiveness result for some specific formulae φ and ψ. More precisely, this is done with the predicates "immediate successor of z", φ(x) = x → z, whence φ is the number of predecessors of z. In Section 5.2, numbers of predecessors are compared. The proof of this result is subject to technical complications but its essence is not so intricate, and it is better illustrated by encoding other kinds of cardinality constraints. For this reason, we make a slight detour in our presentation by first sketching the encoding of the cardinality constraints for the predicate reachable z (x) = z→ * x. This turns out to be a bit simpler to define, and already it provides the key ingredients of our proof. This can be viewed as a warm-up before dealing with the predicate x → z.

Comparing Two List Lengths

Let us first restrict our attention to models composed of two acyclic lists starting at x and y respectively, with no other allocated cells, and with the additional constraint that no location is reachable from x and y simultaneously. We aim now at expressing the fact that both lists have the same length n using the magic wand. To do so, we can say that there exist n locations l 1 , . . . , l n that are not allocated and for which there is a one-one correspondence between these locations and the ones of the list starting at x, and on the other hand there is another one-one correspondence between these same locations and the ones of the list starting at y. The gain for considering non allocated cells is that the one-one correspondence can be materialized by allocating l 1 , . . . , l n so that each of them points to the cell it is in correspondence with. The trickiest point is then how to materialize the guess of the locations l 1 , . . . , l n in such a way that it is possible to refer to them later without confusing them with the cells that were initially allocated. To do so, we may observe that in the original model, all locations have at most one predecessor. We can thus identify some extra locations l 1 , . . . , l n if we impose them to admit exactly two predecessors. With these intuitions in mind, the property that the length of the list starting at x is equal to the length of the list starting at y can be expressed by a formula of the form below:

φ -- * ¬ (ψ -- * ¬ ϕ(x, y)) ∧ (ψ -- * ¬ ϕ(y, x))
where:

• φ expresses that all the locations have either 0 or 2 predecessors,

• ψ expresses that all the locations have either 0 or 1 predecessor,

• ϕ(x, y) expresses the situation depicted in Figure 2: 1. all the locations reachable from x have exactly two immediate predecessors, except x that has one predecessor only; 2. among these one or two predecessors, the one that is not reachable from x has itself exactly two immediate predecessors which themselves do not have immediate predecessors; 3. all extra allocated locations are only the ones of the list y. We claim that there exist such formulae φ, ψ, and ϕ(x, y) in SL, although we do not plan to provide details herein. We shall do it for constraints about the numbers of predecessors. Before doing so, let us first notice that it is not difficult to adapt this technique to express richer constraints on the length of two lists, as for instance the property that one list is one cell longer than another one, and thus using a reduction to counter machines similar with [START_REF] Bozga | Quantitative separation logic and programs with lists[END_REF], this entails the undecidability of SL(-- * ). However, we were not able to encode SO by using cardinality constraints on list lengths, but rather on comparing numbers of predecessors.

Let us also remark that the above construction relies on the fact that in the considered models, all the locations have at most one predecessor. In the general case, it could be harder to distinguish the locations that are initially allocated in the models, and the ones that correspond to the guessed locations l 1 , . . . l n . This last point justifies why the construction presented at the next section is a bit more technical. Actually, we shall rely on a reduction to models where all the locations have at least three predecessors. However, the key ideas are essentially the same.

Comparing the Numbers of Predecessors

In this section, we show how SL(-- * ) can express properties of the form x + c y + c with c, c ∈ N and ∈ {=, ≥, ≤} where x denotes the number of predecessors of s(x) in a model. This is a key property in the forthcoming proof establishing that weak second-order logic is equivalent to SL(-- * ). Note that x c can be easily expressed in SL(-- * ), even without magic wand (indeed c is a fixed value). By contrast, expressing a constraint x y + c is natural in second-order logic, for instance by introducing an adequate finite binary relation between the predecessors of x and those of y. We show below that this can be done also in SL(-- * ) but requires much more work.

In a nutshell, expressing constraints of the form x + c y + c will be done as follows. First, thanks to Boolean connectives it is sufficient to express properties of the form x+c ≤ y+c with c, c ∈ N (strictly speaking, we can assume that c × c = 0). Moreover, x + c ≤ y + c is precisely equivalent to the fact that for all n ∈ N, y-c ≤ n implies x-c ≤ n (indeed N ≤ N iff for every M ≥ 0, we have N ≤ M implies N ≤ M ). Quantification over the set of natural numbers will be simulated by a quantification over disjoint heaps in which n is exactly the cardinal of their domains. Such a quantification is performed thanks to the magic wand and we require that disjoint heaps are segmented and current heap is flooded (to be defined below). A model (s, h) is segmented whenever dom(h) ∩ ran(h) = ∅ and no location has strictly more than one predecessor. For instance, the heap h 2 in Figure 4 restricted to cells labelled by 2 is segmented. (s, h) is flooded when no location has one or two predecessors. The store s is indeed irrelevant for these concepts. These conditions on heaps are needed in order to guarantee that the heaps obtained from the original heap and the disjoint heaps easily determine which part of the heap has been added. A nice feature is that the fact of being flooded or segmented can be naturally expressed in SL(-- * ) (see Lemma 5.1). Finally, any heap such that x, y ≥ 3 can be extended to a flooded heap without modifying the numbers of predecessors for x and y, respectively. This explains why the term 'flooded' has been chosen. In the case x ≤ 2 or y ≤ 2, we perform a simple case analysis and we obtain Boolean combinations of constraints of the form x c or y c (that can be easily handled, details will follow).

Lemma 5.1 There are formulae flooded and seg in SL(-- * ) such that for every model (s, h),

(I) (s, h) |= flooded iff (s, h) is flooded, (II) (s, h) |= seg iff (s, h) is segmented.
Proof It is easy to check that the formulae below do the job.

• flooded ∀x. ( x = 0 ∨ x > 2). • seg ∀x, y. (x → y ⇒ ( y = 1 ∧ ¬(∃z z → x ∨ y → z))).
Note that the formulae x = 0, x > 2 and y = 1 are indeed formulae without separating connectives. Now, we present a few crucial definitions about specific patterns in memory states, namely markers. A [resp. strict] marker in (s, h) is a sequence of distinct locations l, l 0 , . . . , l n for some n ≥ 0 such that • h(l 0 ) = l [resp. and dom(h) = {l 0 , . . . , l n }],

• for every i ∈ {1, . . . , n}, h(l i ) = l 0 and l i = 0,

• l 0 = n.
The marker is said to be of degree n with endpoint l (n-marker). Markers have simple structure with natural graphical representation. In Figure 3, we present an heap h containing a 2-marker and a 3-marker, both having the same endpoint l. Note that there are disjoint heaps h 1 and h 2 such that h = h 1 * h 2 , h 1 has a strict 2-marker and h 2 has a strict 3-marker.

Figure 3 An heap with a 2-marker and a 3-marker. l A model (s, h) is said to be k-marked whenever there is no location in dom(h) that does not belong to a marker of degree k. Moreover, it is strictly k-marked when no distinct markers share the same endpoint (no aliasing).

Markers are essential building blocks to express a constraint of the form x -c ≤ n with c, n ∈ N. Before presenting the formal treatment, let us explain the principle of the encoding. Assume that h 1 is a flooded heap (i.e, no location has one or two predecessors), and h 2 is a segmented heap such that 1. h 1 and h 2 are disjoint, 2. card(dom(h 2 )) = n, 3. h 1 * h 2 does not contain locations with two predecessors, 4. if a location l has exactly one predecessor l in h 1 * h 2 then l has no predecessor and l does not belong to dom(h 1 * h 2 ).

Hence, h 1 * h 2 is almost flooded since the only reason for not being flooded is possibly to contain isolated memory cells from h 2 . Figure 4 presents two heaps h 1 and h 2 satisfying the above conditions. Cells of the heap h 2 are labelled by 2. Note also that h 1 * h 2 is not flooded because of some isolated cells from h 2 such as l →l . Obviously, h 1 * h 2 does not contain any 2-marker and in particular no predecessor of s(x) is the endpoint of some 2-marker.

A c-completion of h 1 * h 2 consists in adding a disjoint heap h = h 1 * h 2 such that 1. h 1 is 1-marked, 2. h 2 is strictly 2-marked and contains exactly c distinct 2-markers.

Consider the number of 2-markers in the heap h 1 * h 2 * h resulting from such a completion. First, observe that strictly more than c 2-markers can be present since an isolated memory cell from h 2 and a 1-marker from h 1 may produce a 2-marker in h 1 * h 2 * h (see the locations l 1 , l 2 , l 3 and l 4 in Figure 5) Second, observe that at least the c 2-markers from h are still in h 1 * h 2 * h , because the definition of * prevents a 2-marker from combining with a 1marker to form a 3-marker. Observe also that the insertion of markers of degree strictly less than 3 in the almost flooded heap allows to safely identify them as markers in the new model. Consequently, there are at most n + c predecessors of s(x) that are endpoints of 2-markers in h 1 * h 2 * h . Now, we say that h 1 * h 2 * h is x-completed whenever all the predecessors of s(x) are endpoints of 2-markers. Figure 5 presents a 2-completion of h 1 * h 2 (cells in h 1 are those pointing to x and cells in h 2 are labelled by 2 whereas the cells of the 2-completion are represented by dashed arrows. The heap restricted to dashed edges satisfies complete 2 -it is composed of two 2-markers and two 1-markers. Moreover, the total resulting heap is x-completed: every predecessor of x is an endpoint of some 2-marker.

It is easy to observe that x -c ≤ n iff there is a c-completion h of h 1 * h 2 such that h 1 * h 2 * h is x-completed (see the exact statement in Lemma 5.3). Lemma 5.2 below states that the heaps obtained by completion can be specified in SL(-- * ). (I) completed(x) is equal to:

∀y y → x ⇒ (∃z z → y ∧ z = 2 ∧ ∀z z → z ⇒ z = 0)) (II)
In order to define complete c we perform a case analysis and introduce below a few formulae. First, ψ 0 and let ψ n be the formula below:

∃x 1 • • • x n , y 1 • • • y n ( i =j x i = x j ) ∧ ( n i=1 ((y i → x i ) ∧ y i = 2 ∧ ∀z z → y i ⇒ z = 0))
ψ c ∧ ¬ψ c+1 states that the model contains exactly c 2-markers with disjoint endpoints. Let ψ cases be the formula below:

∀x alloc (x) ⇒ (ψ 1 extr (x) ∨ ψ 2 extr (x) ∨ ψ 1 end (x) ∨ ψ 2 end (x))
where ψ i extr (x) [resp. ψ i end (x)] states that h(s(x)) [resp. h(h(s(x)))] is the endpoint of some i-marker. By way of example, ψ 1 extr (x) is defined as follows:

x = 1 ∧ (∀y (y → x) ⇒ y = 0) ∧ (∃y x → y ∧ ¬∃z y → z)
The formula complete c is defined as the conjunction ψ c ∧¬ψ c+1 ∧ψ cases .

We say that two heaps h 1 and h 2 are completely disjoint if (dom(h 1 )∪ran(h 1 ))∩ (dom(h 2 ) ∪ ran(h 2 )) = ∅. Moreover, a pair of heaps (h 1 , h 2 ) is said to be compatible whenever

• (s, h 1 ) is flooded, • (s, h 2 ) is segmented,
• h 1 and h 2 are completely disjoint.

Note that h 1 and h 2 from Figure 4 are not compatible since ran(h 1 ) ∩ ran(h 2 ) = ∅.

Lemma 5.3 below presents the formal statement related to the intuitive explanations that were already presented. Lemma 5.3 Let s be a store and (h 1 , h 2 ) be a compatible pair of heaps such that x has i predecessors in h 1 for some i ≥ 1. Then the following two are equivalent:

(i) (s, h 1 * h 2 ) |= complete c -- * ¬ completed(x), (ii) card(dom(h 2 )) ≥ (i -c). Proof Proof of (i) → (ii).
Assume (i). Let h 1 be an 1-marked heap, h 2 be a strict 2-marked heap with exactly c 2-markers, and

h = h 1 * h 2 * h 1 * h 2 with (s, h) |= completed(x).
Then, the set of endpoints from 2-markers in h includes h -1 1 (s(x)) and its cardinal b satisfies b ≥ i. Markers of degree 2 witnessing the satisfaction of completed(x) do not come from h 1 since h 1 is flooded. So, either they come directly from h 2 or they are markers of degree 1 which have been converted into markers of degree 2 thanks to isolated cells from h 2 . Let a be the number of converted markers, then b ≤ a + c. Since none of h 1 , h 2 contributes to the conversion of an 1-marker, the amount of converted markers is bounded by card(dom(h 2 )), i.e. card(dom(h 2 )) ≥ a. Consequently,

i -c ≤ b -c ≤ a ≤ card(dom(h 2 )).
Proof of (ii) → (i). Assume (ii). In the sequel, we shall introduce locations that are involved in 2markers; the exponents below in the locations refer to the following intended positions in the schema

A C ↓ D B
for 2-markers (of course "A" and "B" could have been permuted). By letting

N = i-c, we have card(dom(h 2 )) ≥ N . The set of locations h -1 1 (s(x)) (set of predecessors of s(x) in h 1 ) contains N +c ele- ments that can be written l D 1 , . . . , l D N +c . Since card(dom(h 2 )) = card(ran(h 2 )), there exist at least N locations l C 1 , . . . , l C N in ran(h 2 ). Moreover, since X = dom(h 1 * h 2 ) ∪ ran(h 1 * h 2 ) is finite, there exist distinct locations l B 1 , . . . , l B N that are not in X. Let h 1 be the heap disjoint from (h 1 * h 2 )
with the memory cells below:

h 1 = {l B 1 →l C 1 , l C 1 →l D 1 , . . . , l B N →l C N , l C N →l D N } Let h 2 be heap disjoint from (h 1 * h 2 * h 1 )
that contains c 2-markers with endpoints l D N +1 , . . . , l D N +c respectively. It is easy to check that (s,

h 1 * h 2 ) |= complete c and (s, h 1 * h 2 * h 1 * h 2 ) |= completed(x), which is sufficient to guarantee (i).
Satisfying that for all n ∈ N, y -c ≤ n implies x -c ≤ n suggests a simple contest between two players: Spoiler aims at disproving that the constraint holds, and Duplicator tries to prove it. The whole play of the contest is depicted on Figure 6. The steps of context go as follows:

1. We start with an initial heap h 0 without any hypothesis; if x ≤ 2 or y ≤ 2, the contest is over (these cases are handled elsewhere), otherwise the contest may start. 2. Spoiler reduces to the case of a flooded model h 1 (whole heap on the second frame of Figure 6) by adding cells (the five new arrows in the second frame) in a controlled way-this will be formalized later. 3. Spoiler picks a segmented heap h 2 (the three new arrows in the third frame) such that card(dom(h 2 )) equals n and (h 1 , h 2 ) is compatible. Figure 6 summarizes a contest with a successful outcome for Duplicator.

The above contest supposes that it is possible to characterize the heaps h 1 * h 2 such that (h 1 , h 2 ) is compatible. A heap h is said to be almost flooded whenever there exist h 1 and h 2 such that h = h 1 * h 2 and (h 1 , h 2 ) is compatible.

Lemma 5.4 Let (s, h) be a memory state. h is almost flooded iff (s, h) |= flooded with flooded (∀x, y (x → y∧ y = 1) ⇒ ( x = 0∧¬alloc (y)))∧(¬(∃x x = 2)).
The proof of Lemma 5.4 is by an easy verification. It remains to define the formula contest(x, y, c, c ) that defines a contest and that is essential to establish Theorem 5.5 below.

flooded ∧ ((seg ∧ x = 0 ∧ y = 0) -- * ( flooded ⇒ ((complete c -- * completed(y)) ⇒ (complete c -- * completed(x))))).
Theorem 5.5 For c, c ≥ 0, there is a formula φ in SL(-- * ) of quadratic size in c+c such that for every model (s, h), we have (s, h) |= φ iff x+c ≤ y+c . Proof By packing the previous developments, we shall show that

(♥) When h is flooded, (s, h) |= contest(x, y, c, c ) iff x + c ≤ y + c .
Even though h is not necessarily flooded, when x ≥ 3 and y ≥ 3 it can be safely extended to a flooded heap without modifying the number of predecessors of x and y. When x ≤ 2 or y ≤ 2 such an extension is not anymore possible. Nevertheless, by a simple case analysis, x+c ≤ y+c is equivalent y,c,c ) and

to i≤2 ( x = i ∧ y ≥ i + c -c ) ∨ i≤2 ( y = i ∧ x ≤ i + c -c), which can be easily expressed in SL(-- * ). Let us consider φ def = φ special ∨ φ main with φ main ( x = 0 ∧ y = 0) -- * ¬ contest(x,
φ special i≤2 ( x = i ∧ y ≥ i + c -c ) ∨ i≤2 ( y = i ∧ x ≤ i + c -c)
First, it is clear that x + c ≤ y + c and ( x ≤ 2 or y ≤ 2) is equivalent to (s, h) |= φ special . Now, suppose that x ≥ 3 and y ≥ 3. Assuming that (♥) holds, we have the following equivalences:

(1) (s, h) |= ( x = 0 ∧ y = 0) -- * ¬ contest(x, y, c, c ).

(2) There is h ⊥ h such that (s, h ) |= ( x = 0 ∧ y = 0) and (s, h * h ) |= contest(x, y, c, c ).

(3) There is h ⊥ h such that (s, h ) |= ( x = 0 ∧ y = 0) and (s, h * h ) |= flooded and y + c ≥ x + c (in h * h ) by (♥).

(

) y + c ≥ x + c in h. 4
Observe that x and y in h are equal to their values in h * h since (s, h ) |= ( x = 0 ∧ y = 0). Moreover, ( 4) implies (3) since it is always possible to extend a model into a flooded one while preserving x and y (when x ≥ 3 and y ≥ 3).

It remains to show that (♥) holds true. The statements below are equivalent (h is assumed to be flooded):

1. (s, h) |= contest(x, y, c, c ). 2. for every segmented disjoint heap h e such that (s, h e ) |= x = y = 0, if (s, h * h e ) |= complete c -- * ¬ completed(y) and h * h e is almost flooded, then (s, h * h e ) |= complete c -- * ¬ completed(x). 3.
for every segmented disjoint heap h e such that (s, h e ) |= x = y = 0, there exist h * h e = h * h e such that (h , h e ) is compatible and the number of predecessors of x and y in h are equal to those of x and y in h , if card(dom(h )) ≥ y -c, then card(dom(h )) ≥ x -c . 4. for every n ≥ 0, we have n ≥ y -c in h implies n ≥ x -c in h. 5. x + c ≤ y + c . Lemma 5.4 is used from (1) to (2). Lemma 5.3 is used for the equivalence between ( 2) and ( 3). Moreover, one needs to observe that h is flooded, h e is a disjoint segmented heap, (s, h e ) |= x = y = 0 and h * h e is almost flooded iff there are h * h e = h * h e such that (h , h e ) is compatible and the number of predecessors of x and y in h are equal to those of x and y in h . Equivalence between (3) and ( 4) is due to the fact that for every n ≥ 0 there is a heap h e such that card(dom(h e )) = n, (h, h e ) is compatible and (s, h e ) |= x = y = 0.

In Section 6, only constraints of the form x + c ≤ y + c with c, c ≤ 3 are used. In particular, this means that for the forthcoming formulae using advanced arithmetical constraints, c + c can be viewed as a constant.

SL(-- * ) is Equivalent to SO

By combining Proposition 2.5 and Proposition 2.6, we know that DSO is at least as expressive as SL and there is a logarithmic-space translation from SL into DSO (logarithmic-space reductions are closed under compositions). Now, we show the converse.

A syntactic convention. In the sequel, without any loss of generality, we require that the sentences in DSO satisfy the Barendregt convention as far as the second-order variables are concerned. Assuming that a sentence contains the second-order variables P 1 , . . . , P n , quantifications over P j can only occur in the scope of quantifications over P 1 , . . . , P j-1 (we call this restriction the extended Barendregt convention). Typically, we exclude sentences of the form ∃P 2 ∃P 1 φ. Observe that any sentence in DSO can be transformed in logspace into an equivalent sentence verifying this convention. The quantifier depth of the occurrence of a subformula ψ in φ is therefore the maximal i such that this occurrence is in the scope of ∃P i (by convention it is zero if it is not in the scope of any quantification).

Encoding environments as specific parts of the memory state. Before defining the translation of a DSO sentence φ, let us explain how environments can be encoded in SL. First, let us introduce some terminology. We say that a location l is an extremity in a given model if l has at least one predecessor and no predecessor of l has a predecessor. The following formula states that s(x) is an extremity: extr(x) (¬∃y. (y → x ∧ ∃z.z → y)) ∧ (∃y. y → x). In the particular case of a marker, an extremity is the location that points to the endpoint of the marker.

An environment is encoded as a finite set of new markers distinct from the original heap; this heap is called the environment heap (and it is written h E ). The main idea is that a pair of locations (l, l ) belongs to the interpretation of a dyadic second-order variable if l and l are the endpoints of two markers of h E that have respectively degrees d and d + 1.

Let us illustrate this idea on a simple example. Assume we want to express in SL the pure SO sentence "all finite orders have a minimal element", stated by the formula ∀P.φ min (P), with φ min (P)   ∀x, y.P(x, y) ⇒ P(x, x) ∧ P(y, y) ∧ ∀x, y. P(x, y) ∧ P(y, x) ⇒ x = y ∧ ∀x, y, z. P(x, y) ∧ P(y, z) ⇒ P(x, z)   ⇒ ∃x.∀y.P(y, x) ⇒ x = y.

We could actually illustrate the idea with any other SO sentence using one SO variable only, with this variable quantified in outermost position. Let P(x, y) be the SL formula

P(x, y) ∃x , y .(x → x ∧ y → y ∧ x + 1 = y ).
This formula expresses that x and y are the endpoints of two markers of consecutive degrees. To any heap h, we can associate the binary relation Ph composed of pairs of such locations. Conversely, any finite binary relation on locations is realized by some Ph . As a consequence, the SO formula ∀P.φ min (P) is satisfied by the empty heap if and only if the SL formula -- * φ min ( P) is.

The generalization of this encoding to arbitrary formulas raises several problems. The first problem is to distinguish the environment heap from the the original one (in the example above, this is solved by restricting ourselves to an original empty heap, but this is not possible in general). In the previous section, we solved this issue by first extending the original heap to a flooded heap, and then by using markers of small degrees (one or two) that were clearly distinct from the original heap. The same approach is not possible here, because one may need arbitrarily large degrees. Transforming an original heap into a flooded one in a controlled way is possible for counting the number of predecessors (see Section 5), but it might be much more difficult if the property of interest is not just a property on the number of predecessors, but an arbitrary second-order property. For all these reasons, we adopt a different strategy, and we ensure that the degree of a marker in h E is strictly greater than the maximal number of predecessors of any location from the original heap. Nonetheless, our investigation on counting the number of predecessors is precious (see Section 5), and will be used when expressing that two endpoints l, l are consecutively marked.

The second problem is, given a pair (l, l ) of locations marked by markers of consecutive degrees, to determine the second-order variable P i whose interpretation contains (l, l ). In the example above, we only had one secondorder variable, but we may not reduce to the case of a unique second-order variable in general. To do so, we impose some more structure on h E . First, for any natural number n, there is at most one extremity with degree n in h E . The spectrum of h E is then defined as the finite set of natural numbers n for which there is a marker of degree n in h E . Second, we require that the spectrum of h E , depicted as a marking of the sequence of naturals, has the following shape for some a, b ∈ N (we later call such a spectrum a clean spectrum). This simple and regular structure makes the characterisation of well-formed environment heaps easier at every step of the translation (in particular, every time the environment is extended by a new quantified second-order variable). In order to identify markers that are attached to a given second-order variable,

empty . . . • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • empty • • • • . . .
1. we ensure that the markers of a given second-order variable follow each others in a given interval, 2. these intervals do not overlap for two distinct second-order variables, 3. there is no unused space between these intervals. This is achieved by introducing, for each P j , two variables z m j and z M j that are placed on the upper and lower bound of the interval of the interpretation of P j . For technical reasons, mainly related to bootstrapping, we also consider the two distinguished variables z m 0 and z M 0 . So, the spectrum of h E can be graphically depicted as

. . . • • • • z m 0 • • z M 0 • bootstrap z m 1 • • • • • • • • z M 1 • code of P 1 z m 2 • • • • • • • • z M 2 • code of P 2 z m 3 • • • • • • • • z M n • • • • • . . .

Encoding Environments

First, let us show how to express structural properties about the environment heap. In the proof of Lemma 6.1 below, advanced arithmetical constraints are expressed thanks to Theorem 5.5. Lemma 6.1 There is a formula PseudoEnv(z, z ) in SL(-- * ) such that the conditions below hold true iff (s, h E ) |= PseudoEnv(z, z ):

• z < z , z ≡ z + 2 (mod 3) and z and z are extremities.

• for all i in [ z, . . . , z ],

if i ≡ z + 1 (mod 3) then there is no extremity l in (s, h E ) such that l = i, if i ≡ z + 1 (mod 3), then there is exactly one location l such that l is an extremity and l = i. This unique location l belongs to dom(h E ). Proof The formula PseudoEnv(z, z ) is the conjunction of the formulae below expressing the following properties:

1. z < z and z,z are extremities: z < z ∧ extr(z) ∧ extr(z ).

2. There is no extremity with number of predecessors equal to either z+1 or z -1.

(¬∃x extr(x) ∧ z + 1 = x) ∧ (¬∃x extr(x) ∧ z = 1 + x)
3. There is an extremity with number of predecessors equal to z+2

[resp. z -2]. ∃x (extr(x) ∧ ( z + 2 = x)) ∧ ∃x (extr(x) ∧ ( z = 2 + x))
4. For every extremity x with a number of predecessors strictly between z and z , there is an extremity with a number of predecessors equal to either x + 1 or x -1.

∀x [extr(x) ∧ x > z ∧ x < z ] ⇒ (∃y y = 1 + x ∨ ∃y y + 1 = x)
5. Constraint on two extremities with two consecutive numbers of predecessors:

∀x.∀y [extr(x) ∧ extr(y) ∧ ( x > z) ∧ ( x < z ) ∧ ( y > z)∧ ( y < z ) ∧ ( y + 1 = x)] ⇒ [(¬∃y y = 1 + x) ∧ (∃y y = 2 + x)∧
(¬∃y y + 1 = y) ∧ (∃y . y + 2 = y)] 6. There are no two distinct extremities with an equal number of predecessors.

∀x[extr(x) ∧ x ≥ z ∧ x ≤ z ] ⇒ ¬∃y (extr(y) ∧ x = y ∧ x = y)
It is then easy to check that the above conjunction satisfies the statement. By induction on k ranging from 1 to ( zz -2)/3, one can show that there is no extremity l in (s, h E ) such that l = z + 3k -2, and there are extremities l and l such that l = z+3k -1 and l = z+3k. This concludes the proof.

In the sequel, when (s, h) is j-well-formed, by default h E denotes the environment part and h B the base part.

We state below a crucial result, basically stating that adding an environment heap to a j-well-formed memory state leads to a (j + 1)-well-formed memory state. This is central to interpret a new second-order variable (extending the environment part) and this can be performed thanks to -- * (details will follow). Lemma 6.6 (Composition) Let (s, h) be a j-well-formed memory state and (s , h E ) be a memory state such that 1. h E is disjoint from h and s differs from s at most for the variables z m j+1 and z M j+1 . 2. s (z m j+1 ) and s (z M j+1 ) do not belong to dom(h) ∪ ran(h).

(s , h E

) is an environment between z m j+1 and z M j+1 .

(s , h

* h E ) |= z M j + 1 = z m j+1 . 5. dom(h E ) ∩ ran(h) = ∅.
Then, (s , h * h E ) is (j + 1)-well-formed with the base part h B and the environment part h E * h E .

The proof of Lemma 6.6 is tedious and requires some care. We provide the details below. Proof The proof mainly rests on establishing the property below.

(♠) Any extremity in h E or in h E is an extremity in h * h E with exactly the same number of predecessors.

Consequently, this implies that in the model (s , h * h E ) we have the following relationships:

( ) z m 0 < z M j = z m j+1 -1 < z M j+1 -1, z m 0 + 2 ≡ z M j+1 (mod 3
) and z m j+1 ≡ z m 0 (mod 3). Assuming (♠) and ( ), let us check the conditions from Definition 6.3 for ensuring that (s , h * h E ) is (j + 1)-well-formed with base part h B . After doing that, we shall establish that (♠) holds true.

First, we show that (s , h E * h E ) is a (j + 1)-marked environment.

(P1) Let us prove that (s , h E * h E ) |= PseudoEnv(z m 0 , z M j+1 ). Below, the numbers of predecessors are relative to (s , h E * h E ). Let i ∈ { z m 0 , . . . , z M j+1 }.

-Assume i ≡ z m 0 + 1 (mod 3). Ad absurdum, suppose that there is a location l such that l is an extremity and l = i. Then l is an extremity with i predecessors either in h E or in h E , which leads to a contradiction since (s , h E ) is an environment between z m j+1 and z M j+1 and (s, h E ) is an environment between z m 0 and z M j .

-Assume i ≡ z m 0 + 1 (mod 3). If i ∈ { z m 0 , . . . , z M j }, then by (♠) there is a unique extremity l k such that l k = i. Otherwise (i ∈ { z m j+1 , . . . , z M j+1 }), by (♠), there is a unique extremity l new k such that l new k = i.

(P2) Suppose that l ∈ dom(h E * h E ). Two cases are distinguished below.

l ∈ dom(h E ).

We distinguish again two subcases since h is j-well-formed. * In the case l is an extremity in h E , the location l is an extremity in h * h E by (♠). Consequently, l is an extremity in h E * h . * In the case h(l) is an extremity in h E , the proof is analogous.

-l ∈ dom(h E ).
The proof is analogous.

(P3) Let l be an extremity in h E . Let us show that h(l) / ∈ dom(h E * h E ). Since (s, h) is j-well-formed, h(l) / ∈ dom(h E ). Ad absurdum, suppose that h(l) ∈ dom(h E ). Then, either h(l) is an extremity in h E or h(l) is a predecessor of an extremity l in h E . In the first case, it leads to a contradiction since the extremities of h E are not in ran(h E ), by hypothesis [START_REF] Bouajjani | Verifying programs with dynamic 1-selector-linked structured in regular modelchecking[END_REF]. In the second case, l is not an extremity in h * h E which is in contradiction with (♠). Consequently, h(l) / ∈ dom(h E * h E ).

Let l be an extremity in h E . Since (s , h E ) is an environment between z m j+1 and z M j+1 , we know that h E (l) / ∈ dom(h E ). It remains to check that h E (l) ∈ dom(h E ). Ad absurdum, suppose that h E (l) ∈ dom(h E ). Then there is l ∈ {h E (l), h(h E (l))} such that l is an extremity in h E . By (♠), l is an extremity in h E * h E . This leads to a contradiction since l has predecessors in h E * h E .

(P4) Let l be an extremity in h E . We have

z m 0 ≤ l ≤ z M j < z M j+1 since (s, h) is j-well-
< x < z M j+1 . (PM2) Let 0 < i ≤ j + 1. If i ≤ j, then since (s, h) is j-well-formed we obtain (s, h) |= z M i + 1 = z m i+1 . By (♠), (s , h * h E ) |= z M i + 1 = z m
i+1 (s and s agree for these variables). If i = j + 1, then hypothesis (4) precisely states that (s , h

* h E ) |= z M j + 1 = z m j+1 .
It remains to verify the conditions (WF2) and (WF3).

(WF2) Since h and h * h E have the same base part and (s, h) is j-well-formed, we get that there is no location l such that l in (s, h B ) is strictly greater than

z m 0 -2 in (s, h * h E ) (equal to z m 0 -2 in (s, h) by (♠)). (WF3) Since (s, h) is j-well-formed, we have dom(h E ) ∩ ran(h B ) = ∅. By hypothesis (5), dom(h E ) ∩ ran(h) = ∅. Consequently, dom(h E * h E ) ∩ ran(h B ) = ∅.
Now, let us prove that (♠) holds true. First, we prove the case when an extremity is a location of the form s (z k ) with k ∈ {0, . . . , j + 1} and ∈ {m, M }. By hypothesis (2), s (z m j+1 ) and s (z M j+1 ) do not belong to ran(h). So the values z m j+1 and z M j+1 remain unchanged from (s , h E ) to (s , h * h E ). Now let k ∈ {0, . . . , j} and ∈ {m, M }. Assume that z k has changed from (s , h) to (s , h * h E ). Consequently, s (z k ) ∈ ran(h E ). By Lemma 6.4, there are two possibilities.

1. s (z k ) is an extremity in (s , h E ).
As (s , h E ) is an environment between z m j+1 and z M j+1 , every extremity belongs to dom(h E ), whence s (z k ) ∈ dom(h E ). This leads to a contradiction since h and h E are disjoint: s (z k ) ∈ dom(h E ) since (s, h) is j-well-formed. 2. There is a location l such that h E (l) = s (z k ) (also equal to s(z k )) and l is an extremity. So s (z k ) is not an extremity in h * h E , which also leads to a contradiction.

Observe that all the extremities in h E are either of the form l k , or s (z m 0 ) or s (z M j ). Moreover, l 3β = z M j -2 in (s , h). Finally, as (s , h E ) |= PseudoEnv(z m j+1 , z M j+1 ), for every k ∈ E γ , there is a location l new k verifying the properties below in (s , h E ):

• l new k = ( z m j+1 -(3β + 3)) + k, • l new k is an extremity,
• there is no location l such that l = l new k , l = l new k and l is an extremity.

Observe that all the extremities of h E are either of the form l new k , or s (z m j+1 ) or s (z M j+1 ). We can establish additionnal arithmetical properties:

l new 3×γ = z M j+1 -2 in (s , h E ) and l new k in (s , h E ) is equal to z m 0 + k in (s , h * h E ).
We are going to prove that for all k ∈ E β , l k = l * k , and for all k ∈ E γ , l new k = l * k . This will terminate the proof of (♠) since the only extremities

in h E are {l k : k ∈ E β } ∪ {s (z m 0 ), s (z M j )} and the only extremities in h E are {l new k : k ∈ E γ } ∪ {s (z m j+1 ), s (z M j+1 )}.
The proof is ad absurdum and we distinguish two cases (each of them will therefore lead to a contradiction):

(I) There is k ∈ E β such that l k = l * k . (II) There is k ∈ E γ such that l new k = l * k .
(I) Let us first establish that l * k ∈ ran(h E ) (proof ad absurdum). Suppose that l * k ∈ ran(h E ). So, l * k remains unchanged from (s , h) to (s , h * h E ). As in (s , h * h E ), we have z m 0 < l * k < z M j , and z m 0 and z M j remain unchanged from (s , h) to (s , h * h E ), we can infer that z m 0 < l * k < z M j in (s , h). Additionnally, as in (s , h * h E ), we have l * k = z m 0 + k, this is also true in (s , h). Finally, as l * k is an extremity in (s , h * h E ), it is also an extremity in (s , h). Consequently, l * k = l k , which leads to a contradiction. We have established that l * k ∈ ran(h E ). By Lemma 6.4, there are two possibilities:

• l * k is an extremity in h E . Consequently, in h E , we have l * k > z m j+1 . As z m j+1 remains unchanged from (s , h E ) to (s , h * h E ), in h * h E we obtain l * k > z m j+1 = z M j + 1, which leads to a contradiction since l * k = l k = z m 0 + k and l k < z M j .
• There is a location l 0 such that l 0 is an extremity in h E and h E (l 0 ) = l * k . So l * k is not an extremity in h E , and it cannot either be an extremity in h * h E , which leads to a contradiction.

(II) Let k be the smallest element of E γ such that l new k = l * k . In (s , h * h E ), we know that l * k > z m j+1 > z M j . Moreover, as l * k is an extremity in (s , h * h E ), either l *
k is an extremity in (s , h) too or l * k has no predecessor in (s , h). Since no extremity of (s , h) has more than z M j predecessors (in both h and h * h E ), the location l * k cannot have all of its predecessors in dom(h). Let l 0 be one of the predecessors of l * k that belongs to dom

(h E ), i.e. h E (l 0 ) = l * k . Recall that (s , h E ) is an environment between z m j+1 and z M j+1 . Since l 0 ∈ dom(h E ), there is l ∈ {l 0 , h E (l 0 )} such that in h E : (a) l is an extremity, (b) l ∈ dom(h E ), (c) z m j+1 ≤ l ≤ z M j+1 , (
d) no other extremity has exactly l predecessors. Indeed, (a) comes from (P2), the conditions (b) and (d) come from (s , h E ) |= PseudoEnv(z m j+1 , z M j+1 ), (c) from satisfaction of (P4). In the case l = l 0 , l * k is not an extremity in h E and hence l * k is not an extremity in h * h E . This leads to a contradiction. Consequently, we have

l = h E (l 0 ) = l * k . Let
= l * k in (s , h * h E )
. By definition of the locations l * k and l new p , we obtain p < k, which leads to a contradiction by minimality of k.

The Translation

In this section, we provide the translation from DSO into SL(-- * ). First, we introduce additional formulae that will be useful in the translation process. It is worth observing that in order to translate first-order quantification, we should guarantee that first-order variables x are not interpreted as locations from the domain of the environment part. Typically, the number of predecessors of s(x) and h(s(x)) (if it exists) should be less than z M 0 and none of

• t j (x = y) x = y, • t j (x → y) x → y,
• for i ≤ j, t j (P i (x, y)) is defined by

∃z, z (z → x) ∧ (z → y) ∧ ( z > z m i ) ∧ ( z < z M i ) ∧ ( z = 1 + z) ∧ extr(z) ∧ extr(z )
So (s(x), s(y)) belongs to the interpretation of P i when s(x) and s(y) are endpoints of markers with consecutive degrees between z m i and z M i . • t j is homomorphic for Boolean connectives.

• t j (∃x ψ) ∃x notonenv(x) ∧ t j (ψ).

• t j (∃P j+1 , ψ), is defined by

∃z m j+1 , z M j+1 isol(z m j+1 ) ∧ isol(z M j+1 )∧ (relation j+1,FV(ψ) -- * ¬ (PseudoEnv(z m 0 , z M j+1 )∧ z M j +1 = z m j+1 ∧t j+1 (ψ)))
In order to translate ∃P j+1 ψ, we introduce two locations whose numbers of predecessors determine the bounds for the degrees for any marker used to encode a pair for the interpretation of P i . There is a way to add markers (expressed thanks to the connective -- * ¬ ) that guarantees that the new part of the heap encodes the interpretation of the variable P j+1 by using the above formula relation j+1,X .

Observe that T (φ) and φ have the same first-order free variables.

Correctness

Before stating the correctness of the translation T (•), we need to formally define how to extract an environment from a j-well-formed model (but now, that is easy). Definition 6.9 Let (s, h) be a j-well-formed model, and let h E be the associated environment heap. The environment E extracted from h is

E(P i ) def = {(h E (l), h E (l )) : z m i < l, l + 1 = l , l < z M i in h E }
for all i ∈ {1, . . . , j}.

Correctness of T (•) is based on Proposition 6.10 below. The proof shall use several results established earlier.

Proposition 6.10 Let φ be a DSO formula using the extended Barendregt convention and ψ be a subformula of φ at quantifier depth j. Let (s, h) be a j-well-formed model, with base part (s, h B ) and environment part (s, h E ), such that for each x ∈ FV(ψ), s(x) ∈ dom(h E ). Let E j be the environment extracted from h E . Then, (s, h) |= t j (ψ) iff (s, h B ), E j |= ψ. Proof Let us start by a preliminary definition. We say that a location l occurs in a binary relation R when there is a location l such that (l, l ) ∈ R or (l , l) ∈ R. Let φ be a DSO sentence satisfying the extended Barendregt convention. We want to show by induction on ψ that given:

• ψ is a subformula of φ of quantifier depth j,

• (s, h) is j-well-formed with base part h B and environment part h E such that for every variable x ∈ FV(ψ), we have s(x) ∈ dom(h E ),

• E j is the environment {P 1 → R 1 , . . . , P j → R j } extracted from h E , • no location occurring in R 1 ∪ • • • ∪ R j belongs to dom(h E ), we have (s, h) |= t j (ψ) iff (s, h B ), E j |= ψ.
Base cases.

The base cases x = y and x → y are by an easy verification since t j restricted to them is the identity map. Let us consider the more interesting base case, i.e. when ψ = P k (x, y) with k ≤ j.

(→) Suppose that (s, h) |= t j (P k (x, y)). Then, in the heap h, the locations s(x) and s(y) have predecessors in h that are also extremities, let us call them respectively l x and l y . In the heap h, we have z m k < l x = l y -1 < z M k -1. By Definition 6.3, both l x and l y have predecessors in dom(h E ) and all of their predecessors are also in dom(h E ). Since z m k and z M k have also all of their predecessors in dom(h E ), we have z m k < l x , l x + 1 = l y and l y < z M k in h E . By Definition 6.9, we get (h(l x ), h(l y )) ∈ R k , that is (s(x), s(y)) ∈ R k . Consequently, (s, h B ), E j |= P k (x, y). (←) Suppose that (s, h B ), E j |= P k (x, y). By definition of |= and E j , we have (s(x), s(y)) ∈ R k . So s(x) and s(y) have respectively predecessors l x and l y in dom(h E ). In the heap h E , l x and l y are extremities and z m k < l x = l y -1 < z M k -1. By Definition 6.3, the predecessors of any location among s(z m k ), l x , l y and s(z M k ) belong to dom(h E ). So the above inequalities and equality are also true in h. By Definition 6.3, the locations s(z m k ), l x , l y and s(z M k ) are extremities in h. So (s, h) |= t j (P k (x, y)).

Induction step. Our induction hypothesis is the following: for every subformula ψ of size strictly less than the size of ψ, for j ∈ {0, . . . , n} (n is the quantifier depth of φ) and for any j-well-formed model (s, h) such that for every variable x ∈ FV(ψ), we have (s, h) |= t j (ψ ) iff (s, h B ), E j |= ψ . Case 1: ψ = ∃x ψ . The statements below are equivalent: Let us justify below why (4) implies (3). Suppose (4) and l ∈ dom(h E ). Since (s, h) is j-well-formed, l / ∈ (dom(h B ) ∪ ran(h B )). Since Loc is an infinite set, there is a location l

(0) (s, h) |= t j (∃x ψ ), (
is l ∈ Loc such that (s , h B ), E j |= ψ and l ∈ dom(h E ) with s = s[x → l] (by induction hypothesis since FV(ψ ) ⊆ FV(∃x. ψ )∪{x}), (3) there
is l ∈ Loc such that (s , h B ), E j |= ψ with s = s[x → l], (4) there
∈ (Loc \ (dom(h B ) ∪ ran(h B ) ∪ dom(h E )) such that l does not occur in (R 1 ∪ • • • ∪ R j ). By Lemma 2.1, (s[x → l ], h B ), E j [l ← l ] |= ψ .
Suppose ad absurdum that l occurs in R k for some 1 ≤ k ≤ j. So, l has a predecessor that is an extremity in dom(h E ) and by (P3), l ∈ dom(h E ), which leads to a contradiction. Hence, E j [l ← l ] = E j . We have established that (s[x → l ], h 1 ), E j |= ψ and l ∈ dom(h E ). Since we aim at having locations in h E that do not interfere with the store, we need to be more restrictive about R.

Replacing R by some R . We build below a finite binary relation R from R such that no location in dom(h E ) occurs in R and (s, h B ), E j [P j+1 → R ] |= ψ .

dom(h E ) ∩ ran(h) = ∅.

These claims essentially follow from the definition of formula t j (∃P j+1 ψ ), the only difficult part being claim 5. Let us detail this last point: while merging h and h E , no new marker can be created so any marker in h * h E is a marker either from h E or from h, with the same degree. Moreover, h * h E satisfies PseudoEnv(z m 0 , z M j+1 ), so the spectrum of h E is included in the one of h * h E . Combining these two facts, it follows that all markers of h E are still markers of the same degree in h * h E , and in particular claim 5 holds. Now, claims 1-5 are precisely the assumptions from Lemma 6.6 and therefore (s , h * h E ) is (j + 1)-well-formed. Observe that ( 5) is consequence of (3). Since (s , h * h E ) |= t j (ψ ) and for every x ∈ FV(ψ ) s(x) / ∈ dom(h E * h E ), we can then apply the induction hypothesis and obtain (s, h B ), E j+1 |= ψ , that is (s, h B ), E j |= ∃P j+1 ψ where E j+1 is extracted from h E * h E .

Here is our main result about the expressive power of SL.

Theorem 6.11 SL(-- * ) ≡ SL ≡ SO ≡ DSO.

Proof The proof follows from the following properties:

• SL(-- * ) SL and DSO SO by simply considering syntactic fragments.

• SL DSO and SO DSO by Proposition 2.6.

• DSO SL(-- * ).

It remains to show that DSO SL(-- * ) by using Proposition 6.10. Let φ be a DSO sentence. Without any loss of generality, we can assume that φ has no free occurrence of first-order variables of the form z j (otherwise, other auxilliary variables are used) and φ satisfies the extended Barendregt convention since every DSO sentence can be reduced to an equivalent one in logspace. Let (s, h) be a model. The statements below are equivalent

• (s, h) |= T (φ),

• There are h E ⊥ h, l, l and s = s[z m 0 → l, z M 0 → l ] such that l and l / ∈ dom(h) ∪ ran(h), l, l ∈ dom(h ) and for every location l ∈ dom(h E ) \ {l, l }, we have h E (l ) ∈ {l, l }. -In (s , h * h E ), z M 0 = 2 + z m 0 and for every l ∈ dom(h), we have z m 0 ≥ 3 + l .

l and l are extremities in (s , h * h E ).

-(s , h * h E ) |= t 0 (φ). Observe that all the equivalences are obtained with logarithmic-space translations. Consequently, Corollary 6.12 SL(-- * ) satisfiability problem is undecidable. Proof We have seen that for every sentence such that φ in DSO, there is an effective way to compute φ in SL(-- * ) such that φ and φ hold on exactly the same models. In order to show undecidability of SL(-- * ), it is sufficient to provide a reduction from finitary satisfiability for classical predicate logic restricted to a single binary predicate symbol (see e.g. [START_REF] Trakhtenbrot | The impossibility of an algorithm for the decision problem for finite models[END_REF]) to DSO. Let φ be a first-order formula built over the binary predicate symbol R. One can easily show that φ is satisfiable iff ∃D ∃R (∀x y R(x, y) ⇒ D(x, x) ∧ D(y, y)) ∧ t(φ) is satisfiable. The map t is the identity map for atomic formulae, homomorphic for Boolean connectives and performs a relativization for first-order quantification: t(∀x ψ) = ∀x D(x, x) ⇒ t(ψ). The intention is obviously that D(x, x) holds true whenever x belongs to the finite model. Undecidability of SL(-- * ) can be obtained much more easily by encoding the halting problem for Minsky machines by using the fact that x = y and x = y + 1 can be expressed in SL(-- * ) (Section 5). Indeed, computations of length n can be encoded as lists of length 3n; three successive locations encode a configuration of the machine and for two of those locations, counter values are encoded by the numbers of predecessors. Corollary 6.12 is obtained with the stronger result SL(-- * ) ≡ DSO since DSO is undecidable.

Extensions with More Than one Selector

In order to express advanced arithmetical constraints (see Section 5) or to encode finite sets of pairs of locations (see Section 6), we have introduced additional parts in the heaps via markers. In order to distinguish these auxiliary markers from the original heap, we have decided to use markers of small degree (as in Section 5) or markers of large degree (as in Section 6). However, in the presence of memory cells with strictly more than one selector it is even easier to identify these auxiliary markers; for example, the memory cells l → l introduced in a model to check arithmetical constraints or to encode environments can be replaced by memory cells of the form l → l , (k-1) times ⊥, . . . , ⊥ where ⊥ is a location that is not present in the original model (i.e. not in ran(h) ∪ dom(h)). We write kSL [resp. kSO] to denote the variant of SL [resp. SO] with k selectors. In that case, a heap h is defined as a partial function h : Loc Loc k with finite domain. The atomic formulae of the form x → y from SL are replaced by x → y 1 , . . . , y k . Obviously 1SL [resp. 1SO] corresponds to SL [resp. SO]. We write kSO k to denote the restriction of kSO to second-order variables in VAR k .

In the rest of this section, we assume that k > 1. We dedicate the rest of this section to show Theorem 7.1 below can be proved by adapting what we did for a unique selector. We may overload symbols but no confusion should occur. The case k = 1 requires a lot of care but a simpler direct proof is possible for k = 1. Indeed, for k = 1 the identification of auxiliary memory cells is performed thanks to structural properties whereas for k > 1, this could be done by simply checking the presence of distinguished values. Theorem 7.1 For every k > 1, kSL ≡ kSL(-- * ) ≡ kSO.

We establish Theorem 7.1 by adapting the proof for k = 1. However, a simpler proof for k > 1 is possible but it would require a different approach that cannot find its place in this paper. First, an obvious adaptation of the proof of Propositions 2.5 and 2.6 allows us to show the statement below. Lemma 7.2 kSL kSO k+1 and kSO k+1 kSO 2 .

It remains to show that kSO 2 kSL(-- * ). The basic observation is that all the auxiliary memory cells l → l introduced in a model to check arithmetical constraints or to encode environments are replaced by memory cells of the form l → l , (k-1) times ⊥, . . . , ⊥ where ⊥ is a location that is not present in the original model. Observe that it is easy to check that a memory cell is auxiliary by simply inspecting the presence of ⊥. We shall also enforce that in a new memory cell, l is different from ⊥ and the (k -1) remaining locations are exactly ⊥.

Before explaining the adaption, we introduce alternative definitions:

• Given (s, h) and a location l, we write l to denote the cardinal of {l ∈ Loc : h(l ) = (l, . . .)} (number of 1-predecessors of the location l in (s, h)).

• We write x → y as a shortcut for ∃y 2 • • • y k x → y, y 2 , . . . , y k .

• A [resp. strict] marker in (s, h) is a sequence of distinct locations l, l 0 , . . . , l n for some n ≥ 0 (all distinct from ⊥) such that h(l 0 ) = (l, k-1 times ⊥, . . . , ⊥) [resp. and dom(h) = {l 0 , . . . , l n }],

for every i ∈ {1, . . . , n}, h(l i ) = (l 0 , k-1 times ⊥, . . . , ⊥) and l i = 0, l 0 = n.

• We define an extremity as a location l in a model such that l has at least one 1-predecessor and no 1-predecessor l of l appears in some tuple from ran(h).

This solves two central open problems: the decidability status of SL and the characterization of its expressive power. Moreover, the above results about expressive power extend naturally to the case with k selectors, for some k ≥ 1: kSL ≡ kSL(-- * ) ≡ kSO.

  Using a technique similar to the proof of Lemma 3.1, we can translate SL( * ) into MSO. Proposition 3.2 SL( * ) MSO via a logspace translation. Proof Any formula φ in SL( * ) is satisfiable iff

Figure 1

 1 Figure 1 Memory state encoding the finite word a 1 a 2 a 3 a 1

  Use of -- * ¬ Let us define SL( * + n -- * ¬ ) as an extension of SL( * ) by adding the binary operators n -- * ¬ for every n ∈ N. Unlike the plain operator -- * ¬ , a formula with outermost connective n -- * ¬ states the existence of a disjoint heap for which the cardinality of the domain is bounded by n. More formally, we require that

  The proof is by a straightforward structural induction. Since computing | φ | from φ can be done in polynomial-time, we obtain the following reduction that becomes especially interesting after showing decidability of SL( * + n -- * ¬ ).

Lemma 4 . 2

 42 There is a polynomial-time reduction from satisfiability for SL restricted to formulae such that the left argument of any -- * -formula belongs to SL -( * ) to satisfiability for SL( * + n -- * ¬ ).

Theorem 4. 9 (

 9 I) There is a polynomial-time reduction from SL( * + n -- * ¬ ) satisfiability problem to SL( * ) satisfiability problem. (II) SL( * + n -- * ¬ ) satisfiability is decidable.

Figure 2

 2 Figure 2 How to compare the length of two lists: situation ϕ(x, y), with sub-model satisfying φ in bold, and sub-model satisfying ψ in broken line.

Figure 4 h

 4 Figure 4 h 1 and h 2 satisfying the conditions 1.-4.

Figure 5 A 2 -Lemma 5 . 2

 5252 Figure 5 A 2-completion of h 1 * h 2 that leads to a x-completed heap.

Figure 6 A 4 .

 64 Figure 6 A contest won by Duplicator. n = 3, c = c = 0

(

  a symbol '•' on position n indicates the presence of a marker of degree n, and '•' its absence). In other words, the spectrum is a finite set of naturals of the form {n | a ≤ n ≤ b and n = a + 1 (mod 3)}

  (s, h B ), E j |= ψ (by definition of |=).

Case 2 :

 2 ψ = ∃P j+1 ψ . (←) Suppose that (s, h B ), E j |= ∃P j+1 ψ . By definition of the satisfaction relation |=, there is R ∈ P f (Loc 2 ) such that (s, h B ), E j [P j+1 → R] |= ψ .

(

  by definition of T (•) and |=)• There are h ⊥ h, l and l such that-(s , h * h E ) is an environment with z M 0 = 2 + z m 0 . -(s , h * h ) |= t 0 (φ).

(

  by Definition 6.3 and Lemma 6.5)• There are h ⊥ h, l and l such that-(s , h * h E ) is an environment with z M 0 = 2 + z m 0 . -(s , h), E 0 |= φ for any environment E 0 extracted from h E .(by Proposition 6.10)• (s, h) |= φ sincethe variables z m 0 and z M 0 do not occur in φ and φ is a sentence.h E can always be built since h is essentially a finite structure.

  There is a logarithmic-space translation from SL to SO (hence SL SO).

	(I) (s, h) |= ls(x, y) iff (s, h) is a list segment between x and y.
	(II) (s, h) |= x→ * y [resp. (s, h) |= x→ + y ] iff y is a descendant [resp. strict
	descendant] of x.
	2.3. Preliminary Translations
	Before showing advanced results in the forthcoming sections, we show
	below how SL can be encoded into SO by simply internalizing the semantics
	and how SO can be encoded in its fragment DSO by representing multi-edges
	by finite sets of edges.
	Proposition 2.5
	Lemma 2.4 Let (s, h) be a model.

  formed and (♠). Let l be an extremity in h E . The values l, z m j+1 and z M j+1 do not change from h E to h * h E . Since (s , h E ) is

	an environment between z m j+1 and z M j+1 , z m j+1 ≤ l ≤ z M j+1 . So in
	(s , h * h E ), we have z m 0 < z m j+1 ≤ l ≤ z M j+1 .
	(PM1) By (♠), for each variable x in {z m 0 , . . . , z m j+1 }∪{z M 0 , . . . , z M j+1 }, the value
	x remains unchanged from h or h E to h * h E . Considering that h is
	j-well-formed, h E is an environment between z m j+1 and z M j+1 and (s , h *
	h E ) |= z M j +1 = z m j+1 , we conclude that for every x ∈ {z m 1 , . . . , z m j+1 }∪
	{z M 0 , . . . , z M j }, s(x) is an extremity and z m 0

  us conclude the proof. In h E , the location l *

	k is an extremity. As (s , h E ) is an environment
	between z m j+1 and z M j+1 , we have l * k ∈ dom(h E ) and z m j+1 ≤ l * k ≤ z M j+1 in
	(s , h E ). Since s(z m j+1 ) = l * k and s(z M j+1 ) = l * k , we obtain z m j+1 < l * k < z M
	p	= l * p . Since l new p	can only
	increase from h E to h * h E , we can conclude that l new p	in (s , h E ) is strictly
	smaller than l new p

j+1 in h .

So there is p ∈ E γ such that l * k = l new p . We have that the value l new p changes from h E to h * h E , and therefore l new

  1) there is l ∈ Loc such that (s , h) |= t j (ψ ) and (s , h) |= notonenv(x)

with s = s[x → l] (by definition of t j ),

(2) there is l ∈ Loc such that (s , h) |= t j (ψ ) and l ∈ dom(h E ) with s = s[x → l] (by Lemma 6.7),

Preprint submitted to ElsevierDecember 29, 2011

Acknowledgments. We would like to thank the following colleagues for fruitful discussions related to this work: Anuj Dawar, Arnaud Durand, Didier Galmiche, Dominique Larchey-Wendling, Daniel Méry. Moreover, we wish to thank the anonymous referees for their numerous helpful suggestions and comments on an earlier version of this paper. This has been a great help to improve the quality of the paper.

Consequently, if (s, h E ) |= PseudoEnv(z, z ), then h E has a clean spectrum:

In that case, (s, h E ) is called a pseudo-environment between z and z .

An environment between z and z is a memory state (s, h E ) such that (P1) (s, h E ) |= PseudoEnv(z, z ).

(P2) If l ∈ dom(h E ), then either l or h E (l) is an extremity in h E .

(P3) For every extremity l in h E , l ∈ dom(h E ) and h E (l) ∈ dom(h E ).

(P4) For every extremity l in h E , z ≤ l ≤ z .

Roughly speaking, (s, h E ) is a finite set of markers with the abovementioned spectrum. Figure 7 presents a simple environment with z = 1 and z = 6, which allows to encode a single pair ((l, l) in the present figure). Note that in full generality, the number of pairs that can be encoded by an environment between z and z is equal to z -z-2 3 .

Figure 7 A simple environment encoding the pair (l, l) z z l Lemma 6.2 There exists a formula Env(z, z ) ∈ SL(-- * ) such that for every memory state (s, h), we have (s, h) |= Env(z, z ) iff (s, h) is an environment between z and z . Proof Let us consider the conjunction Env(z, z ) of the formulae below.

(F1) PseudoEnv(z, z ).

(F2) ∀x (alloc (x) ⇒ (extr(x) ∨ ∃y x → y ∧ extr(y))).

(F3) ∀x extr(x) ⇒ (alloc (x) ∧ ∃y x → y ∧ ¬alloc (y)).

(F4) ∀x extr(x) ⇒ ( z ≤ x ∧ x ≤ z ).

Formula (Fi) captures the condition (Pi). Consequently, if (s, h E ) |= Env(z, z ), then h E is equal to a set of markers of the clean spectrum

Consequently, when (s, h) is a j-marked environment, the spectrum of h E contains the following values:

) is another j-marked environment with identical store, then h and h have the same spectrum. Definition 6.3 below specifies how a heap can be divided into a base part and an environment part with constraints on the values z m 0 , z M 0 , . . . , z m j , z M j . These values are helpful to determine the range of marker degrees that should be considered to encode the interpretation of second-order variables. Definition 6.3 A memory state (s, h) is j-well-formed for some j ≥ 0 iff there are heaps h B , h E with h = h B * h E satisfying the properties below:

(WF2) There is no location l such that l in (s, h B ) is strictly greater than

(s, h B ) is called the base part and (s, h E ) the environment part. Condition (WF3) guarantees that when (s, h) is j-well-formed, for every extremity l in h E , l in h E is equal to l in h. Consequently, any extremity in h with more than z m 0 predecessors has all predecessors in dom(h E ). Moreover, (s, h) |= PseudoEnv(z m 0 , z M j ), that is (s, h) is a pseudo-environment between z m 0 and z M j . We establish below a few lemmas that are helpful in the sequel. Lemma 6.4 Let h E be the environment part of some j-well-formed model. For every location l ∈ ran(h E ), either l is an extremity in h E or there is l such that h E (l ) = l and l is an extremity.

Note that the above property holds true for any environment but we shall use it for j-well-formed models only. Proof If l ∈ ran(h E ), then there is a location l such that h E (l ) = l. By (P2) on (s, h E ), either h E (l ) is an extremity or l is an extremity. Lemma 6.5 below states unicity of decomposition when a memory state is j-well-formed. Lemma 6.5 (Unicity) Whenever (s, h) is j-well-formed with base part h B and environment part h E , there is no (h B , h E ) = (h B , h E ) such that (s, h) is j-well-formed with base part h B and environment part h E . Proof Let k 0 = ( z M jz m 0 -2)/3 and S = {k : k ≡ 1 (mod 3) and 0 ≤ k ≤ 3 × k 0 + 2} be the spectrum of h E and h E . Indeed, (s, h E ) and (s, h E ) are both j-marked environments and there are precisely card(S) extremities l in (s, h) such that z m 0 ≤ l ≤ z M j . For each k ∈ S, we write l k to denote the unique extremity such that l k = z m 0 + k. Notice that each location l k has no predecessor in h B by Definition 6.3(WF3), l 0 = s(z m 0 ) and l 3k 0 +2 = s(z M j ). The set dom(h E ) contains at least the following locations: for every k ∈ S, the location l k and the z m 0 +k predecessors of l k in h. Let X be the set of the above locations. Assume there is some l ∈ (dom(h E )\X). By (P2), either l or h E (l) is an extremity in h E (let us call it l ). Since each predecessor of some location in X is also in X and l ∈ X, l is not a predecessor of an element in X. Consequently, l is an extremity that does not belong to {l k : k ∈ S} (let us call this set Y ). Since z m 0 ≤ l ≤ z M j , either l has as many predecessors as an element in Y or l ≡ z m 0 + 1 (mod 3). This entails that (s, h E ) does not satisfy PseudoEnv(z m 0 , z M j ) which leads to a contradiction. Consequently,

Consequently, for all k ∈ {0, . . . , j} and ∈ {m, M }, z k is unchanged from h to h * h E . Based on these preservations and since (s , h E ) is an environment between z m j+1 and z M j+1 , (s , h) is j-well-formed and (s , h * h E ) |= z M j + 1 = z m j+1 , we can conclude ( ). Before treating the proof for the other types of extremities, let us provide a few basic definitions and facts. We define the natural numbers α, β and γ as follows:

Notice that γ = α -β -1. These values are simply related to the spectrum below where the first value is z m 0 and the last one is z M j+1 .

0 and z M j (remember (s, h) is j-wellformed) and (s , h E ) is an environment between z m j+1 and z M j+1 , we get that (s , h * h E ) |= PseudoEnv(z m 0 , z M j+1 ). So, for every k ∈ E α , there is a location l * k verifying the properties below in (s , h * h E ):

Similarly, as (s , h) |= PseudoEnv(z m 0 , z M j ), for every k ∈ E β , there is a location l k verifying the properties below in (s , h):

• there is no location l such that l = l k , l = l k and l is an extremity. these locations is an extremity. The formula notonenv(•) is introduced for this purpose:

Lemma 6.7 Let (s, h) be a j-well-formed model. Then (s, h) |= notonenv(x) iff s(x) ∈ dom(h E ). Proof As (s, h) is j-well-formed, by Definition 6.3, for any location l, we have l ∈ dom(h E ) iff there is a location l ∈ {l, h(l)} such that in the heap h E , we have l ≥ z m 0 and l is an extremity. Moreover, by Definition 6.3, we get in the heap h that l ≥ z m 0 and l is an extremity. Assume that s(x) ∈ dom(h E ), then thanks to the explanations just above, (s, h) |= notonenv(x). Now, ad absurdum, suppose that s(x) ∈ dom(h E ) and (s, h) |= notonenv(x). Then there is l ∈ {s(x), h(s(x))} such that l ≥ z m 0 and l is an extremity, by definition of notonenv. Furthermore, by Definition 6.3(WF3), the location l is not an extremity in h E , all of its precedessors are in h B . Then by Definition 6.3, l ≥ z m 0 -2, which leads to a contradiction. The formula relation j,X defined below is helpful to build environments. Proposition 6.8 Let j ≥ 0 and X be a finite set of variables disjoint from {z m 0 , z M 0 , . . . , z m j , z M j }. Then, there is a formula relation j,X such that for every model (s, h), we have (s, h) |= relation j,X iff (s, h) is an environment between z m j and z M j and for every x ∈ X, s(x) ∈ dom(h).

The formula relation j,X is simply

The translation of the formula φ, written T (φ), is defined with the help of the translation t j where j records the quantifier depth.

The formula isol(x) is an abbreviation for ¬∃y (x → y) ∨ (y → x); this guarantees that s(x) ∈ dom(h) ∪ ran(h). It remains to define recursively the map t j (•).

More precisely, R will be obtained from R by replacing its image under a permutation of the set of locations that leaves the locations in s and h B fixed. The relation R is constructed by successively replacing the locations in dom(h E ) that occur also in R. Suppose that for some l ∈ dom(h E ), l occurs also in R. By the induction hypothesis, for every variable x ∈ FV(ψ ), l = s(x). By Definition 6.3 on (s, h), we have l /

Since {s(x) : x ∈ FV(ψ )}), dom(h), ran(h) and R 1 , . . . , R j are finite sets, there is l ∈ Loc such that:

If p ≥ 1 locations in dom(h E ) occur in R, then p -1 locations in dom(h E ) occur in R . Applying the above transformation iteratively p times, we can build a relation R such that no location in dom(h E ) occurs in R and

Hence, (s, h B ), E j |= ∃P j+1 ψ if and only if there is a finite binary relation

Defining (s , h E ). Let us build s and h E such that

Suppose that R contains α ≥ 0 pairs, say R = {(l 1 , l 1 ), . . . , (l α , l α )}. Let us build an environment (s , h E ) whose spectrum, for β = z M j + 1, can be depicted as

A location l is said to be fresh if l is not in the set

By finiteness of the involved objects, let X be the following set of fresh locations (there is no need to provide here precise values):

The store s is defined from s by only imposing that s (z m j+1 ) = l 0 and s (z M j+1 ) = l α+1 . The heap h E has domain X and it is defined as follows:

By an easy (and long) verification, one can check that (A) and (B) hold true. Moreover, the relations extracted from h E * h E (see Definition 6.9) are precisely R 1 , . . . , R j , R and for every x ∈ FV(ψ ), s (x) ∈ dom(h E * h E ). By the induction hypothesis, (s , h B ),

Let ϕ ⊥ be the formula specifying that auxiliary memory cells are of the above shape:

Following the developments from Section 5, we can show the following theorem.

Theorem 7.3 For c, c ≥ 0, there is a formula φ in kSL(-- * ) of quadratic size in c + c such that for every model (s, h), we have (s, h) |= φ iff x + c ≤ y + c .

Basically, we consider the formula from Section 5 in which we add to the first argument to any subformula with outermost connective either -- * ¬ or -- * the conjunct ϕ ⊥ , exactly when we need to introduce markers. Moreover, in some cases, formulae of the form x → y for the one selector case from Section 5 are replaced by x → y, x ⊥ , . . . , x ⊥ when markers are involved.

Let us consider the reduction from kSO 2 into kSL. Given a sentence in kSO 2 satisfying the extended Barendregt convention and with n second-order variables, its translation is defined below

where T (φ) is a variant of the map T (φ) for the one selector case in which the definition of t j (ψ) is modified as follows.

1. T (φ) takes the value below:

2. notonenv(x) is defined by ¬(∃y x → y, x ⊥ , . . . , x ⊥ ∨ y → x, x ⊥ , . . . , x ⊥ ) ∧ x = x ⊥ .

t j (x = y)

x = y, 4. t j (x → y)

x → y, 5. for i ≤ j, t j (P i (x, y)) is defined by ) ∧ z M j + 1 = z m j+1 ∧ t j+1 (ψ))) in which relation j+1,FV(ψ) and PseudoEnv(z m 0 , z M j+1 ) are slightly updated in order to take into account that the markers are made of memory cells of the form l → l , ⊥, . . . , ⊥.

Adapting Definition 6.9 with 1-predecessors, we can state a proposition similar to Proposition 6.10 leading to Theorem 7.1.

Concluding Remarks

In the paper, we have mainly studied first-order separation logic with one selector SL for which we have shown the following results:

1. SL( * ) is decidable with non-elementary complexity.

SL( * +

n -- * ¬ ), extending SL( * ) with bounded septraction is also decidable. 3. SL is as expressive as weak second-order logic SO. 4. SL is as expressive as SL(-- * ) as a by-product of our proof technique. 5. SL(-- * ) satisfiability is undecidable.