Dominique Larchey-Wendling

Didier Galmiche
email: galmiche@loria.fr

The Undecidability of Boolean BI through Phase Semantics (full version)

We solve the open problem of the decidability of Boolean BI logic (BBI), which can be considered as the core of separation and spatial logics. For this, we define a complete phase semantics for BBI and characterize it as trivial phase semantics. We deduce an embedding between trivial phase semantics for intuitionistic linear logic (ILL) and Kripke semantics for BBI. We single out a fragment of ILL which is both undecidable and complete for trivial phase semantics. Therefore, we obtain the undecidability of BBI.

Introduction

The logic of Bunched Implications (denoted BI) of Pym and O'Hearn [START_REF] O'hearn | The logic of bunched implications[END_REF] is a well-known sub-structural logic which freely combines additive connectives ∧, ∨, → and multiplicative connectives * , - * . The additives of BI behave either intuitionistically or classically giving rise to intuitionistic BI or Boolean BI (denoted BBI). The language of BI, and in particular its composition operators * and - * , is at the heart of separation and spatial logics frameworks (see [START_REF] Larchey-Wendling | Exploring the relation between Intui. BI and Boolean BI: an unexpected embedding[END_REF] for a discussion on these aspects).

It is striking that the proof-theoretical developments on BI have so far focused mainly on (intuitionistic) BI, especially since the numerous program verification applications of BI -notably separation logic [START_REF] Ishtiaq | BI as an Assertion Language for Mutable Data Structures[END_REF] or spatial logic [START_REF] Calcagno | Deciding Validity in a Spatial Logic for Trees[END_REF] -are mainly based on its Boolean variant. Intuitionistic BI has been given a well-behaved proof theory [START_REF] Pym | The Semantics and Proof Theory of the Logic of Bunched Implications[END_REF] composed of a bunched sequent calculus enjoying cut-elimination since its inception. Later, Galmiche et al. [START_REF] Galmiche | The semantics of BI and resource tableaux[END_REF] gave BI a labelled tableaux system from which decidability was derived. On the contrary, the proof theory of BBI was reduced to the addition of a double negation principle to that of (intuitionistic) BI, as Pym did in [START_REF] Pym | The Semantics and Proof Theory of the Logic of Bunched Implications[END_REF]. For long, the main prooftheoretical result was the completeness of the corresponding Hilbert style system [START_REF] Galmiche | Expressivity properties of Boolean BI through relational models[END_REF] and not much more. It was even unknown whether the relational Kripke semantics (corresponding to the Hilbert system) and the partial monoidal Kripke semantics (corresponding to the labelled tableaux system) define the same notion of validity.

This situation evolved recently with two main families of results. On the one hand, in the spirit of his work with Calcagno on Classical BI [START_REF] Brotherston | Classical BI: a logic for reasoning about dualising resources[END_REF], Brotherston provided a Display Logic style proof system for relational BBI and derived a cut-elimination result from this Display framework [START_REF] Brotherston | A cut free proof theory for Boolean BI[END_REF]. He then tried to obtain decidability with syntactic techniques similar to those Restall successfully used in relevant logics [START_REF] Restall | Displaying and Deciding Substructural Logics 1: Logics with Contraposition[END_REF]. But for some fundamental logical reasons explained in this paper, his attempt was bound to fail. On the other hand, the authors recently obtained a sound and faithful embedding of BI into BBI (both defined with their partial deterministic Kripke semantics), illustrating the counter-intuitive fact that Boolean BI is surprisingly more expressive than intuitionistic BI [START_REF] Larchey-Wendling | Exploring the relation between Intui. BI and Boolean BI: an unexpected embedding[END_REF]. The result is based on the study of the specific properties of the counter-models generated by proof-search in labelled tableaux systems.

Many questions remained open in relation to the proof theory and semantics of BBI. In particular:

1. Do the relational and the partial deterministic Kripke semantics define the same set of valid formulae?

2. Is validity decidable in either of these semantics?

In this paper we solve both questions and give them a negative answer. Indeed, we first show that the notion of invertibility, definable by the BBI formula I = ¬(⊤ - * ¬I), is not stable by composition in relational Kripke semantics whereas it is in partial deterministic Kripke semantics. Hence the formula (I * I) → I distinguishes these two semantics. Then, we prove the main contribution of this paper which is the undecidability of (universal) validity in BBI, be it relational BBI, partial deterministic BBI or even total deterministic BBI.

We begin by exploring the relation between phase semantics and Kripke semantics in the context of BBI. Compared to the phase semantics of ILL, we characterize the phase semantics of BBI as trivial because it corresponds to the choice of the least stable closure: the identity closure.

We point out the direct correspondence between Kripke semantics and trivial phase semantics. From this correspondence, we derive a map from ILL sequents to BBI formulae that is a sound and faithful embedding, as soon as validity in ILL is defined by trivial phase semantics.

On the one hand, it could appear at first that we have only displaced the problem from the language of BBI to the language of ILL. On the other hand, the undecidability of various fragments of ILL is already known, but of course, not with validity defined by trivial phase semantics. It turns out we have changed the question: instead of searching for an undecidable fragment, we have to identify, among the known existing undecidable fragments of ILL, one which is at the same time complete for trivial phase semantics.

This fragment of ILL must include the bang ! connective because IMALL is decidable [START_REF] Lafont | The finite model property for various fragments of linear logic[END_REF][START_REF] Lincoln | Decision problems for propositional linear logic[END_REF]. As in phase semantics the definition of & and ⊸ does not rely on the closure (as opposed to and ), a naive idea would be to keep only those connectives in the desired fragment. If we consider the first fragments of linear logic that were proved undecidable like full propositional linear logic [START_REF] Lincoln | Decision problems for propositional linear logic[END_REF] or the (!, )-Horn fragment [START_REF] Kanovich | The direct simulation of Minsky machines in linear logic[END_REF], we observe that, unfortunately, they include both and . Recently, a fragment of IMELL denoted s-IMELL ⊸ 0 has been studied and characterized as equi-decidable to IMELL [START_REF] De Groote | Vector addition tree automata[END_REF]. This fragment is important to us because it contains neither nor and it is very simple. However, decidability for IMELL is still an open question.

It turns out that s-IMELL ⊸ 0 is indeed complete for trivial phase semantics. We extend its goal-directed proof system [START_REF] De Groote | Vector addition tree automata[END_REF] with the addition of the & connective, in the spirit of Kanovich's [START_REF] Kanovich | The direct simulation of Minsky machines in linear logic[END_REF] and Lafont's [START_REF] Lafont | The undecidability of second order linear logic without exponentials[END_REF] ideas for encoding Minsky machines in linear logic. The fragment obtained, denoted ILL 0 ⊸,&,! , is sufficient to encode Minsky machines computations, because the & connective can be used to simulate forking. We show that, as with s-IMELL ⊸ 0 , ILL 0 ⊸,&,! is still complete for trivial phase semantics.

Non-Deterministic Monoids, ILL and BBI

In this section, we define BBI and its non-deterministic (or relational) Kripke semantics, ILL and its non-deterministic phase semantics and establish a semantic link between those two logics: trivial phase semantics.

Non-Deterministic Monoids

Let us consider a set M . We denote by P(M ) the powerset of M , i.e., its set of subsets. A binary function 1The extension of • to P(M ) thus induces a commutative monoidal structure with unit element {ǫ} on P(M ).

• : M × M -→ P(M ) is naturally extended to a binary operator on P(M ) by X • Y = {x • y | x ∈ X, y ∈ Y }
. ∀a ∈ M, ǫ • a = {a} (neutrality) 2. ∀a, b ∈ M, a • b = b • a (commutativity) 3. ∀a, b, c ∈ M, a • (b • c) = (a • b) • c (associativity)
The term non-deterministic was introduced in [START_REF] Galmiche | Expressivity properties of Boolean BI through relational models[END_REF] in order to emphasize the fact that the composition a • b may yield not only one but an arbitrary number of results including the possible incompatibility of a and b in which case

a • b = ∅. If (M,
•, e) is a (usual) commutative monoid then, defining a•b = {a•b} and ǫ = e induces a non-deterministic monoid (M, •, ǫ). Using the bijection x → {x} mapping elements of M to singletons in P(M ), we can view (usual) commutative monoids as a particular case of non-deterministic monoids (later called total deterministic monoids). Partial monoids can also be represented using the empty set ∅ as the result of undefined compositions.

The term relational is sometimes used because the map • : M × M -→ P(M ) can equivalently be understood as a ternary relation -• -∋ -: M × M × M -→ {0, 1} through the Curry-Howard isomorphism and the axioms correspond to those of an internal monoid in the category of relations [START_REF] Ghilardi | Modal logics with n-ary connectives[END_REF]. The two presentations are equivalent but we rather use the monoidal presentation in this paper because of the context of Kripke and phase semantics. Definition 2.2. Let us consider a non-deterministic monoid (M, •, ǫ). It is a partial deterministic monoid if for all x, y ∈ M , the composition x • y is either empty or a singleton. It is a total deterministic monoid if for all x, y ∈ M , the composition x • y is a singleton. The class of nondeterministic (resp. partial deterministic, resp. total deterministic) monoids is denoted ND (resp. PD, resp. TD).

The reader may have noticed that total deterministic monoids (of class TD) exactly correspond to those nondeterministic monoids derived from usual commutative monoids because the composition • is a functional relation (exactly one image for each pair of parameters). Obviously, there is also a strict inclusion between those classes of monoids.

Proposition 2.3. TD PD ND

We now exploit the notion of non-deterministic monoid to establish links between the semantics of BBI and ILL.

Kripke Semantics for BBI

The syntax of BBI is exactly the syntax of BI augmented with negation, although negation could be defined by ¬A = A → ⊥ like in classical logic. Thus, the formulae of BBI are defined as follows: starting from a set Var, they are freely built using the logical variables in Var, the logical constants in {I, ⊤, ⊥}, the unary connective ¬ or the binary connectives in { * , - * , ∧, ∨, →}. Formally, the set of formulae is described by the following grammar:

A ::= v | c | ¬A | A A with v ∈ Var, c ∈ {I, ⊤, ⊥} and ∈ { * , - * , ∧, ∨, →}.
Validity in BBI has not always been unequivocally defined. Indeed, the initial proposition of Pym [START_REF] Pym | The Semantics and Proof Theory of the Logic of Bunched Implications[END_REF] was simply to add a double negation principle to the cut-free bunched proof system of BI. But of course, this does not lead to a proof-theoretically well-behaved proof-system for BBI: it does not enjoy cut-elimination, sub-formula property, etc. Then, the syntax of BBI has been used as a foundation for various forms of separation logic with the common property that the additive operator → is interpreted classically whereas it is interpreted intuitionistically in BI. The removal of the pre-order in the Kripke semantics is moreover necessary for the interpretation of classical negation ¬.

In this paper, we choose to present BBI as a family of logics defined by their Kripke semantics rather than proofsystems. Given a non-deterministic monoid (M, •, ǫ) and an interpretation δ : Var -→ P(M) of propositional variables, we define the Kripke forcing relation by induction on the structure of formulae: In some papers, you might find BBI defined by nondeterministic monoidal Kripke semantics [START_REF] Brotherston | A cut free proof theory for Boolean BI[END_REF][START_REF] Galmiche | Expressivity properties of Boolean BI through relational models[END_REF], in other papers it is defined by partial but deterministic monoidal Kripke semantics and generally separation logic models are particular instances of partial (deterministic) monoids. See [START_REF] Larchey-Wendling | Exploring the relation between Intui. BI and Boolean BI: an unexpected embedding[END_REF] for a general discussion about these issues. Definition 2.4. We denote by BBI ND (resp. BBI PD , resp. BBI TD ) the set of formulae of BBI which are valid in every monoid of the class ND (resp. PD, resp. TD).

m v iff m ∈ δ(v) m ⊥ iff never m ¬A iff m A m ⊤ iff always m I iff m = ǫ m A ∧ B iff m A and m B m A ∨ B iff m A or m B m A → B iff m A or m B m A * B iff
On the proof-theoretic side, we briefly recall that BBI ND has been proved sound and complete w.r.t. a Hilbert proofsystem [START_REF] Galmiche | Expressivity properties of Boolean BI through relational models[END_REF] and also, more recently w.r.t. a Display Logic based proof-system [START_REF] Brotherston | A cut free proof theory for Boolean BI[END_REF] enjoying cut-elimination. BBI PD can be proved sound and complete w.r.t. the semantic constraints based tableaux proof-system presented in [START_REF] Larchey-Wendling | Exploring the relation between Intui. BI and Boolean BI: an unexpected embedding[END_REF] (although only the soundness proof is presented in that particular paper) and the adaptation of this tableaux system to BBI TD should be straightforward (contrary to BBI ND ).

As it turns out, the three different classes of models ND, PD and TD define three different logics, i.e., universally valid formulae differ from one class of models to another. The relation of strict inclusion between BBI ND and BBI PD was, to our knowledge, an undecided proposition.

Theorem 2.5. BBI ND BBI PD BBI TD Proof. The following inclusion relations TD ⊆ PD ⊆ ND hold between the classes of models which respectively define those three logics. Hence, only the strictness of the inclusion of validities is not obvious. This strictness is established by upcoming Theorem 2.6 and Proposition 2.7.

Consider the formula I = ¬(⊤ - * ¬I) and a non-deterministic monoid (M, •, ǫ). Since I does not contain any variable, its Kripke interpretation does not depend on the choice of δ. One can check that for any x ∈ M , x

I iff there exists x ′ ∈ M s.t. ǫ ∈ x • x ′ . So I expresses "invertibility" in
′ , c ′ ∈ M such that ǫ ∈ b • b ′ and ǫ ∈ c • c ′ . As • is (par- tial) deterministic, we have b • b ′ = {ǫ}, c • c ′ = {ǫ} and b•c = {a}. Thus we have (b•b ′ )•(c•c ′ ) = {ǫ}•{ǫ} = {ǫ}. If b ′ • c ′ = ∅ then we would have (b • c) • (b ′ • c ′ ) = {a} • ∅ = ∅ but also (b • b ′ ) • (c • c ′ ) = {ǫ} and thus ∅ = {ǫ} by associativity/commutativity, which is absurd. Thus b ′ • c ′ = {a ′ } and we obtain (b • c) • (b ′ • c ′ ) = {a} • {a ′ } = a • a ′ and then a • a ′ = {ǫ} by associativity/commutativity. Hence, ǫ ∈ a • a ′ and a I.
The formula (¬I - * ⊥) → I is inspired from the example given to establish the incompleteness of (total) monoidal Kripke semantics w.r.t. (intuitionistic) BI (see [START_REF] Pym | The Semantics and Proof Theory of the Logic of Bunched Implications[END_REF] page 63).

Proposition 2.7. The formula (¬I- * ⊥)→I is valid in every total deterministic monoid. There exists a partial deterministic monoid which is a counter-model to (¬I - * ⊥) → I.

The proof can be found in [START_REF] Larchey-Wendling | The Undecidability of Boolean BI through Phase Semantics[END_REF] (Appendix A). Having defined the Kripke semantics of BBI within the framework of non-deterministic monoids, let us consider nondeterministic phase semantics for ILL.

Non-Deterministic Phase Spaces for ILL

The formulae of ILL are defined by the following grammar:

A ::= v | c | ! A | A A with v ∈ Var, c ∈ {1, ⊤, ⊥} 2 and ∈ { , ⊸, &, }. A sequent is a pair denoted Γ ⊢ A
where Γ is a multiset of formulae and A is a single formula. The sequent calculus Sill (see Figure 1) is provided for ILL and the set of derivable sequents is the least set closed under its rules. Notice that Γ, ∆ denote multisets of formulae and A, B, C denote formulae.

In rule ! R , ! Γ denotes the multiset ! Γ = ! A 1 , . . . , ! A k if Γ = A 1 , . . . , A k .
The notion of sequent calculus proof is defined as usual: an ordered tree where each node together with its sons correspond to an instance of one of the rules of Sill. Hence, a sequent is derivable if and only if there exists a proof of it in Sill. By historical definition of ILL [START_REF] Girard | Linear logic[END_REF], the sequents which are provable in Sill are exactly the valid sequents of ILL, and a formula A of ILL is valid if ⊢ A is a valid sequent.

We extend the notion of intuitionistic phase space [START_REF] Girard | Linear logic[END_REF] to non-deterministic monoids and show that this semantic interpretation is sound and complete w.r.t. Sill, and thus equivalent to the original notion (see Corollary 2.12). Definition 2.8. A non-deterministic (intuitionistic) phase space is given by a non-deterministic monoid (M, •, ǫ) = M together with a stable closure operator (•)

⋄ : P(M )-→ P(M ) and a sub-monoid K included in J = {x ∈ M | x ∈ {ǫ} ⋄ ∩ (x • x) ⋄ }.
The closure property corresponds to the condition X ⊆ Y ⋄ iff X ⋄ ⊆ Y ⋄ for any X, Y ∈ P(M ). We recall that the monoidal composition • is naturally extended to P(M ) by

X • Y = {x • y | x ∈ X, y ∈ Y } providing a (commuta- tive) monoidal structure on P(M ) with unit {ǫ}.
The stability property3 corresponds to the condition

X ⋄ • Y ⋄ ⊆ (X • Y ) ⋄ for any X, Y ∈ P(M ). A subset X of M is (•) ⋄ -closed (or simply closed when the closure is obvious from the context) if X ⋄ = X or equivalently X ⋄ ⊆ X.
The set of closed subsets is denoted M ⋄ = {X ∈ P(M ) | X ⋄ = X}, not to be confused with M ⋄ where M is viewed as the (total) subset of M (and in this case, M ⋄ = M ). Any intersection of closed subsets is a closed subset and thus M ⋄ is invariant under arbitrary intersections, inducing a complete lattice structure on (M ⋄ , ⊆).

The set K is just a sub-monoid of M included in J, i.e., K verifies ǫ ∈ K ⊆ J and K • K ⊆ K. Let --• be the binary operator on P(M ) defined by X --• Y = {k ∈ M | k • X ⊆ Y }.
In the lattice (P(M ), ⊆), the operator --• is contra-variant in its first parameter and co-variant in its second and

K ⊆ X --• Y iff K • X ⊆ Y for any K, X, Y ∈ P(M ). By stability of the closure operator (•) ⋄ , the subset X --• Y is closed as soon as Y is closed and X --• Y ⋄ = X ⋄ --• Y ⋄ for any X, Y ∈ P(M ).
We see that we have a (quite direct) generalization of the usual notion of phase space in the case where the monoid is neither supposed to be total nor deterministic. In the particular case of total deterministic monoids, we recover the usual notion of phase space.

The interpretation of ILL connectives is done in the following way. Given an interpretation [[•]] : Var -→ M ⋄ of logical variables into closed subsets, this interpretation is extended to all the formulae of ILL by structural induction as follows:

[[⊥]] = ∅ ⋄ [[A B]] = ([[A]] ∪ [[B]]) ⋄ [[⊤]] = M [[A & B]] = [[A]] ∩ [[B]] [[1]] = {ǫ} ⋄ [[A B]] = ([[A]] • [[B]]) ⋄ [[! A]] = (K ∩ [[A]]) ⋄ [[A ⊸ B]] = [[A]] --• [[B]]
Again, when the interpretation is done in a total deterministic monoid, we obtain exactly the same value for [[A]] as in the usual phase semantics interpretation. A sequent

A 1 , . . . , A k ⊢ B of ILL is valid in the interpretation [[•]] if [[A 1 ]] • • • • • [[A k ]] ⊆ [[B]
]. We recall the soundness theorem which states that provability in Sill entails semantic validity in non-deterministic intuitionistic phase semantics. Theorem 2.9.

If the sequent A 1 , . . . , A k ⊢ B has a proof in Sill, then the inclusion [[A 1 ]] • • • • • [[A k ]] ⊆ [[B]] holds.
Proof. The proof of this theorem can be done directly by generalizing the soundness proof of usual phase semantics [START_REF] Girard | Linear logic[END_REF], or else, as done in [START_REF] Larchey-Wendling | The Undecidability of Boolean BI through Phase Semantics[END_REF] (appendix B), by using the algebraic semantic characterization of ILL of [START_REF] Troelstra | Lectures on Linear Logic[END_REF].

Definition 2.10. We denote by ILL p the set of sequents which have a proof in Sill. We denote by ILL ND (resp. ILL PD , resp. ILL TD ) the set of sequents which are valid in every non-deterministic phase semantic interpretation where the base monoid is of the class ND (resp. PD, resp. TD).

Let us consider the following inclusion sequence: Proof. Total deterministic monoids (of the class TD) are in one to one correspondence with (usual) commutative monoids and this correspondence trivially extends to phase semantics. The result is simply a reformulation of the completeness of usual phase semantics [START_REF] Girard | Linear logic[END_REF][START_REF] Troelstra | Lectures on Linear Logic[END_REF] w.r.t. ILL. Corollary 2.12. ILL p = ILL ND = ILL PD = ILL TD and non-deterministic intuitionistic phase semantics is both sound and complete w.r.t. Sill.

ILL p ⊆ ILL ND ⊆ ILL PD ⊆ ILL TD ⊆ ILL p (1) A ⊢ A id Γ ⊢ A A, ∆ ⊢ B Γ, ∆ ⊢ B cut Γ ⊢ B Γ, ! A ⊢ B w Γ, ! A, ! A ⊢ B Γ, ! A ⊢ B c Γ, A ⊢ B Γ, ! A ⊢ B !L ! Γ ⊢ B ! Γ ⊢ ! B !R Γ, A, B ⊢ C Γ, A B ⊢ C L Γ ⊢ A ∆, B ⊢ C Γ, ∆, A ⊸ B ⊢ C ⊸L Γ ⊢ A ∆ ⊢ B Γ, ∆ ⊢ A B R Γ, A ⊢ B Γ ⊢ A ⊸ B ⊸R Γ, A ⊢ C Γ, A & B ⊢ C & 1 L Γ, B ⊢ C Γ, A & B ⊢ C & 2 Γ ⊢ B Γ ⊢ A B 2 R Γ ⊢ ⊤ ⊤R ⊢ 1 1R
Proof. With Proposition 2.11, we have closed the circular inclusion sequence [START_REF] Brotherston | A cut free proof theory for Boolean BI[END_REF]. In particular ILL p = ILL ND .

Trivial Phase vs. Kripke Semantics

In this section, we define trivial phase semantics which is a particular case of phase semantics that can be viewed as Kripke semantics put in a particular form. Definition 2.13. Given a non-deterministic monoid M = (M, •, ǫ), the trivial phase space is defined by taking the identity map on P(M ) as closure operator (i.e., for all X ∈ P(M ), X ⋄ = X) and by taking K = {ǫ}.

It is clear that the identity on P(M ) is both a closure and stable. Obviously also, K = {ǫ} verifies the conditions ǫ ∈ K ⊆ J and K • K ⊆ K. 4 In a trivial phase space, every subset of M is closed and thus M ⋄ = P(M ). The interpretation of ILL connectives becomes:

[[⊥]] = ∅ [[A B]] = [[A]] ∪ [[B]] [[⊤]] = M [[A & B]] = [[A]] ∩ [[B]] [[1]] = {ǫ} [[A B]] = [[A]] • [[B]] [[! A]] = {ǫ} ∩ [[A]] [[A ⊸ B]] = [[A]] --• [[B]]
Replacing 1/I, /∨, &/∧, / * and ⊸/- * in the previous equations and defining

[[A → B]] = M \[[A]] ∪ [[B]] and [[¬A]] = M \[[A]
] provides a complete (non-deterministic) trivial phase semantics to BBI, in direct correspondence to its Kripke semantics. Thus, there is an embedding of the connectives of ILL into BBI, which can be formalized with the following inductively defined map (•) ⊛ : ILL -→ BBI:

v ⊛ = v for v ∈ Var ⊥ ⊛ = ⊥ (A B) ⊛ = A ⊛ ∨ B ⊛ ⊤ ⊛ = ⊤ (A & B) ⊛ = A ⊛ ∧ B ⊛ 1 ⊛ = I (A B) ⊛ = A ⊛ * B ⊛ (! A) ⊛ = I ∧ A ⊛ (A ⊸ B) ⊛ = A ⊛ - * B ⊛
∀F ∈ ILL, ∀m ∈ M, m ∈ [[F ]] iff m F ⊛ (2)
Proof. By structural induction on F . We only consider the case

F = A B. Let m ∈ M , we have m ∈ [[A B]] iff m ∈ [[A]] • [[B]] iff ∃a ∈ [[A]], ∃b ∈ [[B]], m ∈ a • b iff ∃a, b, (a A ⊛ and b B ⊛ and m ∈ a • b) iff m A ⊛ * B ⊛ iff m (A B) ⊛ .
So if the interpretation of logical variables coincide, trivial phase semantics and Kripke semantics correspond to each other through the map (•) ⊛ . Given a sequence S = A 1 , . . . , A k of formulae of ILL, we define S ⊛ by structural induction on S:

() ⊛ = I (A 1 , . . . , A k+1 ) ⊛ = A ⊛ 1 * (A 2 , . . . , A k+1 ) ⊛ When [[•]
] and δ are identical maps on propositional variables, it is then straightforward to prove this equivalence by induction on k:

m ∈ [[A 1 ]] • • • • • [[A k ]] iff m (A 1 , . . . , A k ) ⊛ (3) Lemma 2.15. If A 1 , . . . , A k ⊢ B has a proof in Sill then the formula (A 1 , . . . , A k ) ⊛ → B ⊛ belongs to BBI ND .
Proof. Let us suppose that the sequent A 1 , . . . , A k ⊢ B is provable in Sill. We show that (A 1 , . . . , A k ) ⊛ → B ⊛ belongs to BBI ND . Let us consider a non-deterministic monoid (M, •, ǫ) and an interpretation δ : Var -→ P(M ).

For the non-deterministic trivial phase space associated to (M, •, ǫ), we choose the phase interpretation [[v]] = δ(v) for any variable v ∈ Var. By soundness of non-deterministic phase semantics (see Theorem 2.9), we obtain the inclusion Proof. Let us suppose that there exists a total deterministic monoid (M, •, ǫ) (in TD) and a trivial phase semantics interpretation

[[A 1 ]] • • • • • [[A k ]] ⊆ [[B]].
[[•]] : Var -→ P(M ) such that [[A 1 ]] • • • • • [[A k ]] [[B]].

The Undecidability of Boolean BI

From the preceding results, we establish the undecidability of BBI. We define a reverse map from multisets of formulae of ILL into lists of formulae by choosing an arbitrary computable total order among the formulae of ILL (e.g. lexicographic ordering). For any multiset Γ of formulae of ILL, there exists a unique and computable ordered sequence of formulae A 1 , . . . , A k s.t. Γ = {A 1 , . . . , A k } and we define

Γ ⊛ = (A 1 , . . . , A k ) ⊛ . The map (•) ⊛ : ILL -→ BBI defined by (Γ ⊢ B) → (Γ ⊛ → B ⊛ ) is thus a computable map from sequents of ILL into formulae of BBI.
We introduce the key result that links undecidability in ILL and in BBI. The fragment ILL 0 ⊸,&,! is a recursive subset of the set of sequents of ILL (see Definition 3.4). Theorem 3.1. In ILL 0 ⊸,&,! , validity is both undecidable and complete for total deterministic trivial phase semantics.

The proof of this theorem spans over the remaining sections of the paper (see Theorems 3.7 and 3.14). x is defined by trivial phase semantics with the monoid belonging to the class x ∈ {ND, PD, TD}. The question is: are these two inclusions strict? Indeed, the counter-examples of Theorem 2.6 and Proposition 2.7 cannot be used because both formulae contain a negation.

A Trivially Complete Fragment of ILL

We define and characterize an extension of the fragment s-IMELL ⊸ 0 of ILL [START_REF] De Groote | Vector addition tree automata[END_REF] which we denote ILL 0 ⊸,&,! . We provide a simple goal-directed proof system, denoted Gill 0 , which is itself an extension of the goal-directed proof system of s-IMELL ⊸ 0 , obtained by the addition of a new additive rule. Then we show that the proof system Gill 0 and trivial phase semantics are both sound and complete w. From this definition, it is obvious that membership in the fragment to s-IMELL ⊸ 0 , the only new form is (u & v) ⊸ w. The validity of sequents in ILL 0 ⊸,&,! can be established using the proof system Sill but we rather provide an alternative goal-directed proof system called Gill 0 in Figure 2. Apart for the axiom rule Ax , each other rule ⊸ , (⊸)⊸ , ⊸(⊸) or (&)⊸ is named according to the form of its side condition. Compared to s-IMELL ⊸ 0 , the only new rule is (&)⊸ . In [START_REF] De Groote | Vector addition tree automata[END_REF], the authors did not provide a proof of soundness/completeness of the system s-IMELL ⊸ 0 , leaving it to the reader. Here we present a full proof of soundness/completeness for our extension Gill 0 not only to please the reader but also to derive completeness of the fragment w.r.t. trivial phase semantics.

ILL 0 ⊸,&,! is a recursive property. Compared ! Σ, a ⊢ a Ax ! Σ, Γ ⊢ a ! Σ, Γ ⊢ b a ⊸ b ∈ Σ ! Σ, Γ, a ⊢ b ! Σ, Γ ⊢ c (a ⊸ b) ⊸ c ∈ Σ ! Σ, Γ ⊢ a ! Σ, ∆ ⊢ b ! Σ, Γ, ∆ ⊢ c a ⊸ (b ⊸ c) ∈ Σ ! Σ, Γ ⊢ a ! Σ, Γ ⊢ b ! Σ, Γ ⊢ c (a & b) ⊸ c ∈ Σ
Hence, even though validity in ILL 0 ⊸,&,! is the same as in the whole ILL (established for instance by a proof in Sill), here we show that in this specific fragment, validity is also sound and complete both w.r.t. the system Gill 0 and w.r.t. total deterministic trivial phase semantics. Proof. The proof of Lemma 3.5 can be found in [START_REF] Larchey-Wendling | The Undecidability of Boolean BI through Phase Semantics[END_REF] (Appendix C). For the proof of Lemma 3.6, we apply a technique similar to the one of Okada [START_REF] Okada | A uniform semantic proof for cut-elimination and completeness of various first and higher order logics[END_REF] for obtaining strong completeness through phase semantics. Let us consider a fixed multiset Σ of (⊸, &)-elementary formulae. We consider the free commutative monoid over the set of logical variables, i.e., the set of finite multisets of variables endowed with multiset addition (denoted by the comma) as monoidal composition and with the empty multiset (denoted ǫ = ⌊∅⌋) as neutral element. We write ⌊a, a, b⌋ for the multiset composed of two occurrences of a and one of b. Let us define the total deterministic monoid (M, •, ǫ = ⌊∅⌋) where M is the set of finite multisets of variables and

• : M × M -→ P(M ) is defined by ⌊Γ⌋ • ⌊∆⌋ = {⌊Γ, ∆⌋}.
We define the following semantic interpretation in the trivial phase space based on (M, •, ǫ):

[[c]] = ⌊Γ⌋ | ! Σ, Γ ⊢ c has a proof in Gill 0 for c ∈ Var
Let us now show that ǫ ∈ [[σ]] holds for any σ ∈ Σ. We pick one σ ∈ Σ and proceed by case analysis.

If

σ = u ⊸ v. Then ǫ ∈ [[u ⊸ v]] iff ǫ • [[u]] ⊆ [[v]] iff [[u]] ⊆ [[v]]. So let us consider one ⌊Γ⌋ such that ⌊Γ⌋ ∈ [[u]]. Let us prove that ⌊Γ⌋ ∈ [[v]]. By definition of [[u]], the sequent ! Σ, Γ ⊢ u has a proof in Gill 0 . Then, by rule ⊸ , the sequent ! Σ, Γ ⊢ v has a proof in Gill 0 . So we deduce ⌊Γ⌋ ∈ [[v]]. Hence [[u]] ⊆ [[v]] and we obtain ǫ ∈ [[σ]]. If σ = (u ⊸ v) ⊸ w. We have ǫ ∈ [[(u ⊸ v) ⊸ w]] iff [[u]] --• [[v]] ⊆ [[w]]. Let use choose ⌊Γ⌋ ∈ [[u]] --• [[v]]. Then {⌊Γ⌋} • [[u]] ⊆ [[v]]. By rule Ax , ! Σ, u ⊢ u has a proof in Gill 0 and thus ⌊u⌋ ∈ [[u]]. Thus {⌊Γ, u⌋} = ⌊Γ⌋•⌊u⌋ ⊆ [[v]]. Then ! Σ, Γ, u ⊢ v has a proof in Gill 0 . By rule (⊸)⊸ , ! Σ, Γ ⊢ w has a proof in Gill 0 . We conclude ⌊Γ⌋ ∈ [[w]]. Thus [[u]] --• [[v]] ⊆ [[w]] holds, hence ǫ ∈ [[σ]]. If σ = u ⊸ (v ⊸ w). We have ǫ ∈ [[u ⊸ (v ⊸ w)]] iff [[u]] • [[v]] ⊆ [[w]]. Let us choose ⌊Γ⌋ ∈ [[u]] and ⌊∆⌋ ∈ [[v]] and let us prove ⌊Γ⌋ • ⌊∆⌋ ⊆ [[w]]. Both ! Σ, Γ ⊢ u and ! Σ, ∆ ⊢ v have a proof in Gill 0 . By rule ⊸(⊸) , the sequent ! Σ, Γ, ∆⊢w has a proof in Gill 0 . Thus ⌊Γ⌋•⌊∆⌋ = {⌊Γ, ∆⌋} ⊆ [[w]]. We deduce [[u]] • [[v]] ⊆ [[w]] and thus conclude ǫ ∈ [[σ]]. If σ = (u & v) ⊸ w. We have ǫ ∈ [[(u & v) ⊸ w]] iff [[u]] ∩ [[v]] ⊆ [[w]]. If ⌊Γ⌋ ∈ [[u]] ∩ [[v]] then both ! Σ, Γ ⊢ u and ! Σ, Γ ⊢ v have a proof in Gill 0 . By rule (&)⊸ , the sequent ! Σ, Γ ⊢ w has a proof in Gill 0 . Thus ⌊Γ⌋ ∈ [[w]]. We have proved that [[u]]∩[[v]] ⊆ [[w]] and we conclude ǫ ∈ [[σ]]. Now let Σ = {σ 1 , . . . , σ k }. Then for any i ∈ [1, k] we have [[! σ i ]] = {ǫ}∩[[σ i ]] = {ǫ}. Consider Γ = ⌊a 1 , . . . , a p ⌋ and let us suppose that the sequent ! Σ, Γ ⊢ c of ILL 0 ⊸,&,!
is valid in every total deterministic trivial phase semantics interpretation. As a particular case, it is valid in the inter- pretation (M,•,ǫ,[[•]]) and thus the inclusion

[[! σ 1 ]] • • • • • [[! σ k ]] • [[a 1 ]] • • • • • [[a p ]] ⊆ [[c]]
holds. By rule Ax , for any i ∈ [1, p] the sequent ! Σ, a i ⊢a i has a proof in Gill 0 and thus we have

⌊a i ⌋ ∈ [[a i ]]. Also remember that for any i ∈ [1, k], we have ǫ ∈ [[! σ i ]]. So ⌊Γ⌋ ∈ {⌊a 1 , . . . , a p ⌋} = ǫ • • • • • ǫ • ⌊a 1 ⌋ • • • • • ⌊a p ⌋ ⊆ [[c]]
holds and we conclude that ! Σ, Γ⊢c has a proof in Gill 0 . Theorem 3.7. The system Gill 0 and total deterministic trivial phase semantics are both sound and complete for the fragment ILL 0 ⊸,&,! .

Proof. For a given sequent ! Σ, Γ ⊢ c of ILL 0 ⊸,&,! , if it has a proof in Gill 0 then, by Lemma 3.5, it has a proof in Sill. If ! Σ, Γ ⊢ c is provable in Sill then, as a particular case of Theorem 2.9, it is valid in every total deterministic trivial phase semantics interpretation. Finally, if ! Σ, Γ ⊢ c is valid in every total deterministic trivial phase semantics interpretation then, by Lemma 3.6, it is provable in Gill 0 .

Encoding Minsky machines in ILL

0 ⊸,&,!
We propose an encoding of two counter Minsky machines in the fragment ILL 0 ⊸,&,! of ILL. Kanovich [START_REF] Kanovich | Linear Logic as a Logic of Computations[END_REF][START_REF] Kanovich | The direct simulation of Minsky machines in linear logic[END_REF] already proved that Minsky machines can be encoded into the (!, )-Horn fragment of ILL. In his encoding, the recovery of computations from proofs is done through some form of proof normalization and the connective is used to simulate forking. Lafont later showed that the use of proof normalization can be avoided and replaced by a phase semantics argument [START_REF] Lafont | The undecidability of second order linear logic without exponentials[END_REF][START_REF] Lafont | The undecidability of second order multiplicative linear logic[END_REF]. In our encoding of Minsky machines in ILL 0 ⊸,&,! , the & connective is used to simulate forking and we will show that a trivial phase semantics argument is sufficient to recover computability from provability.

Let a and b be two distinct counter symbols. A (deterministic) two counter Minsky machine is a pair (l, ψ) where l > 0 is a strictly positive natural number of instructions and Then for any two states (i, m, n) and (i ′ , m ′ , n ′ ), we define the relation (i, m, n) → M (i ′ , m ′ , n ′ ) by:

ψ : [1, l] -→ ⊎ {+} × {a, b} × [0, l] {-} × {a, b} × [0, l] × [0, l]
ψ(i) = (+, x, i ′ ) and (m ′ , n ′ ) = (m, n) + x or ψ(i) = (-, x, i ′ , k), (m, n) x = 0 and (m ′ , n ′ ) = (m, n) or ψ(i) = (-, x, j, i ′ ), (m, n) x = 0 and (m ′ , n ′ ) + x = (m, n)
holds for some x ∈ {a, b} and j, k ∈ [0, l]. Notice that (i, m, n) → M (i ′ , m ′ , n ′ ) does not hold if i = 0 because ψ(0) is not defined. Let → ⋆ M be the reflexive and transitive closure of the relation → M . We say that the machine M accepts the input (m, n) if starting from the state (1, m, n), there exists a sequence of transitions leading to the state (0, 0, 0) and we define the set A(M) of accepted inputs:

A(M) = (m, n) ∈ N × N | (1, m, n) → ⋆ M (0, 0, 0)
Theorem 3.8. There exists a two counter Minsky machine M for which the set A(M) is not recursive [START_REF] Minsky | Recursive unsolvability of Post's problem of 'tag' and other topics in the theory of Turing machines[END_REF].

Let us consider the two counter symbols a and b as two (different) logical variables and let us choose two new variables u and v so that the set {a, b, u, v} has cardinal four. Let us choose an infinite set 5 of new logical variables {q i | i ∈ N} such that q i = q j unless i = j and {a, b, u, v}

∩ {q i | i ∈ N} = ∅.
Let Σ 0 be the following multiset composed of five (⊸, &)-elementary formulae:

Σ 0 = a ⊸ (u ⊸ u), b ⊸ (v ⊸ v), (a ⊸ a) ⊸ u, (a ⊸ a) ⊸ v, (a ⊸ a) ⊸ q 0
We define the two abbreviations a = v and b = u. Given a Minsky machine M = (l, ψ), for i ∈ [1, l], we define the multisets Σ 1 , . . . , Σ l of (⊸, &)-elementary formulae by:

Σ i = {(x ⊸ q j ) ⊸ q i } when ψ(i) = (+, x, j) and Σ i = {(x & q j ) ⊸ q i , x ⊸ (q k ⊸ q i )} when ψ(i) = (-, x, j, k)
Let Σ M be the multiset Σ M = Σ 0 , Σ 1 , . . . , Σ l . Given a natural number n and a logical variable x ∈ {a, b}, we define x n = x, x, . . . , x as the multiset composed of n occurrences of the variable x. Then, it is trivial to verify that for any natural numbers m, n and any i ∈ [0, l], the sequent ! Σ M , a m , b n ⊢ q i belongs to the fragment ILL 0 ⊸,&,! .

Theorem 3.9. For any two counter Minsky machine M and for any pair m, n ∈ N, we have (m, n) ∈ A(M) if and only if the sequent ! Σ M , a m , b n ⊢ q 1 is provable in Gill 0 .

We detail the proof in the following discussion. Let us consider a fixed Minsky machine M = (l, ψ). Then we denote Σ M (resp. → M ) simply by Σ (resp. →). We decompose the proof in four main intermediate results. Proof. We prove the case with a/u. The case of b/v is similar (see [START_REF] Larchey-Wendling | The Undecidability of Boolean BI through Phase Semantics[END_REF], Appendix D). Here is a suitable proof tree:

Ax ! Σ, a ⊢ a Ax ! Σ, a ⊢ a Ax ! Σ, a ⊢ a (a ⊸ a) ⊸ u ∈ Σ ! Σ ⊢ u a ⊸ (u ⊸ u) ∈ Σ . . . applied m -1 times ! Σ, a m-1 ⊢ u a ⊸ (u ⊸ u) ∈ Σ ! Σ, a m ⊢ u
In fact, this is the only possible proof tree but the demonstration of this uniqueness result is left to the reader. Lemma 3.11. For any r, m, n ∈ N and any i ∈ [0, l], if (i, m, n) → r (0, 0, 0) then the sequent ! Σ, a m , b n ⊢ q i is provable in Gill 0 .

Proof. We proceed by induction on r. If r = 0 then we have (i, m, n) = (0, 0, 0). The sequent ! Σ ⊢ q 0 has the following proof tree:

Ax ! Σ, a ⊢ a (a ⊸ a) ⊸ q 0 ∈ Σ ! Σ ⊢ q 0
Let us now consider a transition sequence (i, m, n) → (i ′ , m ′ , n ′ ) → r (0, 0, 0) of length r + 1. By induction hypothesis, let P be a proof tree for the sequent ! Σ, a m ′ , b n ′ ⊢ q i ′ . We consider the three cases for (i, m, n) → (i ′ , m ′ , n ′ ).

If ψ(i) = (+, x, i ′ ) and (m ′ , n ′ ) = (m, n) + x. Without loss of generality, we consider the case x = a (the case x = b is similar). Then m ′ = m + 1 and n ′ = n. We provide the following proof tree for ! Σ, a m , b n ⊢ q i :

P ! Σ, a m , b n , a ⊢ q i ′ (a ⊸ q i ′ ) ⊸ q i ∈ Σ ! Σ, a m , b n ⊢ q i If ψ(i) = (-, x, i ′ , k), (m, n) x = 0 and (m ′ , n ′ ) = (m, n).
We consider the case x = a without loss of generality. Then m = m ′ = 0 and n = n ′ . Let Q be a proof tree for ! Σ, b n ⊢ v according to Proposition 3.10. We provide the following proof tree for ! Σ, b n ⊢ q

i : Q ! Σ, b n ⊢ v P ! Σ, b n ⊢ q i ′ (v & q i ′ ) ⊸ q i ∈ Σ ! Σ, b n ⊢ q i If ψ(i) = (-, x, j, i ′ ), (m, n) x = 0 and (m ′ , n ′ ) + x = (m, n).
We consider the case x = a without loss of generality. Then m = m ′ + 1 and n = n ′ . We provide the following proof tree for ! Σ, a, a m

′ , b n ′ ⊢ q i : Ax ! Σ, a ⊢ a P ! Σ, a m ′ , b n ′ ⊢ q i ′ a ⊸ (q i ′ ⊸ q i ) ∈ Σ ! Σ, a, a m ′ , b n ′ ⊢ q i
In any case we obtain a proof tree for ! Σ, a m , b n ⊢ q i which fulfills the induction step. 6We point out that the form (&)⊸ is used to encode forking in a way similar Kanovich does with (see [START_REF] Kanovich | The direct simulation of Minsky machines in linear logic[END_REF]).

Let us now consider the following total deterministic trivial phase semantics interpretation. The free commutative monoid over two elements is (N × N, +, (0, 0)). We define x • y = {x + y} and (N × N, •, (0, 0)) is thus a total deterministic monoid. Every subset of N × N is closed in trivial phase semantics and we define

[[a]] = {(1, 0) = a} [[u]] = N × {0} [[b]] = {(0, 1) = b} [[v]] = {0} × N [[q i ]] = {(m, n) ∈ N × N | (i, m, n) → ⋆ (0, 0, 0)}
It is crucial that variables a, b, u, v, q 0 , q 1 , . . . , q l were chosen distinct from one another for this definition to be valid.

Let us now consider the trivial phase semantics interpretation of the compound formulae of Σ.

Proposition 3.12. For any

σ ∈ Σ, [[! σ]] = {(0, 0)} holds. Proof. As the identity [[! σ]] = {(0, 0)} ∩ [[σ]
] holds in the trivial phase semantics interpretation, it is necessary and sufficient to prove that (0, 0) ∈

[[σ]] holds for any σ ∈ Σ. First let us prove that [[a ⊸ a]] = {(0, 0)}. Indeed, (m, n) ∈ [[a ⊸ a]] iff (m, n) • [[a]] ⊆ [[a]] iff (m, n) • {(1, 0)} ⊆ {(1, 0)} iff {(m + 1, n)} ⊆ {(1, 0)} iff (m, n) = (0, 0). Then [[(a ⊸ a) ⊸ x]] = {(0, 0)} --• [[x]] = [[x]] for any variable x, in particular for x ∈ {u, v, q 0 }. Also (m, n) ∈ [[a ⊸ (u ⊸ u)]] iff (m, n) • {(1, 0)} • N × {0} ⊆ N × {0} iff n = 0. Thus [[a ⊸ (u ⊸ u)]] = N × {0}. By a similar argument, we get [[b ⊸ (v ⊸ v)]] = {0} × N. So for any formula σ ∈ Σ 0 , we have (0, 0) ∈ [[σ]].
Let us consider the formulae in

Σ i for i ∈ [1, l]. Let us prove that the relation (0, 0) ∈ [[σ]] holds for any σ ∈ Σ i . If ψ(i) = (+, x, j). Let us prove (0, 0) ∈ [[(x ⊸ q j ) ⊸ q i ]], i.e., [[x ⊸ q j ]] ⊆ [[q i ]]. Let us consider (m, n) ∈ [[x ⊸ q j ]]. Then {(m, n) + x} = {(m, n)} • [[x]] ⊆ [[q j ]] and thus (m ′ , n ′ ) = (m, n) + x ∈ [[q j ]]. Thus we have (i, m, n) → (j, m ′ , n ′ ) → ⋆ (0, 0, 0). We conclude (m, n) ∈ [[q i ]]. If ψ(i) = (-, x, j, k). Let us first prove that (0, 0) ∈ [[(x & q j ) ⊸ q i ]], i.e., [[x]] ∩ [[q j ]] ⊆ [[q i ]]. Let us con- sider (m, n) ∈ [[x]] ∩ [[q j ]]. Then (m, n) x = 0 and (j, m, n) → ⋆ (0, 0, 0). Thus (i, m, n) → (j, m, n) → ⋆ (0, 0, 0) and (m, n) ∈ [[q i ]]. Hence [[x]] ∩ [[q j ]] ⊆ [[q i ]] holds. Let us finally prove that (0, 0) ∈ [[x ⊸ (q k ⊸ q i )]], i.e., [[x]] • [[q k ]] ⊆ [[q i ]]. As [[x]] = {x} for x ∈ {a, b}, let us choose an arbitrary pair (m ′ , n ′ ) ∈ [[q k ]] and define (m, n) = x + (m ′ , n ′ ). Then (m, n) x = 1 + (m ′ , n ′ ) x = 0 and (i, m, n) → (k, m ′ , n ′ ) → ⋆ (0, 0, 0). We obtain (m, n) ∈ [[q i ]] and thus conclude x + (m ′ , n ′ ) ∈ [[q i ]]. Hence, for any (m ′ , n ′ ) ∈ [[q k ]] we get [[x]] • (m ′ , n ′ ) ⊆ [[q i ]]. Then [[x]] • [[q k ]] ⊆ [[q i ]] holds.
As a consequence, for any σ ∈ Σ, we obtain (0, 0) ∈

[[σ]]. The identity [[! σ]] = {(0, 0)} holds for any σ ∈ Σ. Lemma 3.13. For any m, n ∈ N, if ! Σ, a m , b n ⊢ q 1 is provable in Gill 0 then (m, n) ∈ A(M) holds.
Proof. Let Σ = {σ 1 , . . . , σ r }. We suppose that the sequent ! Σ, a m , b n ⊢ q 1 has a proof in Gill 0 . By the soundness part of Theorem 3.7, in our particular total deterministic trivial phase semantics interpretation, we have

[[! σ 1 ]] • • • • • [[! σ r ]] • [[a]] • • • • • [[a]] • [[b]] • • • • • [[b]] ⊆ [[q 1 ]]
where a occurs m times and b occurs n times. By Proposition 3.12, we deduce (m, n) = r.(0, 0) + m.(1, 0) + n.(0, 1) ∈ [[q 1 ]] and thus (1, m, n) → ⋆ (0, 0, 0) holds. This concludes the proof of Theorem 3.9 as direct consequence of Lemma 3.11 and Lemma 3.13.

The reader may have noticed that more than the simple encoding of computability with provability, we can even show that computations and proofs match one to one. Even though this result is not necessary to our argumentation, this suggests that the system Gill 0 is a natural choice to illustrate the relations between Minsky machines and linear logic, and may be more straightforward than the (!, )-Horn fragment [START_REF] Kanovich | The direct simulation of Minsky machines in linear logic[END_REF]. Whereas the decidability of s-IMELL ⊸ 0 is still unclear (but nevertheless known to be equivalent to the decidability of MELL [START_REF] De Groote | Vector addition tree automata[END_REF]), we have proved that the simple addition of the form (&)⊸ to s-IMELL ⊸ 0 is sufficient to encode forking and thus, computations of Minsky machines. Theorem 3.14. Validity in ILL 0 ⊸,&,! is undecidable. Proof. By Theorem 3.8, let M be a two counter Minsky machine s.t. A(M) is not recursive. Compute Σ M . If there is an algorithm that discriminates between provable and unprovable sequents of ILL 0 ⊸,&,! , use it to decide A(M) = {(m, n) ∈ N × N | ! Σ, a m , b n ⊢ q 1 is provable in Gill 0 } This identity is a direct consequence of Theorem 3.9. Thus A(M) would be recursive. We obtain a contradiction.

example. So we deduce [[A

1 ]] • • • • • [[A k ]] ⊆ [[B]].
C. The soundness of Gill 0 Lemma 3.5 Every proof of a sequent in Gill 0 can be transformed into a proof of the same sequent which uses only the rules id , w , c , ⊸ L , ⊸ R , ! L and & R of Sill.

Proof. We proceed by induction on the proofs in Gill 0 and by case analysis, depending on the last rule applied. Let n be the cardinal of the multiset Σ. Proof. We prove the remaining case with b and v. Here is a suitable proof tree:

Ax ! Σ, b ⊢ b Ax ! Σ, b ⊢ b Ax ! Σ, a ⊢ a (a ⊸ a) ⊸ v ∈ Σ ! Σ ⊢ v b ⊸ (v ⊸ v) ∈ Σ . . . applied n -1 times ! Σ, b n-1 ⊢ v b ⊸ (v ⊸ v) ∈ Σ ! Σ, b n ⊢ v
Lemma 3.11 For any r, m, n ∈ N and any i ∈ [0, l], if (i, m, n) → r (0, 0, 0) then the sequent ! Σ, a m , b n ⊢ q i is provable in Gill 0 .

Proof. We provide proof trees for the cases that where left to the reader in the body of the paper. Recall that P is a proof tree for the sequent ! Σ, a m ′ , b n ′ ⊢ q i ′ .

• Case where ψ(i) = (+, b, i ′ ), m ′ = m and n ′ = n+1.

Here is a proof tree for ! Σ, a m , b n ⊢ q i :

P ! Σ, a m , b n , b ⊢ q i ′ (b ⊸ q i ′ ) ⊸ q i ∈ Σ ! Σ, a m , b n ⊢ q i
• Case where ψ(i) = (-, b, i ′ , k), m = m ′ and n = n ′ = 0. Let Q be a proof tree for ! Σ, a m ⊢ u according to Proposition 3.10. Here is a proof tree for ! Σ, b n ⊢q i :

Q ! Σ, a m ⊢ u P ! Σ, a m ⊢ q i ′ (u & q i ′ ) ⊸ q i ∈ Σ ! Σ, a m ⊢ q i
• Case where ψ(i) = (-, b, j, i ′ ), m ′ = m and n ′ + 1 = n. Here is a proof tree for ! Σ, a m ′ , b, b n ′ ⊢ q i :

Ax ! Σ, b ⊢ b P ! Σ, a m ′ , b n ′ ⊢ q i ′ b ⊸ (q i ′ ⊸ q i ) ∈ Σ ! Σ, a m ′ , b, b n ′ ⊢ q i

  for any subsets X, Y of M . Using this extension, we can view an element m of M as the singleton set {m} and derive the equations m • X = {m} • X and a • b = {a} • {b}. Definition 2.1. A non-deterministic (or relational) monoid is a triple (M, •, ǫ) where ǫ ∈ M and • : M ×M -→P(M ) for which the following conditions hold: 1

  ∃a, b, m ∈ a • b and a A and b B m A - * B iff ∀a, b (b ∈ m • a and a A) ⇒ b B A formula F is valid in a non-deterministic monoid (M, •, ǫ) if for any interpretation δ : Var -→ P(M ) of propositional variables, the relation m F holds for any m ∈ M . A counter-model of the formula F is given by a non-deterministic monoid (M, •, ǫ), an interpretation δ : Var-→P(M ) and an element m ∈ M such that m F .

Theorem 2 . 6 .

 26 Kripke semantics. The formula (I * I)→I expresses stability of invertibility by monoidal composition. The formula (I * I) → I is valid in every partial deterministic monoid, where I = ¬(⊤ - * ¬I). There exists a non-deterministic monoid which is a counter-model of (I * I) → I. Proof. First the counter-model. Consider the non-deterministic monoid ({ǫ, x, y}, •, ǫ) uniquely defined by x•x = {ǫ, y}, y • α = {y} for any α ∈ {ǫ, x, y} and the conditions 1 & 2 of Definition 2.1. Then x I because there exists α (α = x) such that ǫ ∈ x • α. On the other hand, y I because there is no α such that ǫ ∈ y • α holds. So, as y ∈ x • x, we have y I * I. Thus y (I * I) → I. Now let us prove that (I * I) → I is valid in every partial deterministic monoid. Let (M, •, ǫ) be a partial deterministic monoid. Let us choose a ∈ M and prove that a (I * I) → I. So we suppose a I * I holds and we have to prove a I. As a I * I, there exist b, c ∈ M such that a ∈ b • c, b I and c I. Thus there exist b

Figure 1 .

 1 Figure 1. Sequent calculus Sill for ILL

Lemma 2 . 14 .

 214 In trivial phase semantics, if the phase interpretation [[•]] :Var -→ M ⋄ and the Kripke interpretation δ : Var-→P(M ) are identical maps then the phase semantics and the Kripke semantics are in relation as follows:

  Considering the Kripke interpretation defined by δ(v) = [[v]] for any v ∈ Var, by equivalences (2) and (3), there exists m ∈ M such that m (A 1 , . . . , A k ) ⊛ → B ⊛ . So (A 1 , . . . , A k ) ⊛ → B ⊛ has a Kripke counter-model in TD. Hence, this formula does not belong to BBI TD .

  r.t. the fragment ILL 0 ⊸,&,! . Definition 3.4. A formula of ILL is (⊸, &)-elementary if it is of the form u⊸v, (u⊸v)⊸w, u⊸(v⊸w) or (u&v)⊸ w where u, v and w are logical variables. The sequents of the fragment ILL 0 ⊸,&,! are those of the form ! Σ, Γ ⊢ c where Γ is a multiset of variables, c is a variable and Σ is a multiset of (⊸, &)-elementary formulae.

Figure 2 .

 2 Figure 2. Gill 0 : a goal-directed sequent calculus for ILL 0 ⊸,&,!

Lemma 3 . 5 .Lemma 3 . 6 .

 3536 Every proof of a sequent in Gill 0 can be transformed into a proof (of the same sequent) which uses only rules id , w , c , ⊸ L , ⊸ R , ! L and & R of Sill. If the sequent ! Σ, Γ ⊢ c of ILL 0 ⊸,&,! is valid in every total deterministic trivial phase semantic interpretation then it has a proof in Gill 0 .

  is a total map representing the list of instructions (here, ⊎ represents disjoint set union). Minsky machines instructions (incrementation, zero test/decrementation) are encoded as illustrated in the two following examples: ψ(1) = (+, a, 3) 1: a:=a+1 ; goto 3 ψ(2) = (-, b, 4, 5) 2: if b=0 then goto 4 else b:=b-1 ; goto 5 Given a two counter Minsky machine M = (l, ψ), we define the set S(M) of states of the machine by S(M) = [0, l]×N×N and a (binary) transition relation between states → M ⊆ S(M)×S(M). We define the following notations: a = (1, 0), b = (0, 1), (m, n) a = m and (m, n) b = n.

Proposition 3 . 10 .

 310 For any m, n ∈ N, the sequents ! Σ, a m ⊢ u and ! Σ, b n ⊢ v are provable in Gill 0 .

  For each rule of Gill 0 , we propose the corresponding (open) proof tree in Sill:• Case of rule Ax . id a ⊢ a w . . . applied n times w ! Σ, a ⊢ a • Case of rule ⊸ : ! Σ, Γ ⊢ a id b ⊢ b ⊸ L ! Σ, Γ, a ⊸ b ⊢ b ! L ! Σ, Γ, !(a ⊸ b) ⊢ b c ! Σ, Γ ⊢ b • Case of rule (⊸)⊸ : ! Σ, Γ, a ⊢ b ⊸ R ! Σ, Γ ⊢ a ⊸ b id c ⊢ c ⊸ L ! Σ, Γ, (a ⊸ b) ⊸ c ⊢ c ! L ! Σ, Γ, !((a ⊸ b) ⊸ c) ⊢ c c ! Σ, Γ ⊢ c • Case of rule ⊸(⊸) : ! Σ, Γ ⊢ a ! Σ, ∆ ⊢ b id c ⊢ c ⊸ L ! Σ, ∆, b ⊸ c ⊢ c ⊸ L ! Σ, Γ, ! Σ, ∆, a ⊸ (b ⊸ c) ⊢ c ! L ! Σ, Γ, ! Σ, ∆, !(a ⊸ (b ⊸ c)) ⊢ c c . . . applied n + 1 times c ! Σ, Γ, ∆ ⊢ c • Case of rule (&)⊸ : ! Σ, Γ ⊢ a ! Σ, Γ ⊢ b & R ! Σ, Γ ⊢ a & b id c ⊢ c ⊸ L ! Σ, Γ, (a & b) ⊸ c ⊢ c ! L ! Σ, Γ, !((a & b) ⊸ c) ⊢ c c ! Σ, Γ ⊢ cD. The soundness of the encoding Proposition 3.10 For any m, n ∈ N, the sequents ! Σ, a m ⊢ u and ! Σ, b n ⊢ v are provable in Gill 0 .

  Then, by (2) and (3), for any m ∈ M we have m (A 1 , . . . , A k ) ⊛ → B ⊛ . As this holds for any non-deterministic Kripke interpretation, we deduce that (A 1 , . . . , A k ) ⊛ → B ⊛ belongs to BBI ND .

Lemma 2.16. If the sequent A 1 , . . . , A k ⊢ B has a countermodel in total deterministic trivial phase semantics then the formula (A 1 , . . . , A k ) ⊛ → B ⊛ does not belong to BBI TD .

  Theorem 3.2. Let x ∈ {ND, PD, TD}. The restricted map (•) ⊛ : ILL 0 ⊸,&,! -→BBI x is a sound and faithful embedding. Proof. Let us consider a given sequent Γ ⊢ B of ILL 0 ⊸,&,! . Let Γ = {A 1 , . . . , A k } where the sequence A 1 , . . . , A k is sorted according to the previously chosen total order. Then(Γ ⊢ B) = (A 1 , . . . , A k ⊢ B) and (Γ ⊢ B) ⊛ = (A 1 , . . . , A k ) ⊛ → B ⊛ . On the one hand, if Γ ⊢ B is valid in ILL,then it has a proof in Sill and thus, according to Lemma 2.15, the formula Γ ⊛ → B ⊛ belongs to BBI ND . It thus belongs to BBI x because BBI ND ⊆ BBI x holds (Theorem 2.5). On the other hand, if Γ ⊢ B is invalid in ILL, then as it belongs to the fragment ILL 0 ⊸,&,! which is complete w.r.t. total deterministic trivial phase semantics, it has a counter-model in this semantics. Hence by Lemma 2.16, the formula Γ ⊛ → B ⊛ does not belong to BBI TD . Thus, it does not belong to BBI x either because BBI x ⊆ BBI TD holds (Theorem 2.5). Theorem 3.3. (Universal) validity in the logic BBI ND (resp. BBI PD , resp. BBI TD ) is undecidable. Proof. For any x ∈ {ND, PD, TD}, by Theorem 3.2, a decision procedure for BBI x would lead to a decision procedure for ILL 0 ⊸,&,! by composition with the obviously computable map (•) ⊛ , which contradicts Theorem 3.1.

	Before we describe the fragment ILL 0 ⊸,&,! and the proof
	of Theorem 3.1, we wish to point out the inclusion sequence
	ILL t ND ⊆ ILL t PD ⊆ ILL t TD as a remaining open question where ILL t

Associativity should be understood using the extension of • to P(M ).

Sometimes the neutral of is denoted 0, but we favor ⊥ as in[START_REF] Troelstra | Lectures on Linear Logic[END_REF].

A stable closure is a quantic nucleus in quantale theory[START_REF] Yetter | Quantales and (Noncommutative) Linear Logic[END_REF]. The "stability" property itself seems to have no well-established terminology.

Γ, A ⊢ C Γ, B ⊢ C Γ, A B ⊢ C L Γ, ⊥ ⊢ A ⊥L Γ ⊢ A Γ, 1 ⊢ A 1L Γ ⊢ A Γ ⊢ B Γ ⊢ A & B &R Γ ⊢ A Γ ⊢ A B 1 R

In fact, there is no other choice forK because J = {x ∈ M | x ∈ {ǫ} ⋄ ∩ (x • x) ⋄ } = {ǫ} when (•)⋄ is the identity map on P(M ).

For our particular purpose, we only need as many q i 's as there are instructions in the Minsky machine obtained from Theorem 3.8.

Again, but this is left to the reader, it can be demonstrated that the proof tree recursively built from the transition sequence (i, m, n) → r (0, 0, 0) is the unique proof tree for the sequent ! Σ, a m , b n ⊢ q i .

Acknowledgments. The authors dedicate this work and the resulting paper to the memory of Pr. Noëlle Carbonell.

A. A witness for BBI TD ⊆ BBI PD Proposition 2. [START_REF] Ghilardi | Modal logics with n-ary connectives[END_REF] The formula (¬I - * ⊥) → I is valid in every total deterministic monoid. There exists a partial deterministic monoid which is a counter-model to (¬I - * ⊥) → I.

Proof. It could be done by induction on ILL proof trees but we rather use the algebraic semantic characterization of ILL of [START_REF] Troelstra | Lectures on Linear Logic[END_REF]. We prove that

X ⋄ and we deduce that for any closed subset X (i.e. X = X ⋄ ), we have

Let us prove that

Associativity follows from this last identity and associativity/commutativity of • on P(M ).

It is obvious that

because it is obtained by composition of two monotonic operators, namely • and (•)

The fact that --• is contra-variant w.r.t. its first operand and co-variant w.r.t. its second operand is deducible from the monotonicity of • and the fact that --• is right adjoint to •. We finish by proving that X 7 The last condition to check is

We can then apply Theorem 8.21 (page 80) from [START_REF] Troelstra | Lectures on Linear Logic[END_REF]. If


Robustness illustration

In most of these applications, the watermarking should be robust. What is robust watermarking?

The robust watermarking is the art of modifying a media (image, sound, video, ...) such that:

it contains a message most of the time in relation with the media, degradation is most of the time imperceptible, the hidden message is not lost when media degradation occurs (attacks).

Robust watermarking families

The three major families (multi-bits): Not informed : Spread Spectrum (DM-SS), Informed : Quantized-based (QIM, SCS, P-QIM), Informed : Trellis-based (DPTC).

Brief conclusion

Good

Definition

The classical framework of security:

Kerckhoffs's framework The embedding and extracting algorithms are known by the attacker and the attacker owns observations. The only secret parameter is the key.

Security attack

A security attack is an attack for which secrets parameters or secret informations are obtained.

Security subject addresses those technical points: Analysis and creation of secure algorithm, Analysis and creation of security attack. The best probabilistic code (coming from cryptography community): The Tardos code.

A video watermarking technique inside H.264, before quantization, taking into account RD optimization, robust to photometric attacks, and real time.

Collusion attacks

f k : a video frame from a colluder k. C: the set of colluders. K : the number of colluders. Shahid, Chaumont and Puech, ICIP'2010; remarks An interesting practical scheme, but the watermarking scheme is not enough secure, and the algorithm is not robust to spatial and temporal desynchronizations.

f min = min{f k } k∈C f max = max{f k } k∈C f avg = k∈C f k K f median = median{f k } k∈C f minmax = f min +fmax 2 f modNeg = f min + f max -f median 'bus', '
Another interesting approach (outside H.264): There is still lots of work...

End

Slides may be downloaded at: http://www.lirmm.fr/∼chaumont/Publications.html e-mail : marc.chaumont@lirmm.fr

Figure :

 : Figure: Motion estimation in temporal direction.

  Photometric Noise addition, DA/AD conversion Gamma correction Transcoding and video format conversion Intra and inter-frames filtering Chrominance resampling (4:4:4, 4:2:2, 4:2:0) Spatial Desynchronization Changes display formats (4/3, 16/9, 2.11/1) Changes resolution (NTSC, PAL, SECAM) Positional jitter Hand-held camera recording (curved-bilinear transform) Temporal Desynchronization Changes of frame rate Frame dropping / insertion Frame decimation / duplication Video editing Cut-and-splice and cut-insert-splice Fade-and-dissolve and wipe-and-matte Graphic overlay (subtitles, logo) "Security issue and collusion attacks in video watermarking", PhD Thesis, G. Doërr, Supervised by J.-L. Dugelay, University of Nice-Sophia Antipolis, France, june 2005.

[[[

  Photometric robustness√ (should reduce payload)Video bitrate weakly modified √ respect 'quiet well' RD constraintsNo Drift √Real-time √

  Girod, Signal Processing 1998] [Gong and Lu, ISM'2008] … SS [Cox et al., TIP' ] DPTC [Miller et al., TIP' 4] P-QIM [Li a d Cox,

  video watermarking -Marc Chaumont -IPTA'2010 Watermarking A practical example: the traitor tracing (active fingerprinting) Example of watermarking for security: traitor tracing application An investigation experiment: Z. Shahid, M. Chaumont and W. Puech, "Spread Spectrum-Based Watermarking for Tardos Code-Based Fingerprinting of H.264/AVC Video", ICIP'2010, IEEE International Conference on Image Processing, Hong-Kong, China, 26-29 September, 2010, 4 pages.

F

  . Xie, T. Furon, C. Fontaine, "On-Off Keying Modulation and Tardos Fingerprinting", MM & Sec'08, September 22-23, 2008, Oxford, United Kingdom.

  news There are good solutions robust to photometric attacks INSIDE H.264 (or a similar codec).

	H.264 video watermarking -Marc Chaumont -IPTA'2010 H.264 video watermarking -Marc Chaumont -IPTA'2010
	Watermarking Watermarking
	Security of video watermarking Security of video watermarking
	Outline
	1 Preamble
	2 H.264
	3 Watermarking Bad news Definitions
	Most of the solutions (all?) INSIDE H.264 (or a similar codec) Video watermarking
	are not robust (or not enough robust) to temporal and spatial Security of video watermarking
	desynchronizations. A practical example: the traitor tracing (active fingerprinting)
	→ What about security? 4 Conclusion & Perspectives

F. Cayre, C. Fontaine, T. Furon, "Watermarking Security: Theory and Practice", IEEE Transactions on Signal Processing, vol. 53, no. 10, pp. 3976-3987, 2005. H.264 video watermarking -Marc Chaumont -IPTA'2010 Watermarking Security of video watermarking

Security of few images schemes

Security addresses the problem of recovering secret parameters.

Images Proposed attacks Spread Spectrum "Comparison of secure spread-spectrum modulations applied to still image watermarking" B. Mathon, P. Bas P, F. Cayre F, and B. Macq. Annals of Telecommunication, 2009.

Broken Arrows

"Two Key Estimation Techniques for the Broken-Arrows Watermarking Scheme", P. Bas and A. Westfeld, MM&Sec'2009. Counter Attack : "Better security levels for 'Broken Arrows' ", F. Xie, T. Furon, and C. Fontaine, SPIE'2010. → main security "danger" is Intra video collusion.


Edward Lee

M A Frcophth

Robert E Maclaren
email: robert.maclaren@merton.ox.ac.uk

Dphil Frcs Frcophth

Sources of RPE for replacement therapy

Keywords: cell, AMD, cloning, Yamanaka, transplantation

Stem cells with their capacity to regenerate and replace diseased tissues have recently been proposed as having great potential in the treatment of age-related macular degeneration (AMD). A stem cell therapeutic approach could operate either to replace the retinal pigment epithelium (RPE), or the neurosensory retina, or a combination of both. From the scientific perspective, RPE replacement alone is likely to be far more straightforward than rebuilding the complex circuitry of the neurosensory retina. Furthermore, recent advances with induced pluripotent stem (iPS) cells have raised the real possibility of transplanting healthy "young" autologous RPE into patients with early signs of AMD. At this stage, however, it is useful to reconsider some of the earlier clinical studies that used suspensions of autologous RPE cells harvested from the peripheral retina. These showed that isolated RPE cell suspensions had little capacity to recreate a monolayer on the diseased Bruch's membrane of AMD. To counter this problem, researchers from Southampton in the UK report use of a synthetic polymer alternative to Bruch's membrane, 1 which could provide a scaffold for future RPE derived from stem cells, or possibly reopen opportunities for autologous RPE cells harvested from the peripheral retina.

This has traditionally involved macular translocation, [START_REF] Machemer | Retinal separation, retinotomy, and macular relocation: II. A surgical approach for age-related macular degeneration?[END_REF][START_REF] Wolf | Macular translocation for surgical management of subfoveal choroidal neovascularizations in patients with AMD: first results[END_REF][START_REF] Eckardt | Macular rotation with and without counter-rotation of the globe in patients with age-related macular degeneration[END_REF] RPE suspension, [START_REF] Binder | Transplantation of autologous retinal pigment epithelium in eyes with foveal neovascularization resulting from age-related macular degeneration: a pilot study[END_REF][START_REF] Van Meurs | Autologous peripheral retinal pigment epithelium translocation in patients with subfoveal neovascular membranes[END_REF] or patch graft techniques, [START_REF] Peyman | A technique for retinal pigment epithelium transplantation for age-related macular degeneration secondary to extensive subfoveal scarring[END_REF][START_REF] Stanga | Retinal pigment epithelium translocation after choroidal neovascular membrane removal in age-related macular degeneration[END_REF][START_REF] Van Meurs | Autologous retinal pigment epithelium and choroid translocation in patients with exudative age-related macular degeneration: short-term follow-up[END_REF][START_REF] Joussen | Autologous translocation of the choroid and retinal pigment epithelium in age-related macular degeneration[END_REF][START_REF] Maclaren | Autologous transplantation of the retinal pigment epithelium and choroid in the treatment of neovascular age-related macular degeneration[END_REF] developed by vitreoretinal surgeons over the last two decades. Surgery was typically most effective following the acute development of choroidal new vessels (CNV) and haemorrhage, because this provided a window of opportunity for RPE replacement before secondary degeneration of the overlying neurosensory retina. The advent of effective anti-vascular endothelial growth factor (VEGF) therapies, however, has made it difficult to justify surgical interventions which have potentially severe complications, except for specific mechanical conditions such as RPE tears. [START_REF] Maaijwee | Retinal pigment epithelium (RPE)-choroid graft translocation in the treatment of an RPE tear: preliminary results[END_REF] This applies also for nonexudative AMD, because some patients will retain good vision for many years, which could otherwise be compromised acutely by a surgical complication. For surgical treatments to be re-established as a potential treatment for AMD it will be necessary to find some way of simplifying the process to reduce the risks of severe sight threatening complications, such as proliferative vitreoretinopathy (PVR), sub macular haemorrhage and retinal detachment. Stem cells have been proposed as providing a simpler surgical alternative, but this concept is also likely to be complex, because some means of restoring Bruch's membrane would almost certainly still be necessary and this would require further surgical manipulations beyond a simple subretinal injection of a cell suspension.

Here we discuss the essential physiological properties of Bruch's membrane that would need to be replaced by a polymer-based scaffold and the potential sources of RPE cells that could be combined with this new technology as a future treatment for AMD.

Morphology and function of the RPE-Bruch's interface

In the healthy retina, RPE cells form a continuous layer of polarised cells, adherent through intervening tight junctions to create a physiological barrier between the choriocapillaris and outer retina. By controlling the passage of water, ions and selected molecules, the RPE cell layer actively maintains the chemical environment and homeostasis of the outer retina. Integral to this barrier function is the polarised arrangement of the cells, with different proteins expressed on the apical and basal surfaces and adjoining tight junctions. [START_REF] Economopoulou | Expression, localization, and function of junctional adhesion molecule-C (JAM-C) in human retinal pigment epithelium[END_REF] The apical microvilli interdigitate between photoreceptors within the extracellular matrix and phagocytose outer segments. RPE replacement should aim as closely as possible to restore this polarised arrangement, which is crucial for normal RPE function and maintenance of the outer blood-retina barrier. This can be assumed following full-thickness RPE-choroid grafts, because scanning electron microscopy has demonstrated the maintenance of RPE polarity on graft tissue removed from the eye during surgery. [START_REF] Maclaren | Autologous transplantation of the retinal pigment epithelium and choroid in the treatment of neovascular age-related macular degeneration[END_REF] In contrast, RPE cells differentiated from human embryonic stem (hES) cells need to be differentiated on a basal substrate, such as matrigel, [START_REF] Vugler | Elucidating the phenomenon of HESC-derived RPE: anatomy of cell genesis, expansion and retinal transplantation[END_REF] or synthetic transwell membranes in order to re-establish polarity. [START_REF] Carr | Protective effects of human iPSderived retinal pigment epithelium cell transplantation in the retinal dystrophic rat[END_REF] Although a soluble substrate such as Matrigel might be more biocompatible, in the subretinal space any trophic properties of an RPE substrate may induce CNV formation, [START_REF] Qiu | A new model of experimental subretinal neovascularization in the rabbit[END_REF] which would rapidly compromise any transplanted RPE cell sheet even if optimally polarised.

The search for a suitable RPE substrate is further complicated by the multiple roles that the normal Bruch's membrane has on RPE cell function beyond inducing polarity, which include powerful influences on cell survival and differentiation. In the absence of protein binding interactions with Bruch's membrane, transplanted RPE cells may de-differentiate to become fibroblast-like and undergo increased rates of apoptosis. [START_REF] Tezel | Reattachment to a substrate prevents apoptosis of human retinal pigment epithelium[END_REF] It is doubtable whether the host Bruch's membrane could act as a substrate for transplanted cells, because in AMD it is likely that compromise of this layer is at least in part the reason for RPE cell death in the first place. Evidence for this comes from two key studies of human aged Bruch's membrane. First, when single dissociated RPE cells were harvested from the nasal retina in patients with macular degeneration and transplanted into the damaged foveal region, the cells were unable to attach to the damaged Bruch's membrane under the fovea. [START_REF] Binder | Transplantation of autologous retinal pigment epithelium in eyes with foveal neovascularization resulting from age-related macular degeneration: a pilot study[END_REF] Significantly however the donor site in the nasal retina was able to restore RPE continuity, presumably because these RPE cells were able to divide and adhere to the undamaged Bruch's membrane. [START_REF] Binder | Transplantation of autologous retinal pigment epithelium in eyes with foveal neovascularization resulting from age-related macular degeneration: a pilot study[END_REF] This clinical observation implies that it is not the age of the RPE donor cells but the damaged host Bruch's membrane which is the limiting factor for adherence of isolated cells. In support of this clinical observation, an in vitro study also showed that embryonic RPE cells could adhere onto normal but not aged Bruch's membrane obtained from post-mortem specimens. [START_REF] Gullapalli | Impaired RPE survival on aged submacular human Bruch's membrane[END_REF] Similarly the concept of repairing a pigment epithelial detachment (PED) with RPE derived from stem cells is not a logical approach if the pathogenesis of the PED is due to changes in conductance of the underlying Bruch's membrane. [START_REF] Bird | Retinal pigment epithelial detachments in the elderly[END_REF] Hence we might conclude from these longstanding observations that any successful RPE replacement therapy for AMD must also take into consideration the need to replace the underlying Bruch's membrane.

The pentilaminar structure of Bruch's membrane, with the layers being formed from distinct origins and at different stages of development, [START_REF] Takei | Origin and development of Bruch's membrane in monkey fetuses: an electron microscopic study[END_REF] is a relatively complex structure to repair or replace. Its composition varies considerably with geographic location in the eye, as the sub-macular membrane is significantly thinner than that found more peripherally. [START_REF] Nakaizumi | The ultrastructure of Bruch's Membrane. I. Human, Monkey, Guinea pig and rat eyes[END_REF] With age additional proteins and lipids are seen to be deposited within the membrane leading to increased thickness, and there are degenerative changes including fragmentation of the elastins and the development of abnormal cross-links within the proteins. [START_REF] Spraul | Histologic and morphometric analysis of the choroid, Bruch's membrane, and retinal pigment epithelium in postmortem eyes with age-related macular degeneration and histologic examination of surgically excised choroidal neovascular membranes[END_REF][START_REF] Guymer | Changes in Bruch's membrane and related structures with age[END_REF] These aging changes are most pronounced in the macular region and have an adverse effect on RPE cell binding, function and survival and conductivity across the membrane. [START_REF] Zarbin | Current concepts in the pathogenesis of age-related macular degeneration[END_REF] Gullapalli and colleagues studied cultured foetal human RPE cells in combination with segments of Bruch's membrane extracted from 27 donor eyes (55 to 75 years of age), and found the RPE cell coverage and morphology to be poor on aged submacular Bruch's membrane, and to deteriorate further with time; the binding was worse still in the membrane of an eye with large soft drusen. [START_REF] Gullapalli | Impaired RPE survival on aged submacular human Bruch's membrane[END_REF] The finding that aged Bruch's membrane does not support transplanted RPE survival and differentiation is of fundamental importance for RPE transplantation strategies as ultimately the fate of donor cells will depend on whether they can maintain or develop attachments to suitable substrates. These age-related changes in Bruch's membrane also represent one of the critical differences between potential patients and the laboratory animals in which many of the successes of RPE transplantation experiments have been reported, because the latter are generally young and have healthy Bruch's membrane. [START_REF] Carr | Protective effects of human iPSderived retinal pigment epithelium cell transplantation in the retinal dystrophic rat[END_REF][START_REF] Li | Inherited retinal dystrophy in the RCS rat: prevention of photoreceptor degeneration by pigment epithelial cell transplantation[END_REF][START_REF] Girman | Cortical visual functions can be preserved by subretinal RPE cell grafting in RCS rats[END_REF] An advantage of the autologous RPE grafting technique in use clinically, is that the RPE is harvested from the equatorial region en bloc with attached Bruch's membrane and superficial choroid. [START_REF] Peyman | A technique for retinal pigment epithelium transplantation for age-related macular degeneration secondary to extensive subfoveal scarring[END_REF][START_REF] Stanga | Retinal pigment epithelium translocation after choroidal neovascular membrane removal in age-related macular degeneration[END_REF][START_REF] Van Meurs | Autologous retinal pigment epithelium and choroid translocation in patients with exudative age-related macular degeneration: short-term follow-up[END_REF][START_REF] Joussen | Autologous translocation of the choroid and retinal pigment epithelium in age-related macular degeneration[END_REF][START_REF] Maclaren | Autologous transplantation of the retinal pigment epithelium and choroid in the treatment of neovascular age-related macular degeneration[END_REF][START_REF] Joussen | Autologous translocation of the choroid and retinal pigment epithelium in patients with geographic atrophy[END_REF] Age-related changes are less pronounced in peripheral Bruch's membrane which although different in structure, [START_REF] Guymer | Changes in Bruch's membrane and related structures with age[END_REF] can support continued RPE function when transplanted into the macular region as evidenced by pigmentation and continued autofluorescence. [START_REF] Maclaren | Autologous transplantation of the retinal pigment epithelium and choroid in the treatment of neovascular age-related macular degeneration[END_REF][START_REF] Joussen | Autologous translocation of the choroid and retinal pigment epithelium in patients with geographic atrophy[END_REF] A limitation of the procedure however is the surgical morbidity, with a high proportion of patients undergoing repeat surgery because of PVR, macular pucker, retinal detachment or vitreous haemorrhage. [START_REF] Joussen | Autologous translocation of the choroid and retinal pigment epithelium in age-related macular degeneration[END_REF][START_REF] Maclaren | Autologous transplantation of the retinal pigment epithelium and choroid in the treatment of neovascular age-related macular degeneration[END_REF] In one series there was also evidence of further loss of function, possibly related to the initial trauma of surgery. [START_REF] Chen | Long-term visual and microperimetry outcomes following autologous retinal pigment epithelium choroid graft for neovascular age-related macular degeneration[END_REF] Unless modifications can be made to reduce the surgical complexity and risks involved of full thickness RPE-choroid grafts, the applicability of this procedure is likely to remain limited when compared to the new medical therapies currently being developed.

Other approaches have been to manipulate molecules such as the integrins to facilitate RPE cell integration on damaged Bruch's membrane, [START_REF] Afshari | Improving RPE adhesion to Bruch's membrane[END_REF][START_REF] Fang | Overexpression of integrin alpha6 and beta4 enhances adhesion and proliferation of human retinal pigment epithelial cells on layers of porcine Bruch's membrane[END_REF][START_REF] Gullapalli | Culture-induced increase in alpha integrin subunit expression in retinal pigment epithelium is important for improved resurfacing of aged human Bruch's membrane[END_REF] or to develop biological or synthetic membranes that can be used in combination with replacement cells from a variety of sources. [START_REF] Lu | Retinal pigment epithelium cell culture on thin biodegradable poly(DL-lactic-co-glycolic acid) films[END_REF][START_REF] Tomita | Biodegradable polymer composite grafts promote the survival and differentiation of retinal progenitor cells[END_REF] There are considerable challenges for any artificial substrate on which RPE cells are transplanted; it must be well tolerated in the subretinal space, and either biodegrade with time, or integrate. There will also be discerning membrane transport and permeability requirements, and any artificial substrate must be both robust enough to withstand surgical manipulation and remain in place under the fovea, whilst also being flexible enough to allow delivery through a small retinotomy. These requirements may still present a limiting factor in the clinical application of stem cell derived or other sources of cultured RPE cell suspensions.

Immunological considerations for subretinal RPE transplantation

Although immune privilege have been demonstrated in the sub-retinal space of animal transplantation models, the features of local tolerance are best described as relative rather than absolute. [START_REF] Zhang | Transplantation of retinal pigment epithelial cells and immune response in the subretinal space[END_REF] The RPE cells are central to maintaining the features of immune privilege seen in healthy eyes, by making up the outer bloodretinal barrier and expressing and secreting a variety of immuno-modulatory molecules; these include surface bound molecules such as FasL (which induces apoptosis of CD94+ inflammatory cells) and immuno-modulatory factors such as transforming growth factor-β , thrombospondin-1, somatostatin and pigment epithelial derived factor. [START_REF] Zamiri | Immunosuppressive properties of the pigmented epithelial cells and the subretinal space[END_REF][START_REF] Zamiri | Pigment epithelial growth factor suppresses inflammation by modulating macrophage activation[END_REF][START_REF] Jorgensen | Human retinal pigment epithelial cell-induced apoptosis in activated T cells[END_REF] Loss of RPE cells, aging, and disease within the retina have all been demonstrated in animal models to increase the risk of immunogenetically mismatched grafts in the subretinal space undergoing rejection. [START_REF] Enzmann | Immunological problems of transplantation into the subretinal space[END_REF][START_REF] Lund | Immunological considerations in neural transplantation[END_REF] The resultant inflammation may lead to further damage to the host tissues. [START_REF] Jiang | Immunologic consequences of intraocular implantation of retinal pigment epithelial allografts[END_REF] Studies in animals have demonstrated that aggressive immunosuprressant dosing may be required. In a xenotransplantation study (donor and recipient of different species) Del Priore and colleagues transplanted porcine foetal RPE cells into the subretinal space of albino rabbits and found that even with the combination of prednisolone, cyclosporine and azathioprine from the day of surgery, the transplanted cell survival remained poor. [START_REF] Del Priore | Triple immune suppression increases short-term survival of porcine fetal retinal pigment epithelium xenografts[END_REF] Similarly Crafoord and co-workers studied RPE allografts (donor and recipient of same species) in rabbits, and found that immunosuppression with cyclosporin was inadequate to prevent rejection. [START_REF] Crafoord | Long-term outcome of RPE allografts to the subretinal space of rabbits[END_REF] It therefore seems highly likely that immune tolerance cannot be assumed for embryonic stem cell treatments that use cells from an allograft donor, particularly when the subretinal environment is already in a heightened inflammatory state due to the active AMD process.

In keeping with these animal studies a trial some years ago of non-HLA matched fetal RPE cells in humans without immunosuppression, demonstrated post-operative macula oedema (likely to be a manifestation of host-graft rejection) in those who had undergone prior removal of fibrovascular membranes. [START_REF] Algvere | Transplantation of RPE in agerelated macular degeneration: observations in disciform lesions and dry RPE atrophy[END_REF] However, the corresponding clinical changes of leak were not seen in patients with dry AMD undergoing the same procedure, suggesting the threshold for rejection may be higher in non-exudative AMD because there was less pathogenic disruption to the RPE layer and Bruch's membrane prior to transplantation. [START_REF] Algvere | Transplantation of RPE in agerelated macular degeneration: observations in disciform lesions and dry RPE atrophy[END_REF] Similarly transplantation of intact sheets of foetal retina appear to survive in the subretinal space of patients with retinitis pigmentosa, possibly because the RPE-Bruch interface is relatively intact in these patients. [START_REF] Radtke | Transplantation of intact sheets of fetal neural retina with its retinal pigment epithelium in retinitis pigmentosa patients[END_REF] Conversely a recent study suggested that non-HLA matched foetal grafts did not undergo immunological rejection when placed in the subretinal space of four patients with AMD, [START_REF] Radtke | Vision improvement in retinal degeneration patients by implantation of retina together with retinal pigment epithelium[END_REF] however, it was also suggested that rejection might still occur, but more slowly, as evidenced by progressive RPE atrophy rather than vasculitis in these patients. [START_REF] Zarbin | Retinal pigment epithelium-retina transplantation for retinal degenerative disease[END_REF] The question of rejection is inherently difficult to determine in patients where no histology is available and against the background of a disease such as AMD, which is itself inflammatory. Nevertheless, there is convincing histological evidence from animal studies that non-matched cells are rejected from the sub-retinal space in time when not accompanied by systemic immune suppression, [START_REF] Enzmann | Immunological problems of transplantation into the subretinal space[END_REF][START_REF] Jiang | Immunologic consequences of intraocular implantation of retinal pigment epithelial allografts[END_REF][START_REF] Crafoord | Long-term outcome of RPE allografts to the subretinal space of rabbits[END_REF][START_REF] Grisanti | Xenotransplantation of retinal pigment epithelial cells into RCS rats[END_REF] albeit less floridly than may be expected in other parts of the body. The use of immune suppressants in clinical practice is possible, but brings risks of malignancy, susceptibility to infection and hepatic or renal toxicity, rendering a non-immunogenic source of replacement RPE cells far preferable. In this regard, using RPE obtained by therapeutic cloning or induction of pluripotent stem cells would be ideal, because donor cells could ultimately be derived from the patient and therefore provide a precise HLA match.

Sources of autologous RPE from stem cells

The cloning of Dolly the sheep by somatic cell nuclear transfer (SCNT) in 1997 was a landmark scientific discovery, because it showed for the first time that a single cell taken from an adult mammal could be reprogrammed into an embryonic stem cell that could subsequently give rise to every cell type in the mammalian body. [START_REF] Wilmut | Viable offspring derived from fetal and adult mammalian cells[END_REF] In somatic cell nuclear transfer, DNA is taken from a donor cell (in the case of Dolly the sheep -a mammary gland cell from her genetic mother) and transferred into an oocyte which has had its original nucleus removed. This oocyte is then able to reprogram the DNA via undefined cytoplasmic factors and differentiate into an embryonic stem cell following the normal pattern of embryonic development. Although the mitochondrial DNA will be different as it is derived from the oocyte, all chromosomal DNA in the fully cloned animal should be identical to the DNA of the donor cell and could thus provide ideally matched tissue for transplantation. Dolly the sheep could see and had a normal functional retina which meant that the DNA from the mammary gland donor cell had been reprogrammed to express the correct genes required for normal RPE cell differentiation and function. [START_REF] Wilmut | Viable offspring derived from fetal and adult mammalian cells[END_REF] A decade later the first cloning of primate DNA was achieved using a similar method, [START_REF] Byrne | Producing primate embryonic stem cells by somatic cell nuclear transfer[END_REF] raising the possibility of cloning human cells.

One major drawback however with cloning through somatic cell nuclear transfer, is that the reprogramming goes back to the embryonic state and must begin with a donor oocyte. [START_REF] Maclaren | Stem cell therapy and the retina[END_REF] This raises additional ethical questions because another life-form is involved during the cloning process. In 2006 however a major breakthrough occurred in deriving stem cells directly from adult differentiated cells without the need for an oocyte, by transducing cells directly with a series of four transcription factors (Oct4, Sox2, Klf4 and c-Myc) capable of reprogramming DNA without need for an oocyte. [START_REF] Takahashi | Induction of pluripotent stem cells from mouse embryonic and adult fibroblast cultures by defined factors[END_REF] Essentially this process involves manipulation of the DNA binding proteins known as histones to inactivate the genes active in an adult skin cell and reactivating developmentally regulated genes -reprogramming the cell directly to become an embryonic 'induced' pluripotent stem (iPS) cell (see Figure 1).

As more is understood about the molecular mechanisms of differentiation, recent progress has shown how embryonic and pluripotent stem cells can be differentiated into adult cell types with a particular morphology and phenotype without needing to recreate the whole organism. Fortunately human embryonic stem cells can differentiate relatively easily into RPE cells, possibly because they arise early in during embryogenesis, [START_REF] Haruta | In vitro and in vivo characterization of pigment epithelial cells differentiated from primate embryonic stem cells[END_REF] and similar techniques can be applied to iPS cells to regenerate RPE cells in vitro, [START_REF] Buchholz | Derivation of functional retinal pigmented epithelium from induced pluripotent stem cells[END_REF] which show similar properties to EScell derived RPE in vivo. [START_REF] Carr | Protective effects of human iPSderived retinal pigment epithelium cell transplantation in the retinal dystrophic rat[END_REF] A drawback of using stem cells, however, is that these cells may de-differentiate within the subretinal space, potentially giving rise to teratoma formation. In one study of embryonic stem cell derived neural precursor cells injected into the mouse subretinal space, over 50% of eyes had developed teratomas within 8 weeks following injection. [START_REF] Arnhold | Neurally selected embryonic stem cells induce tumor formation after long-term survival following engraftment into the subretinal space[END_REF] Conversely, another study using 18 different human embryonic stem cell lines showed no evidence of tumour formation, [START_REF] Lund | Human embryonic stem cellderived cells rescue visual function in dystrophic RCS rats[END_REF] perhaps due to more stringent selection of appropriate cell lines. With induced pluripotent stem cells there are additional concerns about using the oncogenic c-Myc transcription factor, but recent developments have shown that iPS cells can be derived without c-Myc [START_REF] Yu | Induced pluripotent stem cell lines derived from human somatic cells[END_REF][START_REF] Nakagawa | Generation of induced pluripotent stem cells without Myc from mouse and human fibroblasts[END_REF][START_REF] Ebert | Induced pluripotent stem cells from a spinal muscular atrophy patient[END_REF] , albeit with a reduced yield of cells. Furthermore, there is now evidence that human iPS cells may be derived using non-integrating episomal vectors, [START_REF] Yu | able to de-differentiate fibroblast cells into induced pluripotent stem (iPS)[END_REF] which theoretically reduces the risk of tumour formation and host gene mutagenesis. Hence earlier safety concerns with iPS cells are now being addressed.

Conclusions

Stem cell technology is moving rapidly and it is highly likely that within the next decade we may have the ability to take a skin sample from an AMD patient and return it to them as a fully differentiated and healthy RPE monolayer suitable for autologous transplantation. The unknown question relates again to the scaffold on which these cells might be placed to restore the function of Bruch's membrane and the technical challenges of transplanting RPE cells into the subretinal space without causing damage to surrounding tissues. These particular problems and solutions are best addressed by ophthalmologists and it is therefore vital that we take time to follow developments in the stem cell field carefully and use our clinical expertise to guide progress towards future treatments. It is also possible that if we can solve the scaffold problem, we may be able to go back and reassess the option of using not stem cells, but suspensions of autologous RPE cells harvested from the retinal equator in patients with AMD. Hence we may be led into solving an old problem by developing a new surgical technique that may not actually require stem cells at all. cells by reactivating embryonic genes: Key: Klf4, Kruppel-like factor 4; Oct 4, Octamer 4; RA, SOX2, sex determining region Y-box 2; c-Myc, chromosomal-Myelocytomatosis gene. These transcription factors are believed to act through methylation mechanisms on the histone proteins that bind DNA into secondary coils. Collectively they provide a molecular switch to reactivate embryonic genes that are otherwise dormant in adult differentiated cells. In somatic cell nuclear transfer (the method used to clone Dolly the sheep) undefined factors in oocyte cytoplasm reprogram DNA extracted from the adult cell and injected into the oocyte through a similar process. The advantage of applying these transcription factors directly to the adult cell is that no oocyte is required to make iPS cells.

These iPS cells could subsequently be differentiated into retinal pigment epithelial cells for autologous transplantation back into a patient with age-related macular degeneration.

Figure legend: 1 Figure: 1

 11 Figure legend: 1 Figure: 1 x 600 dpi, 8 bit RGB colour, 18.50 cm x 9.41 cm JPEG

Acknowledgements EL is a Wellcome Trust Clinical Training Fellow; REM is a Health Foundation Clinician Scientist Fellow. This research is also supported by the Medical Research Council, the Royal College of Surgeons of Edinburgh, Fight for Sight, the John Fell Fund of Oxford University Press, the Special Trustees of Moorfields Eye Hospital and the NIHR Ophthalmology Biomedical Research Centre. The authors declare no conflicts of interest with anything discussed in this article.

Licence for Publication

The Corresponding Author has the right to grant on behalf of all authors and does grant on behalf of all authors, an exclusive licence (or non exclusive for government employees) on a worldwide basis to the BMJ Publishing Group Ltd and its Licensees to permit this article (if accepted) to be published in BJO editions and any other BMJPGL products to exploit all subsidiary rights, as set out in the licence (http://group.bmj.com/products/journals/instructions-forauthors/licence-forms/).