Stéphane Demri
email: demri@cs.nyu.edu

Morgan Deters
email: mdeters@cs.nyu.edu

Expressive Completeness of Separation Logic With Two Variables and No Separating Conjunction *

Keywords: F, 4, 1 [Mathematical Logic and Formal Languages]: Mathematical Logic Keywords separation logic, expressive completeness

We show that first-order separation logic with one record field restricted to two variables and the separating implication (no separating conjunction) is as expressive as weak second-order logic, substantially sharpening a previous result. Capturing weak secondorder logic with such a restricted form of separation logic requires substantial updates to known proof techniques. We develop these, and as a by-product identify the smallest fragment of separation logic known to be undecidable: first-order separation logic with one record field, two variables, and no separating conjunction.

Introduction

Expressive completeness The literature is rich with results comparing the expressive power of non-classical logics with first-order or second-order logic. For instance, the celebrated Kamp's Theorem 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] Weis | Expressiveness and Succinctness of First-Order Logic on Finite Words[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 FO2 [START_REF] Lutz | Modal logic and the two-variable fragment[END_REF]. 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].

[Copyright notice will appear here once 'preprint' option is removed.] 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] 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]. 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] to translation to theories handled by SMT solvers [START_REF] Piskac | Automating separation logic using SMT[END_REF], passing via graph-based algorithms [START_REF] Haase | SeLoger: A tool for graph-based reasoning in separation logic[END_REF].

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] Antonopoulos | Foundations for decision problems in separation logic with general inductive predicates[END_REF][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]. 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 (called herein 2SL) is undecidable (with a proof that does not require separating connectives and uses Trakhtenbrot's Theorem). 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 (called herein 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] but without touching the central question of expressive completenessthe 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]). In this paper, we go one step further by showing that two variables suffice to get expressive completeness. As a consequence, 1SL2(- * ) (that is, 1SL2 without separating conjunction) is undecidable too, which 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 | The undecidability of Boolean BI through phase semantics[END_REF] obtained in an alternative setting with propositional variables and no first-order quantification. It is fair to recall that separating implication has been less wellstudied than separating conjunction in the literature, but its use for program verification is far more recognized nowadays; see e.g. [25, Section 1] for a recent, insightful analysis (see also [START_REF] Hou | Proof search for propositional abstract separation logics via labelled sequents[END_REF]Section 8]).

Our contribution In this paper, we sharpen the main result in [START_REF] Brochenin | On the Almighty Wand[END_REF], namely 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 | Separation Logic: Expressiveness, Complexity, Temporal Extension[END_REF][START_REF] Brochenin | On the Almighty Wand[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] Brochenin | On the Almighty Wand[END_REF][START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[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 twovariable logics[END_REF][START_REF] Immerman | The boundary between decidability and undecidability for transitiveclosure logics[END_REF], we show undecidability of a two-variable logic with second-order features, and our main undecidability result cannot be derived from [START_REF] Grädel | Undecidability results on twovariable logics[END_REF][START_REF] Immerman | The boundary between decidability and undecidability for transitiveclosure logics[END_REF] since in 1SL models, we deal with a single functional binary relation. 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 PSPACE-complete [START_REF] Demri | Separation logic with one quantified variable[END_REF]. Below, we illustrate how the main result of the paper (Theorem 23) compares with known results from the literature (Section 2 contains definitions of the different logics).

1SL

≡ DSOL ≡ WSOL ≡ 1SL(- * ), undec. [START_REF] Brochenin | On the Almighty Wand[END_REF] 2SL undec. [START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF] 1SL2 undec. [START_REF] Demri | Two-variable separation logic and its inner circle[END_REF] 1SL( * ) dec., non-elem. [START_REF] Brochenin | On the Almighty Wand[END_REF] 1SL2(- * ) ≡ DSOL, undec.

(Theorem 23)

1SL2( * )

dec., non-elem. [START_REF] Demri | Two-variable separation logic and its inner circle[END_REF] 1SL1 PSPACE-C. [START_REF] Demri | Separation logic with one quantified variable[END_REF] Propositional 1SL PSPACE-C. [START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF] 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 is known today (see e.g., the proof of Lemma 5). 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. 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. Another contribution 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. Extensions with program variables or with heaps having k > 1 record fields are presented in Section 5.5.

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 h1, h2 are said to be disjoint, if their domains are disjoint; when this holds, we write h1 h2 to denote the disjoint union. Locations are elements of N and are denoted by l, possibly decorated with exponents or subscripts. We write l1 → l2 →

• • • → lm to mean that for every i ∈ [1, m -1], h(li) = li+1.
In that case {l1, . . . , lm-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 iff (either l ∈ dom(h) or h(l) = l).

Let FVAR = {u1, u2, . . .} be a countably infinite set of variables. Formulae of 1SL are defined by the grammar φ ::

= ui = uj | ui → uj | φ ∧ φ | ¬φ | φ * φ | φ - * φ | ∃ ui φ.
The connective * is called the separating conjunction and - * is called the separating implication (also known as the magic wand). We make use of standard notations for the derived connectives.

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

• h |= f ui = uj iff f(ui) = f(uj). • h |= f ui → uj iff f(ui) ∈ dom(h) and h(f(ui)) = f(uj). • h |= f φ1 * φ2 iff there exist h1, h2 such that h1 and h2 are disjoint, h = h1 h2, h1 |= f φ1 and h2 |= 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 ∃ ui φ iff there is l ∈ N such that h |= f[u i →l] φ.
We also introduce so-called septraction operator ¬ - * :

φ ¬ - * ψ is defined as ¬(φ - * ¬ψ). So, h |= f φ ¬ - * ψ iff there is h disjoint from h such that h |= f φ and h h |= f ψ.
Septraction states the existence of a disjoint heap satisfying a formula and for which its addition to the original heap satisfies another formula.

For i ≥ 1, 1SLi denotes the fragment of 1SL restricted to i variables and 1SLi(- * ) to denote 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 h such that h |= φ (regardless of valuation, as φ has no free variables).

Theorem 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 1SL2.

Weak second-order logic (WSOL)

We consider a family SVAR = (SVARi) i≥1 of second-order variables, denoted by P, Q, R, . . . and interpreted as finite relations over N. A second-order valuation f is an interpretation of the secondorder variables such that for every P ∈ SVARi, f(P) is a finite subset of N i . Formulae φ of WSOL are defined by φ ::

= ui = uj | ui → uj | φ ∧ φ | ¬φ | ∃ ui φ | ∃ P φ | P(u1, . . . , un)
, where the P are second-order variables with P ∈ SVARn for some n ≥ 1. We write DSOL (dyadic second-order logic) to denote the restriction of WSOL to second-order variables in SVAR2. Like 1SL, models for WSOL are finite heaps and quantifications are done over all the locations. Satisfaction relation |= is defined as follows (f is a hybrid valuation providing interpretation for any variable):

• h |= f ∃ P φ iff there is a finite relation R ⊆ N n such that h |= f[P →R] φ where P ∈ SVARn. • h |= f P(u1, . . . , un) iff (f(u1), . . . , f(un)) ∈ f(P).
The satisfiability problem for WSOL takes as input a sentence φ in WSOL and asks whether there is h such that h |= φ. By Trakhtenbrot's Theorem (see e.g. [START_REF] Börger | The Classical Decision Problem[END_REF][START_REF] Trakhtenbrot | Impossibility of an algorithm for the decision problem in finite classes[END_REF]), the satisfiability problem for DSOL (and therefore for WSOL) is undecidable since finite satisfiability for first-order logic with a unique binary relation symbol is undecidable. Note that a monadic second-order variable can be simulated by a binary second-order variable from SVAR2, and this can be used to relativize a formula from DSOL in order to check finite satisfiability. Theorem 2. [7] 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 extends to 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 5.5).

Expressing Properties in 1SL2(- * )

In the following, let u and u be the variables u1 and u2, in either order. Throughout this paper, 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.

In 1SL2(- * ) it is not difficult to state that the domain of the heap is empty or that it is a singleton-for example, 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 out of variables if we attempt to use a similar technique. Below, we propose a new and natural method to compare a number of predecessors against a constant or to express a reachability property. First, though, we define simple, standard formulae.

• u has a successor: alloc(u)

def = ∃ u u → u. • u is an isolated location (it is not in dom(h) ∪ 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)) .

• u has at least one predecessor: u > 0 def = ∃ u u → u. Naturally, 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 locations. Without an adequate number of variables to refer to locations of interest, we instead "remember" locations by installing a large (and unique) 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 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 k).

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 are all z-predecessors:

allzpred(u) def = ∀ u u → u ⇒ u = 0.
• u has zero z-predecessors:

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 with z u ≤ 0 defined as z u = 0. Lemma 3. Let h be a heap, f be a valuation, and k ∈ N. h |= f z u ≤ k iff card({l ∈ N : l = 0, h(l) = f(u)}) ≤ k.
Variants z u k with ∈ {=, <, >, ≥} are easily defined.

A matter of forks and knives

To address the problem of referring to memory locations despite not having the 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. Forks are also a critical building block for comparing predecessors in Section 4. A fork in h is a sequence of distinct locations l, l0, l1, l2 such that h(l0) = l, l0 = 2, h(l1) = h(l2) = l0 and l1 = l2 = 0. The endpoint of the fork is l. The fork is isolated iff l = 1 and l / ∈ dom(h). Similarly, a knife in h is a sequence of distinct locations l, l0, l1 such that h(l0) = l, l0 = 1, h(l1) = l0 and l1 = 0. The endpoint of the knife is l. The knife is isolated iff l = 1 and l / ∈ dom(h). To identify fork and knife endpoints in a heap, we define:

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 except f(u), are endpoints of forks: forky(u)

def = ∀ u ((u → u ∧ u = u) ⇒ forkendpt(u)).
Three forks, two endfork endpoints forky points, and a forky location are depicted at left. 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)) and antiknify(u) def = ∀ u (u → u ⇒ ¬knifeendpt(u)).
Note the asymmetry between forky(u) and antiforky(u) since f(u) does not have to be the endpoint of a fork in forky(u) (which would be then impossible to realize for all the predecessors of f(u) if f(u) were a self-loop). It is also easy to enforce that the heap is made of a single fork, which will be useful afterwards.

Lemma 4. There is a formula 1fork in 1SL2(- * ) such that for all h, we have h |= 1fork iff h is only made of a single, isolated fork.

Now let us build formulae that constrain the number of predecessors (not just z-predecessors): with

k ∈ Z, we define u ≤ k def = ⊥ if k < 0, u ≤ 0 def = ¬∃ u u → u, and for k > 0, u ≤ k def = (u → u ∧ u ≤ k -1) ∨ (¬(u → u) ∧ u ≤ k) where u ≤ 0 def = ¬∃ u (u → u ∧ u = u) and u ≤ k def = ( u = 0) ¬ - * (antiforky(u) ∧ (1fork ¬ - * • • • ¬ - * 1fork k times ¬ - * forky(u))
for 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 (always possible) and then adding k forks to make f(u) forky (we distinguish the case when f(u) is a self-loop).

Lemma 5. 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.
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.
Lonely memory cells Now, we can express a useful property on the heap itself. The formula below states that f(u) is an isolated cell: isocell(u)

def = alloc(u) ∧ u = 0 ∧ (∃ u u → u ∧ u = 1 ∧ ¬alloc(u)).
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 are isolated. Being segmented can be naturally expressed in 1SL2(- * ) too:

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, itself a variant of material from [START_REF] Brochenin | On the Almighty Wand[END_REF][START_REF] Dawar | Expressiveness and complexity of graph logic[END_REF]. Without the separating conjunction, we can still specify reachability from f(u) to f(u), but we need a new technique: we put a fork on f(u), propagate this fork forward in the heap, and finally 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, and that the property of being the endpoint of some fork is propagated along memory cells. The reachability predicate 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 " - * " is to destroy forks in the original heap (if any) and to augment it with new forks such that propagate(u) is satisfied. Of course, a disjoint subheap could change the very reachability property we are testing. But some such subheaps do not, and the 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 6. Given a heap h and valuation f,

we have h |= f reach(u, u) iff h k (f(u)) = f(u) for some k ≥ 0.
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 transitiveclosure 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 f(u) + k ≤ f(u) + k can be expressed in 1SL2(- * ) itself. Since a property f(u) + k ≤ f(u) + k requires a formula with O(k + k ) variables in 1SL(- * ) according to [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.

Principles and difficulties with 1SL2(- * )

Let h be a heap and f be a valuation for which we wish to check if Theorem 10). Below, we explain which extensions of h must be performed to achieve this. 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(- * ).

f(u) + k ≤ f(u) + k holds (it is easy to conclude if f(u) + k ≤ f(u) + k holds, see the proof of

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 cells-these properties will be necessary in later stepswhile maintaining the number of predecessors at f(u) and f(u). To do this, we augment h with a heap hp so that (a) hp is disjoint from h; (b) f(u) has the same number of predecessors in h and in h hp, say f(u) = m ≥ 0; (c) f(u) has the same number of predecessors in h and in h hp, say f(u) = m ≥ 0; (d) In h hp, f(u) has no predecessor that is an endpoint of a fork or knife; (e) In h hp, f(u) has no predecessor that is an endpoint of a fork or knife; (f) h hp has no isolated memory cell. 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 the adequate position. We take advantage of the formulae antiforky(•) and antiknify(•) to establish properties (d) and (e); the others are straightforward.

Addition of a segmented heap

This step consists in checking whether, for each segmented heap hs satisfying certain properties, the condition (P) defined below holds true. The heap hs must be segmented and also must satisfy the following: (a) hs is disjoint from h hp; (b) f(u) and f(u) have no predecessors in hs; (c) In h hp hs, neither f(u) nor f(u) has a predecessor that is an endpoint of a fork or knife (they are antiforky and antiknify). Let n be the number of isolated memory cells in h hp hs. Note that for each q ≥ 0, it is possible to build h q s so that h hp h q s has exactly q isolated memory cells and h q s satisfies the above conditions. In order to construct forks in h hp hs 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 hp hs leads to a fork whose endpoint is a predecessor of f(u) or f(u). See Figure 1, 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 hp hs made of isolated knives and k isolated forks so that f(u) is forky in h hp hs h [k] , then there is a heap h [k ] disjoint from h hp hs made of isolated knives and k isolated forks so that f(u) is forky in h hp hs 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). The number of forks in h hp hs h [k] whose endpoints are predecessors of f(u) is bounded by n + k and similarly, the number of forks in h hp hs 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 hp hs h [k ] and the number of predecessors of f(u) is the same in h and in h hp hs h

[k] . So, n + k ≥ m implies n + k ≥ m, i.e. n ≥ m -k implies n ≥ m -k .

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 10). Below, we present the technical developments.

Building blocks

Apart from forks, we introduce the notions of collections and large forks (instrumental in the proof of Lemma 7 below). A large fork is a sequence of distinct locations l1, • • • , l5 such that l1, l2, and l3 have no predecessors, h(l1) = h(l2) = h(l3) = l4, l4 = 3 and h(l4) = l5. Location l5 is called the endpoint of the large fork, and as with forks and knives, the large fork is called isolated iff l5 = 1 and l5 / ∈ 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 7. 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.

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

Lemma 8. 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 and m = f(u) . We have

h |= f (ksfs k ¬ - * forky(u)) iff n ≥ m -k.
The proof of Lemma 8 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) ). Let anti be antiforky(u) ∧ antiknify(u) ∧ antiforky(u) ∧ antiknify(u) and let comp(u, u, k, k ) be

(seg ∧ u = 0 ∧ u = 0) - * anti ⇒ ksfs k ¬ - * forky(u) ⇒ ksfs k ¬ - * forky(u) Proposition 9. Let k, k ≥ 0, f and h such that h |= f anti ∧ ¬∃ 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 .
Here is the main result in this section using comp(u, u, k, k ).

Theorem 10. For k, k ≥ 0, there is φ in 1SL2(- * ) (of linear size in k + k ) such that for all h, f, (h |= f φ iff f(u) + k ≤ f(u) + k ).
We denote such a formula φ as u+k ≤ u+k and, as usual, easily extend to <, ≥, >, =. The structure of the proof of Theorem 10 is similar to the structure of the proof of [7, 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 ) 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 easily 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 )
So it only remains to define the formulae φ k,k with k, k ≥ 0. By Proposition 9, we have the following property for any h, f:

( ) When h satisfies anti ∧ ¬∃ 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 does not satisfy the formula anti ∧ ¬∃ 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 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 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 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 isocell(u) while preserving f(u) and f(u) . W.l.o.g., 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 isocell(u)) ∧ comp(u, u, 0, k ))))
Formulae of the form u ≥ k (and variants) can be defined thanks to Lemma 5.

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 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 maxdeg(u) def = ¬∃ u u > u. For all h and f, we have h |= f maxdeg(u) iff f(u) = max ({ l : l ∈ N}).

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 Pi whenever l and l can be identified by special patterns involving l and l that uniquely characterize the interpretation by Pi. 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 l1, . . . ,

l d , l ind , l such that h(l1) = • • • = h(l d ) = l ind , l ind = d, l1 = • • • = l d = 0 and h(l ind ) = l.
The location l is called the element, l ind the index and the locations l1, . . . , 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 2. So, the pair of locations (l, l ) is identified as part of the interpretation of Pi 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 arithmetical constraints, which is possible thanks to Theorem 10, 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 firstorder 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.

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 secondorder 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 , l1, . . . , l d , l ind such that (u)

h(l1) = • • • = h(l d ) = l ind ; l ind = d; l j+1 = l3 = l4 = • • • = l d = 0, (v) l ind ∈ dom(h); l j+1 → l j → l j-1 → • • • → l 1 → l1; l j = l j-1 = • • • = l 1 = l1 = 1
, and (w) l2 = 0. The location l ind is called the index. The heap at the left of Figure 2 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 , l1, . . . , l d , l ind such that (u), (v), l j+1 = 0,

l j = l j-1 = • • • = l 1 = l2 = 1, and l j+1 → l j → l j-1 → • • • → l 1 → l2.
The location l ind is also called the index. The heap at the right of Figure 2 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 whether it is a left or a right parenthesis.

Lemma 11. 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.

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

onp i (u) def = i+2 j=0 disti(j, u) with disti(0, u) def = lp i (u) ∨ rp i (u) and disti(j + 1, u) def = ∃ u (u → u) ∧ disti(j, u) for all j ≥ 0.
Lemma 12. Let h be a heap, f be a valuation and i ≥ 0. Then, h |= f onp i (u) iff f(u) is on some i-parenthesis in h.

The role of parentheses

First, we introduce the interval [1, K] (K ∈ N \ {0}) assuming that for each j ∈ [1, K], either Pj or uj 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 [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 X-well-formed heap h (see Definition 18 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 uj (see Figure 2 with d r j = 5 and d l j = 3). That explains why the parentheses are viewed as delimiters. Similarly, let {(l1, l 1 ), . . . , (l β , l β )} be a finite set of pairs of locations, understood as the interpretation of a second-order variable Pj 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 li and l i respectively, which allows to encode the pair (li, 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 [START_REF] Antonopoulos | Separating graph logic from MSO[END_REF] in Definition 14,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. 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 write ispect(h) to denote { l : l is the index of some entry or parenthesis in h} and call this the index spectrum of h. Let hB be a heap such that α = max ({ l : l ∈ N}). We have seen in Section 4 that it is possible to characterize the locations that witness this maximal value α thanks to maxdeg(u). A valuation heap hV for hB is made of entries and parentheses only whose degrees are greater than max (3, α + 1). The heap hV satisfies the following simple conditions (more constraints will follow): min(ispect(hV )) is greater than max (3, α + 1) and it is witnessed by the degree of some left 0-parenthesis; each degree in ispect(hV ) is witnessed by exactly one entry or parenthesis. Formula imin(u) below is satisfied in h = hB hV by a location l witnessing the minimal value in ispect(hV ):

imin(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, imin(u) holds when f(u) is the unique location that is the index of some left 0parenthesis with greatest degree. Lemma 13. Let f be a valuation and h be a heap. We have h |= f imin(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 11. Once a heap h satisfies ∃ u imin(u), the unique location l0 such that h |= [u →l 0 ] imin(u) (say with l0 = d0) plays the role of a delimiter between the original heap and the part of the heap than 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 imin(u). Let us define the set spect(h) as { l : l is an index of some entry or parenthesis in h} ∩ [d0, +∞[

The set spect(h) is called the spectrum of h. This illustrates how l0 and l0 = d0 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 does the job:

(∃ u imin(u) ∧ u ≤ u) ∧ i∈[0,K] (lp i (u) ∨ rp i (u)) ∨ eindex(u)
(u is interpreted as a large index). Entries and parentheses with large indices are also called large entries and parentheses, respectively. It is easy to define a large index that is also the index of a left [resp. right] parenthesis. Let llp i (u) Lemma 11). The large index with a maximal degree can be also characterized as follows:

def = lindex(u) ∧ lp i (u) and lrp i (u) def = lindex(u) ∧ rp i (u) (see
maxlindex(u) def = (∀ u lindex(u) ⇒ ( u ≤ u)) ∧ lindex(u)
Below, we state how the parentheses are organized.

Definition 14. Let X = {i0, . . . , is} ⊆ [0, K] with 0 = i0 < i1 < • • • < is. 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 i j (u) [resp. h |= [u →l r j ] lrp i j (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.

h |= [u →l r

s ] maxlindex(u). 5. For every j ∈ [1, s], if ij is the index of a first-order variable, then l l j = l r j -2 (see Figure 2). 6. For every j ∈ (

[1, K] \ X), there is no location l such that h |= [u →l] llp j (u) ∨ lrp j (u).
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 |= imin(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 |= maxlindex(u)
Lemma 15. There is awfhX in 1SL2(- * ) such that h |= awfhX iff h is X-almost-well-formed.

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

lindex(u) ∧ eindex(u) ∧ (∃ u llp i (u) ∧ u < u) ∧ (∃ u lrp i (u) ∧ u > u)
It characterizes indices whose degree is strictly between the degree of some large left i-parenthesis and the degree of some large right i-parenthesis. We write degrees(i, h) to denote the set: { l : h |= [u →l] vindi(u), l ∈ N}.

Lemma 16.

Let h be such that h |= ∃ u imin(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] vindi(u) iff l is the index of some entry and lp < l < rp.

The translation of Pi(uj, u k ) is therefore:

∃ u (onj(u) ∧ ∃ u (u → u ∧ vindi(u)∧ ∃ u ( u = u + 1 ∧ vindi(u) ∧ ∃ u (u → u ∧ on k (u)))))
, where onj(u) def = ∃ u (u → u) ∧ vindj(u). Formula onj(u) holds true when u is interpreted as the element of the unique entry attached to uj. These definitions take advantage of the fact that there are unique large left and right parentheses for each variable index. Figure 3 illustrates the constraints when j < i < k. From left to right, it represents explicitly a left j-parenthesis, then a right j-parenthesis, then a left i-parenthesis, a right i-parenthesis 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 translation of Pi(uj, 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 i-parenthesis 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 i-parenthesis, or to an entry, 2. h contains a unique left [resp. right] i-parenthesis, 3. min(ispect(h)) is the degree of some left i-parenthesis, 4. max (ispect(h)) is the degree of some right i-parenthesis, 5. ispect(h) is of the form below for some α ≥ 3, β ≥ 0, {α} ∪ {α + 3(i -1) + 1, α + 3(i -1) + 2 : i ∈ [1, β]} ∪ {α + 3β + 1} (when β = 0, ispect(h) is equal to {α, α + 1}), 6. there are no two distinct indices with the same degree.

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 characterize them by 1SL2(- * ) formulae. This is the purpose of the result below.

Lemma 17. Let i ∈ [0, K]. There is localvali(u) in 1SL2(- * ) such that h |= f localvali(u) iff h is a local i-valuation and f(u)
is the index of its left i-parenthesis.

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

Definition 18. Let X = {i0, . . . , is} ⊆ [0, K] with 0 = i0 < i1 < • • • < is. A heap h is X-well-formed def ⇔ 1.
h is X-almost-well-formed, 2. for every j ∈ [1, s], if ij is the index of a first-order variable, then degrees(ij, h) is a singleton, 3. for every j ∈ [1, s], if ij is the index of a second-order variable, degrees(ij, h) is the set below for some αj ≥ 3, βj ≥ 0: {αj + 3(i -1) + 1, αj + 3(i -1) + 2 : i ∈ [1, βj]}, 4. for every location l such that h |= [u →l] lindex(u), there is no l = l such that h |= [u →l ] lindex(u) and l = l .

When h is X-well-formed, we write h = hB hV such that dom(hV ) is made of entries and parentheses of degree d ≥ l0 for some l0 ∈ N such that h |= [u →l 0 ] imin(u). By Definition 18, we have spect(h) = ispect(hV ) and clearly the decomposition is unique since l0 is unique.

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

Lemma 19. Given {0} ⊆ X ⊆ [0, K], there is a formula wfhX in 1SL2(- * ) such that h |= wfhX iff h is X-well-formed.
Let us define a valuation from a valuation heap. Definition 20. Let h be an X-well-formed heap for some {0} ⊆ X ⊆ [0, K]. For every second-order i ∈ X, we define V h (Pi) def = {(hV (l), hV (l )) : l = l + 1, l, l ∈ degrees(i, h), l, l are index locations} and for every first-order i ∈ X, V h (ui) def = hV (l) 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 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 ivaluation heap h are directly used in the translation of quantified formulae (see Section 5.4). Lemma 21 is only used in the proof of Lemma 22 but it is stated here in order to emphasize how the heaps can be safely composed.

Lemma 21 (Composition). Let f be a valuation, h be an X-wellformed heap with {0} ⊆ X ⊆ [0, K], i ∈ [1, K] \ X with i > max (X), and h be a disjoint heap such that:

1. h |= f imin(u) ∧ isoloc(u), 2. h |= f localvali(u), 3. h h |= f wfh X∪{i} ∧ imin(u) ∧ llp i (u).

Then, spect(h h ) = spect(h) ispect(h ).

The proof of Lemma 21 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 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.

A reduction from DSOL into 1SL2(- * )

Below, we define a translation from a sentence φ in DSOL into a sentence in 1SL2(- * ) that uses only logspace. Without any loss of generality, we assume that (1) two occurrences of quantified variables in φ have distinct variable indices (e.g., P4 and u4 cannot both occur in φ and "∀ u4" cannot occur more than once) and (2) if ∃ ui ψ1 is a subformula of ∃ uj ψ2, then i > j and this holds for any combination of first-order/second-order variables. We may rename variables so that these conditions are satisfied. We assume that the variable indices are among [1, K].

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

ttop(φ) def = ∃ u isoloc(u) ∧ (localval0(u) ¬ - * (wfh {0} ∧ imin(u)∧(∀ u ((u = u)∧¬lrp 0 (u)) ⇒ ( u < u))∧t({0}, φ))) l l Figure 3: How the translation of Pi(uj, u k ) works (j < i < k): (l, l ) ∈ V h (Pi).
The first step of the translation consists in adding 0-parentheses so that the heap that evaluates t({0}, φ) is {0}-well-formed. The recursive map t(•) is inductively defined as follows (X ⊆ [0, K], ψ subformula of φ):

• t(X, •) is homomorphic for Boolean connectives, • t(X, ui = uj) def = ∃ u oni(u) ∧ onj(u), • t(X, ui → uj) def = ∃ u ∃ u (oni(u) ∧ onj(u) ∧ u → u), • t(X, Pi(uj, u k )) def = ∃ u (onj(u) ∧ ∃ u (u → u ∧ vindi(u) ∧ ∃ u ( u = u + 1 ∧ vindi(u) ∧ ∃ u (u → u ∧ on k (u))))).
• For the quantifier ∃ ui, we choose l and l such that l is the index of the left 0-parenthesis and l is an isolated location. 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 21).

t(X, ∃ ui ψ) def = ∃ u ∃ u ((imin(u) ∧ isoloc(u)) ∧ (localvali(u) ¬ - * (wfh X∪{i} ∧ imin(u) ∧ llp i (u) ∧ t(X ∪ {i}, ψ))))
• The translation with second-order variables is analogous (the formula localvali(u) is actually defined differently, see the proof of Lemma 17

): t(X, ∃ Pi ψ) def = ∃ u ∃ u ((imin(u) ∧ isoloc(u)) ∧ (localvali(u) ¬ - * (wfh X∪{i} ∧ imin(u) ∧ llp i (u) ∧ t(X ∪ {i}, ψ)))).
Every subformula t(X, ψ) has no free variable from fr(ψ) ⊆ X where fr(ψ) 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 23.

Lemma 22. Let φ be a DSOL sentence of the above form, ψ be one of its subformulae and (fr(ψ) ∪ {0}) ⊆ X ⊆ [0, K]. Let h = hB hV be a X-well-formed heap and V h be the valuation extracted from h. Then, hB |= V h ψ iff h |= t(X, ψ).

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

Observe that T(φ) can be computed in logspace (to do this, one must check the size of all the formulae built in the proofs). So, the restriction to two variables does not reduce the expressive power, unlike restrictions in [START_REF] Etessami | First-order logic with two variables and unary temporal logics[END_REF], for instance.

We get the ultimate undecidability result below (no separating conjunction, two quantified variables, one record field).

Corollary 24. Satisfiability problem for 1SL2(- * ) is undecidable.

The absence of program variables in 1SL2(- * ) makes the proof of Corollary 24 even more difficult to design, which is perfect to obtain the sharpest undecidability result. An expressivity result with program variables is briefly presented in Section 5.5.

It is also possible to establish the following consequences. 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 the 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 21). 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.

Adding an unbounded number of program variables

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. Let PVAR = {x1, x2, . . .} 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. 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 26. 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(φ).

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. For instance, the map t(•) is extended as follows (more details in the proof of Theorem 26): t(X, ui = x) def = ∃ u (oni(u) ∧ u = x) and t(X, ui → x) def = ∃ u (oni(u) ∧ u → x).

Extension with k record fields So far, memory cells have a unique record field but it is possible to extend our results to k > 1 record fields, along the lines of [START_REF] Brochenin | On the Almighty Wand[END_REF]Section 7]. Let kSL2(- * ) be the logic in which heaps are partial functions h : N N k with finite domain and atomic formulae include uj i → u j (i ∈ [1, k]); kWSOL and kDSOL are defined similarly. 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(- * ).

Conclusion

We have shown that 1SL2(- * ) is as expressive as weak secondorder logic on concrete heaps (Theorem 23). As a consequence, the satisfiability problem for 1SL2(- * ) is undecidable (Corollary 24) and we have identified the undecidable core of separation logic, apart from illustrating further the power of separating implication when interpreted on concrete heaps. 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 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 fragment 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 and will be the subject of future work.

Figure 1 :

 1 Figure 1: The construction of forks used for comparison.

Figure 2 :

 2 Figure 2: Encoding [uj → l].

Corollary 25 .

 25 (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 25(II) follows from Theorem 23 and 1SL( * ) is strictly less expressive than MSO [1, Corollary 5.3]. Our main results are Theorem 23 and Corollary 24, significantly improving previously known results (see the figure in Section 1).

  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 φ ::= π | φ ∧ ψ | ¬φ | φ * ψ | φ - * ψ | ∃ 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 ].

Demri & Deters, Expressive Completeness of Separation Logic with Two Variables 1 2014/7/18

Demri & Deters, Expressive Completeness of Separation Logic with Two Variables 2 2014/7/18

Demri & Deters, Expressive Completeness of Separation Logic with Two Variables 3 2014/7/18

Demri & Deters, Expressive Completeness of Separation Logic with Two Variables 4 2014/7/18

Demri & Deters, Expressive Completeness of Separation Logic with Two Variables 5 2014/7/18

Demri & Deters, Expressive Completeness of Separation Logic with Two Variables 6 2014/7/18

Demri & Deters, Expressive Completeness of Separation Logic with Two Variables 7 2014/7/18

Demri & Deters, Expressive Completeness of Separation Logic with Two Variables 8 2014/7/18

Demri & Deters, Expressive Completeness of Separation Logic with Two Variables 9 2014/7/18

Demri & Deters, Expressive Completeness of Separation Logic with Two Variables 10 2014/7/18

Acknowledgments

We would like to thank the anonymous referees for their suggestions and remarks to improve the quality of the paper.

* 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).


Goëry Genty

Frederic Dias

Bertrand Kibler

Nail Akhmediev

John M Dudley

Akhmediev Breather dynamics and the nonlinear modulation instability spectrum

Keywords: Solitons, nonlinear optics, supercontinuum generation, photonic crystal fiber, rogue waves

We consider various aspects of supercontinuum generation in the quasi-CW regime through analysis, numerical simulations and experiments. A new interpretation of certain features of the developing spectrum in terms of localized periodic structures known as "Akhmediev Breathers" is proposed. We also briefly consider the role of breather collisions and turbulence in the presence of higher order dispersion and show that they lead to the formation of very large amplitude localized structures that may be analogous to the infamous oceanic rogue waves.

INTRODUCTION

There has recently been much interest in the study of "rogue" events in nonlinear fiber optics [START_REF] Solli | Optical rogue waves[END_REF][START_REF] Dudley | Harnessing and control of optical rogue waves in supercontinuum generation[END_REF][START_REF] Erkintalo | Rogue wave like characteristics in femtosecond supercontinuum generation[END_REF]. Interest in this area began in 2007 with reports of extreme value soliton statistics during supercontinuum generation [START_REF] Solli | Optical rogue waves[END_REF]. Although many aspects of fibre SC generation are now well-understood [START_REF]Nonlinear Fiber Optics[END_REF][START_REF] Dudley | Supercontinuum Generation in Photonic Crystal Fiber[END_REF] these recent results have shown how noise-induced fluctuations in the long pulse quasi-CW regime can modify the dynamics so as to lead to very rare cases where high amplitude "optical rogue waves" are generated. These experiments attracted attention because they were carried out in a regime where spectral broadening was seeded by modulation instability (MI), allowing important links to be made with proposed formation mechanisms of oceanic rogue waves. The degree to which MI seeds either high power optical solitons or oceanic rogue waves is a subject of ongoing research, but insights into both optical and oceanic nonlinear propagation have already been obtained. In this regard, although the initial description of optical rogue waves was applied to rare high amplitude soliton pulses generated on the long-wavelength edge of a broadband fibre SC spectrum, there has recently been an improved understanding that a more likely analogy with the oceanic case is to be found in the onset phase of supercontinuum generation when coherent breather structures begin to emerge [START_REF] Akhmediev | Waves that appear from nowhere and disappear without a trace[END_REF][START_REF] Akhmediev | Extreme waves that appear from nowhere: On the nature of rogue waves[END_REF]. This realization has led to the "rediscovery" by the optics community of powerful analytic solutions that rigorously describe induced MI and ultrashort pulse train formation from an initial beat signal. Although previous studies of this process have used numerical simulations or truncated sideband models, we show that the rediscovered 1985 "Akhmediev Breather" (AB) model provides an exact formalism with which to interpret this evolution [START_REF] Akhmediev | Modulation instability and periodic solutions of the nonlinear Schrodinger equation[END_REF]. In fact, despite intensive research over three decades, there are surprisingly-few analytic solutions describing nonlinear pulse evolution in optical fibers. Certainly there are exceptions such as the well-known soliton and self-similar solutions [START_REF] Dudley | Self Similarity in Ultrafast Nonlinear Optics[END_REF], but complex processes such as supercontinuum generation have generally been considered to require numerical approaches. In this paper, however, we summarize recent results that have shown that an analytic theory of "Akhmediev Breather" (AB) propagation can be successfully applied to quantitatively explain the form of the developing SC spectrum under longpulse excitation conditions [START_REF] Dudley | Modulation instability, Akhmediev Breathers and continuous wave supercontinuum generation[END_REF][START_REF] Dudley | Modulation Instability, Akhmediev Breathers and 'Rogue Waves[END_REF]. Note that this present paper both summarizes the results in these previous works but also provides some additional unified and updated discussion in terms of other recent work we have carried out linking these ideas to the notion of soliton turbulence [START_REF] Genty | Collisions and turbulence in optical rogue wave formation[END_REF]. We show that the AB theory provides new insight into the properties of the initial broadening and nonlinear spectral transformation of CW supercontinuum generation seeded by noise. We discuss how the temporal structure that develops from spontaneous modulation instability (MI) can be naturally interpreted in terms of the characteristics of AB evolution, and we show how the frequency-domain properties of the maximally-compressed AB solution reproduce the characteristic triangular shape of the MI spectrum when plotted on a semi-logarithmic scale. Numerical and analytic results are confirmed by experimental studies of quasi-CW spectral broadening induced by nanosecond pulse pumping in the anomalous dispersion regime of a photonic crystal fiber (PCF). Finally, we present simulations that go beyond the initial phase of AB evolution in the presence of symmetry-breaking third-order dispersion. We show that this leads to collisions and interactions between the emergent localized AB structures that may provide a natural link to the instabilities that occur in an oceanographic context.

THEORY

The AB theory we present here was developed in mid-1980s by Akhmediev and co-workers who used an insightful analytical approach to construct novel solutions to the nonlinear Schrodinger equation describing fiber propagation. This work has already been summarized by us in [START_REF] Dudley | Modulation instability, Akhmediev Breathers and continuous wave supercontinuum generation[END_REF] but we re-present it here again for completeness. We first write the NLSE in dimensional form [START_REF]Nonlinear Fiber Optics[END_REF]:

2 2 2 2 | | 0 , 2 A A i A A z T β γ ∂ ∂ + + = ∂ ∂ (1)
where |A| 2 has dimensions of instantaneous power in W and the dispersion and nonlinearity coefficients β 2 (< 0) and γ have dimensions of ps 2 km -1 and W -1 km -1 respectively. The AB solution describes the evolution along the propagation direction z of a wave with initial constant amplitude on which is superimposed a T-dependent low amplitude modulation.

The solution then consists of an evolving train of pulses that is periodic in T and that exhibits periodic recurrence in z.

In contrast to soliton solutions which are localized in T, the ideal breather solution is localised in the z direction. In fact, certain initial conditions can also yield periodic evolution along the z-direction, but even in this case, the pulse train characteristics nonetheless remain well-described by the analytic AB solution. The AB solution to Eq. ( 1) is:

mod , 0 mod (1 4 )cosh( ) sinh( ) 2 cos( ) ( , ) 2 cos( ) cosh( ) a bz ib bz a T A z T P a T b z ω ω - + + = - (2)
which shows growth-return evolution over -∞ < z < ∞. The variable independent parameter ω mod is the (perturbation) frequency of the initial temporal modulation. Coefficients a and b depend on ω mod, defined by: 2a = [1 -( ω mod / ω c ) 2 ] and b = [8a (1-2a)] 1/2 with ω c 2 = 4 γ P 0 / |β 2 | and P 0 the CW power at large |z|. The solution is valid over modulation frequencies that experience MI gain: ω c > ω mod > 0 such that a varies in the interval 0 < a < 1/2 while the parameter b > 0 governs the MI growth. Maximum gain b = 1 occurs for a = 1/4, i.e. ω mod = ω c / 2 . The solution in Eq. ( 2) describes an evolving periodic train of ultrashort pulses with temporal period T mod = 2π/ω mod . The individual temporal sub-pulses have maximum amplitude and minimum temporal width at z = 0. The solution here describes the "maximally-compressed" AB:

mod 0 mod (1 4 ) 2 cos( ) ( 0, ) . 2 cos( ) 1 a a T A z T P a T ω ω - + = = - (3)
The spectrum of this field consists of discrete frequency sideband modes with separation ω mod , and intensities that decrease following a geometric progression. For the particular case of the maximally-compressed solution of Eq. ( 3), the mode intensities are: S 0 = P 0 (2 1/2 -1) 2 for the pump, and S n = 2 P 0 (2 1/2 -1) 2|n| (where n = ±1, ±2, ±3, … ) for the sidebands. The pump and sideband intensities follow the relative progression {I 0 , I 1 , I 2 , I 3 , I 4 …} = {1, 2, 0.3431, 0.0589, 0.0101…} This geometric progression yields a characteristic triangular shape in the wings of the spectrum when plotted semilogarithmically.

LINK TO SUPERCONTINUUM GENERATION EXPERIMENTS

We now present some experimental results: Fig. 1(a) shows spectral measurements at the output of 3.9 m of a highly nonlinear photonic crystal fiber with zero-dispersion wavelength at 780 nm for various peak powers using 1 ns pulses from a passively-modelocked microchip laser operating at 1064 nm. The experiment results in the top panel are compared with generalised nonlinear Schrödinger equation (GNLSE) simulations in the bottom panels. Full simulation details are to be found in Ref. [START_REF] Dudley | Modulation instability, Akhmediev Breathers and continuous wave supercontinuum generation[END_REF] but we note that the major parameters were: β 2 = -75 ps 2 km -1 and γ = 60 W -1 km -1 .

The numerical techniques used are standard although we note that the nanosecond simulations did require extensive computational time at the highest peak powers. We stress that the simulations did model the full temporal envelope of these long pulses. We note immediately that the agreement between experiment and simulation is very good and illustrate the key steps of initial sideband development followed by the merging and formation of a continuous triangular pedestal about the pump. At the lowest power of 26 W, the spectrum consists of small number of distinct sidebands separated by the frequency of peak MI gain. As the power increases to 43 W, we enter an "extended MI" regime where we can still resolve sidebands close to the pump, but we also see the development of continuous low amplitude wings. These wings appear triangular when plotted with a semi-logarithmic y-axis and although this is a characteristic feature of this regime that we and many authors have noted in many years of experimental studies, this particular feature has thus far not been the subject of specific analysis or investigation. The spectral width in this regime approaches 60 nm at the -40 dB level, and we note the first sign of a very low amplitude Raman peak around 1120 nm. At higher power levels approaching 100 W (bottom), the characteristics of a "fully-developed" supercontinuum are observed [START_REF] Dudley | Supercontinuum Generation in Photonic Crystal Fiber[END_REF]. In this case the spectrum extends significantly to longer wavelengths with features resembling soliton structures.

We focus now on the characteristics of the extended MI spectrum at 43 W peak power. In fact, although we have used GNLSE simulations in Fig. 1(b), this power level actually describes a regime before the onset of higher-order effects become significant and thus is a parameter regime where we expect the AB theory (which is after all based on an NLSE system) to provide a good description. Moreover, we expect that the point of maximum spectral broadening within the framework of the AB evolution would correspond to the point where the temporal structure is maximally compressed. Or in other words, to the point where the spectrum would be modeled by the spectrum of the maximally-compressed AB pulse described above. Indeed, we can confirm this using experimental spectral measurement by comparing the form of the measured spectrum with the geometric progression predicted for the maximally-compressed AB. Figure 2 compares numerical and analytic results with the experimental results of Fig. 1 for P 0 = 43 W. The numerical results show averaged multi-shot simulations using the full GNLSE with a 1 ns pulse input field (blue, short dashes) and using only the NLSE with a CW input field (red, long dashes). It is clear that both GNLSE and NLSE simulations produce similar results in agreement with experiment, with the GNLSE of course also predicting the onset of a small Raman peak on the long wavelength edge around 1120 nm; but this is largely insignificant in the context of the conclusions drawn here relating to AB dynamics. In fact these results also provide confirmation of the assumption that the spectrum at this point is explained by essentially NLSE dynamics.

Fig. 2 Experiments (black line),simulations using the full GNLSE (blue dashed line), numerical simulations using the NLSE only (red dashed line), and the calculated spectrum of the maximally-compressed AB (green lines from zero) [START_REF] Dudley | Modulation instability, Akhmediev Breathers and continuous wave supercontinuum generation[END_REF].

Perhaps the most important result here is the excellent agreement between the experimental decay of the spectral wings and the calculated amplitudes of the discrete frequency modes associated with the analytic form of the maximallycompressed AB. Because spontaneous MI is seeded by broadband noise, the spectral structure is of course not discrete, but rather consists of a continuous span of frequencies. Nonetheless, as with the time domain characteristics, we expect the spectral characteristics to contain a dominant component from the maximally-compressed AB solution calculated at peak MI gain. Thus, normalising to the n = ± 1 sideband amplitudes of experiment, the decay of spectral intensity with frequency in experiment and simulations is reproduced very well by the analytic geometric progression of the maximally-compressed AB breather.

TURBULENCE DYNAMICS

These results suggest that the characteristics of emergent SC generation can be explained in terms of the development of high amplitude Akhmediev Breather sub-pulses. But of course this is not a complete explanation of how these sub-pulses subsequently separate from the extended MI spectrum and temporal pulse train and evolve towards higher-amplitude pulses that exhibit rogue wave statistics. In this context, however we note that any realistic optical fiber system would contain symmetry-breaking physical effects due to odd orders of chromatic dispersion and Raman scattering. In fact, both these effects are important in that they can induce collisions between the emergent breathers, but for illustrative purposes, we consider only the effect of third order dispersion in the results that follow. Recent work has also shown how the effect of third-order dispersion can lead to an additional form of convective instability [START_REF] Taki | Third-order dispersion for generating optical rogue solitons[END_REF].

The particular physical dynamics that we consider here involves the regime of soliton turbulence, where an initial phase of multiple soliton formation from a noisy background is followed by the emergence of a single large soliton that extracts energy from the background and acts as a statistical attractor. With this model, the initial phase of multiple soliton emergence is the AB regime considered in the previous section, and we now consider its longer time evolutionary limit. Understanding the intermediate phase of evolution is still an open problem.

We now consider the dynamics of soliton turbulence with an ideal cubic nonlinearity and only TOD perturbation and show that this leads to an appreciable growth of a single soliton. We consider different parameters here with input pulses duration of 10 ps (FWHM) and a propagation distance of 500 m. Periodic boundary conditions were imposed over a time window of 20 ps. Further details are given in [START_REF] Genty | Collisions and turbulence in optical rogue wave formation[END_REF]. Figure 3 shows the results obtained, plotting temporal intensity (top) and the corresponding spectrum (bottom) at selected distances of 20, 70, and 500 m. From the temporal trace it can be seen how a large-amplitude localized structure emerges from an ensemble of waves with significantly lower amplitude, and the emergence of this large-amplitude localized structure is correlated to the gradual broadening of the spectrum both on the long-wavelength and short-wavelength edges. With more detailed consideration of these results, we have found that the emerging large-amplitude pulse is well-fitted by a hyperbolic-secant profile and has soliton order nearunity, confirming the interpretation of a giant rogue soliton pulse emerging from and propagating amidst an otherwise low amplitude noise background.

CONCLUSIONS

In conclusion, our numerical studies of spontaneous MI have shown that the well-known triangular form of the spontaneous MI spectrum when plotted semi-logarithmically can been explained naturally in terms of the analytic geometric progression describing the frequency dependence of AB modal amplitudes. In addition, other results have shown that SC generation described by an NLSE model perturbed only by TOD can lead to large amplitude localized optical rogue soliton and rogue wave structures. Generally speaking, any single perturbation that destroys the integrability of the NLSE is sufficient to observe "survival of the fittest" soliton amplification as a result of collisions. These results may have wide impact in improving understanding of the seeds of rogue wave formation in optics as well as hydrodynamics.

Fig. 1

 1 Fig.[START_REF] Solli | Optical rogue waves[END_REF] Experimental results (left) and numerical simulation results (right) for 1 ns pulses at 1064 nm injected into highly nonlinear PCF at peak powers as shown. Note that the simulation results are averaged and convolved with a spectral resolution function matching the bandwidth of the spectrum analyzer used in the experiments (0.1 nm for 26 W results; 0.4 nm for 43 W results; 1.6 nm for 98 W results)[START_REF] Dudley | Modulation instability, Akhmediev Breathers and continuous wave supercontinuum generation[END_REF].

Fig. 3

 3 Fig.3Spectral (top) and temporal (bottom) profiles of evolving SC field at selected distances as shown in a long-distance limit with multiple collisions. Simulations use an NLSE with only TOD perturbation[START_REF] Genty | Collisions and turbulence in optical rogue wave formation[END_REF].