Mnacho Echenim

Radu Iosif

Nicolas Peltier

The Lower Bound of Decidable Entailments in Separation Logic with Inductive Definitions

.

Introduction

In this paper, we consider the fragment of separation logic formulae known as symbolic heaps, defined as (separated) conjunctions of atoms. Such atoms may be either equational atoms, asserting equalities or disequalities between memory locations, points-to atoms asserting that some location refers to a given record, or may be built on additional predicates that assert that a part of the memory has a specific shape. For genericity, such predicates are associated with user-provided inductive definitions that allow one to describe custom data-structures. Satisfiability is EXPTIME-complete for such formulae [START_REF] Brotherston | A decision procedure for satisfiability in separation logic with inductive predicates[END_REF], but entailment is not decidable in general 3 [START_REF] Iosif | Deciding entailments in inductive separation logic with tree automata[END_REF][START_REF] Antonopoulos | Foundations for decision problems in separation logic with general inductive predicates[END_REF]. However, the entailment problem was proven to be decidable for a large class of inductive definitions, whose syntactical restrictions ensure that the generated heap structures have a bounded-tree width [START_REF] Iosif | The tree width of separation logic with recursive definitions[END_REF], using a reduction to monadic second order logic interpreted over graphs. A EXPTIMEhard bound was established in [START_REF] Iosif | Deciding entailments in inductive separation logic with tree automata[END_REF], and very recently, a 2EXPTIME algorithm has been proposed [START_REF] Katelaan | Effective entailment checking for separation logic with inductive definitions[END_REF]. However, personal communication with the authors of [START_REF] Katelaan | Effective entailment checking for separation logic with inductive definitions[END_REF] revealed several problems related to quantifier instantiation that are potential sources of incompleteness. Thus we believe that their decision procedure might not cover the entire class of entailments between symbolic heaps and is complete for a strict subclass in which the existential quantifiers of the right-hand side of entailments can be instantiated by the free variables on the left. In this paper, we show that the problem is 2EXPTIME-hard, even if only entailment between predicate atoms is considered. The proof uses a reduction from the membership problem for alternating Turing machines [START_REF] Ashok | [END_REF] whose working tape is exponentially bounded in the size of the input. Proving a matching 2EXPTIME upper bound reduces essentially to fixing the issues of the algorithm proposed in [START_REF] Katelaan | Effective entailment checking for separation logic with inductive definitions[END_REF] and is considered for future work.

Separation Logic with Inductive Definitions

For a finite set S , we denote by ||S || ∈ N its cardinality. For a partial mapping f : A B, let dom( f ) def = {x ∈ A | f (x) ∈ B} and img( f ) def = { f (x) | x ∈ A} be its domain and range, respectively, and we write f : A fin B if ||dom( f )|| < ∞. Given integers n ≤ m, we denote by n . . m the set {n, n + 1, . . . , m}. For a tuple t = (t 1 , . . . , t n ) and i ∈ 1 . . n , we denote by t i the element on the i-th position in t. By slight abuse of notation, we write t ∈ t if t = t i , for some i ∈ 1 . . n .

Let Var = {x, y, . . .} be an infinite countable set of logical first-order variables and Pred = {p, q, . . .} be an infinite countable set of uninterpreted relation symbols, called predicates. Each predicate p has an arity #p ≥ 1, denoting the number of arguments. In addition, we consider a special function symbol nil, of arity zero. A term is an element of the set Term def = Var ∪{nil}. Let k ≥ 1 be an integer constant fixed throughout this paper. The logic SL k is the set of formulae generated inductively as follows:

φ := emp | t 0 → (t 1 , . . . , t k ) | p(t 1 , . . . , t #p ) | t 1 =t 2 | t 1 ˙ t 2 | φ 1 * φ 2 | ∃x . φ 1
where p ∈ Pred, t 1 , t 2 , . . . , t #p ∈ Term and x ∈ Var. We write ⊥ for t ˙ t, for any t ∈ Term.

A ground formula is a formula of SL k in which no predicates occur. We write fv(φ) for the set of free variables, that occur in φ not within the scope of an existential quantifier. By writing φ(x 1 , . . . , x n ) we mean x 1 , . . . , x n ∈ fv(φ) and φ[y 1 /x 1 , . . . , y n /x n ] is the formula obtained from φ by simultaneously substituting each x i with y i , for i ∈ 1 . . n . A substitution is a mapping σ : Var → Term and we denote by φσ the formula φ[σ(x 1 )/x 1 , . . . , σ(x n )/x n ].

To interpret SL k formulae, we consider an infinite countable set Loc of locations and a designated location nil ∈ Loc. Let Loc i def = {( 1 , . . . , i ) | 1 , . . . , i ∈ Loc}. The semantics of SL k formulae is defined in terms of structures (s, h, I), where:

s : Term → Loc is a total mapping of terms into locations, called store, such that always s(nil) = nil, h : Loc fin Loc k is a finite partial mapping of locations into k-tuples of locations, called heap, such that nil dom(h). Let Heaps denotes the set of heaps, and -I : Pred → i≥1 2 Loc i ×Heaps is an interpretation associating each predicate p a set of pairs ( 1 , . . . , #p ), h ∈ Loc #p × Heaps. Two heaps h 1 and h 2 are disjoint iff dom(h 1 ) ∩ dom(h 2 ) = ∅, in which case their disjoint union is denoted h 1 h 2 , undefined otherwise. The satisfaction relation | = between structures and SL k formulae is defined, as usual, recursively on the syntax of formulae:

(s, h, I) | = t 1 =t 2 ⇔ h = ∅ and s(t 1 ) = s(t 2 ) (s, h, I) | = t 1 ˙ t 2 ⇔ h = ∅ and s(t 1 ) s(t 2 ) (s, h, I) | = emp ⇔ h = ∅ (s, h, I) | = t 0 → (t 1 , . . . , t k ) ⇔ dom(h) = {s(t 0 )} and h(s(t 0 )) = (s(t 1 ), . . . , s(t k )) (s, h, I) | = p(t 1 , . . . , t #p ) ⇔ (s(t 1 ), . . . , s(t #p )), h ∈ I(p) (s, h, I) | = φ 1 * φ 2
⇔ there are disjoint heaps h 1 and h 2 , such that h = h 1 h 2 and (s,

h i , I) | = φ i , for each i = 1, 2 (s, h, I) | = ∃x . φ ⇔ (s[x ← ], h, I) | = φ, for some ∈ Loc
where s[x ← ] is the store mapping x into and behaving like s for all t ∈ Term \ {x}.

Given formulae φ and ψ, we write φ ac = ψ if ψ is obtained from φ by a reordering of *connected subformulae. Since * is associative and commutative, any two such formulae are equivalent. It is known that, for any formulae φ and ψ, if x fv(ψ) then the formulae (∃x . φ) * ψ and ∃x . φ * ψ are equivalent [START_REF] Samin | Bi as an assertion language for mutable data structures[END_REF]. Thus, each SL k formula φ can be written as ∃x 1 . . . ∃x n . ψ * * m j=1 p j (u j 1 , . . . , u j #p j ), where φ def = ψ is a ground formula, called the hat of φ. Note that, moreover, φ is unique, up to the ac = relation. In the rest of this paper, we consider that the predicates are intepreted by a set S of rules p(x 1 , . . . , x #p ) ⇐ ρ, where ρ is an SL k formula, such that fv(ρ) ⊆ {x 1 , . . . , x # p }. We refer to p(x 1 , . . . , x #p ) as to the head and to ρ as to the body of the rule. A rule is a base rule if its body is a ground formula. W.l.o.g., we assume that any two heads with the predicate symbol p share the same tuple of variables x p (this can be achieved by variable renaming) and by writing p(x p ) we mean that x p is the unique tuple of variables associated with p. We write p(x p ) ⇐ S ρ if the rule p(x p ) ⇐ ρ belongs to S.

A set S of rules defines a transformer function T S on interpretations of predicates. For an interpretation I, the interpretation T S (I) is defined as:

T S (I) def = λp . , h | ([x p ← ], h, I) | = ρ, p(x p ) ⇐ S ρ
where x p = (x 1 , . . . , x #p ), = ( 1 , . . . , #p ) and [x p ← ] is any store mapping x i into i , for all i ∈ 1 . . #p . It is not hard to prove that the set of interpretations forms a complete lattice, equipped with the pointwise inclusion as a partial order, union as join and intersection as meet. Moreover, the transformer function is monotonic, because no predicate symbol occurs under negation in a rule body. Consequently, T S has a unique least fixed point T µ S . In the rest of this paper, given a set of rules S, we write (s, h) | = S φ for (s, h, T µ S ) | = φ and refer also to the pairs (s, h) as structures. We are now ready to define the class of entailment problems, which are the concern of this paper: Definition 1 (Entailment Problem). Given a set of rules S and two SL k formulae φ and ψ is it the case that for every store s and every heap h such that (s, h) | = S φ, we have (s, h) | = S ψ ? Instances of the entailment problem are denoted φ | = S ψ.

Unfolding Trees

In many cases it is useful to think of heaps from the least fixed point interpretation of a predicate symbol as obtained by a finite unfolding of the predicate, which produces a ground formula in which all the predicate symbols have been successively replaced with the bodies of their defining rules. In this section, let S be a given set of rules.

Definition 2 (Unfolding).

A formula ψ is a 1-unfolding of a formula φ, written φ =⇒ S ψ, if ψ is obtained by substituting an occurrence of an atom p(y 1 , . . . , y #p ) in φ with ρ[y 1 /x 1 , . . . , y #p /x #p ], where (p(x 1 , . . . , x #p ), ρ) ∈ S is a rule. An unfolding of φ is a formula ψ such that φ =⇒ * S ψ, where =⇒ * S is the reflexive and transitive closure of =⇒ S . Moreover, ψ is a ground unfolding of φ if ψ is a ground formula.

It is often convenient to place the steps of an unfolding sequence in a tree that records the partial order in which these steps occur. We assume the set of nodes in a tree t, denoted as nodes(t), to be a finite prefix-closed subset of N * , where N * is the set of finite sequences of positive integers, such that if w and wi are nodes of t, for some i ∈ N \ {0}, then so are w j, for all j ∈ 0 . . i -1 . We write |w| for the lenght of the sequence w and λ for the empty sequence (|λ| = 0). The label of a node w ∈ nodes(t) is denoted by t(w) and the subtree of t rooted at w by t |w . The height of a tree is height(t) def = max w∈nodes(t) |w|. A traversal of a tree t is an enumeration of nodes(t) such that the index of a node is smaller than all indices of its successors.

Definition 3 (Unfolding Tree). Given a formula φ, an unfolding tree for φ is a tree u, labeled with pairs (p, ψ), where p ∈ Pred ∪ {⊥} and ψ is a formula, such that:

t(λ) = (⊥, φ), and if u(w) = (p, ψ), then there exists a bijective mapping from the set of occurrences of atoms q(t 1 , . . . , t #q ) in ψ and the children of w, such that if q(t 1 , . . . , t #q ) is mapped to wi, then u(wi) = (q(t 1 , . . . , t #q ), ρ[t 1 /x 1 , . . . , t #q /x #q ]), where q(x 1 , . . . , x #q ) ⇐ S ρ. We denote by T S (φ) the set of unfolding trees for φ.

Clearly, every traversal of an unfolding tree u ∈ T S (φ 0 ) corresponds to a ground unfolding sequence σ : φ 0 =⇒ S φ 1 =⇒ S . . . =⇒ S ψ where, for each node w i of label (q(t), ψ) in σ, φ i is obtained from φ i-1 by replacing q(t) by ψ. It is easy to check that the outcome ψ only depends on u, not on σ. In other words, all traversals of u yield the same ground formula, denoted by F (t). By convention, we let F (u) def = φ if nodes(u) = {λ}. The following lemma provides an equivalent definition for the semantics of SL k formulae: Lemma 1. Given a SL k formula φ, for any store s and any heap h, we have (s, h) | = S φ if and only if (s, h) | = F (u), for some unfolding tree u ∈ T S (φ).

Proof : It is sufficient to give the proof only in the case φ = p(t 1 , . . . , t #p ), for a predicate symbol p ∈ Pred and terms t 1 , . . . , t #p ∈ Term, the generalization to the case where φ is any SL k formula being immediate. We start by proving the following fact: Fact 1 Let u ∈ T S p(t 1 , . . . , t #p ) be an unfolding tree, such that (necessarily) u(0) = (p(t 1 , . . . , t #p ), ρσ), for some rule: p(x 1 , . . . , x #p ) ⇐ ∃y 1 . . . ∃y n . ρ * m * j=1 p j (t j 1 , . . . , t j #p j ) ρ and some substitution σ such that σ(x k ) = t k , for all k ∈ 1 . . #p , then F (u) ac = ∃y 1 . . . ∃y n . ρσ * * m j=1 F (u j ), where u j ∈ T S p j (t j 1 , . . . , t j #p j )σ , for all j ∈ 1 . . m . Proof : Let s : φ 0 = p(t 1 , . . . , t #p ) =⇒ S φ 1 = ρσ =⇒ S . . . =⇒ S φ r = F (u) be a ground unfolding sequence. Then there exists ∈ 1 . . m and a position j ∈ 1 . . r in this sequence such that the sequence φ 1 =⇒ S . . . =⇒ S φ j traverses all nodes from u | . W.l.o.g., let and j be the least such numbers, respectively. We re-organize the unfolding sequence s into s 1 by moving all steps between 1 and j, corresponding to visits of nodes from u | , for ∈ 1 . . m \ { }, after j and let k ≤ j be the new position of φ j in s 1 . Clearly this re-organization does not change the outcome φ r , who is the same for s and s 1 . Because all nodes from u | j are visited by s 1 :

φ 1 0 = φ 0 =⇒ S φ 1 1 = φ 1 =⇒ S . . . =⇒ S φ 1
k =⇒ S . . . =⇒ S φ 1 r = φ r , we obtain:

φ 1 k ac = ∃y 1 . . . ∃y n . ρσ * * j∈ 1. .m \ p j (t j 1 , . . . , t j #p j ) * F (u )
The unfolding sequence φ 1 k =⇒ S . . . =⇒ S φ r is strictly smaller than s and we apply the same argument inductively until the ground formula F (u) is derived.

Let

t def = (t 1 , . . . , t #p ) and s(t) def = (s(t 1 ), . . . , s(t #p )). Let T 0 S def = λp.
∅ be the interpretation mapping each predicate symbol into the empty set. We have (s, h)

| = S p(t) if and only if s(t), h ∈ T µ S (p) = ∞ i=0 T i S (p).
The last equality uses the fact that T S is monotone and continuous which, by Kleene's Fixpoint Theorem, guarantees that its least fixpoint is the limit of the increasing sequence of approximants T i S i≥0

. For any predicate symbol p ∈ Pred and any tuple of terms t = (t 1 , . . . , t #p ), we prove the following equivalence by induction on i ≥ 0:

s(t), h ∈ T i S (p) ⇔ (s, h) | = F (u)
, for some u ∈ T S (p(t)), such that height(u) ≤ i In the base case i = 0, the equivalence holds because both s(t), h ∈ T 0 S (p) is false and T S (p(t)) contains no unfolding tree of height 0. For the induction step i ≥ 1, we consider two directions:

"⇒" If s(t), h ∈ T i S (p) then s, h, T i-1 S | = ρσ, for some rule: p(x 1 , . . . , x #p ) ⇐ S ∃y 1 . . . ∃y n . ρ * m * j=1 p j (t j 1 , . . . , t j #p j ) ρ
and substitution σ such that σ(x k ) = t k , for all k ∈ 1 . . #p . Then there exists locations 1 , . . . , n ∈ Loc and heaps h 0 , h 1 , . . . , h m such that h = m j=0 h j and the following hold: -(s , h 0 ) | = ρσ, and s (t j σ), h j ∈ T i-1 S (p j ), for all j ∈ 1 . . m , where s def = s[y 1 ← 1 , . . . , y n ← n ] and t j def = (t j 1 , . . . , t j #p j ), for all j ∈ 1 . . m . By the induction hypothesis, we obtain unfolding trees u j ∈ T S p j (t j σ) , of height at most i -1, such that (s , h j ) | = F (u j ), for all j ∈ 1 . . m . Note that, by Definition 3, the root of each u j has a single child and let u j |0 be the subtree of u j rooted at the child of λ. Then we define an unfolding tree u, such that u(λ

) def = (⊥, p(t)), u(0) def = (p, ρσ) and u | j def = u j |0 , for all j ∈ 1 . . m . It is straightforward to check that u ∈ T S (p(t)
) and that the height of u is at most i. We are left with proving that (s, h) | = F (u), which follows from Fact 1 and the inductive hypothesis (s ,

h j ) | = F (u j ), for all j ∈ 1 . . m . "⇐" If (s, h) | = F (u)
then, by Definition 3, the root of u has a single child 0 whose label is u(0) = (p(t), ρσ), for a rule:

p(x 1 , . . . , x #p ) ⇐ S ∃y 1 . . . ∃y n . ρ * m * j=1 p j (t j 1 , . . . , t j #p j )
ρ and a substitution σ(x k ) = t k , for all k ∈ 1 . . #p . By Fact 1, we obtain:

F (u) ac = ∃y 1 . . . ∃y n . ρσ * m * j=1 F (u j )
for some unfolding trees u j ∈ T S p j (t j 1 , . . . , t j #p j ) , of height at most i -1, for j ∈ 1 . . m . Since (s, h) | = F (u), there exists locations 1 , . . . , n ∈ Loc, such that:

-(s , h 0 ) | = ρσ and -(s , h j ) | = F (u j ), for all j ∈ 1 . . m ,
where

s def = s[y 1 ← 1 , . . . , y n ← n ] and h = m j=0 h j .
By the inductive hypothesis, we obtain:

s (t j σ), h j ∈ T i-1 S (p j ) ⊆ T µ S (p j )
where

t j def = (t j 1 , . . . , t j #p ), for all j ∈ 1 . . m . But then (s , h j ) | = S p j (t j σ), for all j ∈ 1 . . m , thus (s, h) | = S ρσ and (s, h) | = S p(t) follows.

A Decidable Class of Entailments

In general, the entailment problem is undecidable, proofs can be found in [START_REF] Iosif | Deciding entailments in inductive separation logic with tree automata[END_REF][START_REF] Antonopoulos | Foundations for decision problems in separation logic with general inductive predicates[END_REF]. Thus we consider a subclass of entailments for which decidability (with elementary recursive complexity) was proved in [START_REF] Iosif | The tree width of separation logic with recursive definitions[END_REF] and provide a 2EXPTIME lower bound for this problem. The decidable class is given by three restrictions of the systems used for the interpretation of predicates, namely progress, connectivity and establishment, defined in the rest of this section.

First, the progress condition requires that each rule adds to the heap exactly one location, namely the one associated to the first parameter of the head. Second, the connectivity condition requires that all locations added during an unfolding of a predicate atom p(t) form a connected tree-like structure.

Definition 4 (Progress & Connectivity).

A set of rules S is progressing if and only if, the body ρ of each rule p(x 1 , . . . , x #p ) ⇐ S ρ is of the form ∃z 1 . . . ∃z m . x 1 → (y 1 , . . . , y k ) * ψ and ψ contains no occurrence of a → atom. If, moreover, each occurrence of a predicate atom in ψ is of the form q(y i , u 1 , . . . , u #q-1 ), for some i ∈ 1 . . k , then S is connected.

For upcoming developments, we make the connection between heaps and unfolding trees more precise, in the context of progressing connected sets of rules. Lemma 2. Assume that S is a progressing and connected set of rules and that (s, h) is a structure such that (s, h) | = S p(t 1 , . . . , t #p ), for some predicate symbol p ∈ Pred and terms t 1 , . . . , t #p ∈ Term. Then there exists an unfolding tree u ∈ T S p(t 1 , . . . , t #p ) and a bijection Λ : dom(h) → nodes(u)\{λ} such that (s, h) | = F (u) and for each node wi ∈ nodes(u)\{λ}, where i ∈ N, we have Λ -1 (wi) ∈ h(Λ -1 (w)).

Proof : If (s, h) | = S p(t 1 , . . . , t #p ), by Lemma 1, there exists u ∈ T S p(t 1 , . . . , t #p ) , such that (s, h) | = F (u). Note that, by Definition 3, the root of u is labeled by u(λ) = (⊥, p(t 1 , . . . , t #p )) and has a single child, namely 0. The bijection Λ is built inductively on the structure of the subtree u |0 of u, rooted at 0, taking into account Definition 4.

Given a structure (s, h) such that (s, h) | = S p(t 1 , . . . , t #p ), for any location ∈ dom(h), necessarily must be allocated by a 1-unfolding of some atom q(t), which corresponds to a node in an unfolding tree Λ( ) ∈ T S p(t 1 , . . . , t #p ) . In the following, we shall denote by Pr s,h,Λ ( ) the predicate symbol q. Note that the existence of the unfolding tree u and bijection Λ : dom(h) → nodes(u) \ {λ} are guaranteed by Lemmas 1 and 2, respectively. The notation Pr( ) stands for Pr s,h,Λ ( ), for some Λ as in Lemma 2, where the structure (s, h) is clear from the context.

The third condition requires that all the existentially quantified variables introduced during a can only be associated with locations from the heap, in every ground unfolding of a formula. To formalize this condition, for a ground formula φ, we define the partial satisfaction relation as (s, h) φ iff h = h 1 h 2 and (s, h 1 ) | = φ and partial entailment as

φ ψ iff (s, h) ψ for each structure (s, h), such that (s, h) | = φ. If φ is ground, its set of allocated variables is alloc(φ) def = {x ∈ fv(φ) | x → (y 1 , . . . , y k ) occurs in φ and φ x =x }.
Note that alloc(φ) = fv(φ) if φ is unsatisfiable. Extending this notion to formulae that are not necessarily ground, we define alloc S (φ) def = u∈T S (φ) alloc(F (u)), i.e. a variable is allocated in φ iff it is allocated in every ground unfolding of φ w.r.t. a set of rules S.

Definition 5 (Establishment).

A set of rules S is established if and only if, for each rule (p(x p ), ∃z 1 . . . ∃z m . ψ) ∈ S, where ψ is quantifier-free, we have z 1 , . . . , z m ∈ alloc S (ψ).

In the following, we consider only sets of rules that are progressing, connected and established (PCE). The interest for PCE sets of rules is motivated by the following decidability result, proved in [START_REF] Iosif | The tree width of separation logic with recursive definitions[END_REF]: Theorem 1 (Decidability). Given a PCE set of rules S and two formulae φ and ψ such that the free variables of ψ are also free in φ, the problem φ | = S ψ belongs to

ELEMENTARY.

The rest of this paper is concerned with proving that the entailment problem φ | = S ψ, for PCE sets of rules S, is 2EXPTIME-hard. Previously, a EXPTIME-hard bound for this problem was established in [START_REF] Iosif | Deciding entailments in inductive separation logic with tree automata[END_REF].

Syntactic Shorthands

Before proving 2EXPTIME-hardness by reduction from the membership problem of alternating Turing machines running in exponential space, we define several syntactical shorthands that simplify the presentation.

Given a term t and n ≥ 0, we denote by t n the tuple consisting of n occurrences of t. In the rest of the paper we silently assume that any heap entry of the form h( ) = ( 1 , . . . , k ) is represented by a binary heap h 2 :

Loc fin Loc 2 such that dom(h 2 ) = { } ∪ i 0 | i ∈ 1 . . k -1 , h 2 ( ) = ( 1 0 , 1 ) and h 2 ( i 0 ) = ( i+1 0 , i+1 ), for all i ∈ 1 . . k -1 , with k 0 = nil.
This allows one to encode records of non constant length (for instance tuples of length N) by using only a constant number of record fields (i.e., k = 2).

Deep Hats For a tuple t = (t 1 , . . . , t j ) ∈ Term j , j ≥ 1 and n ≥ 0, by writing:

p(x 1 , . . . , x #p ) ⇐ ∃y 1 . . . ∃y r . x 1 → (u 1 , . . . , u i-1 , [t] n , u i+1 , . . . , u m ) * ψ
we denote the rules: p(x 1 , . . . , x #p ) ⇐ ∃y 1 . . . ∃y r . x 1 → (u 1 , . . . , u i-1 , t 1 , . . . , t j , u i+1 , . . . , u m ) * ψ, if n = 0 and, recursively, for all n > 0:

p(x 1 , . . . , x #p ) ⇐ ∃y 1 . . . ∃y r ∃z . x 1 → (u 1 , . . . , u i-1 , z, u i+1 , . . . , u m ) * p n-1 (z, x 1 , . . . , x #p , y 1 , . . . , y r ) * ψ p (z 1 , . . . , z #p+r+1 ) ⇐ ∃z 1 . z 1 → (z 1 ) * p -1 (z 1 , z 2 , . . . , z #p+r+1 ), for ∈ 1 . . n -1 p 0 (z 1 , . . . , z #p+r+1 ) ⇐ z 1 → (t 1 , . . . , t j ) * ψ
where p , for ∈ 0 . . n -1 are fresh predicate symbols of arity # p = #p + r + 1 and ψ (resp. ψ ) is the separating conjunction of all atoms of ψ whose first argument is in t (resp. is not in t). Clearly, ψ * ψ ac = ψ, and the obtained rules are connected.

Special Variables

We assume the existence of the following special variables that occur free in each formula: 0, 1, γ 1 , . . . , γ N , for some fixed constant N ≥ 2, used throughout the paper. These variables will always be allocated and denote separate locations, as required by the following rule:

Const(x) ⇐ x → (0, 1, γ 1 , . . . , γ N ) * 0 → (nil) * 1 → (nil) * * N i=1 γ i → (nil) (1)
Considering special variables is without loss of generality in the following, because these variables can be added to the parameter list of each head in the system, at the expense of cluttering the presentation.

Binary Choices

The symbol • occurring in the body of a rule ranges over the special variables 0 and 1. Thus any rule of the form: Note that eliminating the occurrences of • will increase the number of rules in S by a constant at most 2 k , because k is assumed to be constant (i.e. independent of the input of a decision procedure).

p(
Binary Variables A binary variable b is understood as ranging over the domain of the interpretation of 0 and 1, namely the locations assigned to 0 and 1 by the formula Const (1). Additionally, for each binary variable b, we consider the associated variable b, intended to denote the complement of b. More precisely, the formula ∃b . ψ is understood as ψ[0/b, 1/b] ∨ ψ[1/b, 0/b]. However, this direct substitution of the (existentially quantified) binary variables by 0 and 1 within the rules of an established system would break the establishment condition (Definition 5), because 0 and 1 are not necessarily allocated within the body of the rule 4 . This problem can be overcome by passing 0 and 1 as parameters to a fresh predicate. More precisely, a rule of the form:

p(x 1 , . . . , x #p ) ⇐ ∃b 1 . . . ∃b i ∃y 1 . . . ∃y n . x 1 → ([t] m ) * ψ (2)
where 1 ≤ i ≤ m, is a shorthand for the following set of rules:

p(x 1 , . . . , x #p ) ⇐ ∃y . x 1 → (y) * p (y, x 1 , . . . , x #p , 0, 1) p(x 1 , . . . , x #p ) ⇐ ∃y . x 1 → (y) * p (y, x 1 , . . . , x #p , 1, 0) p (y, x 1 , . . . , x #p , b 1 , b 1 ) ⇐ ∃b 2 . . . ∃b i ∃y 1 . . . ∃y n . y → ([t] m-1 ) * ψ
Clearly, the elimination of the binary existential quantifiers from the rule (2) will add 2i rules to the set. Note that the hat [t] m , of height m ≥ i decreases at each step of the elimination. This guarantees that rules resulting from the elimination of ∃b 1 , . . . , ∃b i respectively, are progressing (Definition 4).

Next, for a vector b = (b 1 , . . . , b n ) of binary variables, we denote by b the vector (b 1 , . . . , b n ). The following rule:

p(x 1 , . . . , x #p ) ⇐ ∃y 1 . . . ∃y m . x 1 → t * ψ | (b 1 , . . . , b n ) (c 1 , . . . , c n ) (3)
where b 1 , . . . , b n ∈ {x 2 , . . . , x #p , y 1 , . . . , y m } occur only once in t and do not occur in ψ and c 1 , . . . , c n ∈ {x 2 , . . . , x #p , y 1 , . . . , y m }, is a shorthand for the following set of rules:

p(x 1 , . . . , x #p ) ⇐ ∃y 1 . . . ∃y m . x 1 → (t[c i /b i ]) [•/b j ] j∈ 1. .n \{i} * ψ, i ∈ 1 . . n (4)
Intuitively, the rule (3) introduces new binary variables b 1 , . . . , b n , such that not all of them are equal to the complement of c 1 , . . . , c n , respectively. In other words, at least one b i must be equal to c i , for some i ∈ 1 . . n . Note that expanding the rule (3) as described above results in at most n rules of the form (2), hence the full elimination of binary variables from the system is possible in polynomial time.

Alternating Turing Machines

An Alternating Turing Machine (ATM) is a tuple M = (Q, Γ, δ, q 0 , g) where:

-Q is a finite set of control states, -Γ = {γ 1 , . . . , γ N , b} is a finite alphabet, b is the blank symbol and each symbol from Γ \ {b} is named after a special variable, -δ ⊆ Q×Γ × Q×(Γ \{b})×{←, →} is the transition relation, (q, a, q , b, µ) ∈ δ meaning that, in state q, upon reading symbol a, the machine moves to state q , writes b b to the tape 5 and moves the head by one to the left (resp. right) if µ =← (resp. µ =→), q 0 ∈ Q is the initial state, and g : Q → {∨, ∧} partitions the set of states into existential (g(q) = ∨) and universal (g(q) = ∧) states. A configuration of M is a tuple (q, w, i) where q ∈ Q is the current state, w : N → Γ is (the contents of) the tape, such that ||{ j ∈ N | w( j) b}|| < ∞ and i ∈ 0 . . max { j ∈ N | w( j) b}+ 1 is the current position of the head on the tape. We denote by the empty word over Γ. For any tape w and integer i, we denote by w[i ← a] the tape w such that w (i) = a and w ( j) = w( j) for all j i. In the following, we write w i def = w(i), i ← def = i -1 and i → def = i + 1. The step relation of M is the following relation between configurations: we write (q, w, i) (q,a,q ,b,µ) -------→ (q , w , j) if and only if there exists a transition (q, a, q , b, µ) ∈ δ such that w i = a, w = w[i ← b] and j = i µ . We write (q, w, i) -→ (q , w , j) when the applied transition is not important. An execution is a sequence (q 0 , w 0 , 0)

(q 0 ,a 0 ,q 1 ,b 0 ,µ 0 ) ----------→ (q 1 , w 1 , i 1 ) (q 1 ,a 1 ,q 2 ,b 1 ,µ 1 )
----------→ . . . Note that an execution is entirely determined by the initial configuration (q 0 , w 0 , 0) and the sequence (q 0 , a 0 , q 1 , b 0 , µ 0 ), (q 1 , a 1 , q 2 , b 1 , µ 1 ), . . . of transition rules applied to it.

Given a function f : N → N, an execution is f -space bounded if and only if there exists a constant c > 0 such that |w i | ≤ c• f (|w 0 |), for all i > 0. The ATM M is exponentialspace bounded if it admits only f -space bounded executions, where f (x) = 2 g(x) and g is a univariate polynomial function. Definition 6. A derivation of an ATM M = (Q, Γ, δ, q 0 , g), starting from a configuration (q 0 , w 0 , 0), is a tree t, whose nodes are either:

1. branching nodes labeled with configurations (q, w, i) ∈ Q × Γ * × N, or 2. action nodes labeled with tuples (a, b, µ) ∈ Γ × Γ \ {b} × {←, →}, where a is the symbol read, b is the symbol written and µ is the move of the head at that step, such that the root of t is a branching node, t(λ) = (q 0 , w 0 , 0) and, moreover: a. each branching node labeled by (q, w, i), such that g(q) = ∨, has exactly one successor, that is an action node labeled by (a, b, µ), where (q, a, q , b, µ) ∈ δ, whose successor is a branching node labeled by (q , w , j) such that (q, w, i) (q,a,q ,b,µ)

-------→ (q , w , j), b. each branching node labeled by (q, w, i), such that g(q) = ∧ has exactly one successor for each tuple (q, a, q , b, µ) ∈ δ such that a = w(i), and the successor associated with a transition (q, a, q , b, µ) is a branching node, labeled by (q , w , j) with (q, w, i) (q,a,q ,b,µ)

-------→ (q , w , j). We say that M accepts (q 0 , w 0 , i 0 ) iff it has a derivation starting from (q 0 , w 0 , i 0 ). Definition 7. The membership problem (M, w) asks the following: given an ATM M = (Q, Γ, δ, q 0 , g) and an input word w ∈ (Γ \ {b}) * does M accept (q 0 , w, 0) ?

The complexity class AEXPSPACE is the class of membership problems where M is exponential-space bounded. It is known that AEXPSPACE=co-AEXPSPACE=2EXPTIME [START_REF] Ashok | [END_REF], where co-AEXPSPACE is the complement class of AEXPSPACE 6 . In the following, we shall w.l.o.g. consider only the membership problem (M, ). Indeed, let (M, w) be any instance of the membership problem, and let c and g be the constant and polynomial function witnessing the fact that M is exponential-space bounded. Let M w be the ATM that produces w starting from input . Clearly, M w uses at most |w| working space, thus the machine M w ; M which runs M w on the empty word and then continues with M runs in space c • 2 g(|w|) and accepts (q 0 , , 0) if and only if M accepts (q 0 , w, 0). If N ≥ log 2 (c) + g(w), then M w ; M runs in space 2 N . Therefore, we assume from now on that M = (Q, Γ, δ, q 0 , g) is an ATM started in the configuration (q 0 , , 0) and that M runs in space at most 2 N on (q 0 , , 0), where N is polynomial w.r.t. the length of w.

Pseudo-derivations as Heaps

Given an ATM M = (Q, Γ, δ, q 0 , g), we consider its pseudo-derivations, which are the trees of Definition 6 relaxed so that any sequence of three consecutive branching-actionbranching node labels (q, w, i), (a, b, µ) and (q , w , i ) only needs to ensure the existence of a transition (q, a, q , b, µ) ∈ δ, i.e. we drop the requirements w i = a, w = w[i ← b] and i = i µ from the condition (q, w, i) (q,a,q ,b,µ) -------→ (q , w , i ) in Definition 6. Clearly, the leaves of a pseudo-derivation are all labeled by universal states.

We represent the pseudo-derivations of M as tree-shaped heaps generated by a set of rules where, intuitively, each predicate q(x) allocates a branching node labeled by a configuration (q, w, i), for some w ∈ Γ * and some i ∈ 0 . . 2 N -1 , and each predicate q(x, a, b, µ) allocates an action node labeled (a, b, µ). Importantly, since M starts on the empty word , the tape contents in a branching node can be derived from the sequence of actions along the path from the root to that node. For this reason, we shall not explicitly represent tape contents within the configurations and label branching nodes with pairs (q, i)

∈ Q × 0 . . 2 N -1 .
We represent each position i ∈ 0 . . 2 N -1 on the tape succintly, by an N-tuple of binary digits bin(i) ∈ {0, 1} N and encode the left and right moves as

← def = 0 and → def = 1. Let τ(q, a) def = δ ∩ ({q} × {a} × Q × Γ \ {b} × {←, →}
) be the set of transitions of M with source state q, reading symbol a from the tape.

As previously mentioned, we simplify the presentation by considering atoms of the form x → (y 1 , . . . , y m ) for an arbitrary m ≥ 1, with the understanding that the heap corresponding to this atom is uniquely encoded by a binary heap. This is without loss of generality, because a rule containing such atoms can be transformed into a finite set of rules containing only atoms of the form x → (y 1 , y 2 ), resulting in a progressing, connected and established set of rules. With this in mind, we consider the following rules, for each state q ∈ Q:

q(x) ⇐ ∃x . x → (• N , x ) * q (x , a, b, µ) (5) if g(q) = ∨ and (q, a, q , b, µ) ∈ τ(q, a) q(x) ⇐ ∃y 1 . . . ∃y n . x → (• N , y 1 , . . . , y m ) * m * j=1 q j (y j , a, b j , µ j ) (6) if g(q) = ∧ and τ(q, a) = {(q, a, q 1 , b 1 , µ 1 ), . . . , (q, a, q m , b m , µ m )} q(x, y, z, u) ⇐ ∃x . x → (y, z, u, x ) * q(x ) (7)
The heaps defined by the above rules ensure only that the control structure of a derivation of M is respected, namely that the branching and action nodes alternate correctly, and that the sequence of control states labeling the branching nodes on any path is consistent with the transition relation of M. In other words, these trees encode pseudoderivations of M. Further, we introduce a top-level predicate p M (x) that allocates the special variables 0, 1, γ 1 , . . . , γ N and ensures that the initial state q 0 of M is the first control state that occurs on an path of a pseudo-derivation:

p M (x) ⇐ ∃y 0 ∃z 0 . x → ([y 0 ] N , z 0 ) * q 0 (y 0 ) * Const(z 0 ) (8)
Note that the hat [y 0 ] N above ensures that every heap in the least fixed point interpretation of p begins with a tree of height N. The use of this tree will be made clear below.

For now, let S be the set consisting of the rules above. We formalize the encoding of a pseudo-derivation by a structure:

Definition 8. A structure (s, h) such that (s, h) | = S p M (x)
encodes a pseudo-derivation t of M, written as (s, h) t, if and only if there exists a injective mapping f : nodes(t) → dom(h) \ s(Γ ∪ {0, 1}) such that, for all w ∈ nodes(t), the following hold:

1. for all i ∈ N, if wi ∈ nodes(t) then f (wi) ∈ h( f (w)), 2. if w is a branching node and t(w) = (q, i) then Pr( f (w)) = q and h( f (w)) = ( 1 , . . . , N+1 ), where j = s(bin(i) j ), for all j ∈ 1 . . N and N+1 ∈ dom(h), 3. if w is an action node and t(w) = (a, b, µ) then h( f (w)) = (s(a), s(b), s( µ), 4 ), where 4 ∈ dom(h), We write (s, h) > t instead of (s, h) t if condition (2) above is replaced by the weaker: 2'. if w is a branching node and t(w) = (q, i) then h( f (w)) = ( 1 , . . . , N+1 ), where j = s(bin(i) j ), for all j ∈ 1 . . N and N+1 ∈ dom(h).

Note that, by Lemma 1 (s, h) | = S p M (x) iff there exists an unfolding tree u ∈ T S (p M (x)) such that (s, h) | = F (u) and, by Lemma 2, there exists a bijection Λ : dom(h) → nodes(u)\ {λ}, such that Λ -1 (wi) ∈ h(Λ -1 (w)), for all wi ∈ nodes(u). Then the occurrence of Pr(.) at point (2) of Definition 8 stands for Pr s,h,Λ (.), the structure (s, h) being clear from the context and the existence of Λ being guaranteed by Lemma 2. The weaker relation (s, h) > t shall be used next to encode pseudo-derivations by structures that are not necessarily models of the above rules (more rules will be added later).

Lemma 3. (A) For each pseudo-derivation t of an ATM M = (Q, Γ, δ, q 0 , g), there exists a structure (s, h) | = S p M (x) such that (s, h) t. (B) Dually, for each structure (s, h) | = S p M (x), there exists an accepting pseudo-derivation t of M such that (s, h) t.

Proof : (A) Let t be a pseudo-derivation of M. We build an isomorphic tree u, such that nodes(t) = nodes(u) and the labels of u are of the form (q, φ), where q ∈ Pred and φ is a formula. The definition of u is top-down on the structure of t, for each node w ∈ nodes(t), with label t(w) = (q, i):

if g(q) = ∨ , where t(w0) = (a, b, µ) and t(w00) = (q , i ) (we have necessarily w0, w00 ∈ nodes(t), where w0 and w00 are the only children of w and w0, respectively), then we define:

u(w) def = (q, ∃x . x → (bin(i), x ) * q(x , a, b, µ)) (see rule 5) u(w0) def = (q, ∃x . x → (a, b, µ, x ) * q(x )) (see rule 7)
otherwise, g(q) = ∧ and t(w j) = (a j , b j , µ j ) for j ∈ 1 . . n are the children of w, and t(w j0) = (q j , i j ), for all j ∈ 1 . . n , in which case we define: u(w) def = q, ∃y 1 . . . ∃y n . x → (bin(i), y 1 , . . . , y n ) * * n j=1 q j (y j , a j , b j , µ j ) (see rule 6) u(w j) def = q j , ∃x . y j → (a j , b j , µ j , x ) * q j (x ) (see rule 7)

Finally, either one of the following holds:

w = vi, for some v ∈ nodes(t), i ∈ N and the atom q(x) occurs exactly once in u(v), w = λ and the variable x in the definition of u(w) is the same as y 0 , in which case necessarily t(λ) = (q 0 , 0).

Next, we extend u to an unfolding tree û ∈ T S (p M (x)) by adding to it a hat of height N and a sibling tree u ∈ T S (Const(z 0 )). It is not hard to check that û ∈ T S (p M (x)) and that F (û) is satisfiable, since there are no equality or disequality atoms and no variable occurs allocated in two different subtrees of û. Then, let (s, h) be a structure such that (s, h) | = F (û). To check that (s, h) t, we need to exhibit an injective mapping f : nodes(t) → dom(h) that meets the conditions (1), ( 2) and (3) from Definition 8. Because S is a progressing and connected set of rules and (s, h) | = F (û), by Lemma 2, there exists a bijective mapping Λ : dom(h) → nodes(û) \ {λ} such that Λ -1 (wi) ∈ h(Λ -1 (w)), for all w ∈ nodes(û) \ {λ} and all i ∈ N, such that wi ∈ nodes(û). Let f be the restriction of Λ -1 to nodes(u). Point [START_REF] Antonopoulos | Foundations for decision problems in separation logic with general inductive predicates[END_REF] follows by the definition of Λ, whereas points (2) and ( 3) are simple checks.

(B) Conversely, if (s, h) | = S p M (x) then, by Lemma 1, there exists an unfolding tree u ∈ T S (p M (x)) such that (s, h) | = F (u). Since S is progressing and connected, by Lemma 2, there exists a bijective mapping Λ : dom(h) → nodes(u) \ {λ}, as before. By the definition of S, all nodes w ∈ nodes(u) \ {λ} that are labeled with predicates q and q, for some q ∈ Q, occur below a unique node w 0 ∈ nodes(u), such that t(w 0 ) = (q 0 , φ), for some formula φ. We build a pseudo-derivation t of M such that nodes(t) = nodes(u |w 0 ), by induction on the structure of u |w 0 . Namely, for each w ∈ nodes(u |w 0 ):

-If u |w 0 (w) = (q, φ) then φ is the body of a rule [START_REF] Iosif | Deciding entailments in inductive separation logic with tree automata[END_REF] or [START_REF] Samin | Bi as an assertion language for mutable data structures[END_REF]. In the case (5) (the other case is similar and left to the reader) we have h(Λ -1 (w)) = ( 1 , . . . , N+1 ), with 1 , . . . , N ∈ {s(0), s(1)} and let i be the integer such that bin(i) = (s -1 ( 1 ), . . . , s -1 ( N )). Note that, since 0 and 1 are always allocated separately in F (u), the restriction of s to the set {0, 1} is a bijection. In this case, we define t(w) def = (q, i). -Otherwise, u |w 0 (w) = (q, φ) and φ is the body of a rule [START_REF] Katelaan | Effective entailment checking for separation logic with inductive definitions[END_REF]. In this case, we have h(Λ -1 (w)) = ( 1 , 2 , 3 , 4 ), with 1 ∈ s(Γ), 2 ∈ s(Γ \ {b}) and 3 ∈ {s(0), s(1)}. Note that, since each γ ∈ Γ ∪ {0, 1} is allocated separately in F (u), the restriction of s to the set Γ ∪ {0, 1} is a bijection. In this case, we define t(w

) def = (s -1 ( 1 ), s -1 ( 2 ), µ), where µ =← if 3 = s(0) and µ =→ if 3 = s(1).
It is easy to check that, indeed t is a pseudo-derivation of M. To check that (s, h) t, we take f : nodes(t) → dom(h) as the restriction of Λ -1 to the nodes of u |w 0 . Clearly, f is injective and the conditions (1), ( 2) and (3) of Definition 8 are easy checks.

Encoding Complement Membership as Entailment Problems

Given an ATM M = (Q, Γ, δ, q 0 , g), a pseudo-derivation of M is a derivation of M if the contents of the tape is consistent with the sequence of the actions applied, in particular the following conditions must hold:

I. If a branching node labeled (q, i) is followed by an action node labeled (a, b, →) [resp. (a, b, ←)], itself followed by a branching node labeled (q , i ) then necessarily i = i + 1 [resp. i = i + 1], i.e. the position of the head changes according to the action executed between the adjacent configurations. II. For every i ∈ 0 . . 2 N -1 , if along a path from a branching node labeled (q, i),

followed by an action node labeled (a, b, µ), to another branching node labeled (q , i), followed by an action node labeled (a , b , µ ), there is no branching node labeled (q , i), then necessarily a = b. Indeed, the symbol read on position i must be the one previously written, since it was not changed in the meantime. III. For every i ∈ 0 . . 2 N -1 , if along a path from the root to a branching node labeled (q, i), followed by an action node labeled (a, b, µ), there is no branching node labeled (q , i), then necessarily a = b, i.e. the tape is initially empty. In the following, we shall not check that the above conditions hold for some derivation of M, but rather the opposite: that for each derivation of M, at least one of the above conditions is broken. In other words, we reduce from the complement of the membership problem (M, ) to an entailment problem, defined next. This does not change the final 2EXPTIME-hardness result, because 2EXPTIME=AEXPSPACE=co-AEXPSPACE, as previously mentioned.

In the following, we shall give the rules for a predicate c M (x) such that the entailment p M (x) | = S c M (x) holds, for a suitable set of rules S, containing the rules for p M (x) and c M (x), iff every pseudo-derivation of M breaks at least one of the conditions (I), (II) or (III), in other words, that M, started on input , has no derivation.

Let B def = max q∈Q,a∈Γ ||τ(q, a)|| be the maximum branching degree of a derivation of M. First, we define an auxiliary predicate r(x) that generates all tree-shaped heaps in which branching nodes correctly alternate with action nodes, with no regard to the labels of those nodes. In the following, we stick to the convention that predicate symbols p represent branching nodes, whereas p represent action nodes: r(x) ⇐ ∃y 1 . . . ∃y n . x → (• N , y 1 , . . . , y n ) * * n j=1 r(y j ), for each n ∈ 0 . . B r(x) ⇐ ∃y . x → (a, b, •, y) * r(y), for each a ∈ Γ and b ∈ Γ \ {b} Next, we define the heap encodings of those derivation trees that violate condition (I). To this end, we guess a vector b in {0, 1} N , encoding a position on the tape i ∈ 0 . . 2 N -1 , a shift µ ∈ {←, →}, encoded by µ ∈ {0, 1} and get the binary complement of the (encoding of the) position reached from b by applying µ. Here we distinguish two cases, depending on the choice of µ:

(a) if µ is → then bin(i) = b def = (b 1 , . . . , b n , 0, 1 N-1-n ) for some n ∈ 0 . . N -1 and let c def = (b 1 , . . . , b n , 0, 1 N-1-n ) be the complement of bin(i + 1) = (b 1 , . . . , b n , 1, 0 N-1-n ). (b) otherwise, bin(i) = b def = (b 1 , . . . , b n , 1, 0 N-1-n ) and let c def = (b 1 , . . . , b n , 1, 0 N-1-n ) be the complement of bin(i -1) = (b 1 , . . . , b n , 0, 1 N-1-n ).
For every n ∈ 0 . . N -1 and every m ∈ 0 . . B and i ∈ 1 . . m , we consider the rules: Then a path to the branching node, labeled (q , i ), that violates condition (I) is chosen, by alternating the branching and action nodes allocated by rules (11) and (13), respectively. The offending branching node is allocated by rule (15) and its predecessors are the branching and the action nodes, labeled with (q, i) and (i, a, b, µ), such that i i µ . These latter nodes are allocated by rules ( 12) and ( 14), respectively.

c 1 (x) ⇐ ∃b 1 . . .∃b n ∃y . x → ([y] N ) * d 1 (y, 1, b 1 . . . b n , 0, 1 N-n-1 b , b 1 . . . b n , 0, 1 N-n-1 c ) (9) c 1 (x) ⇐ ∃b 1 . . .∃b n ∃y . x → ([y] N ) * d 1 (y, 0, b 1 . . . b n , 1, 0 N-n-1 b , b 1 . . . b n , 1, 0 N-n-1 c ) (10) d 1 (x, u, b, c) ⇐ ∃y 1 . . . ∃y m .x → (• N , y 1 , . . . , y m ) * * j∈ 1. .m \{i} r(y j ) * d 1 (y i , u, b, c) (11)
The pseudo-derivations of M that violate condition (II) are encoded by the treestructured heaps defined by the rules below. To this end, we guess a binary vector b ∈ {0, 1} N denoting the position of a write action that has an inconsistent read descendant and let c be its binary complement. Then, for every m ∈ 0 . . B and i ∈ 1 . . m , we consider the rules below: Next, a path to a second branching node labeled by the binary position b is nondeterministically chosen by an alternation of branching and action nodes allocated by the the rules ( 21) and ( 23) respectively, while checking that no branching node with the same position b occurs on this second path (23). At the end, we reach the offending branching node (24), whose predecessor is allocated by rule (22). At this point, we check that the symbol read by the last action node is different than the symbol previously written at position b, by rule (19). This check is done by rules ( 24) and (25), thus ensuring that condition (II) is indeed violated. Next, we define the tree-structured heap encodings of the derivation trees that violate condition (III). To this end, we guess a binary vector b ∈ {0, 1} N denoting the position where a symbol different from b has been read, with no previous write action at that position and let c be its complement. We consider the rules below, for every m ∈ 0 . . B and i ∈ 1 . . m : After the initial guess of the binary position b, by rule (26), a path to a branching node labeled by b is nondeterministically guessed, by an alternation of branching and action nodes corresponding to the rules ( 27) and (28), respectively, while checking that no branching node labeled with position b occurs on this path. Once this node is reached, by rule (29), we check that its action node successor reads a symbol different than b, by rules (30) and (31), which is in violation of condition (III). Finally, the predicate c M (x) that choses the condition (I), (II) or (III) to be violated, is defined by the following rules: c M (x) ⇐ ∃y 0 ∃z 0 . x → (y 0 , z 0 ) * c i (y 0 ) * Const(z 0 ), for all i ∈ {1, 2, 3, }

Let S denote the set of rules introduced so far. The following lemma states the property of the models of c M (x):

Lemma 4. Given a pseudo-derivation t of M and a structure (s, h), such that (s, h) > t, we have (s, h) | = S c M (x) if and only if t is not a derivation of M.

d 1 (

 1 x, u, b, c) ⇐ ∃y 1 . . . ∃y m .x → (b, y 1 , . . . , y m ) * * j∈ 1. .m \{i} r(y j ) * e 1 (y i , u, b, c) (12)d 1 (x, u, b, c) ⇐ ∃y . x → (a, b, •, y) * d 1 (y, u, b, c), for each a ∈ Γ, b ∈ Γ \ {b} (13) e 1 (x, u, b, c) ⇐ ∃y . x → (a, b, •, y) * f 1 (y, u, b, c), for each a ∈ Γ, b ∈ Γ \ {b} (14) f 1 (x,u, b, c) ⇐ ∃y 1 . . . ∃y m . x → (e, y 1 , . . . , y m ) * m * j=1 r(y j ) | e c (15) Intuitively, rules (9) and (10) choose the move u ∈ {0, 1} and the binary vectors b, c ∈ {0, 1} N , according to the cases (a) and (b) above, respectively. Note that we use the hat [y] N to eliminate the binary variables b 1 , . . . , b n , as n ≤ N, according to the elimination procedure described in §3.1.

c 2 (

 2 x) ⇐ ∃b 1 . . . ∃b N ∃y . x → ([y] N ) * d 2 (y, b 1 , . . . , b N b , b 1 , . . . , b N c ) (16)d 2 (x, b, c) ⇐ ∃y 1 . . . ∃y m . x → (• N , y 1 , . . . , y m ) * * j∈ 1. .m \{i} r(y j ) * d 2 (y i , b, c)(17)d 2 (x, b, c) ⇐ ∃y . x → (a, b, •, y) * d 2 (y, b, c), for each a ∈ Γ, b ∈ Γ \ {b} (18) d 2 (x, b, c) ⇐ ∃y . x → (a, b, •, y) * e 2 (y, b, b, c), for each a ∈ Γ, b ∈ Γ \ {b} (19)

e 2 (

 2 x, γ, b, c) ⇐ ∃y 1 . . . ∃y m . x → (b, y 1 , . . . , y m ) * * j∈ 1. .m \{i} r(y j ) * e 2 (y i , γ, b, c) (20)e 2 (x, γ, b, c) ⇐ ∃y . x → (a, b, •, y) * f 2 (y, γ, b, c), for each a ∈ Γ, b ∈ Γ \ {b} (21) e 2 (x, γ, b, c) ⇐ ∃y . x → (a, b, •, y) * g 2 (y, γ, b, c), for each a ∈ Γ, b ∈ Γ \ {b} (22) f 2 (x, γ, b, c) ⇐ ∃y 1 . . . ∃y m . x → (e, y 1 , . . . , y m ) * * j∈ 1. .m \{i} r(y j ) * e 2 (y i , γ, b, c) | e c (23) g 2 (x, γ, b, c) ⇐ ∃y 1 . . . ∃y m . x → (b, y 1 , . . . , y m ) * * j∈ 1. .m \{i} r(y j ) * g 2 (y i , γ)(24)g 2 (x, γ) ⇐ ∃y . x → (a, b, •, y) * r(y), for each a ∈ Γ \ {γ}, b ∈ Γ \ {b} (25) Intuitively, rule (16) uses the hat [y] N to choose the tuple of binary variables b = (b 1 , . . . , b N ) and their complements c = (b 1 , . . . , b N ). First, the path to a branching node labeled by the binary position b is non-deterministically chosen by an alternation of branching and action nodes allocated by the the rules (17) and (18), respectively, until the node and its predecessor are allocated by rules (20) and (19), respectively. The symbol written on the tape by this node is stored in the second parameter of e 2 (x, γ, b, c).

c 3 (

 3 x) ⇐ ∃b 1 . . . ∃b N ∃y . x → ([y] N ) * d 3 (y, b 1 , . . . , b N b , b 1 , . . . , b N c )(26)d 3 (x, b, c) ⇐ ∃y 1 . . . ∃y m . x → (e, y 1 , . . . , y m ) * * j∈ 1. .m \{i} r(y j ) * d 3 (y i , b, c) | e c (27) d 3 (x, b, c) ⇐ ∃y . x → (a, b, •, y) * d 3 (y, b, c), for all a ∈ Γ, b ∈ Γ \ {b}(28)d 3 (x, b, c) ⇐ x → (a, b, •, y) * e 3 (y, b, c), for all a ∈ Γ, b ∈ Γ \ {b}(29)e 3 (x, b, c) ⇐ ∃y 1 . . . ∃y m . x → (b, y 1 , . . . , y m ) * * j∈ 1. .m \{i} r(y j ) * f 3 (y i ) (30) f 3 (x) ⇐ ∃y . x → (a, b, •, y) * r(y), for all a, b ∈ Γ \ {b} (31)

Entailment does not reduce to satisfiability since the considered logic has no negation.

In fact they are allocated by the side condition Const.

A machine never writes blank symbols, that are used only for the initially empty tape cells.

Every ATM can be complemented in linear time, by interchanging the existential with the universal states, thus all alternating classes are closed under complement.

Proof : (sketch) Fact 2 Assume that (s, h) | = S c M (x). For all , ∈ dom(h) and i, j ∈ 1 . . k , h( ) i = h( ) j iff either (i) = h( ) i , (ii) h( ) i ∈ s(Γ ∪ {0, 1}), or (iii) = and i = j.

Proof : By close analysis of allocation within the rules of S.

"⇒" If (s, h) | = S c M (x) then, by Lemma 1, there exists an unfolding tree u ∈ T S (c M (x)) such that (s, h) | = F (u). Since S is a progressing and connected set of rules and, moreover (s, h) | = F (u), by Lemma 2, there exists a bijection Λ : dom(h) → nodes(u)\{λ} such that, for all wi ∈ nodes(u), where i ∈ N, we have Λ -1 (wi) ∈ h(Λ -1 (w)). Moreover, since (s, h) > t, there exists an injective mapping f : nodes(t) → dom(h)\s(Γ ∪{0, 1}) such that, for all w ∈ nodes(t) such that wi ∈ nodes(t), we have f (wi) ∈ h( f (w)). Consequently, we obtain the bijection Λ • f : nodes(t) → nodes(u) \ {λ} where, for all wi ∈ nodes(t), such that i ∈ N, there exists j ∈ N such that f (wi) = h( f (w)) j . Since Λ is bijective and λ img(Λ), there exists a node vk ∈ nodes(u), for some k ∈ N, such that h( f (w)) j = Λ -1 (vk). By Lemma 2, there exists m ∈ N such that

Then we obtain that, for all wi ∈ nodes(t), such that i ∈ N, there exists k ∈ N, such that:

We can conclude that t and u |0 are isomorphic, i.e. nodes(t) = nodes(u) \ {λ}.

By the definition of S, namely rule (32), there exists a unique node w 0 ∈ nodes(u) \ {λ} such that u(w 0 ) = (c i , φ i ), for some formula φ i , where i ∈ {1, 2, 3}. Distinguishing the cases i = 1, 2, 3 and using the fact that (s, h) > t, one shows that t breaks the one of the conditions (I), (II) or (III), respectively, thus t is not a derivation of M. The proof is along the lines of the second point of Lemma 3. "⇐" If t is an accepting pseudo-derivation but not a derivation of M, then t violates one of the conditions (I), (II) or (III). In each case, we build an unfolding tree u ∈ T S (c M (x)), along the lines of the proof of the first point of Lemma 3. Using the fact that (s, h) > t, we show that (s, h) | = F (u), leading to (s, h) | = S c M (x).

Note that, akin to the rule for p M (x) (8), the rules (32) contain an occurrence of Const(z 0 ) as a sibling to a hat of height N, that occurs in c i (y 0 ), for all i = 1, 2, 3. Then the entailment p M (x) | = c M (x) holds if and only if, for each structure (s, h) such that (s, h) | = p M (x) and each extension s[y 0 ← 0 ], for some location 0 ∈ Loc, the heap h is matched by the unfolding of one of the rules with head c 1 (y 0 ), c 2 (y 0 ) or c 3 (y 0 ). This is possible because each such rule uses a hat [y] N , matching the one from the rule with head p M (x) (8). Proof : "⇒" Suppose, for a contradiction, that M accepts (q 0 , , 0). By Definition 6 it has a derivation t. Since t is a derivation, it is also a pseudo-derivation of M and, by Lemma 3, there exists a structure (s, h) such that (s, h) | = S p M (x) and (s, h) t. Moreover, (s, h) > t follows from (s, h) t and, by Lemma 4, we obtain (s, h) | = S c M (x), thus p M (x) | = S c M (x), contradiction.

"⇐" Suppose, for a contradiction, that p M (x) | = S c M (x), hence there exists a structure (s, h) such that (s, h) | = S p M (x) and (s, h) | = S c M (x). By Lemma 3, there exists a pseudoderivation t of M such that (s, h) t, hence (s, h) > t. By Lemma 4, t is a derivation of M, hence (M, ) has a positive answer, contradiction.

We state the main result of this paper below:

Theorem 2. The entailment problem p(x) | = S q(x), where S is a progressing, connected and established set of rules and p, q are predicate symbols in Pred that occur as heads in S, is 2EXPTIME-hard.

Proof : Given an exponential-space bounded ATM M we define a set of rules S, based on the description of M, such that p M (x) | = S c M (x) if and only if (M, ) has a negative answer (Lemma 5). Moreover, the set of rules is easy shown to be progressing, connected and established. The reduction is possible in time polynomial in the size of the standard encoding of M. Indeed, the number of rules in S is O(||Q|| • N • B) and the succint representation of each rule, using deep hats, binary choices and binary variables can be generated in time O(||Γ|| • B • N). Finally, the complete elimination of binary variables is possible in polynomial time. Since we reduce from the complement of a AEXPSPACEcomplete membership problem and co-AEXPSPACE=AEXPSPACE=2EXPTIME, we obtain the 2EXPTIME-hardness result.

Conclusions

We show that the entailment problem, for symbolic heaps with inductively defined predicates, showed to be decidable (with elementary recursive time complexity) in [START_REF] Iosif | The tree width of separation logic with recursive definitions[END_REF] has an actual 2EXPTIME-hard lower bound. In the light of the recent results of [START_REF] Katelaan | Effective entailment checking for separation logic with inductive definitions[END_REF], we expect 2EXPTIME to be the tight complexity for what is currently the most general decidable class of entailments for Separation Logic with inductive definitions.


Keywords: Paper for recycling, characterization, precision, neural network, Monte-carlo, Intelligence Artificial, Correlation, Exact caracterization procedure

Auf deutsch En Francais

Ce document récapitule les enjeux industriels de la caractérisation gravimétrique des mélanges papier graphique-carton ainsi que des méthodes statistiques et modèles probabilistes pour estimer la précision de ces méthodes. Dans la partie 1, apres un rappel de l'état de l'art, sont présentés différentes métriques de précisions de ces estimations de composition. Dans la partie 2 un modèle probabiliste original dans son application est proposé pour calculer ces métriques de manière efficace et une méthode et formule simplifié explique comment mettre en oeuvre cette technique. On propose une maniere fiable d'estimer les paramètres du modèle dans des cas réels avec des tests réalisés dans une usine. Dans la partie 3 sont présentés des méthodes non invasive basée sur de la reconnaissance d'image pour estimer les compositions des mélanges papier-carton. L'estimation de la précision de cette méthode sera réalisé ultérieurement.

L'intérêt du modèle est de permettre de tester les cas maximaux de correlations que l'on peut atteindre entre différentes méthodes de caractérisations. On met particulièrement en avant dans la formule 1 une mesure d'erreur entre la réalité des chargements et la mesure effectuée.

Precision of caracterization of paper for recycling

In English

This document discuss about industrial issues of gravimetric caracterisation of load of paper and board and presents statistical methods and probabilistic model to estimate the precision of these methods. In section 1, after a reminder of the state of the art, differents metrics of precision of estimation of the composition are presented. In section 2, an original model is proposed to compute the metrics efficiently and a simplified methods and formula explain how to use this technic. We propose an efficient way to estimate the parameters of the models with real case with data coming from a sorting plant. In section 3 are presented non invasive methods based on image recognition to estimate composition of load of paper for recycling. Estimation of the precision of this methods will be published lately.

The main idea of the proposed model is to test the maximum value of the correlation that we can achieved between two differents caracterization methods.

The main results is the formula 1 that links the error measured and the error of the methodology with the reality.

Thanks

I would like to thanks the many people that mades this study possible. Arnaud Dauxerre who brought us to the paper industry as long as all its colleague Thomas Krauthauf, Manfred Geistbeck, Marita Pertu, Jean Kubiak and Marc Thebaud still missing some. Employees at Fotonower Jingxuan Feng, Chengcheng Xu, Marine Colin and Stéphane Poirier worked on some aspect of the theoretical or numerical part. Former colleague that made part of the manual caracterization work, Nicolas Gueritat, Pia Chancerel and Romain Pagès. Jan Lemoux and Isabelle Margain enabled Fotonower to present its work to the paper industry.

1 Gravimetric characterisation : state of the art 1.1 Industrials issues, definition and main usage Quality of load of paper for recycling is a key issue in the paper industry. Therefore different characterisation methodology have been developed and their statistic studied.

Among them, gravimetric characterisation of a sample is widely used in the rubbish industry and seen as the best reference available.

We present here a short description based on the norm [START_REF]Déchets ménagers et assimilés -méthode de caractérisation -analyse sur produit brut[END_REF] and [START_REF]Déchets ménagers et assimilés -méthode de caractérisation -analyse sur produit sec[END_REF]. The loose is sampled either by a mechanical way of mixing it and putting a load of it in some recipient or by simply collecting manually inside the heap to avoid selecting (although unconsciously) visually the material to be caracterized as defined in INGEDE 14 described in [START_REF] Faul | Quality requirements in graphic paper recycling[END_REF].

Then, as stated in the norm, the different elements are separated and weighted. Weight proportion are then reported.

Ademe gathered gravimetric caracterization campaign in [START_REF] Follet | Actualisation du guide de mise en oeuvre d'une campagne locale de caractérisation des déchets ménagers et assimilés rapport intermédiaire : Analyse documentaire et état de l'art et analyse statistique[END_REF] and proposed methodology for caracterization and testing its accuracy in [START_REF] Louis-Rose | Guide pour la realisation de campagnes de caracterisation des dechets menagers : Conseils et methodes a destination des collectivites[END_REF].

These study are interested in the caracterization of final garbage. We observe that the caracterization is not perfect and mainly focus on flow of truck.

The norm [START_REF]Déchets ménagers et assimilés -constitution d'un échantillon ponctuel sur une benne de déchets ménagers et assimilés collectés sélectivement[END_REF] interests us specifically because it is for only one truck. The sub-sampling procedure is introduced in it, we discuss about it in section .

Source of errors and uncertainty

The error and uncertainty in the composition of the complete load of materials comes from several reasons :

• The amount of uncharacterized material called "fines" in french. Usually of the order of one percent of the characterized sample.

• Manual error in caracterization or incomplete caracterization of some type of material inconsistency with the norm [START_REF]Paper and board -european list of standard grades of paper and board for recycling[END_REF].

• Bias in the sample versus the complete load.

• Inhomogeneous sample due to incomplete mixing of the load.

• Small size of the samples/Size of each element of material.

The first error can be neglected based on the hypothesis that the "fine" have no bias with the rest of the sample. We can refer to [START_REF] Gottschling | Sampling of paper and board for recycling : model helps to determine suitable sample sizes[END_REF] to have some idea on the distribution of size of the different type of material (paper/board to start with).

The second one can also be taken into account the same way we manage error in automatic detection in section 3.3. We don't take it into account in the first version of "Effective Precision Methodology" presented in section 2.2.

The third one, the bias can also be studied once stated. This is done for example for surfacic scanning of material on conveyor which is for example ineffective to detect glass mixed with paper since almost all of it goes to the bottom of the conveyor.

The last two are the problem tackled in this study. The inhomogeneous sample is not an issue, our methodology apply only for same inhomogeneity of material. We do not introduce homogeneity measure that could explain how to compare two mixing procedure. Here are two example : Some usual sampling procedure

• For one load of a truck : X times using a mecanical loader to mix the material before selecting a sample.

• Picking manually a sample by gathering Y different sub-sample around the load by putting the hand inside the heap (to avoid a bias of manual selection).

Our calibration and precision methodology of the caracterization methods must be applied for one specific mixing and sampling methodology with fixed procedure.

The methodology proposed in 2 gives correlation of a complete caracterization of the load with the chosen caracterization procedure. Without using or (simple) formula it would be untractable either in production of for a test since it would require to characterized the whole load. The best that can be approached is a visual dynamic characterization procedure on top of a conveyor. This is not the subject of this study.

We propose in the next paragraph 1.3.1, 1.3.2 and 1.3.3 three different error metrics between two different caracterization methodology.

Several error metrics

These error metrics are here to estimate the difference between two caracterization methods of a set of load among for example : INGEDE 7 (visual), INGEDE 14 (weight), QUALIPAPIA (introduced in section 3) or any caracterization methods of bales (that are outside the scope of this study) or even the exact composition of a load. In some case, we can also consider two independent exectution of the same caracterisation methods. For INGEDE 7 visual, we can for example, without considering security issues, apply it to one side of the heap and the other side. It is of course easier to consider multiple INGEDE 14. The main results of this study is the relationship between the error metrics for different comparison presented in section 2.2.

An exact caracterization methods could be used by an industrialization of a tools as the one developped at Darmstad Technical University presented here [START_REF] Krebs | Ap messsystem -video presentation[END_REF].

We uses the variable defined in table 1 and introduce most of them when they are used in equation.

Confusion matrix

The most intuitive and business-oriented way of considering the precision of a caracterization method is the confusion matrix, either between the same methodology applied two times independently or between two different methodology.

The confusion matrix which on example can be found in figure 3.

In column are classes on a given measurement methods m and in rows the classes either exact (the complete load), or of a reference methods n.

This matrix as the property of having sum on column equal to one, or 100%, and in a cell of row m 0 and column n 0 : c m0,n0 , is the conditionnal expectancy of having the method m a result m 0 and a result n 0 .

c m0,n0 = E [p n U ∈ n 0 |p m U ∈ m 0 ]
Or in natural language, if the measurment method m gives a class m 0 , c m0,n0 is the probability that the methods n gives a class n 0 .

Correlation

We use the notation listed in table 1.

The correlation is simply :

ρ (i,j) E p (i) A p (j) A -E p (i) A E p (j) A E p (i) A p (i) A -E p (i) A E p (i) A E p (j) A p (j) A -E p (j) A E p (j) A
We usually display the data in a chart in figure 1.

Mean square error, absolute or relative

Mean square error or MSE can be better appreciated by taking its square root in order to have something homogeneous to the quantity studied and become the Square Root Mean Square Error or RMSE.

For the absolute error, we use :

E (i,j) A = p (i) A -p (j) A E E (i,j) A 2 -E E (i,j) A 2
And the relative error will be the same formula by taking :

R (i,j) A = p (i) A -p (j) A p (i) A 1.

Ideal load of mixed paper and board

The model presented in section 2.1 is based on a real physical case (totally intractable in an industrial process of transporting paper and board).

We consider an ideal case of load of mixed paper and board with the following properties :

• all in bullet

• bullet will either be full paper or full board

• bullets will have same size and weight

In this case the model proposed in section 2.1.1 is the exact representation of the reality.

Tractable methodology to estimate the precision of a gravimetric caracterisation method

This model enable to manipulate various data of caracterisation coming from sample of different way. By observing the simplest error metrics presented in section 1.3.3, we calibrate our model by MSE-matching, or maximizing the log-likelihood and then estimate the most business-oriented error metrics that are the confusion matrix.

A first order approximation, exact when the size of sample are the same for each caracterization is presented in the most simple way in section 2.2.

Theoretical settings

Pr. Shauble in [START_REF] Gottschling | Sampling of paper and board for recycling : model helps to determine suitable sample sizes[END_REF] studies statistically the size of different type of material in mixed paper and board. For a sake of simplicity and efficiency we uses a simpler model where all element have the same size. Our methodology can be expanded to multiple size or even continuous distribution of size nearer to the reality. Despite that fact we have the strong belief that this most simpler model is the best first order estimation of the precision of a caracterization procedure.

Implicit independent size Model

Having in mind the ideal load presented in section 1.4, we will calibrate the value of any risk metrics computed on multiple load as the one presented here : 1.3 into an implicit size of independent element of the material considered. This is totally equivalent to considering the intrisic standard deviation of the model or the correlation with the real proportion of unwanted material in the load in 1.3.3 but can in some way be more easy to understand since it can be linked to some physical ideal case described in section 1.4. These ideal case are not tractable in a production process of the industry but can be physically achieved.

As in the survey industry (without using quota methodology), we consider the choice of each asked individual as independent.

Comparison with smile modelling Extending this methodology to a model where the implicit size depends on the proportion of unwanted material is under this real probability the same idea that modelling smile under the risk neutral probability in financial industry.

In fact instead of maximizing the log-likelihood we could also find the same MSE as shown in section 2.1.4.

Binomial or gaussian and poisson approximation of the model

On considère N M C réalisations qui peuvent être : des fractions de balles, des chargements de camions ou des matieres passant sur un convoyeur pour un interval de temps court. Pour chacun de ces ensembles on considère qu'elles ont un taux P de contaminant ou de distribution de deux différentes types de matières et on effectue N N M C tirage de taille S pour chacune d'entre-elles. P et S peuvent être aléatoires avec par exemple une distribution uniforme.

Using Binomial law L'observation P O du taux de contaminant ou répartition des matières suit une loi binomiale de parametres p et S s .

Using CLT for gaussian approximation We will simply apply the Central Limit theorem or uses the known binomial law to find this implicit independent size and then uses it to compute others risk metrics.

Lorsque S tend vers l'infini, S s P O -P converge vers une loi gaussienne de parametre 0, P (1 -P )

On simule donc p O avec une réalisation gaussienne P, P (1 -P ) s S

Poisson approximation For small S a Poisson approximation might be more accurate.

Formula of the metrics in the implicit independent size model

We refer to the metrix defined in section 1.3 Proof are computed in annex 6.3.

Correlation Cor(p gravi , p quali ) =

1 1+ 1 N gravi ( 6 M -4) 1+ 1 N quali ( 6 M -4)

Confusion matrix

Mean square error, absolute or relative Monte-Carlo simulation of complex risk metrics For any risk metrics, it can be easier to implement a Monte-Carlo simulation methods, instead of computing exact or approximated formula of any quantity in the model. This has been done to produce the confusion matrix in the figure 3.

Estimation or calibration of the implicit independent size

The main idea of this study is to observe multiple sampling or sub-sampling in order to estimate the way paper and board are mixed and how a sample represent a complete load.

Proof are in annex 6.3

Regression or MSE-matching formula

The most intuitive way is analog to a regression of the size of the sample on the precision of the methods, and base on matching the mean square error in the model and in the observed data.

s * = S 0 i N M C (p i,0 -p i,1 ) 2 0 i N M C (p i,0 + p i,1 ) (2 -p i,0 -p i,1 )
We propose numerical test of the model in annex 6.4 to observe the convergence.

Correlation matching As shown in figure 4, we can simply calibrate the model by matching the correlation computed in the model presented in 2.1.3 and the correlation computed from the data, 2.2.2.

Log-likelihood Log-likelihood of a realization of a random variable is an additive amount that is simply the logarithm of the density of the realisation. When observing independent realization of the same random variable we can find its law.

When the gaussian approximation is valid, e.g for small value of independent size model, we use the notation listed in table 1 and the procedure of sub-sampling defined in section 2.2.1.

For a sub-sampling realization p O , with the notation of ?? using for the variance the notation

V = p (1 -p) s S
, the log-likelihood will be :

L = - (p o -p) 2 2V - 1 2 log (V ) - 1 2 log (2π)
The value of the parameter ŝ of the calibrated model is

ŝ = arg max s>0 E - (p o -p) 2 2V - 1 2 log (V ) - 1 2 log (2π)
This will be a double sum on all sample of a load on all sub-sample. This is broadly equivalent to having the same MSE since it is equivalent asymptotically. Since the optimized quantity is a convex function of s it can be optimized very easily.

Tractable methodology

Here start the main result of this study.

Sub-sampling or multiple sampling procedure

We refer to the sub-sampling defined in [START_REF]Déchets ménagers et assimilés -constitution d'un échantillon ponctuel sur une benne de déchets ménagers et assimilés collectés sélectivement[END_REF] or remained in section 1.1. Sub-sampling means, having selected a sample, to split it in different sub-sample, this is what has been done to gather the data presented in section 2.3.

The multiple sampling procedure can imply bias since it is not always possible to keep the same procedure, for example when it is destructive as for a bale, or if a mixing process by a bulldozer change the homogenousity of the heap.

Whereas in the sub-sampling procedure, mixing the sample is required and more homogenous it is before sub-sampling, the better it is.

Computation of the correlation

For a bi-sampling procedure, sub-sampling with only two subsample, the formula to compute the correlation of the two independent measure of the same heap are the following. As listed in table 2, we note these estimators p i = p g i (P ) and p = p g i (P ), for several (i N ) different heap or load.

ρ g,g = 1/N p i p i -1/N p i 1/N p i 1/N p 2 i -(1/N p i ) 2 1/N p 2 i -(1/N p i ) 2 2.

Correlation between the real proportion of the heap and the measure

Then the correlation of this sampling procedure with the real proportion p is :

ρ g,p = ρ g,g (1)
And the more general equation for different methodology is :

ρ g,i = ρ g,p ρ p,i (2)
A proof can be found in annex 6.5.

Efficient formula for the confusion matrix

For the sake of simplicity we will not derive here the formula linking the correlation between two measure with the confusion matrix but will only says that it is linked to the gaussian copula.

Numerical Example

We made a practical study on the mixed paper and board coming out from a sorting plant during summer 2019.

Description of the data

The data are 80 caracterizations of bales with 20 classes computed. For three of the classes a sub-sampling procedure of usually 4 differents sub-sample were done.

Statistical calibration of the model

In our case we found that the implicit independent size was 0.16Kg as shown in figure 2.

3 Neural network and image recognition for non invasive caracterisation of loose

Neural network

Neural network are object invented around year 1950' which after long years of gestation have find real application during the year 2010' thanks the cheap computing power of Graphical Processor Unit (GPU) and the large amount of data among them photos made available on the internet thanks ADSL during the year 2000' and smartphone and 3G/4G in the following decade.

Qualipapia

Qualipapia ia a recent developement of a technology to compute caracterization of load of paper for recycling thanks photo of the surface of an heap of loose paper.

Debiasing detection errors

As every machine learning methodology, it contains some errors. First order error or false positive, when we believe having found something but which is wrong. And second order error or false negative of tracked element that we have missed.

Thus. in the same spirit of the computation debiaising of counting Varroa, bee mites thanks deep learning presented in the internal report of Fotonower [START_REF] Xu | Comptage de varroas[END_REF], we propose here to unbiased the surfacic detection of unwanted material.

Notation

We consider a classification or detection of Paper/Unwanted:

• P p is the precision of paper • R p is the recall of paper • P N P is the precision of unwanted material • R N P is the recall of unwanted material

• N P T is the exact number of paper element (or square centimeter)

• N P D is the number of detected paper

• N P DP is the number of paper detected as paper

• N N P T is the exact number of unwanted element

• N N P D is the number of unwanted detected as unwanted

• N N P DN P is the number of unwanted • E r is the real proportion of unwanted material • E m is the measured proportion of unwanted material • E dbm is the unbiased proportion of unwanted material • C is a constante C = P N P * R P P P * R N P
Unbiasing formula

E dbm = C * E m (1 -E m ) + C * E m
A demonstration can be found in section 6.6.

Precision of this method

Precision-recall graph are the main tools to estimate the quality of a neural network detection method.

We provide confusion matrix in some case in figure 3.

From surfacic to weight characterization

Since it is based on private data, the transformation from surfacic to weight caracterization and detection is not in the scope of this study, but it can be achived quite straightforwardly in a caracterization campaign or based on theoretical density of material.

Conclusion

We have proposed in this study an original model to compute precision metrics of caracterization methods for one single load. This is mainly based on estimation of correlation of double sampling procedure.

A simple formula has been proposed to link the correlation for different comparison of methodology. Business-wised metrics as confusion between the quality of a load and the real quality of loads are then proposed to be computed in simple way.

Definition of variable

Definition of notation and their translation can be found in table 2.

2: Definition of variable Proof E(p) = M/2 V ar(p) = M 2 /12 E(p 2 ) = V ar(p) + (E(p)) 2 = M 2 /3 E(p I ) = E(E(p I |p)) = E(p) = M/2 V ar(p I ) = E(p 2 I ) -(E(p I )) 2 = E(E(p 2 I |p)) -(E(p)) 2 E(E(p 2 I |p)) = E(V ar(p I |p) + (E(p I |p)) 2 ) = E( p(1-p) N + p 2 ) On a donc: V ar(p I ) = E( p(1-p) N + p 2 ) -(E(p)) 2 = E(p-p 2 ) N + V ar(p) = M/2-M 2 /3 N + M 2 /12 E(p I p) = E(E(p I p|p)) = E(pE(p I |p)) = E(p 2 ) = M 2 /3 Cov(p, p I ) = E(p I p) -E(p)E(p I ) = M 2 /12 Cor(p, p I ) = Cov(p, p I )/ V ar(p)V ar(p I ) = 1 √ 1+ 1 N ( 6 M -4)
Avec la même méthode de calcul, on peut avoir aussi la corrélation de p gravi et p quali : (p i,j , S i,j ) 0 j N M Ci,0 i N M C Thanks the Central Limit Theorem, we approximate the law of each sub-sample conditionnal to the sample with a gaussian using p o i = 0 j N M Ci p i,j S i,j 0 j N M Ci S i,j

Cor(p gravi , p quali ) = 1 1+ 1 N gravi ( 6 M -4) 1+ 1 N quali ( 6 M -4)
p i,j ∼ N p o i , p o i (1 -p o i ) s S i,j
where s is the implicit independent size. The empirical (observed) variance of sub-sample of a same sample are :

0 j N M Ci p 2 i,j -(p o i )
2 Therefore the estimator s * of the implicit independent size that matchs the variance of the model and the empiric over all the sample follow the equation :

0 i N M C 1 N M C i 0 j N M Ci p 2 i,j -(p o i ) 2 = 0 i N M C p o i (1 -p o i ) s * S i,j s * = 0 i N M C 1 N M C i 0 j N M Ci p 2 i,j -(p o i ) 2 0 i N M C p o i (1 -p o i ) S i,j
In the simple case where all sub-sample have same size S and where N M C i = 2 it simplifies to : 6.5 Proof of the formula linking the correlation between two measure and between the measure and the reality . We prove here the main equation 1 of this study from section 6.5

s * = 0 i N M C p 2 i,0 + p 2 i,1 -2 (p o i ) 2 2 0 i N M C p o i (1 -p o i ) S = S 0 i N M C 2p 2 i,0 + 2p 2 i,
We consider the real proportion of a load being a random variable P , we consider two random variable Q and G conditional representing two independent measure, eventually with the same methods. We suppose independence and that the measure are not biaised :

• Q|P P , G|P P and Q|P G|P

Nous considérons C = P N P * R P P P * R N P une constante quand précision et rappel sont fixés, par [START_REF] Follet | Actualisation du guide de mise en oeuvre d'une campagne locale de caractérisation des déchets ménagers et assimilés rapport intermédiaire : Analyse documentaire et état de l'art et analyse statistique[END_REF], nous avons:

N N P D N P D = E m 1 -E m (10)
Alors, par ( 9) et [START_REF] Gottschling | Sampling of paper and board for recycling : model helps to determine suitable sample sizes[END_REF]:

N N P T N P T = C * E m 1 -E m
Alors par ( 5):

E r = C * Em 1-Em 1 + C * Em 1-Em E r = C * E m (1 -E m ) + C * E m Donc: E dbm = C * E m (1 -E m ) + C * E m

Figure 1 :

 1 Figure 1: Correlation graph

Figure 2 :

 2 Figure 2: Maximising log-likelihood

Figure 3 :

 3 Figure 3: Confusion matrix thanks unbiasing

6. 3 )•s 3 R 3 E

 333 Proof of the law of the metrics in the independent implicit size model Correlation Proof of formula given in 2.1.3. Hypothesis On suppose que: • La taille implicite s soit 200g • Le taux p suit une loi uniforme U(0, 0.1) • La taille de tirage S g soit 40kg par la méthode Gravimetric, d'où le nombre d'objets N gravi est 40kg 200g = 200 • La taille de tirage S q soit 100kg pour le projet Qualipapia, d'où le nombre d'objets N quali est 100kg 200g = 500 • Le tas pèse 20 tonnes • Le taux de erreur réelle p suit une loi uniforme U(0, M )(M < 1) • Le taux de erreur observée p I , p I |p suit une loi normal N (p, p(1-p) N Les deux méthodes (Gravimetric/Qualipapia) sont indépendantes pour un même tas, c'est à dire pour un p fixé, p gravi |p et p quali |p sont indépendants. Implicit size of independent element of a load Kg N M C i, Number of sub-sample for sample i No dimension S i,j Size of a sub-sample j of sample i Kg Precision of a detection method, proportion of the element correctly detected among the element detected.Recall of a detection method, proportion of element detected among all the element to detect.Expectancy against a probability of observed event or in a probabilistic model No Dimension

Table

Figure

  Figure La corrélation est une fonction croissante en N (nombre d'objets), on peut tracer la fonction pour le maximum du taux 10% dans le modele, c'est représenté sur la figure 4.

Figure 4 :

 4 Figure 4: Correlation pour M = 10%

  For the MSEWe observe N M C realizations of sample with N M C i realization of sub-sample for each sample i N M C of size and percentage :

1 - 2 0 2 0 1 ) 6 . 4

 122164 (p i,0 + p i,1 ) i N M C (p i,0 + p i,1 ) (2 -p i,0 -p i,1 ) = S 0 i N M C (p i,0 -p i,1 ) i N M C (p i,0 + p i,1 ) (2 -p i,0 -p i,Numerical validation of the asymptotic convergence of log-likelihood and MSE-matching TODO Simulated data Observed data

•

  E[Q|P ] = P and E [G|P ] = P First we have :V ar [Q] = E [V ar [Q|P ]] =W P + V ar [P ] =V P and Covar [G, Q] = V ar [P ]andCovar [G, P ] = V ar [P ] Then Corr [G, P ] = V P (V P ) (V P + W G )Nous pouvons calculer par (7) et (8): N P T = P P * N P D R P N N P T = P N P * N N P D R N P N N P T N P T = P N P * R P P P * R N P * N N P D N P D

  Gilles Pagès * -Victor Reutenauer † Industrials issues, definition and main usage . . . . . . . . . . . . . . . . . . . . . . . . 1.2 Source of errors and uncertainty . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.3 Several error metrics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.3.1 Confusion matrix . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.3.2 Correlation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.3.3 Mean square error, absolute or relative . . . . . . . . . . . . . . . . . . . . . . . 1.4 Ideal load of mixed paper and board . .. . . . . . . . . . . . . . . . . . . . . . . . . . Tractable methodology . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Numerical Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Lexic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6.2 Definition of variable . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6.3 Proof of the law of the metrics in the independent implicit size model . . . . . . . . .

	Novembre 2019
	Contents
	1 Gravimetric characterisation : state of the art
	1.1 4 Conclusion
	5 Bibliography
	6 Annex
	6.1

2 Tractable methodology to estimate the precision of a gravimetric caracterisation method 2.1 Theoretical settings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.1.1 Implicit independent size Model . . . . . . . . . . . . . . . . . . . . . . . . . . 2.1.2 Binomial or gaussian and poisson approximation of the model . . . . . . . . . . 2.1.3 Formula of the metrics in the implicit independent size model . . . . . . . . . . 2.1.4 Estimation or calibration of the implicit independent size . . . . . . . . . . . . 2.2 2.2.1 Sub-sampling or multiple sampling procedure . . . . . . . . . . . . . . . . . . . 2.2.2 Computation of the correlation . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.2.3 Correlation between the real proportion of the heap and the measure . . . . . . 2.2.4 Efficient formula for the confusion matrix . . . . . . . . . . . . . . . . . . . . . 2.3 2.3.1 Description of the data . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.3.2 Statistical calibration of the model . . . . . . . . . . . . . . . . . . . . . . . . . 3 Neural network and image recognition for non invasive caracterisation of loose 3.1 Neural network . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.2 Qualipapia . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.3 Debiasing detection errors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.4 Precision of this method . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.5 From surfacic to weight characterization . . . . . . . . . . . . . . . . . . . . . . . . . . 6.4 Numerical validation of the asymptotic convergence of log-likelihood and MSE-matching 6.5 Proof of the formula linking the correlation between two measure and between the measure and the reality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6.6 Proof of the unbiasing formula of surfacic detection . . . . . . . . . . . . . . . . . . . .

Table 1 :

 1 Definition of terminology

	Lexic	Definition	Traduction	Übersetzung
	Load	Complete load of opened bales or truck	Chargement	Laden
		of loose material or specific amount of
		material on a conveyor for a fixed time
		or amount
	Sample	Part of a load that should be selected	Echantillon	Probe
		through a specific methods as the one
		listed in 1.2
	Caracterization	Process to identify manually or with a	Procédure de	Charakterisierung
	procedure	specified method all the element of a	caracterization	Prozess
		sample.
	Calibration of	Way to estimate the precision of a char-	Calibration de	Kalibrierung
	the precision	acterisation procedure of a sample of a	la	précision	der
	of the car-	load by having multiple sample of the	d'une méthode	Genauigkeit
	acterization	same load, goal of this study.	de	car-	eines Charak-
	procedure.		actérisation.	terisierung
					Prozess
	6 Annex
	6.1 Lexic
	Lexic can be found in table 1.

which proves the results.

Proof of the unbiasing formula of surfacic detection

Proof of formula found in 3.3.

• P p is the precision of paper • R p is the recall of paper • P N P is the precision of unwanted material

• R N P is the recall of unwanted material

• N P T is the exact number of paper element (or square centimeter)

• N P D is the number of detected paper

Par la définition de Rappel:

Par la définition de Pourcentage non-papier: