Stéphane Demri

Morgan Deters

LSV Stephane Demri

Expressive Completeness

Keywords: F.3.1 [Specifying and Verifying and Reasoning about Programs]: Logics of Programs Theory, Verification separation logic, expressive completeness, two-variable logics, undecidability

  L'archive ouverte pluridisciplinaire

INTRODUCTION

Expressive completeness. The literature is rich with results comparing the expressive power of non-classical logics with most standard logics such as first-or second-order logic. For instance, the celebrated Kamp's Theorem [START_REF] Kamp | Tense Logic and the theory of linear order[END_REF][START_REF] Rabinovich | A Proof of Kamp's theorem[END_REF] amounts to stating that linear-time temporal logic (LTL) is equal in expressive power to first-order logic. More generally, we know the expressive completeness of Stavi connectives for general linear time, see e.g. [START_REF] Gabbay | Temporal Logic -Mathematical Foundations and Computational Aspects[END_REF]]. This has been refined to the restriction to two variables, leading to the equivalence between unary LTL and FO2, see e.g. [START_REF] Etessami | First-Order Logic with Two variables and Unary Temporal logics[END_REF][START_REF] Ph | Expressiveness and Succinctness of First-Order Logic on Finite Words[END_REF] (see also [START_REF] Sreejith | Regular Quantifiers in Logic[END_REF]] for related questions). Monadic second-order logic (MSO) is another yardstick logic and, for instance, it is well-known that ω-regular languages are exactly those definable in MSO, see e.g. [START_REF] Straubing | Finite Automata, Formal Logic, and Circuit Complexity[END_REF]]. Similarly, extended temporal logic ETL, defined in [START_REF] Wolper | Temporal logic can be more expressive[END_REF]] and extending LTL, is also known to be equally expressive with MSO. This applies also to linear µ-calculus [START_REF] Vardi | A temporal fixpoint calculus[END_REF]] or to PSL [START_REF] Lange | Linear Time Logics around PSL: Complexity, Expressiveness, and a little bit of Succinctness[END_REF]], to quote a few more examples. On non-linear structures, bisimulation invariant fragment of MSO and modal µ-calculus have been shown equivalent [START_REF] Janin | On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic[END_REF]. In addition, there is a wealth of results relating first-order logic with two variables and non-classical logics, providing a neat characterization of the expressive power of many formalisms since first-order logic and second-order logic are queen logics. For instance, Boolean modal logic with converse and identity is as expressive as first-order logic with two quantified variables (FO2) [START_REF] Lutz | Modal Logic and the Two-Variable Fragment[END_REF]. For sets of nodes, XPath has also been established equally expressive as FO2, see e.g. an overview in [START_REF] Marx | Semantic characterizations of navigational XPath[END_REF], see also in [START_REF] Bojanczyk | Two-variable logic on data trees and XML reasoning[END_REF]] a version of FO2 on data trees. Sometimes, a third variable is needed to get expressive completeness. For instance, in [START_REF] Venema | A Modal Logic for Chopping Intervals[END_REF]] it is proved that interval logic with connectives Chop, D and T is expressively complete over linear flows of time with respect to first-order logic restricted to three quantified variables. In the realm of interval temporal logics, we also know expressive completeness of metric propositional neighborhood logic with respect to the two-variable fragment of first-order logic for linear orders with successor function, interpreted over natural numbers [START_REF] Bresolin | Metric Propositional Neighborhood Logics: Expressiveness, Decidability, and Undecidability[END_REF].

In this paper, we compare separation logic restricted to two variables with (weak) second-order logic over concrete heaps.

Expressive power of separation logic. Separation logic is used as an assertion language for Hoare-style proof systems about programs with pointers [START_REF] Apt | Ten Years of Hoare's Logic[END_REF][START_REF] Reynolds | Separation logic: a logic for shared mutable data structures[END_REF], and there is an ongoing quest for understanding its complexity and expressive power. Alternatively, there are a lot of activities to develop verification methods with decision procedures for fragments of practical use, see e.g. [START_REF] Cook | Tractable Reasoning in a Fragment of Separation Logic[END_REF][START_REF] Haase | SeLoger: A Tool for Graph-Based Reasoning in Separation Logic[END_REF]]. Many decision procedures have been designed for fragments of separation logics or abstract variants, from analytic methods [START_REF] Galmiche | Tableaux and Resource Graphs for Separation Logic[END_REF][START_REF] Hou | Proof search for propositional abstract separation logics via labelled sequents[END_REF][START_REF] Hou | Automated Theorem Proving for Assertions in Separation Logic with All Connectives[END_REF] to translation to theories handled by SMT solvers [START_REF] Piskac | Automating Separation Logic using SMT[END_REF][START_REF] Navarro Pérez | Separation Logic Modulo Theories[END_REF][START_REF] Piskac | GRASShopper -Complete Heap Verification with Mixed Specifications[END_REF][START_REF] Bansal | Deciding local theory extensions via Ematching[END_REF], passing via graph-based algorithms [START_REF] Haase | SeLoger: A Tool for Graph-Based Reasoning in Separation Logic[END_REF]]. Of course, there are also plenty of methods or heuristics that are even more tailored to verification, see e.g. [START_REF] Calcagno | Compositional Shape Analysis by Means of Bi-Abduction[END_REF][START_REF] Thakur | Satisfiability modulo abstraction for separation logic with linked lists[END_REF] and there are plenty of other methods to verify heap manipulating programs, see a nice overview in [START_REF] Chakraborty | Reasoning about heap manipulating programs using automata techniques[END_REF]] for automata-based techniques.

Theoretical issues for separation logic stem from the design of expressive fragments with relatively low complexity (see e.g. [START_REF] Cook | Tractable Reasoning in a Fragment of Separation Logic[END_REF]) to the extension of known decidability results, see e.g. [START_REF] Bozga | Quantitative Separation Logic and Programs with Lists[END_REF][START_REF] Iosif | The Tree Width of Separation Logic with Recursive Definitions[END_REF][START_REF] Antonopoulos | Foundations for Decision Problems in Separation Logic with General Inductive Predicates[END_REF]]. Indeed, it is known since [START_REF] Calcagno | Computability and Complexity Results for a Spatial Assertion Language for Data Structures[END_REF]] that first-order separation logic with two record fields (herein called 2SL) is undecidable (with a proof that does not require separating connectives and uses Trakhtenbrot's Theorem [START_REF] Trakhtenbrot | Impossibility of an algorithm for the decision problem in finite classes[END_REF]). This is sharpened in [START_REF] Brochenin | On the Almighty Wand[END_REF]] by showing that first-order separation logic with a unique record field (herein called 1SL) is also undecidable, as a consequence of the expressive equivalence between 1SL and weak second-order logic. More recently, 1SL restricted to two variables (1SL2) is shown undecidable too [START_REF] Demri | Two-variable separation logic and its inner circle[END_REF] (by reduction from the halting problem for Minsky machines) but without touching the central question of expressive completeness-the purpose of the current paper. From the very beginning, the relationships between separation logic and second-order logic have been quite puzzling (see e.g. an interesting answer with infinite arbitrary structures in [START_REF] Kuncak | On spatial conjunction as second-order logic[END_REF]). Moreover, comparisons of fragments have been also studied, for instance 1SL( * ) has been established strictly less expressive than MSO in [START_REF] Antonopoulos | Separating Graph Logic from MSO[END_REF] (see also the related work [START_REF] Marcinkowski | On the expressive power of graph logic[END_REF]). In this paper, we go one step further by showing that two variables suffice to get expressive completeness, which is a real technical tour de force while establishing quite a surprising result. As a consequence, we conclude that 1SL2(- * ) (that is, 1SL2 without separating conjunction) is undecidable, too. This should not be confused with undecidability results from [START_REF] Brotherston | Undecidability of Propositional Separation Logic and Its Neighbours[END_REF][START_REF] Larchey-Wendling | Nondeterministic Phase Semantics and the Undecidability of Boolean BI[END_REF], which are obtained in an alternative setting with propositional variables and without first-order quantification. It is fair to recall that separating implication (also called the "magic wand") has been less well-studied than separating conjunction in the literature, but its use for program verification is far more recognized nowadays; see e.g. [Lee and Park 2014, Section 1] for a recent, insightful analysis (see also [Hou et al. 2014, Section 8] or [START_REF] Thakur | Satisfiability modulo abstraction for separation logic with linked lists[END_REF][START_REF] Schwerhoff | Lightweight support for magic wands in an automatic verifier[END_REF]).

Our contribution. In this paper, we show that first-order separation logic with one record field, two quantified variables, and no separating conjunction is as expressive as weak second-order logic on heaps; in short, 1SL2(- * ) ≡ WSOL. Even though conjectured in [START_REF] Brochenin | On the Almighty Wand[END_REF][START_REF] Brochenin | Separation Logic: Expressiveness, Complexity, Temporal Extension[END_REF], it is surprising that two variables suffice, and that further we are able to drop the separating conjunction, thus obtaining expressive completeness and undecidability with only two variables and the magic wand operator. In doing so, we improve previous undecidability results about separation logic [START_REF] Calcagno | Computability and Complexity Results for a Spatial Assertion Language for Data Structures[END_REF][START_REF] Brochenin | On the Almighty Wand[END_REF][START_REF] Demri | Two-variable separation logic and its inner circle[END_REF]. Because we forbid ourselves the use of many syntactic resources, this underlines even further the power of the magic wand. By way of comparison with [START_REF] Grädel | Undecidability Results on Two-Variable Logics[END_REF][START_REF] Immerman | The Boundary Between Decidability and Undecidability for Transitive-Closure Logics[END_REF], we show undecidability of a two-variable logic with secondorder features. Our main undecidability result cannot be derived from [START_REF] Grädel | Undecidability Results on Two-Variable Logics[END_REF][START_REF] Immerman | The Boundary Between Decidability and Undecidability for Transitive-Closure Logics[END_REF]] since in 1SL models, we deal with a single functional binary relation, namely the finite heap. We believe that we have identified the core of separation logic as far as undecidability and expressive completeness are concerned, since, for instance, first-order separation logic with one record field, one quantified variable and an unbounded number of program variables, has recently been shown decidable and it admits a PSPACE-complete satisfiability problem [Demri et al. 2014]. Figure 1 illustrates how the main result of the paper (Theorem 5.13) compares with known results from the literature. Section 2 contains formal definitions of the different logics.

Consequences of 1SL2(- * ) ≡ WSOL. The first consequence of the equivalence 1SL2(- * ) ≡ WSOL is certainly that two variables suffice to capture full 1SL and consequently to express any property on heaps that can be stated in weak second-order logic. As a consequence, undecidability holds, and the set of valid formulae in 1SL2(- * ) is not recursively enumerable. Clearly, this contrasts with many logical formalisms, such as FO2 on first-order structures or FO2 on ω-sequences that are decidable when the number of quantified variables is restricted to two or for which the computational complexity decreases significantly, see e.g. [START_REF] Grädel | On the decision problem for two-variable first-order logic[END_REF][START_REF] Etessami | First-Order Logic with Two variables and Unary Temporal logics[END_REF]. Moreover, such an expressive completeness result can be also used to establish structural completeness of separation logic, as shown in [START_REF] Lozes | Separation Logic: Expressiveness and Copyless Message-Passing[END_REF]]. Hence, our main result has many interesting consequences, apart from the proof technique to show it, which we describe briefly, below.

Proof technique. In our proof, most of the difficulties are concentrated on the use of only two variables: we recycle variables as done for modal logics [START_REF] Gabbay | Expressive Functional Completeness in Tense Logic[END_REF]], but this is insufficient, especially when separating conjunction is also banished. So, as far as the proof for expressive completeness goes, we borrow some of the first principles from [START_REF] Brochenin | On the Almighty Wand[END_REF]], but very quickly we are faced with serious problems when we need to identify in some heap at least k > 0 heap patterns (a typical example is to specify that at least k > 0 locations point to a given location).

Indeed, the standard way to identify such patterns is to use an unbounded number of variables or the separating conjunction. So, in the presence of only two variables and by using only the magic wand operator, instead of chopping the heap in k disjoint subheaps, we add O(k) new patterns so that the newly combined heap satisfies structural properties that witness the presence of the k patterns in the original heap. This high-level description has to be instantiated as many times as we have to identify different types of patterns, but this new point of view allows us to go far beyond what was known previously (see e.g., the proof of Lemma 3.3). At times, it is not strictly necessary to introduce a radically new method, but instead we can be more thrifty in the way formulae are defined to express desirable properties; of course, this may come with more complex proofs and, above all, more ingenuity to design such formulae. At last, after using the new techniques, after saving syntactic resources on formulae and after using first principles from [START_REF] Brochenin | On the Almighty Wand[END_REF], we are able to design a lengthy and tedious proof and to conclude that 1SL2(- * ) is as expressive as weak second-order logic on heaps, and as a by-product it is also the smallest known undecidable fragment of separation logic.

It should be noted that the paper is structured in such a way that we provide more and more complex building blocks to establish our main results. Indeed, after Section 2's preliminary material, Section 3 is dedicated to expressing properties about reachability and comparing a number of location predecessors against a constant, whereas Section 4 deals with much richer comparisons between numbers of location predecessors. Another contribution of the present paper rests on the fact that we considerably simplify some of the technical insights borrowed from [START_REF] Brochenin | On the Almighty Wand[END_REF]] and therefore the current paper proposes a self-contained proof of the equivalence between 1SL2(- * ) and weak second-order logic that in many ways is much simpler than what has been done so far, even though our results are stronger. The main result is proven in Section 5. Extensions with program variables or with heaps having k > 1 record fields are presented in Section 6. Furthermore, the variant when an infinite domain is allowed, is briefly discussed in Section 6.

PRELIMINARIES

First-order separation logic with one selector (1SL)

A heap h is a partial function h : N N with finite domain. We write dom(h) to denote its domain and ran(h) to denote its range. Two heaps h 1 , h 2 are said to be disjoint, if their domains are disjoint; when this holds, we write h 1 h 2 to denote their disjoint union. Locations are elements of N and are denoted by l, possibly decorated with superscripts or subscripts. We write

l 1 → l 2 → • • • → l m to mean that for every i ∈ [1, m -1], h(l i ) = l i+1 .
In that case {l 1 , . . . , l m-1 } ⊆ dom(h). We write l to denote the cardinal of the set {l ∈ N : h(l ) = l} made of predecessors of l (heap h is implicit in the expression l) and l to denote the cardinal of ({l ∈ N : h(l ) = l} \ {l}). So, l = l precisely when either l ∈ dom(h) or h(l) = l (otherwise l = l -1 and h(l) = l). Most probably, the notation ' pred(l, h)' is more suggestive of its meaning than l since it contains 'pred' by reference to the predecessors of l and the heap h is made explicit. However, we believe that ' pred(l, h)' is a bit lengthy, especially when it is used in more complex expressions. The same applies for the alternative notation ' pred \l (l, h)' instead of l . Usually, in models for separation logic(s), memory states have a heap and also a store, for interpreting program variables (see e.g. [START_REF] Reynolds | Separation logic: a logic for shared mutable data structures[END_REF]). Herein, there is no need for program variables; we establish expressiveness results without their help. However, an adaption with program variables is presented in Section 6.

Let FVAR = {u 1 , u 2 , . . .} be a countably infinite set of variables. Formulae of 1SL are defined by the abstract grammar below:

φ ::= u i = u j | u i → u j | φ ∧ φ | ¬φ | φ * φ | φ - * φ | ∃ u i φ.
The connective * is called the separating conjunction and the connective - * is called the separating implication (also known as the magic wand). We make use of standard definitions to derive other standard operations (∀, ∨, ⇒, =, etc.).

A valuation is a map f of the form FVAR → N. The satisfaction relation |= is parameterized by valuations and is defined as follows (Boolean clauses are omitted):

-h |= f u i = u j iff f(u i ) = f(u j ). -h |= f u i → u j iff f(u i ) ∈ dom(h) and h(f(u i )) = f(u j ). -h |= f φ 1 * φ 2 iff there exist h 1 , h 2 such that h 1 and h 2 are disjoint, h = h 1 h 2 , h 1 |= f φ 1 and h 2 |= f φ 2 . -h |= f φ 1 - * φ 2 iff for all h , if h and h are disjoint, and h |= f φ 1 then h h |= f φ 2 . -h |= f ∃ u i φ iff there exists l ∈ N such that h |= f[ui →l] φ where f[u i → l] refers to a map
equal to f except that u i takes the value l.

We also introduce the so-called septraction operator ¬ - * : φ ¬ - * ψ is defined as the formula ¬(φ - * ¬ψ) [START_REF] Vafeiadis | A Marriage of Rely/Guarantee and Separation Logic[END_REF]. So, h |= f φ ¬ - * ψ iff there exists h , disjoint from h, such that h |= f φ and h h |= f ψ. The septraction operator states the existence of a disjoint heap satisfying a formula and for which its addition to the original heap satisfies another formula. Note that the magic wand makes a universal statement about (disjoint) additions to the heap, septraction an existential one.

For every i ≥ 1, 1SLi denotes the fragment of 1SL restricted to i variables and 1SLi(- * ) denotes its restriction when separating conjunction is disallowed. Let L be a logic among 1SL, 1SLi, 1SLi(- * ). The satisfiability problem for L takes as input a sentence φ from L and asks whether there is a heap h such that h |= φ (regardless of valuation, as φ has no free variables). THEOREM 2.1. [START_REF] Brochenin | On the Almighty Wand[END_REF][START_REF] Demri | Two-variable separation logic and its inner circle[END_REF] The satisfiability problem for 1SL is undecidable, even if restricted to two individual variables (1SL2).

Weak second-order logic (WSOL)

In order to define formulae in WSOL, we consider a family SVAR = (SVAR i ) i≥1 of secondorder variables, denoted by P, Q, R, . . . and interpreted as finite relations over N. Each variable in SVAR i is interpreted as an i-ary relation. A second-order valuation f is an interpretation of the second-order variables such that for every P ∈ SVAR i , f(P) is a finite subset of N i .

Formulae of WSOL are defined by the grammar below:

φ ::= u i = u j | u i → u j | φ ∧ φ | ¬φ | ∃ u i φ | ∃ P φ | P(u 1 , . . . , u n )
where u i , u j , u 1 , . . . , u n are first-order variables and the P are second-order variables with P ∈ SVAR n for some n ≥ 1. We write DSOL (dyadic second-order logic) to denote the restriction of WSOL to second-order variables in SVAR 2 . Like 1SL, models for WSOL are finite heaps and quantification is performed over all possible locations. The satisfaction relation |= is defined as follows (f is a hybrid valuation providing interpretation for both first-order and second-order variables):

-

h |= f ∃ P φ iff there exists a finite relation R ⊆ N n such that h |= f[P →R] φ where P ∈ SVAR n . -h |= f P(u 1 , . . . , u n ) iff (f(u 1 ), . . . , f(u n )) ∈ f(P).
The satisfiability problem for WSOL takes as input a sentence φ in WSOL and asks whether there is a heap h such that h |= φ. By Trakhtenbrot's Theorem (see e.g. [START_REF] Trakhtenbrot | Impossibility of an algorithm for the decision problem in finite classes[END_REF][START_REF] Börger | The Classical Decision Problem[END_REF]), the satisfiability problem for DSOL (and therefore also for WSOL) is undecidable since finite satisfiability for first-order logic with a single binary relation symbol is undecidable. Note that a monadic second-order variable can be simulated by a binary second-order variable from SVAR 2 , and this can be used to relativize a formula from DSOL in order to check finite satisfiability. THEOREM 2.2. [START_REF] Brochenin | On the Almighty Wand[END_REF]] 1SL, WSOL and DSOL have the same expressive power.

Consequently, in order to show that 1SL2(- * ) is as expressive as WSOL (our main result), it is sufficient to prove that every sentence from DSOL has an equivalent sentence in 1SL2(- * ). It is worth noting that Theorem 2.2 can be extended to the case with k > 1 record fields [START_REF] Brochenin | On the Almighty Wand[END_REF], which actually requires a simpler proof. A similar adaptation is possible from our main result (see Section 6).

EXPRESSING PROPERTIES IN 1SL2(- * )

In the following, let u and u be the variables u 1 and u 2 , in either order. Throughout this article, we build formulae with the quantified variables u and u. Note that any formula φ(u) with free variable u can be turned into an equivalent formula with free variable u by permuting the two variables.

One of the first challenges we face in tracking information with 1SL2(- * ) is that of remembering references to memory cells. With only two variables, expressing simple properties of the heap becomes difficult. If we care to express the property the domain of the heap is a singleton, there is no trouble; we can write

∃ u ((∃ u u → u) ∧ ∀ u (u = u ⇒ ¬ (∃ u u → u))) .
However, to express that the domain contains exactly two locations, we run into trouble. With additional variables, this would not be a problem, as we would have the ability to refer to these locations at the same time; similarly, with the separating conjunction * , there would be no difficulty, as we could express our simpler property twice on two disjoint subheaps, each of which must then contain a single memory cell. But with the severe syntactic restriction of 1SL2(- * ), a new method is needed.

In this section, we propose a new and natural method to compare a number of predecessors against a constant, and also a way to express a reachability property.

Warming up with basic properties

Let us begin by defining simple, standard formulae. These are easily seen to be correct.

u has a successor in the heap (equivalently, we say it is allocated):

alloc(u) def = ∃ u u → u.
u is an isolated location, that is, it is not in dom(h), nor is it in ran(h):

isoloc(u) def = ¬alloc(u) ∧ ¬∃ u u → u.
-dom(h) has exactly one location:

(size = 1) def = ∃ u alloc(u) ∧ ∀ u (u = u ⇒ ¬alloc(u)) .
Using the separating conjunction * , it is easy to define the formula (size = k) stating that dom(h) has exactly k locations (k > 1).

u has at least one predecessor:

u > 0 def = ∃ u u → u.
Naturally, since the number of predecessors is nonnegative, we can also write:

u = 0 def = ¬( u > 0).
Let us now proceed with more complicated constructions.

Counting z-predecessors

In this paper, we will make heavy use of counting predecessors of memory locations. This is critical to many of the technical developments of this work; without an adequate number of variables to refer to locations of interest, we instead "remember" locations by installing a large (and uniquely identifiable) number of predecessors to a location in the heap. At another point in the formula, we can identify this location and operate on it, having not used any of the logic's limited syntactic resources.

As one may imagine, counting and comparing numbers of predecessors is difficult to do in this logic. We first build up a method of counting a certain type of predecessor, then use it to formulate more involved constructions, and finally introduce a way to count the full number of predecessors of a location-that is, to compare its number of predecessors with some given k ≥ 0. After this is achieved, nearly the entirety of Section 4 extends this to comparing numbers of predecessors between two locations (rather than just a comparison to some given k).

With that in mind, we first introduce the notion of z-predecessors, which are predecessors of a location that themselves have no predecessors ('z' is for 'zero'). We can then write:

u's predecessors (if it has any) are all z-predecessors:

allzpred(u) def = ∀ u u → u ⇒ u = 0.
u has no z-predecessor:

z u = 0 def = ∀ u u → u ⇒ u > 0.
u has at most k > 0 z-predecessors:

z u ≤ k def = (size = 1) ¬ - * ( z u ≤ k -1)
where z u ≤ 0 is defined as z u = 0.

These definitions easily allow us to define z u k for every k ∈ N and ∈ {=, <, ≤, >, ≥}. The following lemma establishes correctness of the above formulae and all of the derivative forms. LEMMA 3.1. Let h be a heap, f be a valuation, and k ∈ N. We have

h |= f z u ≤ k iff card({l ∈ N : l = 0, h(l) = f(u)}) ≤ k.
PROOF. The proof is by induction on k and the base case with k = 0 is by an easy verification. In the induction step, assume k > 0 and suppose that the induction hypothesis is the following:

h |= f z u ≤ k iff card({l ∈ N : l = 0, h(l) = f(u)}) ≤ k for any k < k. In particular this holds for k = k -1. (⇐) First, suppose that card({l ∈ N : l = 0, h(l) = f(u)}) ≤ k. Case 1: card({l ∈ N : l = 0, h(l) = f(u)}) ≤ k -1.
Let h be the heap with singleton domain such that h (l) = l for some l ∈ (dom(h) ∪ ran(h) ∪ {f(u)}). Because l is quite isolated, we also have that card({l

∈ N : l = 0, (h h )(l) = f(u)}) ≤ k -1 and h |= f (size = 1). By (IH), h h |= f z u ≤ k -1. Consequently, by definition of |=, we get h |= f (size = 1) ¬ - * z u ≤ k -1, that is h |= f z u ≤ k. Case 2: card({l ∈ N : l = 0, h(l) = f(u)}) = k. Let l 0 be in {l ∈ N : l = 0, h(l) = f(u)}
and l be a location not in (dom(h) ∪ ran(h) ∪ {f(u)}). Let h be the heap with singleton domain such that h (l) = l 0 . In h h , f(u) has one less z-predecessor, so card({l ∈ N :

l = 0, (h h )(l) = f(u)}) = k -1 and h |= f (size = 1). By (IH), h h |= f z u ≤ k -1. Consequently, by definition of |=, we obtain h |= f (size = 1) ¬ - * z u ≤ k -1, that is h |= f z u ≤ k. (⇒) Now suppose that h |= f (size = 1) ¬ - * z u ≤ k -1. There is a heap h disjoint from h such that card(dom(h )) = 1 and h h |= f z u ≤ k -1. By (IH), f(u) has at most (k -1)
z-predecessors in h h . By removing h from h h , one can augment the number of z-predecessors of f(u) by at most one (since card(dom(h )) = 1). So, f(u) has at most k z-predecessors in h.

A matter of knives and forks

To address the problem of referring to many distinct memory locations despite not having sufficient variables to do so, we introduce the notion of forks. Forks are simple, recognizable shapes that we add to the heap with the magic wand. The forks can then be found at another point, "deeper" in the formula. Forks are also a critical building block for comparing predecessor counts in Section 4.

A fork in h is a sequence of distinct locations l, l 0 , l 1 , l 2 such that h(l 0 ) = l, l 0 = 2, h(l 1 ) = h(l 2 ) = l 0 and l 1 = l 2 = 0. The endpoint of the fork is l, and its midpoint is l 0 . The fork is isolated iff l = 1 and l / ∈ dom(h). Similarly, a knife in h is a sequence of distinct locations l, l 0 , l 1 such that h(l 0 ) = l, l 0 = 1, h(l 1 ) = l 0 and l 1 = 0. The endpoint of the knife is l, and the midpoint of the knife is l 0 . The knife is isolated iff l = 1 and l / ∈ dom(h). By way of example, the heap represented in Figure 2 contains three knives, two forks and four endpoints (identified by ' '). Of these, one of the depicted forks and one of the knives are isolated. The locations participating in the "lasso" shape, at the right of the figure, are not part of any knife or fork.

To identify fork and knife endpoints in a heap, we define the following formulae:

forkendpt(u) def = ∃ u (u → u ∧ z u = 2 ∧ allzpred(u)) knifeendpt(u) def = ∃ u (u → u ∧ z u = 1 ∧ allzpred(u)) .
Now, let forky(u) be a formula stating that all predecessors of f(u), possibly excepting f(u) itself, are endpoints of forks:

forky(u) def = ∀ u ((u → u ∧ u = u) ⇒ forkendpt(u)) .
Three forks, two endpoints, and a forky location are depicted in Figure 3.

Next, let antiforky(u) be a formula stating that no predecessor of f(u) is the endpoint of a fork, and let antiknify(u) be a formula stating that no predecessor of f(u) is the endpoint of a knife. We define these as

antiforky(u) def = ∀ u (u → u ⇒ ¬forkendpt(u)) antiknify(u) def = ∀ u (u → u ⇒ ¬knifeendpt(u)) .
Note the asymmetry between forky(u) and antiforky(u): f(u) does not have to be the endpoint of a fork for forky(u) to hold (which would be then impossible to realize for all the predecessors of f(u) if f(u) were a self-loop, assuming that the number of predecessors of f(u) remains constant). It is also easy to enforce that the heap is made of a single fork, which will be useful in later constructions. LEMMA 3.2. There exists a formula 1fork in 1SL2(- * ) such that for all heaps h, we have h |= 1fork iff h is made of a single, isolated fork (and nothing else).

PROOF. In a heap h, a trident location, in short a tril, is a location l such that 2: A heap with three knives, two forks, and four distinct endpoints (marked ' ').

• • • • • • • • • • • • • • • • • Fig.
(1) l ∈ dom(h), (2) l has exactly two predecessors and none of them has a predecessor, and (3) h(l) ∈ dom(h).

So, a tril has exactly two predecessors that are both z-predecessors, and it points to the endpoint of a fork. Therefore it belongs to a fork, but it may not be isolated (the endpoint may have more than one predecessor).

Let tril(u) be defined as the following 1SL2(- * ) formula:

tril(u) def = z u = 2 ∧ allzpred(u) ∧ ∃ u (u → u ∧ ¬alloc(u)).
It is easy to show that h |= f tril(u) iff f(u) is a tril. Moreover the following property can be easily established:

-. The heap h is made of a single, isolated fork (and nothing else) iff (1) h contains a unique tril, and (2) for all locations l ∈ dom(h), either l is a tril or h(l) is a tril.

Let 1fork be the formula below, which jointly expresses the properties (1) and ( 2) above.

1fork def = property (1) ∃ u tril(u) ∧ ∀ u (u = u ⇒ ¬tril(u)) ∧ ∀ u alloc(u) ⇒ (tril(u) ∨ (∃ u (u → u) ∧ tril(u))) property (2)
.

Clearly, then, h |= 1fork iff h is made of a single, isolated fork (and nothing else).

Counting predecessors

We now have the necessary developments to build formulae that constrain the total number of predecessors (not just z-predecessors) of a location: with k ∈ N, we define

u ≤ k def = ¬∃ u u → u k = 0 (u → u ∧ u ≤ k -1) ∨ (¬(u → u) ∧ u ≤ k) k > 0
fork endpoints forky where

u ≤ k def =        ¬∃ u (u → u ∧ u = u) if k = 0 ( u = 0) ¬ - * (antiforky(u) ∧ (1fork ¬ - * • • • ¬ - * 1fork k times ¬ - * forky(u)) k > 0
In a nutshell, f(u) has at most k > 0 predecessors if one can make f(u) antiforky without changing its predecessor count (which is always possible) and then adding k forks to the heap to make f(u) forky (we distinguish the case when f(u) is a self-loop).

In Figure 4, we present three heaps; the leftmost heap is the original heap. The heap in the middle is obtained from the leftmost heap by destroying forks pointing to predecessors of the location (just add memory cells to destroy the fork shapes). The rightmost heap is obtained from the heap in the middle by adding two forks pointing to predecessors of the location , except for the predecessor equal to the location . This amounts to check the satisfaction of u ≤ 2.

LEMMA 3.3. Let k ∈ N, h be a heap and f be a valuation.

(I) h |= f u ≤ k iff f(u) ≤ k. (II) h |= f u ≤ k iff f(u) ≤ k.
PROOF. With k = 0, the proof is by an easy verification. With k ≥ 1, let us start by giving a few definitions that are useful for the proof. First, we define a family (ψ k ) k∈N of formulae in 1SL2(- * ) so that ψ 0 def = forky(u) and

ψ k+1 def = 1fork ¬ - * ψ k . For all formulae in (ψ k ) k∈N , the variable u is free. Each formula u ≤ k with k ≥ 1 is thus equal to (u → u) ∧ ( u = 0) ¬ - * (antiforky(u) ∧ ψ k-1 ) ∨ ¬(u → u) ∧ ( u = 0) ¬ - * (antiforky(u) ∧ ψ k ) .
Note that in the first disjunct, requiring that u → u holds is not incompatible with the possibility to add a disjoint heap such that u = 0 holds (thanks to disjointness).

• • • • • • • antiforky( ) • • • • • • • • • forky( ) • • • • • • • • • • • • • • •
Fig. 4: Removing and adding forks.

Similarly, each formula u ≤ k with k ≥ 1 is equal to

( u = 0) ¬ - * (antiforky(u) ∧ ψ k ).
Given a heap h and a location l, we write pne(l) to denote the number of predecessors of l in h that are not endpoints of some forks in h and that, further, are different from l. In particular, for all l ∈ N, pne(l) ≤ l , and also h |= [u →l] forky(u) iff pne(l) = 0. We will establish the following property for all k ≥ 0:

(E). For all l ∈ N, for all heaps h, we have h

|= [u →l] ψ k iff pne(l) ≤ k.
For the base case (k = 0), we have h |= [u →l] ψ 0 iff h |= [u →l] forky(u) (by definition of ψ 0 ) iff all the predecessors of l (possibly with the exception of l) are endpoints of some fork (by the property characterizing the formula forky(u)) iff pne(l) = 0 (by definition of pne(•)) iff pne(l) ≤ 0 (pne(l) is always non-negative).

For the induction step, let us assume that pne(l) ≤ k + 1.

Case 1: pne(l) ≤ k. Let h be some disjoint heap such that h |= 1fork and the endpoint of the unique fork in h is not in (dom(h)∪ran(h)∪{l}). It is always possible to construct such an h since h is a finite structure. Still, pne(l) ≤ k in h h and therefore by (IH), we have

h h |= [u →l] ψ k . Consequently, there is a disjoint heap h such that h |= [u →l] 1fork and h h |= [u →l] ψ k , whence h |= [u →l] ψ k+1 .
Case 2: pne(l) = k + 1. Let l be some location such that h(l ) = l and l = l. Let h be some disjoint heap such that h |= 1fork and the endpoint of the unique fork in h is precisely l . Again, it is always possible to construct such an h . So, pne(l) = k in h h and therefore by (IH), we have

h h |= [u →l] ψ k . As for Case 1, we can conclude that h |= [u →l] ψ k+1 . Now assume that h |= [u →l] ψ k+1 , i.e., h |= [u →l] 1fork ¬ - * ψ k .
There is a heap h disjoint from h such that h |= [u →l] 1fork and h h |= [u →l] ψ k . By (IH), pne(l) in h h is less than or equal to k (say it equals k ). If the endpoint of the unique fork in h is a predecessor of l that is not the endpoint of some fork in h and different from l, then pne(l) in h is at most k + 1 ≤ k + 1. Otherwise, if the endpoint of the unique fork in h is not a predecessor of l, then pne(l) in h is at most k ≤ k. In both cases, pne(l) ≤ k + 1 in h. So, we have established (E). Now let h be some heap. We have

( †) h |= [u →l] ( u = 0) ¬ - * (antiforky(u) ∧ ψ k )) iff there exists a heap h disjoint from h such that l in h is equal to l in h h , h h |= [u →l]
antiforky(u) and pne(l) ≤ k in h h . l in h is equal to l in h h (and also l is the same in both heaps), and l is antiforky in h h , so pne(l) in h is less than or equal to pne(l) in h h , and pne(l) = l in h h . Now, ( †) iff there exists a heap h disjoint from

h such that l in h is equal to l in h h , h h |= [u →l] antiforky(u), and l ≤ k in h h .
Since it is always possible to build a disjoint heap h satisfying those properties, we have that ( †) is equivalent to l ≤ k in h. This establishes (I).

By performing a simple case analysis depending whether h(l) = l, we can show that for all heaps h, for all locations l, for all k ≥ 1, we have h

|= [u →l] u ≤ k iff l ≤ k.
As a conclusion, we have established (II) as well.

Thus we can express in 1SL2(- * ) the following properties:

-f(u) has at least k predecessors: u ≥ k def = ¬ ( u ≤ k -1). -f(u) has exactly k predecessors: u = k def = u ≤ k ∧ u ≥ k.
Of course we can also define strict inequalities. Note that these definitions are entirely consistent with the earlier definitions of u > 0 and u = 0 given in Section 3.1. Furthermore, all the difficulties to define u ≥ k vanish if we consider the fragment 1SL2( * ); it is sufficient to consider k identical conjuncts (∃ u u → u) built with the separation conjunction.

Lonely memory cells

The formula below states that f(u) is an isolated cell: it is allocated but has no predecessors, its successor has no other predecessors besides it, and its successor has itself no successor.

isocell(u) def = u = 0 ∧ ∃ u u → u ∧ u = 1 ∧ ¬alloc(u) .
Now, we can express a useful property of the heap itself. A heap h is segmented whenever dom(h) ∩ ran(h) = ∅ and no location has strictly more than one predecessor. Otherwise said, all the memory cells in h are isolated. This segmentation can be naturally expressed in 1SL2(- * ):

seg def = ∀ u ∀ u u → u ⇒ ( u = 1 ∧ u = 0) .

Expressing reachability

In 1SL, reachability can be expressed, and [START_REF] Demri | Two-variable separation logic and its inner circle[END_REF] gives a technique for doing so with the two-variable restriction 1SL2, itself a variant of material from [START_REF] Dawar | Expressiveness and complexity of graph logic[END_REF][START_REF] Brochenin | On the Almighty Wand[END_REF].

In 1SL2(- * ) we do not have the luxury of using the separating conjunction, but we can still specify reachability between a pair of locations-say from f(u) to f(u), since our goal is to write a formula parameterized by u and u. However, we need a new technique: we first install a fork at f(u), we propagate this fork forward in the heap, and finally we check whether f(u) is the endpoint of some fork. This is analogous to the way reachability is handled with a monadic second-order predicate, but here, a finite set of locations is identified by propagation of forks. We define propagate(u) as the formula characterizing the property that f(u) is the endpoint of some fork in h, and that the property of being the endpoint of some fork is propagated along memory cells. The reachability predicate (for reachability from f(u) to f(u)) is written reach(u, u):

propagate(u) def = forkendpt(u) ∧ ∀ u ∀ u (u → u ∧ forkendpt(u)) ⇒ forkendpt(u) reach(u, u) def = - * propagate(u) ⇒ forkendpt(u) .
The purpose of the initial " - * " is to enrich the original heap such that the satisfaction of the formula propagate(u) implies the satisfaction of the formula forkendpt(u). Of course, a disjoint subheap could change the very reachability property we are testing. But some such subheaps do not, and the implicit universal quantification of the magic wand ensures that we are on the safe side: if for all combined heaps satisfying propagate(u), f(u) is the endpoint of a fork, then we can conclude that f(u) reaches f(u) in the original heap. LEMMA 3.4. Given a heap h, a location l, and a valuation f,

if h |= [u →l] propagate(u), then for all k ≥ 0, if h k (l) exists, then h |= [u →h k (l)] forkendpt(u).
PROOF. The proof is by induction on k. To show the base case (k = 0), note that for any location l, h 0

(l) = l. h |= [u →l] propagate(u) implies h |= [u →l] forkendpt(u), so h |= [u →h k (l)] forkendpt(u).
Now we assume the statement holds for some k ≥ 0 and prove the result for k + 1. Assuming h k+1 (l) exists, we need to show h |= [u →h k+1 (l)] forkendpt(u). If h k+1 (l) exists then h k (l) does also (and is its predecessor). By (IH), we get h

|= [u →h k (l)] forkendpt(u). Thus h |= [u →h k (l),u →h k+1 (l)] u → u ∧ forkendpt(u). By the definition of propagate(u) we have h |= ∀ u ∀ u (u → u ∧ forkendpt(u)) ⇒ forkendpt(u) , so therefore h |= [u →h k+1 (l)] forkendpt(u).
LEMMA 3.5. Given a heap h and a valuation f, we have

h |= f reach(u, u) iff h k (f(u)) = f(u) for some k ≥ 0.
PROOF. (⇒) As a direct consequence of h |= f reach(u, u) (that is, expanding the definitions of reach and the magic wand), we know that for all disjoint heaps h such that h h |= f propagate(u), the property h h |= f forkendpt(u) holds. We will next construct such an h where h h |= f forkendpt(u) and use it to demonstrate that f(u) can be reached from f(u) in h.

First, let l reach 0 , . . . , l reach k be the locations reachable from f(u) in h. Let forks = {l ∈ N : l is the midpoint of a fork in h} and let free

def = N \ (dom(h) ∪ ran(h) ∪ {f(u), f(u)}). Next, let l j
i ∈ free be some unique location for all i ∈ [0, k] and j ∈ [1, 3], and let l fork l ∈ free be some unique location for each l ∈ forks, with these two sets of locations disjoint. Now, let h be the unique heap whose graph is exactly the set below:

{(l 1 i , l 3 i ), (l 2 i , l 3 i ), (l 3 i , h i (f(u))) : i ∈ [0, k]} ∪ {(l fork l , l ) : l ∈ forks}.
By construction, h is disjoint from h (since all memory cells are taken from the set free, which does not include any location from dom(h)). The locations l 1 0 , l 2 0 , l 3 0 , f(u) make up a fork with endpoint f(u), so h |= f forkendpt(u), and note that for all i > 0,

l 1 i , l 2 i , l 3 i , h i (f(u)) make up a fork with endpoint h i (f(u)). In particular, this means that for all i ∈ [1, k], l reach i is the endpoint of a fork in h h . Thus h h |= f propagate(u).
Next, observe that l reach 0 , . . . , l reach k are the only fork endpoints that exist in h h . To see this, note that (1) the only forks in h are those with endpoints l reach 0 , . . . , l reach k , (2) forks in h are destroyed such that their endpoints are not endpoints of forks in h h unless they are also endpoints in h , and (3) by construction, h uses locations from the set free that excludes dom(h) ∪ ran(h), so no fork can be "accidentally" constructed by parts from h and h .

Thus, for every location l ∈ N, l is the endpoint of a fork in h h iff l = l reach i for some i.

Now, since we assumed h |= f reach(u, u) and we have found a heap h such that h h |= f propagate(u), the property h h |= f forkendpt(u) holds. Since f(u) is the endpoint of a fork in h h , it must be equal to l reach i (for some i), and consequently must be equal to h i (f(u)) (for some i).

(⇐) Assume that h k (f(u)) = f(u) for some k ≥ 0 and we need to show h |= f reach(u, u). To do so, we must show that for all heaps h disjoint from h, the following property holds true:

( †) If h h |= f propagate(u), then h h |= f forkendpt(u). Assuming h h |= f propagate(u), f(u) is the endpoint of a fork in h h . Now, from Lemma 3.4 we know h h |= f forkendpt(u), completing the proof.
It is notable that 1SL2(- * ) has no need for built-in reachability predicates, in contrast to formalisms from e.g. [START_REF] Immerman | The Boundary Between Decidability and Undecidability for Transitive-Closure Logics[END_REF]]. In the rest of the paper, we generalize, in a sense, what was done here in an ad hoc manner for reachability, so that any second-order property can be represented in 1SL2(- * ).

COMPARING NUMBERS OF PREDECESSORS

The main goal of this section is to define in 1SL2(- * ) a formula expressing that f(u) + k ≤ f(u) + k , where k, k ∈ N, for any heap h and valuation f. Without the restriction on the number of variables, we know that such properties can be expressed in 1SL(- * ) [START_REF] Brochenin | On the Almighty Wand[END_REF]. Note that arithmetical constraints on list lengths can be found in [START_REF] Bozga | Quantitative Separation Logic and Programs with Lists[END_REF]] but this is primitive in the logical formalism. By contrast, we show that constraints of the form f(u) [START_REF] Brochenin | On the Almighty Wand[END_REF]], herein we need to circumvent this issue by proposing an alternative way to express the key properties that are helpful to state that f(u) + k ≤ f(u) + k . Below, we still use first principles from [START_REF] Brochenin | On the Almighty Wand[END_REF]] to construct a formula in 1SL2(- * )-mainly, how to build a fork from a knife and an isolated memory cell-but we will need to bypass the serious problem of having only two variables at our disposal, without permitting ourselves any use of the separating conjunction.

+ k ≤ f(u) + k can be expressed in 1SL2(- * ) itself. Since a property of the form f(u) + k ≤ f(u) + k requires a formula with O(k + k ) variables in 1SL(- * ) according to

Principles of the construction and principal difficulties with 1SL2(- * )

Let h be a heap and f be a valuation for which we wish to check whether f(u) + k ≤ f(u) + k holds (afterward, it will be easy to conclude for f(u) + k ≤ f(u) + k , see the proof of Theorem 4.4). Below, we explain which extensions of h must be performed to achieve this. There will be a correspondence with formulae in 1SL2(- * ) to enforce the construction of these extensions, and this is the subject of the technical developments below. We mainly describe first principles from [START_REF] Brochenin | On the Almighty Wand[END_REF]], but the reader should be warned that in several places, we propose a simplified alternative, apart from the fact that all the formulae need to be part of the restricted fragment 1SL2(- * ).

4.1.1. Preparing the heap. The first step consists in preparing the heap by destroying any forks and knives at f(u) and f(u), and ensuring there are no isolated memory cellsthese properties will be necessary in later steps-while maintaining the number of predecessors at f(u) and f(u). To do this, we augment h with a heap h p so that the following properties are satisfied:

(a). h p is disjoint from h;

(b). f(u) has the same number of predecessors in h and in h h p , say f(u) = m ≥ 0;

(c). f(u) has the same number of predecessors in h and in h h p , say f(u) = m ≥ 0; (d). In h h p , f(u) has no predecessor that is an endpoint of a fork or knife; (e). In h h p , f(u) has no predecessor that is an endpoint of a fork or knife; (f). h h p has no isolated memory cell.

Note that this step is always possible, since to destroy the structure of an isolated memory cell, a fork or a knife, it is sufficient to add a memory cell at some position as to no longer have the object-for instance, to destroy a fork that does not involve either f(u) or f(u) one can give its midpoint a third predecessor. In the case f(u) (or f(u)) is the midpoint of a fork, it is sufficient to add a new memory cell l → l where l is a predecessor of f(u) (so that the fork is destroyed without modifying the number of predecessors of f(u)). We take advantage of the formulae antiforky(•) and antiknify(•) to establish properties (d) and (e); the others are straightforward. (a). h s is disjoint from h h p ; (b). f(u) and f(u) have no predecessors in h s ; (c). In h h p h s , neither f(u) nor f(u) has a predecessor that is an endpoint of a fork or knife (they are antiforky and antiknify).

Although h s is segmented, we cannot assume that h s is completely disconnected from h h p since ran(h s ) ∩ dom(h h p ) may be non-empty but ran(h s ) cannot contain f(u) or f(u). Let n be the number of isolated memory cells in h h p h s . The heap h s may have strictly more than n isolated memory cells but those that really matter are the ones that are isolated in h h p h s . Note that for each q ≥ 0, it is possible to build h q s so that h h p h q s has exactly q isolated memory cells and h q s satisfies the above conditions. In order to construct forks in h h p h s whose endpoints are predecessors of f(u) or f(u), either we can augment the heap with a fork, or we can augment the heap with a knife so that its combination with an isolated memory cell in h h p h s leads to a fork whose endpoint is a predecessor of f(u) or f(u). See Figure 5, which depicts two locations, each with three predecessors. Imagine we are performing the comparison f(u) ≤ f(u) (presently equivalent to f(u) ≤ f(u)). First, a segmented heap is added (allocated locations are marked with a white circle in the figure). The left half of the figure shows the addition of a collection of knives through these segments to make f(u) forky; with the same segments, it must then be possible to add a collection of knives to make f(u) forky. Indeed it is; if this is true for all such segmented heaps, then it must be that f(u) ≤ f(u) . The segments from the segmented heap should really be seen as "potential forks." When k or k is nonzero, we consider additional forks on one or both sides to compensate for the offset.

This illustrates the principle behind the definition of the following property (P): If there is a heap h

[k] disjoint from h h p h s made of isolated knives and k isolated forks so that f(u) is forky in h h p h s h [k] , then there is a heap h [k ] disjoint from h h p h s made of isolated knives and k isolated forks so that f(u) is forky in h h p h s h [k ] . Note that by the conditions satisfied by h [k] or by h [k ] , the number of predecessors of f(u) [resp. f(u)] in h [k] [resp. h [k ]
] is necessarily zero (there is no need to specify explicitly that we do not add predecessors). Indeed, for instance, if in h [k] there were an isolated fork or knife having as endpoint f(u), because h [k] is made of isolated knives and forks, one of the predecessors of f(u) in the newly built heap would not be the endpoint of some fork, and therefore f(u) would not be forky. That predecessor of f(u) in the newly built heap would be the midpoint of the isolated fork or knife that has f(u) as endpoint in h [k] .

Let us return to arithmetical considerations. The number of forks in h h p h s h [k]

whose endpoints are predecessors of f(u) is bounded by n + k and similarly, the number of forks in h h p h s h [k ] whose endpoints are predecessors of f(u) is bounded by n+k . Note also that the number of predecessors of f(u) is the same in h and in h h p h s h [k ] and the number of predecessors of f(u) is the same in h and in

h h p h s h [k] . So, n + k ≥ m implies n + k ≥ m, i.e. n ≥ m -k implies n ≥ m -k .
4.1.3. Checking the resulting heap. By checking step 2 for all n ≥ 0, we get that for all n ≥ 0, we have

n ≥ m -k implies n ≥ m -k , which entails that m -k ≥ m -k , i.e. m + k ≤ m + k , whenever m -k ≥ 0 and m -k ≥ 0.
Universal quantification over n is simulated in a formula by using separating implication. When m < k or m < k, we make a dedicated case analysis (see the proof of Theorem 4.4).

Below, we present the technical developments.

Cutlery revisited

Apart from forks, we introduce the notions of collections and large forks (instrumental in the proof of Lemma 4.1 below). A large fork is a sequence of distinct locations l 1 , • • • , l 5 such that l 1 , l 2 , and l 3 have no predecessors, h(l 1 ) = h(l 2 ) = h(l 3 ) = l 4 , l 4 = 3 and h(l 4 ) = l 5 . Location l 5 is called the endpoint of the large fork and l 4 its midpoint, and as with forks and knives, the large fork is called isolated iff l 5 = 1 and l 5 / ∈ dom(h). A heap h is a collection of knives and forks def ⇔ there is no location in dom(h) that does not belong to an isolated knife or to an isolated fork. Similarly, a heap h is a collection of knives and large forks def ⇔ there is no location in dom(h) that does not belong to an isolated knife or isolated large fork. LEMMA 4.1. There are formulae ksfs, kslfs and ksfs =k (k ≥ 0) in 1SL2(- * ) such that for every heap h, (1). h |= ksfs iff h is a collection of knives and forks, (2). h |= kslfs iff h is a collection of knives and large forks, (3). h |= ksfs =k iff h is a collection of knives and forks with exactly k forks.

It is also worth noting that ksfs =k is of linear size in k and it can be built in space O(log(k)) (see the proof below).

PROOF. First, let us introduce auxiliary formulae. For all ∈ {≤, ≥, =} and i ≥ 0, we define the following formulae (formulae of the form u k are defined in Lemma 3.3):

u 0 k def = u k u +(i+1) k def = ∃ u u → u ∧ u +i k.
For instance, u +6 ≥ 5 states that there is a (necessarily unique) location at distance 6 from u and its number of predecessors is greater than or equal to 5. Note that (for example) ¬ u +i ≥ 0 is not equivalent to u +i < 0 when i = 0, since the negation applies to the existential quantifier rather than to the comparison. This observation allows a shorthand for expressing a property that an ith successor exists; for example,

h |= f u +3 ≥ 0 iff {f(u), h(f(u)), h(h(f(u)))} ⊆ dom(h). Symmetrically, u -(i+1) k def = ∃ u u → u ∧ u -i
k but this plays no role in the rest of the paper and this could be useful in some other context, see e.g. [START_REF] Demri | Two-variable separation logic and its inner circle[END_REF]. Now, in Figure 6, we introduce a classification of the types of allocated locations in knifes, forks and large forks (we take advantage of obvious symmetries) when they occur in collections made of disjoint structures.

1 2 3 4 6 5 ϕ 1 (u) def = ( u = 0)∧( u +1 = 1)∧( u +2 = 1)∧¬( u +3 ≥ 0) ϕ 2 (u) def = ∃ u u → u ∧ ϕ 1 (u) ϕ 3 (u) def = (∃ u u → u ∧ tril(u)) ∧ u +2 = 1 ϕ 4 (u) def = ∃ u u → u ∧ ϕ 3 (u) ϕ 5 (u) def = u = 3 ∧ u +1 = 1 ∧ ¬( u +2 ≥ 0) ∧ allzpred(u) ϕ 6 (u) def = ∃ u u → u ∧ ϕ 5 (u)
Fig. 6: Types of allocated locations in a knife, fork, and large fork, and formulae ϕ τ for each type τ of location.

In order to define the formulae, we make a case analysis depending on the position of an allocated location on a knife, on a fork or on a large fork. This is a bit tedious but without essential technical difficulty. Figure 6 associates a formula ϕ τ for each location of type τ (see the proof of Lemma 3.2 for the definition of tril(u)).

The following properties are then easy to establish (see Figure 6):

(Q 1 ). For all h and f, h |= f ϕ 1 (u) iff f(u) points to the midpoint of an isolated knife.

(Q 2 ). For all h and f, h |= f ϕ 2 (u) iff f(u) is the midpoint of an isolated knife.

(Q 3 ). For all h and f, h |= f ϕ 3 (u) iff f(u) points to the midpoint of an isolated fork.

(Q 4 ). For all h and f, h |= f ϕ 4 (u) iff f(u) is the midpoint of an isolated fork.

(Q 6 ). For all h and f, h |= f ϕ 6 (u) iff f(u) points to the midpoint of an isolated large fork.

(Q 5 ). For all h and f, h |= f ϕ 5 (u) iff f(u) is the midpoint of an isolated large fork.

It is now easy to define ksfs and kslfs:

ksfs def = ∀ u alloc(u) ⇒ ϕ 1 (u) ∨ ϕ 2 (u) ∨ ϕ 3 (u) ∨ ϕ 4 (u) kslfs def = ∀ u alloc(u) ⇒ ϕ 1 (u) ∨ ϕ 2 (u) ∨ ϕ 5 (u) ∨ ϕ 6 (u).
Next, in order to define ksfs =k , the most natural way would be to use * , but in the fragment 1SL2(- * ), separating conjunction is banished. Similarly, using O(k) variables would help to identify k forks but again we have only two variables at hand. It is now time to take advantage of large forks in order to identify forks in the original heap.

We define ψ i as follows:

ψ 0 def = kslfs ψ i+1 def = ∃ u ∃ u ϕ 4 (u) ∧ isoloc(u) ∧ (size = 1 ∧ u → u) ¬ - * ψ i .
Let ksfs =k be defined as ksfs ∧ ψ k .

(A). Let us show that h |= ksfs iff h is a collection of knives and forks.

(⇐) By way of contradiction, assume h is a collection of knives and forks but h |= ksfs. There must exist some location l bad such that h

|= [u →l bad ] alloc(u) ⇒ ϕ 1 (u) ∨ ϕ 2 (u) ∨ ϕ 3 (u) ∨ ϕ 4 (u).
By definition, if h is a collection of knives and forks, every location in the domain of the heap belongs to an isolated knife or to an isolated fork. We consider three cases.

-Assume l bad ∈ dom(h) belongs to an isolated knife. By definition, an isolated knife consists of three distinct locations, l 0 , l 1 , and l, such that h(l 0 ) = l, l 0 = 1, h(l 1 ) = l 0 , l 1 = 0, l = 1, and l ∈ dom(h). There are two cases.

(Case

l bad = l 1 .) l bad = 0, so h |= [u →l bad ] u = 0. h(l bad ) = l 0 and l 0 = 1, so h |= [u →l bad ] u +1 = 1. h(h(l bad )) = l and l = 1, so h |= [u →l bad ] u +2 = 1. Finally, h(h(l bad )) ∈ dom(h), so h |= [u →l bad ] ¬( u +3 ≥ 0). Thus, h |= [u →l bad ] ϕ 1 (u), a contra- diction.
(Case l bad = l 0 .) l bad has a single predecessor l 1 such that h |= [u →l1] ϕ 1 (u) by the same reasoning in the previous case. Thus h |= [u →l bad ] ϕ 2 (u), and we have a contradiction. -Assume l bad ∈ dom(h) belongs to an isolated fork. By definition, an isolated fork consists of four locations l, l 0 , l 1 , and l 2 , such that h(l 0 ) = l, l 0 = 2, h(l 1 ) = h(l 2 ) = l 0 , l 1 = l 2 = 0, l = 1, and l ∈ dom(h).

(Case (⇒) Now assume h |= ksfs but h is not a collection of knives and forks. If h is not a collection of knives and forks, then a location l bad ∈ dom(h) exists that is not on an isolated knife or isolated fork. Contradiction, since ksfs requires such locations to satisfy one of ϕ 1 , ϕ 2 , ϕ 3 , ϕ 4 , which are on isolated knives and isolated forks. Thus, h is a collection of knives and forks. (B). Let us show that h |= kslfs iff h is a collection of knives and large forks (proof very similar to the proof for (A)). (⇐) By way of contradiction, assume h is a collection of knives and large forks but h |= kslfs. There must exist some location l bad such that h

l bad = l 0 .) h(l bad ) = l and l = 1, so h |= [u →l bad ] u +1 = 1. Further, l bad is a tril, so h |= [u →l bad ] tril(u),
|= [u →l bad ] alloc(u) ⇒ ϕ 1 (u) ∨ ϕ 2 (u) ∨ ϕ 5 (u) ∨ ϕ 6 (u).
By definition, if h is a collection of knives and large forks, every location in the domain of the heap belongs to an isolated knife or to an isolated large fork. We consider three cases.

-Assume l bad ∈ dom(h) belongs to an isolated knife. Identical to the first part of Case (A) proven above. -Assume l bad ∈ dom(h) belongs to an isolated large fork. By definition, an isolated large fork consists of five distinct locations l 1 , • • • , l 5 , such that l 1 , l 2 , and l 3 have no predecessors, h(l 1 ) = h(l 2 ) = h(l 3 ) = l 4 , l 4 = 3, h(l 4 ) = l 5 , l 5 = 1, and l 5 ∈ dom(h).

(Case l bad = l 4 .) h(l bad ) = l 5 , l bad = 3, l 5 = 1, and

l 5 ∈ dom(h), so h |= [u →l bad ] u = 3 ∧ u +1 = 1 ∧ ¬( u +2 ≥ 0) ∧ allzpred(u). Thus h |= [u →l bad ] ϕ 5 (u)
, and we have a contradiction.

(Case l bad = l 1 or l bad = l 2 or l bad = l 3 .) h(l bad ) = l 4 , and h |= [u →l4] ϕ 5 (u) by the previous case. Thus h |= [u →l bad ] ϕ 6 (u), and we have a contradiction. -Assume l bad ∈ dom(h). Then h |= [u →l bad ] ¬alloc(u), and we have a contradiction. (⇒) Now assume h |= kslfs but h is not a collection of knives and large forks. If h is not a collection of knives and large forks, then a location l bad ∈ dom(h) exists that is not on an isolated knife or isolated large fork. Contradiction, since kslfs requires such locations to satisfy one of ϕ 1 , ϕ 2 , ϕ 5 , ϕ 6 , which are on isolated knives and isolated large forks. Thus, h is a collection of knives and large forks. (C). Let us show that h |= ksfs =k iff h is a collection of knives and forks with exactly k forks. We first prove an inductive property of ψ i .

We extend the definitions of this section naturally to include a new type of collection. A heap h is a collection of knives, forks and large forks def ⇔ there is no location in dom(h) that does not belong to an isolated knife, fork, or large fork. Inductive property ( * ): For all i ≥ 0, h and f, we have h |= f ψ i iff h is a collection of knives, forks and large forks with exactly i forks. Base case i = 0 is by an easy verification. Indeed, h |= f ψ 0 iff h |= f kslfs (by definition of ψ 0 ) iff h is a collection of knives and large forks (by (B)) iff h is a collection of knives, forks and large forks with exactly zero forks. Now, suppose that the property ( * ) holds for all j ≤ i for some i ≥ 0. Let us show it for i + 1. (⇐) Assume h is a collection of knives, forks and large forks with exactly i + 1 forks. Since h has at least one fork, let l be the midpoint of such a fork and l be an isolated location in h. So, h |= [u →l,u →l ] ϕ 4 (u)∧isoloc(u). Let h be the heap such that card(dom(h )) = 1 and h (l ) = l. Consequently,

(1) h is disjoint from h and h |= [u →l,u →l ] size = 1 ∧ u → u, (2) h h is a collection of knives, forks and large forks with exactly i forks. Actually, in h h , the location l is the midpoint of a large fork and all other locations are untouched by this disjoint union.

By (IH), we have h h |=

[u →l,u →l ] ψ i . By definition of |=, we have h |= [u →l,u →l ] (size = 1 ∧ u → u) ¬ - * ψ i and therefore h |= f ∃ u u (ϕ 4 (u) ∧ isoloc(u)) ∧ (size = 1 ∧ u → u) ¬ - * ψ i (for any valuation f), that is h |= f ψ i+1 . (⇒) Assume that h |= f ψ i+1 . There are locations l and l such that h |= [u →l,u →l ] ϕ 4 (u) ∧ isoloc(u) ∧ ((size = 1 ∧ u → u) ¬ - * ψ i ).
Thus, l the midpoint of a fork in h and by definition of |=, there is a heap

h disjoint from h such that h |= [u →l,u →l ] size = 1 ∧ u → u and h h |= [u →l,u →l ] ψ i .
The heap h is uniquely defined, since card(dom(h )) = 1 and h (l ) = l and by (IH), h h is a collection of knives, forks and large forks with exactly i forks. Since h converts a single fork of h into a large fork, h must be a collection of knives, forks and large forks with exactly i + 1 forks. Now we can proceed with the proof about ksfs =k . (⇐) Assume h is a collection of knives and forks with exactly k forks. By (A), we have h |= ksfs and by ( * ), we have h |= ψ k (indeed h is a collection of knives, forks and large forks with zero large fork and k forks). Since by definition ksfs =k is equal to ksfs ∧ ψ k , we get h |= ksfs =k . (⇒) Now suppose that h |= ksfs =k . Since ksfs =k is equal to ksfs ∧ ψ k , by (A), h is a collection of knives and forks, and by the property ( * ), h is a collection of knives, forks and large forks with exactly k forks. Consequently, h has no large fork and exactly k forks. Hence, h is a collection of knives and forks with exactly k forks.

Using collections of forks for comparison

Here is the way we can use the formulae from Lemma 4.1.

LEMMA 4.2. Let k ≥ 0, h be a heap and f be a valuation such that h |= f antiforky(u) ∧ antiknify(u), h has n isolated memory cells, m = f(u) and m -k ≥ 0.

We have h |= f (ksfs =k ¬ - * forky(u)) iff n ≥ m -k.
The proof of Lemma 4.2 uses principles similar to what has been done in [START_REF] Brochenin | On the Almighty Wand[END_REF][START_REF] Demri | Two-variable separation logic and its inner circle[END_REF] except that all formulae belong to 1SL2(- * ) and we propose a simplified version of the lemma and proof (note also our use of f(u) ).

PROOF. We have h |= f (ksfs =k ¬ - * forky(u)) iff ( †) there is a heap h , disjoint from h, such that h |= f ksfs =k and h h |= f forky(u). First, let us suppose that ( †) holds true with some heap h such that h |= f ksfs =k .

-The only forks in h h whose endpoints are predecessors of f(u) are those from forks in h or those obtained by combining an isolated memory cell from h with a knife from h . Indeed, by assumption h |= f antiforky(u) ∧ antiknify(u). -The number of forks pointing to a predecessor of f(u) in h h is therefore less than or equal to n + k. -The number of predecessors of f(u) (other than f(u) itself, if it has a self-loop) in h h is greater than or equal to its number of predecessors (other than itself) in h. However, since h is collection of knives and forks (and therefore all knives and forks are isolated) and h h |= f forky(u), the number of predecessors of f(u) (excluding f(u) itself) in h is less than or equal to n + k, i.e. n ≥ m -k.

Now suppose that n ≥ m -k and the predecessors of f(u) different from f(u) are p 1 , . . . , p m . Let l 1 1 , l 2 1 , . . . , l 1 n , l 2 n be locations such that for every i ∈ [1, n], we have h(l 2 i ) = l 1 i and l 2 i → l 1 i is an isolated memory cell in h. Let us build h so that it satisfies ( †), which is quite easy to realize. Let l new 1 , . . . , l new m be (new) locations that are not in dom(h) ∪ ran(h) ∪ {f(u)}. We define h so that it contains exactly m -k knives whose endpoints are predecessors of f(u).

For every i ∈ [1, m -k], we define h (l new i ) def = l 1 i and h (l 1 i ) def = p i (which is possible because l 1 i ∈ dom(h)).
We add k additional forks to h whose endpoints are the remaining k predecessors of f(u) different from f(u) itself. It is easy to check that h satisfies ( †).

Consequently,

h |= f (ksfs =k ¬ - * forky(u)) iff n ≥ m -k.
Let anti(u, u) be antiforky(u) ∧ antiknify(u) ∧ antiforky(u) ∧ antiknify(u) and let comp(u, u, k, k ) be defined as follows

comp(u, u, k, k ) def = (seg ∧ u = 0 ∧ u = 0) - * anti(u, u) ⇒ ksfs =k ¬ - * forky(u) ⇒ ksfs =k ¬ - * forky(u) . PROPOSITION 4.3. Let k, k ≥ 0, f be a valuation, h be a heap such that h |= f anti(u, u) ∧ ¬∃ u isocell(u), f(u) -k ≥ 0 and f(u) -k ≥ 0. We have h |= f comp(u, u, k, k ) iff f(u) + k ≤ f(u) + k .
Note that without any loss of generality we could assume that k × k = 0 but we provide below a uniform treatment that does not require to distinguish the case k = 0 from the case k = 0. Moreover, the assumptions f(u) -k ≥ 0 and f(u) -k ≥ 0 in Proposition 4.3 are required for the following reasons. In the proof of Proposition 4.3, we use the fact that for all q, q ∈ N, we have q ≤ q iff for all n ∈ N, we have n ≥ q implies n ≥ q. A similar property holds true for Z, i.e., for all q, q ∈ Z, we have q ≤ q iff for all n ∈ Z, we have n ≥ q implies n ≥ q. However, with q, q ∈ Z, q ≤ q is not equivalent to for all n ∈ N, we have n ≥ q implies n ≥ q. That is why we need to assume that q ( f(u) -k from the statement of Proposition 4.3) and q ( f(u) -k in the statement of Proposition 4.3) belong to N, if the quantification for n is over N.

PROOF. Let h be such that h |= f anti(u, u) ∧ ¬∃ u isocell(u). The statements below are equivalent.

(1) h |= f comp(u, u, k, k ).

(2) For every disjoint heap h such that h

|= f seg ∧ u = 0 ∧ u = 0 and h h |= anti(u, u), if h h |= f ksfs =k ¬ - * forky(u), then h h |= f ksfs =k ¬ - * forky(u). (By definition of |= f .) (3) For every n ≥ 0, let h be a heap disjoint from h such that h h has n isolated memory cells, h |= f seg ∧ u = 0 ∧ u = 0 and h h |= anti(u, u), and if h h |= f ksfs =k ¬ - * forky(u), then h h |= f ksfs =k ¬ - * forky(u).
(By using the fact that it is always possible to add a segmented heap to h so that the resulting heap has n isolated memory cells and doesn't change predecessor counts at f(u) and f(u).)

(4) For every n ≥ 0, we have n ≥ f(u) -k in h implies n ≥ f(u) -k in h. (By Lemma 4.2.) (5) f(u) + k ≤ f(u) + k .
Here is the main result in this section using comp(u, u, k, k ). THEOREM 4.4. For k, k ≥ 0, there is a formula φ in 1SL2(- * ) (of linear size in k + k and it can be built in space O(log(k + k )) such that for all h, f, we have (h

|= f φ iff f(u) + k ≤ f(u) + k ).
We denote such a formula φ as u + k ≤ u + k and, as usual, it easily extends to <, ≥, >, =. The structure of the proof of Theorem 4.4 is similar to the structure of the proof of [Brochenin et al. 2012, Theorem 5.5], except that now all formulae are in 1SL2(- * ) instead of being defined in the less-constrained 1SL(- * ). Moreover, our case analysis is quite different and we also provide several simplifications, making our new proof even more valuable.

PROOF. Below, we show that for k, k ≥ 0, there is a formula φ k,k in 1SL2(- * ) (of linear size in k + k and it can be built in space O(log(k + k )) such that for every heap h and valuation f, we have h |= f φ k,k iff f(u) + k ≤ f(u) + k . Once we have such a φ k,k , we can define φ as:

(u → u ∧ u → u ∧ φ k,k ) ∨ (¬(u → u) ∧ u → u ∧ φ k,k +1 ) ∨ (u → u ∧ ¬(u → u) ∧ φ k+1,k ) ∨ (¬(u → u) ∧ ¬(u → u) ∧ φ k,k ).
Observe that the four disjuncts are exclusive.

So it only remains to define the formulae φ k,k with k, k ≥ 0. By Proposition 4.3, we have the following property for any h, f:

( ). When h satisfies anti(u, u) ∧ ¬∃ u isocell(u), f(u) -k ≥ 0 and f(u) -k ≥ 0, we have h |= f comp(u, u, k, k ) iff f(u) + k ≤ f(u) + k .
Even though the original heap h may not satisfy the formula anti(u, u) ∧ ¬∃ u isocell(u), it can be safely extended to satisfy this property without modifying the number of predecessors of f(u) and f(u).

Whenever f(u) -k ≥ 0 and f(u) -k ≥ 0, we have the following equivalences:

(1) h |= f ( u = 0 ∧ u = 0) ¬ - * (anti(u, u) ∧ (¬∃ u isocell(u)) ∧ comp(u, u, k, k )). (2) There is h disjoint from h such that h |= f ( u = 0 ∧ u = 0), h h |= f anti(u, u) ∧ ¬∃ u isocell(u) and h h |= f comp(u, u, k, k ). (3) There is h disjoint from h such that h |= f ( u = 0 ∧ u = 0) and h h |= f anti(u, u) ∧ ¬∃ u isocell(u) and f(u) + k ≤ f(u) + k (in h h ) by ( ). (4) f(u) + k ≤ f(u) + k in h.
Observe that f(u) and f(u) in h are equal to their values in h h since h |= f ( u = 0 ∧ u = 0). Moreover, (4) implies (3) since it is always possible to extend a model satisfying anti(u, u) ∧ ¬∃ u isocell(u) while preserving f(u) and f(u) . By way of example, if l is a predecessor of f(u), endpoint of the fork l 0 , l 1 , l 2 , l, then adding a memory cell l new → l 2 (assuming that l 2 = f(u)) destroys the fork structure. When l 2 = f(u), we add l new → l 1 instead. Similarly, if f(u) → f(u) and that memory cell is isolated, then it is sufficient to add a new memory cell f(u) → l new with l new distinct from f(u). The other cases can be treated in a similar fashion.

Without any loss of generality, we can assume that k × k = 0. Case k = 0 and k ≥ 0. So f(u) -k ≥ 0 and we need to make a case analysis depending on the satisfaction of f(u) ≥ k . Note that if f(u) < k , then obviously f(u) ≤ f(u) + k . So, we write φ k,k to denote the formula below:

( u < k ) ∨ (( u ≥ k ) ∧ (( u = 0 ∧ u = 0) ¬ - * (anti(u, u) ∧ (¬∃ u isocell(u)) ∧ comp(u, u, 0, k )))).
Formulae of the form u ≥ k (and variants) can be defined thanks to Lemma 3.3. Case k = 0 and k ≥ 0. So f(u) -k ≥ 0 and we need to make a case analysis depending on the satisfaction of f(u

) ≥ k. Note that if f(u) < k, then f(u) + k ≤ f(u) cannot hold.
So, we write φ k,k to denote the formula below:

( u ≥ k) ∧ (( u = 0 ∧ u = 0) ¬ - * (anti(u, u) ∧ (¬∃ u isocell(u)) ∧ comp(u, u, k, 0))).
We can now find locations in a heap with a maximal number of predecessors, and we conclude this section with a definition useful in later constructions. Let us introduce the formula maxdeg(u):

maxdeg(u) def = ¬∃ u u > u.
COROLLARY 4.5. For all h and f, we have h |= f maxdeg(u) iff f(u) = max ({ l : l ∈ N}).

We now have the necessary underlying machinery to tackle the encoding of secondorder formulae in our fragment of separation logic.

EXPRESSIVE COMPLETENESS FOR 1SL2(- * )

In order to express sentences in DSOL by sentences in 1SL2(- * ), a hybrid valuation is encoded in the heap by building a disjoint valuation heap that takes care of pairs of locations (for interpretation of second-order variables) and that takes care of locations (for interpretation of first-order variables). In principle, this makes sense since every heap has a finite domain and therefore there is always an infinite set of locations that is not in its domain. This leaves enough room to encode a finite amount of information such as the interpretation of second-order variables when they are interpreted by finite sets. We can easily add to the original heap with the magic wand; this permits us to create and update the valuation heap. However, we then must always be able to distinguish between the original heap and the valuation heap.

The main idea to build such a valuation heap rests on the fact that a pair of locations (l, l ) belongs to the interpretation of a second-order variable P i whenever l and l can be identified in the valuation heap by special patterns involving l and l that uniquely characterise the interpretation by P i . Similarly, a location l is the interpretation of a first-order variable whenever l can be identified in the valuation heap thanks to some dedicated pattern around l.

Before explaining further the general principles, let us first provide more information about the above-mentioned patterns. An entry of degree d ≥ 2 is a sequence of distinct locations l 1 , . . . , l d , l ind , l such that

-h(l 1 ) = • • • = h(l d ) = l ind , -l ind = d, -l 1 = • • • = l d = 0, and -h(l ind ) = l.
The location l is called the element, l ind the index and the locations l 1 , . . . , l d , the pins. Entries generalize the notions of forks and large forks from Section 3 and are called markers in [START_REF] Brochenin | On the Almighty Wand[END_REF]. See an entry of degree 4 in the middle of Figure 7. So, the pair of locations (l, l ) is identified as part of the interpretation of P i when l and l are elements of entries with very large degree. The above-mentioned special patterns are therefore entries, but we require that the degree of the respective entries for l and l satisfy some arithmetical constraints, which is possible thanks to Theorem 4.4, and which allows us to relate l with l .

Then, the principle of the translation consists in building the valuation heap on demand (typically when a quantification appears) and to find special patterns involving entries with large degree whenever an atomic formula needs to be evaluated.

Apart from our essential restriction to 1SL2(- * ) and therefore the need for encoding also first-order valuations, these principles have been introduced in [START_REF] Brochenin | On the Almighty Wand[END_REF] to translate DSOL formulae into 1SL(- * ) formulae. However, because we are restricted to two first-order variables and because we also require that the separating conjunction is banished, we present below a different way to apply these principles so that we can show that 1SL2(- * ) is expressively equivalent to DSOL (and therefore to WSOL).

This high-level description of the formula translation and of the encoding of some hybrid valuation in the heap hides many of the details, which can be found below. However, before explaining how we apply these principles within 1SL2(- * ), let us emphasize the most obvious and difficult problems to be solved:

(I). we must be able to distinguish the pairs of locations from distinct second-order variables, (II). we also need to encode first-order valuations, and (III). the main problem is certainly to access the original heap properly without interference from the valuation heap.

Left and right parentheses

We introduce variants of entries that are used as delimiters.

A left j-parenthesis of degree d ≥ 3 with j ≥ 0 is a sequence of distinct locations l j+1 , . . . , l 1 , l 1 , . . . , l d , l ind such that

(u). h(l 1 ) = • • • = h(l d ) = l ind ; l ind = d; l j+1 = l 3 = l 4 = • • • = l d = 0, (v). l ind ∈ dom(h); l j+1 → l j → l j-1 → • • • → l 1 → l 1 ; l j = l j-1 = • • • = l 1 = l 1 = 1, and (w). l 2 = 0.
The location l ind is called the index. The heap at the left of Figure 7 presents a left j-parenthesis of degree 3.

A right j-parenthesis of degree d ≥ 3 with j ≥ 0 is a sequence of distinct locations l j+1 , . . . , l 1 , l j+1 , . . . , l 1 , l 1 , . . . , l d , l ind such that (u), (v), and

-l j+1 = 0, -l j = l j-1 = • • • = l 1 = l 2 = 1, and -l j+1 → l j → l j-1 → • • • → l 1 → l 2 .
The location l ind is also called the index. The heap at the right of Figure 7 presents a right j-parenthesis of degree 5. A j-parenthesis can be understood as an entry, except that the index location is not allocated, and containing one or two paths of length j + 1, depending on whether it is a left or a right parenthesis.

LEMMA 5.1. For all j ≥ 0, there is a formula lp j (u) [resp. rp j (u)] in 1SL2(- * ) such that for all heaps h and valuations f, we have h

|= f lp j (u) [resp. h |= f rp j (u)] iff f(u) is the index of some left [resp. right] j-parenthesis in h.
By the proof below, one can add that lp j (u) [resp. rp j (u)] is of linear size in j and it can be built in space O(log(j)).

PROOF. Let us start by defining formulae for backward paths of length j + 1:

-bpath(1, u) def = ( u = 1) ∧ ∀ u (u → u) ⇒ u = 0. -bpath(j + 1, u) def = ( u = 1) ∧ ∃ u (u → u) ∧ bpath(j, u).
So, whenever j ≥ 0, we have h |= f bpath(j + 1, u) iff there are l 0 , . . . , l j such that

l 0 → l 1 → • • • → l j → f(u) and l 0 = 0, for every k ∈ [1, j] l k = 1 and f(u) = 1.
The formula below characterizes the locations such that the predecessors either have no predecessor or have a backward path of length j + 1 exactly:

ϕ j+1 (u) def = ∀ u (u → u) ⇒ ( u = 0 ∨ bpath(j + 1, u)).
Then, the formulae lp j (u) and rp j (u) are defined as follows:

lp j (u)

def = ¬alloc(u) ∧ ϕ j+1 (u) ∧ ( u ≥ 3) ∧ (∃ u (u → u) ∧ bpath(j + 1, u)) ∧ ((size = 1) ¬ - * ϕ j+2 (u)). -rp j (u) def = ¬alloc(u) ∧ ϕ j+1 (u) ∧ ( u ≥ 3) ∧ (∃ u (u → u) ∧ bpath(j + 1, u)) ∧ ¬((size = 1) ¬ - * ϕ j+2 (u)) ∧ ((size = 1) ¬ - * ((size = 1) ¬ - * ϕ j+2 (u))).
The formula lp j (u) states that f(u) is not allocated, it has at least three predecessors and any predecessor of f(u) either has no predecessor or has a backward path of length j + 1. Moreover, there is at least one predecessor of f(u) that has a backward path of length j + 1 thanks to the satisfaction of the subformula (∃ u (u → u) ∧ bpath(j + 1, u)). Satisfaction of the subformula (size = 1) ¬ - * ϕ j+2 (u) entails that there is only one such backward path of length j + 1. A similar analysis can be performed with the formula rp j (u) with the exception that it is required to guarantee that there are exactly two predecessors of f(u) that have a backward path of length j + 1.

In several places, we need to identify the indices from entries as well as their pins. Let eindex(u) be defined as follows:

eindex(u) def = ( z u ≥ 2) ∧ allzpred(u) ∧ ∃ u u → u that characterises indices from entries. Let epin(u) characterise pins from entries: epin(u) def = ∃ u u → u ∧ eindex(u)
. Similarly, we need to characterise the locations from parentheses. We already know how to identify their indices (Lemma 5.1). It remains to identify the other locations via the formula onpar i (u) to characterise the locations on some i-parenthesis: roughly speaking, such locations are exactly those that can reach the index of some i-parenthesis in less than i + 2 steps. Let onpar i (u) be the formula

onpar i (u) def = i+2 j=0 dist i (j, u)
where dist i (j, u) is defined as follows:

dist i (0, u) def = lp i (u) ∨ rp i (u) dist i (j + 1, u) def = ∃ u (u → u) ∧ dist i (j, u) (j ≥ 0).
A rough analysis leads to a construction of onpar i (u) in space O(log(i)) and onpar i (u) is of quadratic size in i.

LEMMA 5.2. Let h be a heap, f be a valuation and i ≥ 0. Then, h |= f onpar i (u) iff f(u) is on some left or right i-parenthesis in h.

PROOF. The proof takes advantage of the following properties.

h |= f dist i (j, u) iff f(u) can reach an index location from a left i-parenthesis or from a right i-parenthesis, in j steps for some j ≥ 0. The proof is obvious, by induction on j. -If f(u) can reach an index location from an i-parenthesis, then f(u) is necessarily on an i-parenthesis. -Every location on an i-parenthesis can reach its index in less than i + 2 steps.

As a conclusion, f(u) is on an i-parenthesis iff it can reach the index of some iparenthesis in less than i + 2 steps, which is exactly the way onpar i (u) is defined with the help of the generalized disjunction.

The role of parentheses

Before explaining the role of parentheses, we introduce the interval of variable indices [1, K] (K ∈ N \ {0}) assuming that for each j ∈ [1, K], either P j or u j occurs in the DSOL formula to be translated (but not both of them). So, the developments below are relative to a finite set of first-order and second-order variables and this is concretized by the interval [1, K] (always possible since a formula has a finite number of variables).

Let us come back to parentheses and assume that X is a subset of [0, K]. In an Xwell-formed heap h (see Definition 5.8 below), the parentheses play the following role. For each j ∈ X, we have the index location lp j from a distinguished left j-parenthesis and the index location rp j from a distinguished right j-parenthesis. Moreover, let d l j = lp j and d r j = rp j (in h). When j ∈ X is related to a first-order variable, we require that d r j = d l j + 2 and there is an entry of degree d l j + 1 such that its element is understood as the interpretation of the variable u j (see Figure 7 with d r j = 5 and d l j = 3). That explains why the parentheses are viewed as delimiters. Similarly, let {(l 1 , l 1 ), . . . , (l β , l β )} be a finite set of pairs of locations, understood as the interpretation of a second-order variable P j with j ∈ X. In h, there are 2β entries whose respective degrees are exactly

{d l j + 3(i -1) + 1, d l j + 3(i -1) + 2 : i ∈ [1, β]} with d r j = d l j + 3β + 1.
A pair of entries of respective degrees d l j + 3(i -1) + 1 and d l j +3(i-1)+2 have exactly as elements l i and l i respectively, which allows to encode the pair (l i , l i ). All this underlying encoding makes sense only if the left and right parentheses as well as the entries whose degrees are related to their degrees are uniquely determined (see Condition (1) in Definition 5.4, below). For this reason, we introduce a left 0-parenthesis and a right 0-parenthesis with d r 0 = d l 0 + 1 (0 is not a variable index), the degree d l 0 is strictly greater than the degree of any location in the original heap, all degrees d l j with j = 0 are strictly greater than d l 0 and finally, the above-mentioned entries and parentheses are the only ones with their respective degrees. This guarantees that any entry from a pair of entries with successive degrees serving for the interpretation of a second-order variable, cannot serve twice for another pair or for another variable. Below, we provide the technical developments.

We say that a heap h is made of entries and parentheses only def ⇔ every location in dom(h) belongs either to a left i-parenthesis for some i ≥ 0, to a right i-parenthesis for some i ≥ 0, or to an entry. Given a heap h made of entries and parentheses only, we define the set indspect(h) as follows: indspect(h) def = { l : l is the index of some entry or parenthesis in h}.

The (finite) set indspect(h) is called the index spectrum of h.

Let h B be a heap such that α = max ({ l : l ∈ N}). For instance, if h B has empty domain, then α = 0. We have seen in Section 4 that it is possible to characterise the locations that witness this maximal value α thanks to the formula maxdeg(u). A valuation heap h V for h B is made of entries and parentheses only whose degrees are greater than max (3, α + 1). The heap h V satisfies the following simple conditions (more constraints will follow): min(indspect(h V )) is greater than max (3, α + 1) and it is witnessed by the degree of some left 0-parenthesis; each degree in indspect(h V ) is witnessed by exactly one entry or parenthesis. The formula indmin(u) below is satisfied in h = h B h V l length (j + 1)

Fig. 7: Encoding [u j → l].
by a location l witnessing the minimal value in indspect(h V ):

indmin(u) def = lp 0 (u) ∧ (∀ u ((u = u) ∧ lp 0 (u)) ⇒ u < u).
Note that thanks to Section 4, we know that it is possible to compare numbers of predecessors as expressed above. So, indmin(u) holds when f(u) is the unique location that is the index of some left 0-parenthesis with greatest degree.

LEMMA 5.3. Let f be a valuation and h be a heap. We have h |= f indmin(u) iff f(u) is an index of some left 0-parenthesis and there is no other location l = f(u) such that l ≥ f(u) and l is the index of some left 0-parenthesis.

The proof is by an easy verification by using Lemma 5.1. Once a heap h satisfies ∃ u indmin(u), the unique location l 0 such that h |= [u →l0] indmin(u) (say with l 0 = d 0 ) plays the role of a delimiter between the original heap and the part of the heap that encodes the hybrid valuation. We have seen that an index spectrum is defined for heaps made of entries and parentheses only. This is fine, but below we adapt the definition to heaps h satisfying ∃ u indmin(u). Let us define the set spect(h) as follows: spect(h) def = { l : l is an index of some entry or parenthesis in h} ∩ [d 0 , +∞[. The (finite) set spect(h) is called the spectrum of h. This illustrates how the location l 0 and the degree l 0 = d 0 play the role of separator between the original heap and the valuation heap.

The subheap encoding the valuation is made of parentheses and entries and we shall need to identify the indices of such patterns. The formula Lindex(u) defined below suffices for this purpose:

Lindex(u) def = (∃ u indmin(u) ∧ u ≤ u) ∧ i∈[0,K] (lp i (u) ∨ rp i (u)) ∨ eindex(u) (u is interpreted as a large index). Given X ⊆ [0, K],
we shall use also the following formula:

Lindex X (u) def = (∃ u indmin(u) ∧ u ≤ u) ∧ i∈X (lp i (u) ∨ rp i (u)) ∨ eindex(u) .
Entries and parentheses with large indices are also called large entries and parentheses, respectively. The elements in [1, K] will be later used as variable indices. Note also that Lindex(u) is of quadratic size in K and it can be built in space O(log(K)). It is easy to define a large index that is also the index of a left [resp. right] parenthesis. Let Llp i (u) def = Lindex(u) ∧ lp i (u) and Lrp i (u) def = Lindex(u) ∧ rp i (u) (see Lemma 5.1). The large index with a maximal degree can be also characterised as follows:

maxLindex(u) def = (∀ u Lindex(u) ⇒ ( u ≤ u)) ∧ Lindex(u).
Below, we state how the parentheses are organized.

Definition 5.4. Let X = {i 0 , . . . , i s } ⊆ [0, K] with 0 = i 0 < i 1 < • • • < i s . A heap h is X-almost-well-formed def ⇔ (1) For every j ∈ [0, s], there is a unique location l l j [resp. l r j ] such that h |= [u →l l j ] Llp ij (u) [resp. h |= [u →l r j ] Lrp ij (u)].
(2) For every j ∈ [0, s], l l j < l r j , and

l r 0 = l l 0 + 1. (3) For every j ∈ [1, s], we have l l j = l r j-1 + 1. (4) h |= [u →l r s ] maxLindex(u).
(5) For every j ∈ [1, s], if i j is the index of a first-order variable, then l l j = l r j -2 (see Figure 7). ( 6) For every j

∈ ([1, K] \ X), there is no location l such that h |= [u →l] Llp j (u) ∨ Lrp j (u).
The definition for X-almost-well-formed heaps mainly specifies the existence of jparentheses with j ∈ X and how their respective degrees are related. The degrees are organized as follows and they all belong to the spectrum of h (below we let d l j = l l j and d r j = l r j ).

d l 0 |= [u →d l 0 ] indmin(u) < d r 0 || d l 0 + 1 < d l 1 < d r 1 || d r 0 + 1 < d l 2 < d r 2 || d r 1 + 1 < . . . < d l s < d r s || d r s-1 + 1 |= [u →d r s ] maxLindex(u)
Moreover, when i j is the index of a first-order variable, we have d r j = d l j + 2. LEMMA 5.5. There exists a formula awfh X in 1SL2(- * ) of cubic size in K (and it can be built in space O(log(K))) such that h |= awfh X iff h is X-almost-well-formed.

PROOF. We consider the conjunction of the formulae below, each of which deals with one of the conditions. The cubic size of awfh X is essentially due to the fact that a linear amount of formulae (in K) is built and each formula is of quadratic size (here, we use the size properties of already introduced subformulae). Below, arithmetical constraints can be expressed thanks to Theorem 4.4 and its immediate consequences. Condition (1) is taken care by the formula below

j∈[0,s] [∃ u Llp ij (u) ∧ ¬(∃ u Llp ij (u) ∧ u = u)] ∧ j∈[0,s] [∃ u Lrp ij (u) ∧ ¬(∃ u Lrp ij (u) ∧ u = u)].
Condition (2) is expressed as follows:

j∈[0,s] [∃ u ∃ u Llp ij (u) ∧ Lrp ij (u) ∧ ( u < u)] ∧ [∃ u ∃ u Llp 0 (u) ∧ Lrp 0 (u) ∧ ( u = u + 1)].
P i (u j , u k ) works (j < i < k): (l, l ) ∈ V h (P i ).
h |= [u →l,u →rp] u > u and therefore l < rp. Consequently, l is the index of some entry and lp < l < rp. Now, suppose that l is the index of some entry and lp < l < rp. Since l is some index, we have h |= [u →l] eindex(u). By (2), we get that d 0 < l and therefore h

|= [u →l] eindex(u) ∧ ∃ u indmin(u) ∧ u ≤ u, which implies h |= [u →l] Lindex(u) by definition of Lindex(u). By assumption, we have h |= [u →l,u →lp] u < u and h |= [u →l,u →rp] u > u and consequently, h |= [u →l] (∃ u Llp i (u) ∧ u < u) and h |= [u →l] (∃ u Lrp i (u) ∧ u > u). So, all the conjuncts of vind i (u) are satisfied and therefore h |= [u →l] vind i (u).
The formula elt j (u) defined below holds true when u is interpreted as the element of the unique entry attached to the first-order variable u j .

elt j (u) def = ∃ u (u → u) ∧ vind j (u).
Let us anticipate a little how the translation from DSOL to 1SL2(- * ) works: the translation of P i (u j , u k ) can be designed as follows:

∃ u (elt j (u) ∧ ∃ u (u → u ∧ vind i (u) ∧ ∃ u ( u = u + 1 ∧ vind i (u) ∧ ∃ u (u → u ∧ elt k (u))))).
These definitions take advantage of the fact that there are unique large left and right parentheses for each variable index. Figure 8 illustrates the constraints satisfied by the formula when j < i < k. From left to right, the figure represents explicitly a left j-parenthesis, then a right j-parenthesis, then a left i-parenthesis, a right iparenthesis and a left k-parenthesis, followed finally by a right k-parenthesis. Other entries and parentheses are present in the figure, but they are represented by dots in order to focus on the memory cells relevant to evaluate the formula obtained by the translation of P i (u j , u k ). The degrees of parentheses and entries increase from left to right.

Taking care of valuations

Now that we have a way of identifying that part of the heap that encodes our valuation, we turn our attention to encoding the valuation itself. Below, we introduce a condition for a subheap to be "glued" to an existing valuation. We distinguish three cases.

-A local 0-valuation is a heap made of a left 0-parenthesis of degree d and a right 0-parenthesis of degree d + 1 only, for some d ≥ 3.

-Let i ∈ [1, K] be the index of some first-order variable. A local i-valuation is a heap made of a left i-parenthesis of degree d, an entry of degree d + 1 and a right iparenthesis of degree d + 2 only, for some d ≥ 3. -Let i ∈ [1, K] be the index of some second-order variable. A local i-valuation is a heap h such that (1) every location l in dom(h) belongs either to a left i-parenthesis, to a right iparenthesis, or to an entry, (2) h contains a unique left [resp. right] i-parenthesis, (3) the minimal value min(indspect(h)) is the degree of some left i-parenthesis, (4) the maximal value max (indspect(h)) is the degree of some right i-parenthesis, (5) the index spectrum indspect(h) is of the form below for some α ≥ 3, β ≥ 0,

{α} ∪ {α + 3(i -1) + 1, α + 3(i -1) + 2 : i ∈ [1, β]} ∪ {α + 3β + 1} (when β = 0, indspect(h) is equal to {α, α + 1}), (6)
there are no two distinct index locations with the same degree.

Note that indspect(h) ⊆ [α, α+3β+1] and the missing values in [α, α+3β+1]\indspect(h) are precisely those in the set {α + 3(i -1) + 3 : i ∈ [1, β]}, i.e. in {α + 3i : i ∈ [1, β]}. Since local i-valuations are typically heaps that are added to the current heap to encode the interpretation of a variable, it is essential to be able to characterise them by 1SL2(- * ) formulae. This is the purpose of the result below.

LEMMA 5.7.

Let i ∈ [0, K]. There is a formula localval i (u) in 1SL2(- * ) (of quadratic size in K and it can be built in space O(log(K))) such that h |= f localval i (u) iff h is a local i-valuation and f(u) is the index of its left i-parenthesis.
PROOF. For characterising local 0-valuations, it is sufficient to express the properties below:

(1) any location in the domain is on some left or on some right 0-parenthesis, (2) there is exactly one left 0-parenthesis whose index is f(u), (3) there is exactly one right 0-parenthesis, (4) l = f(u) + 1 where l is the index of the unique right 0-parenthesis.

(1)-( 4) can be expressed by the formula below:

(∀ u alloc(u) ⇒ onpar 0 (u)) ∧ (lp 0 (u) ∧ ¬(∃ u lp 0 (u) ∧ u = u)) ∧ (∃ u (rp 0 (u) ∧ ¬(∃ u rp 0 (u) ∧ u = u)) ∧ ( u = u + 1)).
Formulae of the form lp i (u) and rp i (u) are provided in the proof of Lemma 5.1 whereas formulae of the form onpar i (u) are provided before the statement of Lemma 5.2.

For characterising local i-valuations for some first-order variable u i , it is sufficient to express the properties below:

(1) any location in the domain is on some left i-parenthesis, or on some right iparenthesis or on some entry, (2) there is exactly one left i-parenthesis whose index is f(u), (3) there is exactly one right i-parenthesis, (4) there is a unique entry, whose degree is d, such that l = f(u) + 2 and f(u

) = d -1
where l is the index of the unique right i-parenthesis.

(1)-( 4) can be expressed by the formula below: around). It is important to guarantee, as the proof does, that adding a new part of the valuation does not destroy what has been built so far. The proof itself is made of an imbrication of case analyses and it takes advantage of our notions of well-formed heaps and local valuations.

Alternative definitions are probably possible (maybe even simpler ones) but their correctness and usefulness should be tested against the satisfaction of Lemma 5.11. We believe that our definitions allow to have relatively clear proofs while avoiding the boredom of repetitive arguments.

PROOF. Let X = {i 0 , . . . , i s } with 0 = i 0 < i 1 < • • • < i s . Since h is X-well-formed, for every j ∈ X, there is a location lp j [resp. rp j ] such that h |= [u →lp j ] Llp j (u) [resp. h |= [u →rp j ] Lrp j (u)].
For instance, each lp j is the index of some left j-parenthesis. Similarly, since h h |= f wfh X∪{i} (so by Lemma 5.9, h h is (X ∪ {i})-well-formed), for every j ∈ (X ∪ {i}), there is a location lp j [resp.

rp j ] such that h h |= [u →lp j ] Llp j (u) [resp. h |= [u →rp j ] Lrp j (u)].
By Definition 5.8, we have the following inequalities in h:

lp i0 < rp i0 < lp i1 < rp i1 < • • • < lp is < rp is . (1)
Similarly, we have the following inequalities in h h :

lp i0 < rp i0 < lp i1 < rp i1 < • • • < lp is < rp is < lp i < rp i . (2)
One of the goals of the proof is to show that (lp i0 , . . . , rp is ) = (lp i0 , . . . , rp is ). Below, we establish the properties (I)-(VIII) and then we show that spect(h h ) = spect(h) indspect(h ).

(I) Let us show that lp 0 = lp 0 and lp 0 in h is equal to lp 0 in h h . Since h |= f indmin(u) and h h |= f indmin(u), we have f(u) = lp 0 = lp 0 . It remains to prove that lp 0 in h is equal to lp 0 in h h .

(1) For every l ∈ dom(h) such that h(l) = lp 0 , there is no l ∈ dom(h ) so that h (l ) = l (otherwise lp 0 is not anymore the index of a 0-parenthesis in h h ). Consequently, lp 0 in h h is not strictly less than lp 0 in h. (2) Let us show now that lp 0 in h h is not strictly more than lp 0 in h. Ad absurdum, suppose that there is a location l such that h (l) = lp 0 and l has no predecessor in h h . So, in h , the location l is necessarily the pin of the left i-parenthesis, or the pin of the right i-parenthesis or the pin of some entry. In all these cases, this implies that lp 0 cannot be anymore the index of a 0-parenthesis in h h , which leads to a contradiction.

Consequently, lp 0 in h is equal to lp 0 in h h and lp 0 = lp 0 .

(II) Any location in dom(h ) belongs either to a left or right i-parenthesis, or to an entry (this is an obvious consequence of the assumption (2) and Lemma 5.7). So, for any l ∈ dom(h ), we can associate a unique index location l ind . We say that a location l ∈ dom(h ) associated to the index location l ind wrongly contributes to a large entry [resp. parenthesis] in h h def ⇔ l belongs to a large parenthesis [resp. entry] in h h with index location l ind distinct from l ind . Below we show that no location in dom(h ) wrongly contributes to a large entry/parenthesis in h h and that the right situation is actually when l ind = l ind . Indeed, if l is an ancestor of l ind in h , adding a disjoint heap preserves that property. So if l belongs to an entry, left or right parenthesis in h h , the only possible index is l ind . So, l cannot wrongly contribute.

Furthermore, if l belongs to ran(h ) and l ∈ dom(h V ) with h = h B h V (such a decomposition is possible because h is X-well-formed), and the associated index location of l in h V is l ind , then l ind is not anymore an index in h h . So glueing two components from h and h V respectively, cannot lead to a new component (with possibly a different index).

As a consequence, an allocated location in h that is not an index cannot be transformed into an index in h h .

(III) Consequently, any large index l in h (either from some entry or from some parenthesis) either remains a large index in h h of the same type and degree, or l is not anymore part of some entry and parenthesis. So, a large index in h cannot be transformed into another type of large index in h h . Roughly speaking, the type of an index is determined by the degree and whether the index is from an entry, from a left j-parenthesis or from a right j-parenthesis for some j.

(IV) lp i in h h is equal to lp i in h . This is a consequence of h |= f isoloc(u), h |= f localval i (u) and h h |= f wfh X∪{i} ∧ Llp i (u).
(V) Let us show that (lp i0 , . . . , rp is ) = (lp i0 , . . . , rp is ), and for every j ∈ [0, s], lp ij in h is equal to lp ij in h h and rp ij in h is equal to rp ij in h h . Suppose that there is j such that lp ij = lp ij . By (III), the left i j -parenthesis with index lp ij cannot be built from (III). By (IV), it cannot be built from the left parenthesis in h neither from the entries in h (because each index is allocated in entries). Similarly, the left i j -parenthesis with index lp ij cannot be built from the right i-parenthesis from h because it contains already two paths of length i + 1. Similarly, suppose that there is j such that rp ij = rp ij . By (III), the right i j -parenthesis with index rp ij cannot be built from (III). By (IV), it cannot be built from the left parenthesis in h neither from the entries in h (because each index is allocated in entries). Similarly, the right i j -parenthesis with index rp ij cannot be built from the right i-parenthesis from h because of the length of the two paths. Additionally, by (III), for every j ∈ [0, s], lp ij in h is equal to lp ij in h h and rp ij in h is equal to rp ij in h h . (2holes) h h |= f wfh X∪{i} implies that there are no d, d + 1 ∈ [min, max] where min is equal to lp i0 in h h , max is equal to rp i in h h , such that neither d nor d + 1 belongs to spect(h h ). This is a direct consequence of the conditions in Definition 5.4 and in Definition 5.8. Similarly, there are no d, d + 1 ∈ [min , max ] where min is equal to lp i in h (lp i is the index of the unique left i-parenthesis), max is equal to rp i in h (rp i is the index of the unique right i-parenthesis), such that neither d nor d + 1 belongs to indspect(h ).

(VI) rp i in h h is equal to rp i in h . Let rp i be the index of the right i-parenthesis in h . Let us first show that rp i = rp i . We know that lp 0 = lp 0 , lp i is the index of the left i-parenthesis in h as well as the index of the large left i-parenthesis in h h (by (IV)). Since lp i in h is equal to lp i in h h (by (IV)), rp i in h h is strictly greater than lp i (in h , or in h h since it is the same value). In particular, lp 0 is strictly less than At the outset, we may rename variables so that these simple conditions are satisfied. We assume that the variable indices for (first-order or second-order) variables are among [1, K]. Obviously, K is less than the size of the formula φ to be translated.

The translation of the formula φ, written T(φ), first applies a top-level translation t top (•) which takes care of initializing the valuation heap (mainly to introduce the left 0-parenthesis and the right 0-parenthesis); then, a recursive map t(•) is applied. So, T(φ) def = t top (φ) where t top (φ) is defined as follows:

t top (φ) def = ∃ u isoloc(u) ∧ (localval 0 (u) ¬ - * (wfh {0} ∧ indmin(u) ∧ (∀ u ((u = u) ∧ ¬Lrp 0 (u)) ⇒ ( u < u)) ∧ t({0}, φ))
). The first step of the translation consists in adding 0-parentheses so that the heap that evaluates t({0}, φ) is {0}-well-formed. The translation map t(•) has two arguments: the formula to be transformed and the set of variable indices for variables that have been quantified so far. The map t(•) is inductively defined as follows (X ⊆ [0, K], ψ subformula of φ):

-t(X, •) is homomorphic for Boolean connectives, -t(X, u i = u j ) def = ∃ u elt i (u) ∧ elt j (u), -t(X, u i → u j ) def = ∃ u ∃ u (elt i (u) ∧ elt j (u) ∧ u → u), -t(X, P i (u j , u k )) def = ∃ u (elt j (u) ∧ ∃ u (u → u ∧ vind i (u) ∧ ∃ u ( u = u + 1 ∧ vind i (u) ∧ ∃ u (u → u ∧ elt k (u))))).
-Translating the quantifiers themselves is a bit trickier, as we need to introduce the new entries to the valuation heap by applying the magic wand. For the quantifier ∃ u i , we choose two locations l and l such that l is the index of the left 0-parenthesis and l is an isolated location in the original heap.

We construct a new heap that is a local i-valuation while enforcing that the index of the left 0-parenthesis is preserved and l becomes the index of the unique large left i-parenthesis (see Lemma 5.11). t(X, ∃ u i ψ)

def = ∃ u ∃ u ((indmin(u) ∧ isoloc(u)) ∧ (localval i (u) ¬ - * (wfh X∪{i} ∧ indmin(u) ∧ Llp i (u) ∧ t(X ∪ {i}, ψ)))).
-The translation with second-order variables is analogous (the formula localval i (u) below is actually defined differently, see the proof of Lemma 5.7):

t(X, ∃ P i ψ) def = ∃ u ∃ u ((indmin(u) ∧ isoloc(u)) ∧ (localval i (u) ¬ - * (wfh X∪{i} ∧ indmin(u) ∧ Llp i (u) ∧ t(X ∪ {i}, ψ)))).
Every subformula t(X, ψ) has no free variable from free(ψ) ⊆ X where free(ψ) denotes the set of variable indices in ψ from either first-order or second-order free variables. As noted by one anonymous referee, a standard trick is to convert first-order variables into second-order ones so that the proof has only to deal with one type of variable. Herein, we do not quite eliminate first-order variables but we provide a uniform treatment for first-order quantifications and second-order quantifications, which essentially amounts to dealing with a single type of encoding. Below, we state the correctness lemma that allows us to get Theorem 5.13 (the proof is by structural induction). LEMMA 5.12 (CORRECTNESS). Let φ be a DSOL sentence of the above form, ψ be one of its subformulae and (free(ψ) ∪ {0}) ⊆ X ⊆ [0, K]. Let h = h B h V be a X-wellformed heap and V h be the valuation extracted from h. Then,

h B |= V h ψ iff h |= t(X, ψ). h |= [u →lj ] vind j (u) and h |= [u →l k ] vind k (u).
Moreover, by definition of V h , there are index locations l i and l i such that (1)

l i = l i + 1, (2) l i , l i ∈ degrees(i, h), (3) h(l i ) = V h (u j ) and h(l i ) = V h (u k ), (4) h |= [u →li] vind i (u) and h |= [u →l i ] vind i (u).
Finally, the formulae elt j (u) and elt k (u) are defined so that h |= [u →V h (uj )] elt j (u) and h |= [u →V h (u k )] elt k (u). So, we have

-l i → V h (u j ) (i.e. h(l i ) = V h (u j )), -l i = l i + 1, -l i → V h (u k ) (i.e. h(l i ) = V h (u k )).
This guarantees the satisfaction of

h |= ∃ u elt j (u) ∧ ∃ u u → u ∧ vind i (u)∧ ∃ u ( u = u + 1 ∧ vind i (u) ∧ ∃ u (u → u ∧ elt k (u))) .
The proof in the other direction is by an easy verification and similar since all of the above implications are indeed equivalences.

Induction step. The induction hypothesis is the following: for every subformula ψ of size strictly less than the size of ψ, for every free(ψ ) ⊆ X ⊆ [0, K], we have h B |= V h ψ iff h |= t(X , ψ ). The cases when the outermost connective is Boolean are by an easy verification.

Case 1: ψ is equal to ∃ u i ψ . Suppose that h B |= V h ∃ u i ψ . By definition of the satisfaction relation |=, there is l ∈ N such that h B |= V h [ui →l] ψ . In case l belongs to the set Y defined below,

Y = dom(h V ) ∪ {l ∈ N : h |= [u →l] j∈X (Llp j (u) ∨ Lrp j (u))}
(and therefore l is an isolated location in h B ), we pick another location l that does not belong to Y and that is also isolated in h B . It is then easy to show that h

B |= V h [ui →l] ψ iff h B |= V h [ui
→l ] ψ . So, without any loss of generality, below we assume that l does not belong to Y .

Let us build h i V and an assignment f such that: (1)

h i V |= f localval i (u), (2) h |= f indmin(u) ∧ isoloc(u), (3) h h i V |= f wfh X∪{i} ∧ indmin(u) ∧ Llp i (u).
Assume that max(X) = j and m is the degree of the right j-parenthesis with greatest degree. It is easy to define a local i-valuation h i V disjoint from h such that the degree of the left i-parenthesis is m + 1, the degree of the right i-parenthesis is m + 3, the degree of the unique entry is m+2, its element is precisely l and all the locations in its domain are isolated in h (always possible since dom(h) ∪ ran(h) is finite).

It is not difficult to check that h i V and f satisfy the above conditions. Since h h i V is (X ∪ {i})-well-formed by construction, by Lemma 5.11, we have

V h [u i → l] equal to V h h i V . Hence, h B |= V h h i V
ψ and by the induction hypothesis, we get h h i V |= whenever there are locations l and l and a disjoint heap h such that:

(1) l is the unique large 0-parenthesis in h and l is isolated in h, (2) h is an i-local valuation such that the index of the left i-parenthesis is l , h h is (X ∪ {i})-well-formed, (3) l is the left 0-parenthesis in h h and l is the left i-parenthesis in h h , (4) h h |= [u →l ,u →l ] t(X ∪ {i}, ψ ).

It is clear that such objects exist by considering the above construction.

The proof in the other direction (i.e. h |= t(X, ψ) implies h B |= V h ∃ P i ψ ) is actually very similar since most of the above implications are indeed equivalences.

Here is the main result of the paper. THEOREM 5.13. For every sentence φ in DSOL, for every heap h, we have h |= φ iff h |= T(φ), so WSOL and 1SL2(- * ) have the same expressive power.

It is worth recalling that we already know that DSOL and WSOL have the same expressive power with 1SL [START_REF] Brochenin | On the Almighty Wand[END_REF].

PROOF. First, we can establish the following lemma: LEMMA 5.14. Let h be some heap, ψ be some sentence in 1SL2(- * ). Then, the propositions below are equivalent: (I). h satisfies the formula below:

∃ u isoloc(u) ∧ (localval 0 (u) ¬ - * (wfh {0} ∧ indmin(u) ∧ (∀ u ((u = u) ∧ ¬Lrp 0 (u)) ⇒ ( u < u) ∧ ψ)).
(II). There is a heap h 0 disjoint from h, that is a local 0-valuation such that h h 0 is {0}-well-formed and its large left 0-parenthesis is precisely the left 0-parenthesis from h 0 . Moreover, h h 0 satisfies ψ.

The proof is by an easy verification but it is helpful to show the correctness of the full translation.

Let φ be a sentence in DSOL. If φ does not satisfy the syntactic conditions defined at the beginning of Section 5.4, one can easily define an equivalent formula in DSOL satisfying those simple conditions. By Lemma 5.14, h |= T(φ) iff there is a heap h 0 disjoint from h, that is a local 0-valuation such that h h 0 is {0}-well-formed and its large 0-parenthesis is precisely the left 0-parenthesis from h 0 and h h 0 satisfies t({0}, φ). It is always possible to build a local 0-valuation h 0 disjoint from h such that its large left 0-parenthesis is precisely the left 0-parenthesis from h 0 . By Lemma 5.12, we have h |= V h 0 φ iff h h 0 |= t({0}, φ). By assumption, if h |= φ, then h |= T(φ) by using Lemma 5.14 and Lemma 5.12. Similarly, if h |= T(φ), by using the equivalences of Lemma 5.14 and Lemma 5.12 in the other direction, we get that h |= φ.

Observe that T(φ) is of cubic size in the size of φ thanks to the size properties of all the subformulae involved in the translation. Moreover, T(φ) can be computed in logarithmic space in the size of φ but here we have to be a bit careful. Indeed, one of the parameters of the translation is the set X of indices and updating it through the translation requires linear space if no further observation is made. However, whenever a formula t(X, ψ) needs to be constructed, X is not arbitrary. The set X is actually the set of variables indices whose variables are quantified above ψ and therefore, it would be possible to omit the first parameter and to reconstruct on demand the set X, which can be done in logarithmic space. Moreover, zero always belongs to X (even though this is not a variable index).

So, the restriction to two variables in 1SL2(- * ) does not reduce the expressive power, unlike restrictions in [START_REF] Venema | A Modal Logic for Chopping Intervals[END_REF][START_REF] Etessami | First-Order Logic with Two variables and Unary Temporal logics[END_REF]] but we know also other logics restricted to two variables that are expressively complete, see e.g. [START_REF] Lutz | Modal Logic and the Two-Variable Fragment[END_REF][START_REF] Marx | Semantic characterizations of navigational XPath[END_REF].

We get the ultimate undecidability result below (no separating conjunction, two quantified variables, one record field). COROLLARY 5.15. Satisfiability problem for 1SL2(- * ) is undecidable.

The absence of program variables in 1SL2(- * ) makes the proof of Corollary 5.15 even more difficult to design, which is perfect to obtain the sharpest undecidability result. An expressiveness result with program variables is briefly presented in Section 6.1. THEOREM 5.16. The set of valid formulae in 1SL2(- * ) is not recursively enumerable.

Indeed, finitary validity for classical predicate logic restricted to a single binary predicate is not recursively enumerable [START_REF] Trakhtenbrot | Impossibility of an algorithm for the decision problem in finite classes[END_REF]], which implies a similar property for DSOL and therefore for 1SL2(- * ) by Theorem 5.13.

It is also possible to establish the following consequences.

COROLLARY 5.17.

(I). Let φ be a sentence in 1SL. There is an equivalent sentence in 1SL2(- * ) of polynomial size in the size of φ.

(II). 1SL2(- * ) is strictly more expressive than 1SL( * ).

Corollary 5.17(II) follows from Theorem 5.13 and 1SL( * ) is strictly less expressive than MSO [Antonopoulos and Dawar 2009, Corollary 5.3] (see also [START_REF] Demri | Expressive power of query languages[END_REF]). Corollary 5.17(I) is a consequence of Theorem 5.13 and of the fact that 1SL can be translated into DSOL in polynomial time. The composition of two maps that increase respectively the formula size only polynomially, provides a formula of polynomial size too.

Our main results are Theorem 5.13 and Corollary 5.15, significantly improving previously known results (see the figure in Section 1). As far as the translation into 1SL2(- * ) is concerned (see the current section but it uses in essential ways the formulae of Section 4), the lack of variables is partially compensated by the introduction of left and right parentheses in order to constrain sufficiently the valuation heap. More importantly, we have shown that this is a viable solution in 1SL2(- * ) despite only having two variables (see the proof of Lemma 5.11). In particular, this means that we were able to apply the method of dividing the heap into two disjoint heaps: the original heap and the heap encoding the valuation without provoking any confusion and this is probably the hardest part of our technical developments (see the proof of Lemma 5.11). This was not at all clear at the outset, and of course, in view of the complexity of the final proof, this led to lengthy arguments to show correctness of the whole enterprise.

Probably, alternative definitions for local i-valuations and X-well-formed heaps are possible, while leading to slightly simpler structures. One may reach the same main results with a unique type of i-parenthesis (instead of having a left version and a right version); maybe only one type of parenthesis is also possible, for instance by repeating the parenthesis i times at the appropriate place. Our current encoding has more constraints and it is more explicit in view of the design of proofs. We believe our current version is a fair compromise between understandable valuation heaps and the complexity of the proofs.

EXTENSIONS

In this section, we present several variants of 1SL2(- * ) for which undecidability or expressive power can be established on the lines of the previous developments.

Adding an unbounded number of program variables

In this section, we consider 1SL with program variables, which is a strict extension of 1SL and therefore undecidability for 1SL2(- * ) is still valid in the presence of program variables. Adding program variables is the usual way to consider separation logic and below we show that the previous developments can be easily lifted to the case with program variables.

Let PVAR = {x 1 , x 2 , . . .} be a countably infinite set of program variables. A memory state is a pair (s, h) such that s : PVAR → N and h is a heap. Actually, the translation T is defined as a variant of the one in Section 5.4 that takes into account program variables. The variant is pretty natural since program variables do not require any encoding.

PROOF. Let us update the translation T from Section 5 as follows so that we can take into account program variables.

t(X, u

i = x) def = ∃ u elt i (u) ∧ u = x t(X, x = x ) def = x = x t(X, x → x ) def = x → x t(X, P i (x, x )) def = P i (x, x ) t(X, u i → x) def = ∃ u (elt i (u) ∧ u → x) t(X, x → u i ) def = ∃ u (elt i (u) ∧ x → u) t(X, P i (u j , x)) def = ∃ u (elt j (u)∧ ∃ u (u → u ∧ vind i (u) ∧ ∃ u vind i (u) ∧ ( u = u + 1 ∧ u → x))) t(X, P i (x, u j )) def = ∃ u ((vind i (u) ∧ u → x)∧ (∃ u vind i (u) ∧ (( u = u + 1) ∧ ∃ u (elt j (u) ∧ u → u)))).
This is all that is required to update the translation, except that we should also guarantee that the allocated locations in the valuation heap do not correspond to the interpretation of program variables. Otherwise, this would lead to an unsound reduction.

To do this, we write PVAR(φ) to denote the set of program variables occurring in φ. In the definition of t top (φ), we replace localval 0 (u) by the formula below:

localval 0 (u) ∧ x∈PVAR(φ) ¬alloc(x) ∧ x∈PVAR(φ) (∀ u (u → x) ⇒ (Lindex(u) ∧ eindex(u))) .
Similarly, in the inductive definition of the translation for quantified formulae, we replace localval i (u) by

localval i (u) ∧ x∈PVAR(φ) ¬alloc(x) ∧ x∈PVAR(φ) (∀ u (u → x) ⇒ (Lindex(u) ∧ eindex(u))) .
The notion of X-well-formed heap is slightly updated in order to exclude the possibility that a location in the domain of the valuation heap corresponds to s(x) for some x ∈ PVAR(φ) and moreover, s(x) cannot be the index of some parenthesis. We have taken care of that in updating the formulae when subformulae of the form localval i (u) were present (see above). So, we can establish the lemma below. Actually, the proof is exactly the proof of Lemma 5.11 since we strengthen the assumptions. LEMMA 6.2 (COMPOSITION). Let f be a valuation, h be an X-well-formed heap with {0} ⊆ X ⊆ [0, K], i ∈ [1, K] \ X and i > max(X), s be a store and h be a disjoint heap such that:

(1) (s, h) |= f indmin(u) ∧ isoloc(u),

(2) (s, h ) |= f localval i (u) ∧ x∈PVAR(φ) ¬alloc(x) ∧ x∈PVAR(φ) (∀ u (u → x) ⇒ (Lindex(u) ∧ eindex(u))) , (3) (s, h h ) |= f wfh X∪{i} ∧ indmin(u) ∧ Llp i (u).

Then, we have spect(h h ) = spect(h) indspect(h ).

With the above update of the translation, we can also establish correctness below, which leads to the proof of the statement. LEMMA 6.3 (CORRECTNESS). Let φ be a DSOL sentence with program variables, ψ be one of its subformulae and (free(ψ) ∪ {0}) ⊆ X ⊆ [0, K]. Let h = h B h V be a X-well-formed heap, s be a store and V h be the valuation extracted from h. Then, we have (s, h B ) |= V h ψ iff (s, h) |= t(X, ψ).

The proof of Lemma 6.3 is similar to the proof of Lemma 5.12 except that there are additional base cases since there are new atomic formulae. By way of example, we present the proof for ψ equal to u j = x.

Since h is X-well-formed and j ∈ X, V h (u j ) is equal to h V (l) where l is the unique index location such that l ∈ degrees(j, h).

Let us recall that elt j (u) = ∃ u (u → u) ∧ vind j (u) with vind j (u) = Lindex(u) ∧ eindex(u) ∧ (∃ u Llp j (u) ∧ u < u) ∧ (∃ u Lrp j (u) ∧ u > u).

First, let us suppose that (s, h B ) |= V h u j = x. This means that V h (u j ) and s(x) are equal, say to l and therefore there is a unique index location l j such that h V (l j ) = l and l j ∈ degrees(j, h). Since l j belong to the index spectrum of h V , the location l j , has the same number of predecessors in h and in h V and it is also an index in h (see Lemma 6.2). Consequently, (s, h) |= [u →l ] elt j (u), whence (s, h) |= ∃ u elt j (u) ∧ u = x. Now suppose that (s, h) |= ∃ u elt j (u) ∧ u = x. There is a location l such that (s, h) |= [u →l ] elt j (u) ∧u = x. Therefore there are an index l j such that l j ∈ degrees(j, h), h(l j ) = l and s(x) = l . By Lemma 6.2, h V (l j ) = l and l j ∈ indspect(h V ). By definition of V h , this implies that V h (u j ) = s(x) and therefore (s, h B ) |= V h u j = x.

The base cases for the other atomic formulae are obtained from those in the proof of Lemma 5.12 in a similar fashion. The cases in the induction step are proved similarly. It is worth noting that we can guarantee that for all x ∈ PVAR(φ), s(x) does not fall in the set Y (see the proof of Lemma 5.12) thanks to the addition of the conjunct

x∈PVAR(φ) ¬alloc(x) ∧ x∈PVAR(φ) (∀ u (u → x) ⇒ (Lindex(u) ∧ eindex(u)))
when a local i-valuation needs to be built.

Extension with k record fields

In this work, we have considered memory cells with a unique record field. It is possible to extend our results to k > 1 record fields, along the lines of [Brochenin et al. 2012, Section 7]. Let kSL be the (separation) logic in which heaps are partial functions h : N N k with finite domain and atomic formulae include u j i → u j (i ∈ [1, k]); kWSOL and kDSOL are defined similarly. Let kSL2(- * ) be the two-variable fragment of kSL with the magic wand as the only separating connective. One can show that every sentence in kDSOL has an equivalent sentence in kSL2(- * ). To do so, we need to adapt the definitions from Sections 3 and 4 so that memory cells involved in the valuation heap are relevant only with respect to 1 → (and comparing numbers of predecessors is performed only with respect to 1 →). Details are tedious because many notions need to be redefined relatively to 1 → but the encoding of valuations is based on the same general principles as for 1SL2(- * ).

Allowing infinite domains

Let kSL ∞ be the variant of kSL in which the heap domain can be either finite or infinite. Remember that in kSL, the heap domain is necessarily finite. The set of valid formulae for kSL ∞ without separating connectives is recursively enumerable, which contrasts with Theorem 5.16. Indeed, the heap can be encoded by a (k + 1)-ary relation that is deterministic on its first argument. By contrast, 1SL ∞ with the separating connectives does not admit a recursively enumerable set of valid formulae. Indeed, finiteness of the heap domain is a property that can be internalised in 1SL ∞ with the quite simple formula seg ¬ - * ∀ u alloc(u). By contrast, classical predicate logic cannot specify finiteness of the model. LEMMA 6.4. For every heap h, dom(h) is infinite iff h |= seg ¬ - * ∀ u alloc(u).

PROOF. Let h be a heap such that dom(h) is infinite. Let l 1 , l 2 , . . . be an arbitrary enumeration of the locations in dom(h). Suppose that N\dom(h) is infinite. Let l 1 , l 2 , . . . be an arbitrary enumeration of the locations in N \ dom(h). Let h be the heap such that dom(h ) = N \ dom(h) and for every i ≥ 1, we set h (l i ) = l i . Since {l 1 , l 2 , . . .}, {l 1 , l 2 , . . .} is a partition of N, we have h |= seg. As dom(h) dom(h ) = N, we conclude that h h |= ∀ u alloc(u), whence h |= seg ¬ - * ∀ u alloc(u). When N \ dom(h) is finite, we follow a similar and even simpler reasoning, the details are omitted. Now, let h be a heap such that dom(h) is finite. Suppose that h |= seg ¬ - * ∀ u alloc(u). So, there is a heap h such that h |= seg and h h |= ∀ u alloc(u). Let l 1 , l 2 , . . . be an arbitrary (infinite) enumeration of the locations in dom(h ). Since h |= seg, h (l 1 ), h (l 2 ), . . . is an infinite sequence of distinct locations. Since dom(h) is finite, there is i such that h (l i ) ∈ dom(h), say h (l i ) = l j , which leads to a contradiction because h is supposed to be a segmented heap.

Let SOL be the variant of WSOL such that quantification over infinite relations is allowed and the models are those of 1SL ∞ . The logic SOL is therefore not a 'weak' version of second-order logic since second-order variables are not required to be interpreted by finite relations. It is open whether there exist statements in SOL that cannot be expressed in 1SL ∞ . A possible candidate statement could be that there are an infinite number of non-empty connected components that are pairwise isomorphic. Indeed, this property can be expressed in SOL, in particular because infinity of a set can be expressed as well as isomorphism between two connected components. By contrast, it is unclear how to express it in 1SL ∞ . Note that if we attempted to adapt the proof from the previous sections to show that 1SL ∞ and SOL have the same expressive power, we encounter a problem. For our encoding (see Section 5), we relied on having an infinite supply of isolated locations to draw from in order to build our valuation heap. If all the locations are "used up," so to speak, this is impossible.

CONCLUSION

We have shown that first-order separation logic with one record field, two quantified variables and no separating conjunction, 1SL2(- * ), is as expressive as weak secondorder logic on concrete heaps (Theorem 5.13). As a consequence, the satisfiability problem for 1SL2(- * ) is undecidable (Corollary 5.15) and we have identified the undecidable core of separation logic, significantly improving several known results from the literature [START_REF] Calcagno | Computability and Complexity Results for a Spatial Assertion Language for Data Structures[END_REF][START_REF] Brochenin | On the Almighty Wand[END_REF]]. Moreover, this entails that 1SL2(- * ) has no finite axiomatization since weak second-order logic is not finitely axiomatizable.

On the positive side, we have provided means to express rich properties by only using a restricted amount of syntactic resources. Nevertheless, first-order separation logic with one record field, one quantified variable and an unbounded number of program variables, has recently been shown decidable and it admits a PSPACE-complete satisfiability problem [Demri et al. 2014]. Similarly, fragments using the list predicate ls and restricted use of the magic wand - * or the separation conjunction * are known to admit decision procedures or semi-procedures, see e.g. [START_REF] Cook | Tractable Reasoning in a Fragment of Separation Logic[END_REF][START_REF] Thakur | Satisfiability modulo abstraction for separation logic with linked lists[END_REF]] and they are useful for formal verification. That is why, there are still some room to find fragments of separation logics that are tailored for verification and that have low computational cost, see also [START_REF] Sighireanu | Report on SL-COMP 2014[END_REF] where is described how the first competition of solvers for several fragments of separation logic has been run and which fragments have been considered.

We only use two variables, and our results also exclude separating conjunction, which is quite remarkable in view of the restricted number of variables. As far as the proofs of these results are concerned, we used first principles from [START_REF] Brochenin | On the Almighty Wand[END_REF]] but we had to provide non-trivial adaptations to fit the restricted frag-ment 1SL2(- * ). However, this illustrates the robustness of those principles since they could be applied by using the proof techniques developed in the present paper. Other semantical variants are possible; those variants may include the case when heap domain may be infinite (see Section 6.3) or when composition of heaps is allowed as soon as they agree on their common part. Finally, we believe that we identified a remarkable example of a two-variable logic that is equivalent to a queen logic, namely weak second-order logic, and that we have illustrated further the power of separating implication when interpreted on concrete heaps.

Certainly, this work can be completed or refined following several directions. We mention some of them below, sometimes inspired by remarks made by the anonymous referees. At the atomic level, the points-to formulae x → y could be replaced by its exact version x → y or even by its undirected version (which is less relevant in the context of links). How does the undecidability status of 1SL2(- * ) evolve with such variants? Similarly, we have established undecidability of 1SL2(- * ) but without placing it precisely in the arithmetical hierarchy: what is an optimal upper bound? Finally, the formulae in 1SL2(- * ) used to encode the formulae from DSOL are constructed with the septraction (or the magic wand) often with restrictions on the antecedents of septraction. What would be an optimal restriction on antecedents of septraction (for instance) that would preserve undecidability? Answering to most of these questions, would refine further the results presented in the paper.

Fig. 1 :

 1 Fig. 1: Contribution of the paper and related work.

Fig. 3 :

 3 Fig. 3: Forky locations.

Fig. 5 :

 5 Fig.5: Using knives and segments to make forks and compare predecessor counts.

  and h |= [u →l bad ] ϕ 4 (u), and we have a contradiction. (Case l bad = l 1 or l bad = l 2 .) h(l bad ) = l 0 , and h |= [u →l0] ϕ 4 (u) by the previous case. Thus h |= [u →l bad ] ϕ 3 (u), and we have a contradiction. -Assume l bad ∈ dom(h). Then h |= [u →l bad ] ¬alloc(u), and we have a contradiction.

Fig. 8 :

 8 Fig.8: How the translation of P i (u j , u k ) works (j < i < k): (l, l ) ∈ V h (P i ).

  Formulae of 1SL with program variables are built from expressions of the form e ::= x | u where x ∈ PVAR and u ∈ FVAR, and atomic formulae of the form π ::= e = e | e → e .Formulae are defined by the grammarφ ::= π | φ ∧ ψ | ¬φ | φ * ψ | φ - * ψ | ∃ u φ, where u ∈ FVAR. A valuation is a map f : FVAR → N.The satisfaction relation |= is extended as follows: -(s, h) |= f e = e iff e = e , with x def = s(x), u def = f(u). Obviously, program variables can be understood as free quantified variables interpreted rigidly. -(s, h) |= f e → e iff e ∈ dom(h) and h( e ) = e .The satisfiability problem takes as input a sentence from 1SL with program variables, in which the only free variables are program variables. The version of DSOL with program variables is defined similarly when models are memory states. THEOREM 6.1. There is a translation T such that for every sentence φ in DSOL with program variables, the sentence T(φ) in 1SL2(- * ) with program variables (of polynomial size in the size of φ) is such that for all (s, h), we have (s, h) |= φ iff (s, h) |= T(φ).

4.1.2. Addition of a segmented heap. This step consists in checking whether, for each segmented heap h s satisfying certain properties, the condition (P) defined below holds true. The heap h s must be segmented and also must satisfy the following:

ACKNOWLEDGMENTS

We would like to thank the anonymous referees for many suggestions that help to improve the quality of the paper. We are also grateful to the anonymous referees of the CSL-LICS 2014 edition of this paper for their suggestions and remarks.

Work partially supported by the EU Seventh Framework Programme (under grant PIOF-GA-2011-301166, DATAVERIF), the Air Force Office of Scientific Research (under award FA9550-09-1-0596), and the National Science Foundation (under grant 0644299). Part of this work was completed when the first author visited the ACSys group at New York University during the outgoing phase of the Marie Curie IOF Project DATAVERIF. This is a completed and extended version of [Demri and Deters 2014].

Condition (3) is dealt with

Condition (4) is expressed by ∃ u Lrp is (u) ∧ maxLindex(u). Condition ( 5) is easily expressed by the formula below:

Because of the unicity of the left or right parentheses, alternative formulae can be defined by using universal quantifiers instead of existential ones. By way of example, the respective formulae expressing the conditions (3) and ( 5) with universal quantifiers are the following:

Finally, Condition ( 6) is expressed by: j∈[1,K]\X ¬∃ u (Llp j (u) ∨ Lrp j (u)).

Let h be an X-almost-well-formed heap for some {0} ⊆ X ⊆ [0, K] and i ∈ X. We write vind i (u) to denote the formula below:

It characterises indices whose degree is strictly between the degree of some large left i-parenthesis and the degree of some large right i-parenthesis. The size of vind i (u) is quadratic in K. We write degrees(i, h) to denote the set:

LEMMA 5.6. Let h be a heap such that h |= ∃ u indmin(u) and i ≥ 0 be such that there are unique locations lp and rp with h |= [u →lp] Llp i (u) and h |= [u →rp] Lrp i (u). For every l ∈ N, we have h |= [u →l] vind i (u) iff l is the index of some entry and lp < l < rp.

PROOF. Let h be a heap such that:

(2) There is a unique index location lp such that h |= [u →lp] Llp i (u) and lp ≥ d 0 .

(3) There is a unique index location rp such that h

For characterising local i-valuations for some second-order variable P i , it is sufficient to express the properties below:

(1) any location in the domain is on some left i-parenthesis, or on some right iparenthesis or on some entry, (2) there is exactly one left i-parenthesis whose index is f(u), (3) there is exactly one right i-parenthesis whose index is the location l, (4) any entry has degree in [ f(u) + 1, l -1] and its index is the unique one with that degree, (5

there is an entry with degree f(u) + 1, (b) there is an entry with degree f(u) + 2, (c) if there are entries with respective degree d and d + 1, then there is no entry or right i-parenthesis of degree d + 2, (d) if there are entries with respective degree d and d + 1 and d + 3 < l, then there are entries of respective degree d + 3 and d + 4.

(1)-( 5) can be expressed by the formula below:

(6a)-(6d) can be expressed by the formula below:

The definition for X-almost-well-formed heaps mainly takes care of parentheses. In Definition 5.8 below, constraints on the degrees of large indices are specified.

(1) h is X-almost-well-formed, (2) for every j ∈ [1, s], if i j is the index of a first-order variable, then degrees(i j , h) is a singleton, (3) for every j ∈ [1, s], if i j is the index of a second-order variable, then degrees(i j , h) is the set below for some α j ≥ 3, β j ≥ 0:

Lindex(u) and l = l . (5) If a location has degree greater than the degree of the unique large left 0parenthesis, then it is a large index.

When h is X-well-formed, we write h = h B h V such that dom(h V ) is made of entries and parentheses of degree d ≥ l 0 for some l 0 ∈ N such that h |= [u →l0] indmin(u) (i.e., l 0 is the index of the left 0-parenthesis with the maximal degree). More precisely, l ∈ dom(h

. By Definition 5.8, we have spect(h) = indspect(h V ) and clearly the decomposition is unique since l 0 is unique.

Again, well-formed heaps can be characterised by formulae in 1SL2(- * ) whose size is cubic in K.

LEMMA 5.9.

PROOF. We consider the conjunction of the formulae below, each of them deals with one of the five conditions. Condition ( 1) is obviously taken care by the formula awfh X (see the proof of Lemma 5.5). Condition ( 2) is dealt with the formula below:

Note that since the heap is already X-almost-well-formed, at most one location can satisfy the above existential quantification for each FO variable index i j . Similarly, Condition (3) is taken care by the formula below (see the proof of Lemma 5.7 and more specifically Condition (6) in that proof with indices from second-order variables):

The above formula expresses the conditions below, mimicking Condition (6) from the proof of Lemma 5.7: (a) there is an entry with degree d l + 1 where d l is the degree of the unique left i jparenthesis, (b) there is an entry with degree d l + 2, (c) if there are entries with respective degree d and d + 1 in degrees(i j , h), then there is no entry or right i j -parenthesis of degree d + 2 in degrees(i j , h), (d) if there are entries with respective degree d and d + 1 in degrees(i j , h) and d + 3 < d r where d r is the degree of the unique right i j -parenthesis, then there are entries of respective degree d + 3 and d + 4 in degrees(i j , h).

Condition ( 4) is expressed as follows by simply internalizing the condition in 1SL2(- * ):

Condition ( 5) can be expressed as follows:

Let us define formally a valuation from a valuation heap.

Definition 5.10. Let h be an X-well-formed heap for some {0} ⊆ X ⊆ [0, K].

-For every second-order i ∈ X, we define

-For every first-order i ∈ X,

where l is the unique index location such that l ∈ degrees(i, h).

We say that V h is the valuation extracted from h.

Below, we present an essential technical result stating how heaps can be composed when a new variable needs to be interpreted. The formulae involved to compose the X-well-formed heap h and the local i-valuation heap h are directly used in the translation of quantified formulae (see Section 5.4). Lemma 5.11 is used in the proof of Lemma 5.12. LEMMA 5.11 (COMPOSITION). Let f be a valuation, h be an X-well-formed heap with {0} ⊆ X ⊆ [0, K], i ∈ [1, K] \ X with i > max (X), and h be a disjoint heap such that:

Roughly speaking, Lemma 5.11 states that given an X-well-formed heap h, adding a disjoint local i-valuation h with i ∈ X, leads to an (X ∪ {i})-well-formed heap so that the interpretation of variables with variable indices in X from the extracted valuation, is the same with h and with h h . The heap h h can be then understood as a conservative extension of the heap h.

The proof of Lemma 5.11 is quite combinatorial and this is the place where we check that the original heap cannot be confused with the valuation heap (and the other way

. Now let us consider the following facts:

(1) An entry in h cannot be transformed into a right or a left parenthesis in h h (simply because the index of the entry is allocated). ( 2) The left i-parenthesis in h is transformed into a left i-parenthesis in h h (IV).

So, the only ways to build a large right i-parenthesis whose degree is greater that lp i is either by considering the right i-parenthesis from h with index rp i or by building another large right i-parenthesis with a different index either from the entries of h or from the right i-parenthesis in h , which is not possible by (II). Consequently, rp i = rp i . So far, we can observe that rp i in h h is greater than rp i in h . Let us show that we have indeed equality between these two degrees. Note that indspect(h ) can be defined as some set below where α = lp i (in h ) and β ≥ 0:

we also have that lp i in h h is equal to α (this is actually (IV)).

So, indspect(h ) contains the following values:

The values in spect(h h ) ∩ [α, +∞[ can only be obtained from the degree of index locations from h and therefore are of the form

These latter values should be understood as the potential differences of degrees.

Since h |= f isoloc(u) and h h |= f Llp i (u), we have α 0 = 0 (this is actually (IV)). Since h h |= f wfh X∪{i} , there is β ≥ 0 such that spect(h h ) ∩ [α, +∞[ is equal to {α} ∪ {α + 3(j -1) + 1, α + 3(j -1) + 2 : j ∈ [1, β ]} ∪ {α + 3β + 1}.

(3) So necessarily β ≥ β. Moreover, if β = 0, then α β+1 = 0, otherwise spect(h h ) ∩ [α, +∞[ cannot be of the form of Equation (3). Assuming that β ≥ 1, we can show by induction on j that α j 1 = 0 and then α j 2 = 0 with j ∈ [1, β]. For instance, α 1 1 = 0 leads to a contradiction, since α + 1 would not belong to spect(h h ) ∩ [α, +∞[ and therefore could not be of the form of Equation ( 3) by (2holes). Then, α 1 2 = 0 leads to a contradiction, since α + 2 would not belong to spect(h h ) ∩ [α, +∞[ (while α + 1 does) and therefore could not be of the form of Equation ( 3). The same reasoning can be performed for all j ∈ [2, β].

(VII) For every l such that h |= [u →l] Lindex(u), we have h h |= [u →l] Lindex(u), and l in h is equal to l in h h . Let l be a large index in h. By (III), either l is a large index in h h or l is not anymore an index in h h . In the latter case, l cannot be the index of some j-parenthesis with j ∈ X by (V). This latter case with l being a large entry index is nevertheless ruled out because h h |= wfh X∪{i} and there will be then a missing value in the spectrum spect(h h ) by (2holes).

As a consequence, an allocated location in h that is not a large index, cannot be transformed into an index in h h , otherwise we would have two large indices with PROOF. The proof is by structural induction. Base case 1: ψ is equal to u i = u j . Since h is X-well-formed and i, j ∈ X, V h (u i ) is equal to h V (l) where l is the unique index location such that l ∈ degrees(i, h). Similarly, V h (u j ) is equal to h V (l ) where l is the unique index location such that l ∈ degrees(j, h). Uniqueness is a consequence of Definition 5.8(2).

Let us recall that elt

First, let us suppose that h B |= V h u i = u j . This means that V h (u i ) and V h (u j ) are equal, say to l and therefore there is a unique index location l i such that h V (l i ) = l and l i ∈ degrees(i, h). Moreover, there is a unique index location l j such that h V (l j ) = l and l j ∈ degrees(j, h). Since l i and l j belong to the index spectrum of h V , the locations l i and l j , have the same number of predecessors in h and in h V and they are also indices in h (see Lemma 5.11). Consequently, h

There is a location l such that h |= [u →l ] elt i (u) ∧ elt j (u). Therefore there are index locations l i and l j such that l i ∈ degrees(i, h), l j ∈ degrees(j, h), h(l i ) = l and h(l j ) = l . By Lemma 5.11,

Base case 2: ψ is equal to u i → u j . Again, since h is X-well-formed and i, j ∈ X, V h (u i ) is equal to h V (l) where l is the unique location such that l ∈ degrees(i, h). Similarly, V h (u j ) is equal to h V (l) where l is the unique location such that l ∈ degrees(j, h).

First, let us suppose that h B |= V h u i → u j . This means that h B (V h (u i )) = V h (u j ), and there is a unique location l i such that h V (l i ) = V h (u i ) and l i ∈ degrees(i, h). There is also a unique location l j such that h V (l j ) = V h (u j ) and l j ∈ degrees(j, h). Since l i and l j belong to the index spectrum of h V , the locations l i and l j , have the same number of predecessors in h and in h V and they are also indices in h (see Lemma 5.11). There are index locations l , l such that h

Consequently, there are locations l and l such that h |= [u →l ,u →l ] elt i (u) ∧ elt j (u) ∧ u → u. Therefore there are locations l i and l j such that l i ∈ degrees(i, h), l j ∈ degrees(j, h), h(l i ) = l , h(l j ) = l and of course h(l ) = l . By Lemma 5.11 and since indspect(h

where l j is the unique index location such that l j ∈ degrees(j, h). Similarly, V h (u k ) is equal to h V (l k ) where l k is the unique index location such that l k ∈ degrees(k, h). So, t(X ∪ {i}, ψ ). However, it is easy to conclude then that h |= t(X, ψ). Indeed, h satisfies the formula below

whenever there are locations l and l and a disjoint heap h such that:

(1) l is the unique large 0-parenthesis in h and l is isolated in h, (2) h is an i-local valuation such that the index of the left i-parenthesis is l , h h is (X ∪ {i})-well-formed, (3) l is the left 0-parenthesis in h h and l is the left i-parenthesis in h h , (4)

It is clear that such objects exist by considering the above construction.

The proof in the other direction (i.e. h |= t(X, ψ) implies h B |= V h ∃ u i ψ ) is actually very similar since most of the above implications are indeed equivalences.

Case 2: ψ is equal to ∃

(and therefore R involves some isolated locations in h B ), we pick another R (of same cardinality β) that does not involve locations in Y . It is then easy to show that h B |= V h [Pi →R] ψ iff h B |= V h [Pi →R ] ψ . So, without any loss of generality, below we assume that R does not involve locations in Y (see also [Brochenin et al. 2012, Lemma 2.1]).

Let us build h i V and an assignment f such that: (1) h i V |= f localval i (u), (2) h |= f indmin(u) ∧ isoloc(u), (3) h h i V |= f wfh X∪{i} ∧ indmin(u) ∧ Llp i (u). Assume that max(X) = j and m is the degree of the right j-parenthesis with greatest degree. It is easy to define a local i-valuation h i V disjoint from h such that (1) the degree of the left i-parenthesis is m + 1, (2) the degree of the right i-parenthesis is (m + 1) + 3β + 1 for some β ≥ 0, (3) there are 2β entries, (4) for every pair (l, l ) in R, there are two entries of consecutive degrees whose elements are l and l respectively. This is always possible since dom(h) ∪ ran(h) and R are finite. It is not difficult to check that h i V and f satisfy the above conditions. Since h h i V is (X ∪ {i})-well-formed by construction, by Lemma 5.11, we have

ψ and by the induction hypothesis, we get h h i V |= t(X ∪ {i}, ψ ). However, it is easy to conclude then that h |= t(X, ψ). Indeed, h satisfies the formula below ∃ u ∃ u (indmin(u) ∧ isoloc(u) ∧ (localval i (u) ¬ - *

(wfh X∪{i} ∧ indmin(u) ∧ Llp i (u) ∧ t(X ∪ {i}, ψ ))))