Matthias Puech
email: puech@cs.unibo.it

Yann Régis-Gianas

Safe Incremental Type Checking

Keywords: D.3.3 [Language Constructs and Features]: Data types and structures; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs -Logics of programs General Terms Theory, Languages incrementality, type checking, logical framework, version control

We study the problem of verifying the well-typing of terms, not in a batch fashion, as it is usually the case for typed languages, but incrementally, that is by sequentially modifying a term, and reverifying each time only a smaller amount of information than the whole term, still ensuring that it is well-typed.

Introduction

As programs grow and type systems become more involved, writing a correct program in one shot becomes quite difficult. On the other hand, writing a program in many correct steps is the usual practice when the time for verification is negligible; the verification tool then rechecks the entire development at each step. But this gets more tedious especially when the language in question contains proof aspects, and verification involves proof search. Some mechanisms already exist to cope with the incrementality of proofs or program development: separate compilation, interactive toplevel with undo, tactic languages; they all provide in different ways a rough approximation of the process of modifying and checking incrementally a large term.

We propose here an architecture for a generic and safe incremental type checker, a data structure for repositories of typed proofs and a language for describing proof deltas. It is based on the simple idea of sharing common subterms to avoid rechecking, and exploits encoding a derivation in a metalanguage to guarantee the well-typing of the result. This way, given a signature declaring the typing rules and an (untrusted) typing algorithm for my language of choice, I get an incremental type checker for that language. The metalanguage approach gives us the ability to encode all the aforementioned usual incrementality mechanisms in a typesafe way, and more, making our system akin to a typed version control system.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. To copy otherwise, to republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. TLDI '12 January 28 2012, Philadelphia, USA. Copyright c 2012 ACM [to be supplied]. . . $10.00

Sharing-based incrementality

As a first example, let us consider a purposedly simplistic sorted language of boolean and arithmetic expressions:

e, e ′ ::

= n | e + e ′ | e ∧ e ′ | e ≤ e ′
The algorithm to determine in a batch fashion whether the term

e1 = (1 + 3 ≤ 2 + 4) ∧ (8 ≤ 3)
is well-sorted is trivial (we don't care about its evaluation here, just its well-sortedness). But what if I then change subterm 2 + 4 in e1 into 7 ≤ 2 + 4, to obtain e2? Clearly, it should be verified that context 7 ≤ [] is well-sorted (it is), that 2 + 4 "fits" into its hole (it does), that the whole expression "fits" into its new context

(1 + 3 ≤ []) ∧ (8 ≤ 3) (it
does not); but the other, unchanged subterms need not be verified again. To achieve this incremental verification, the system would have to "remember" the states of the verifier in some way.

If only we had names (memory addresses, hashes) for enough subterms of our initial term,

e1 = ( X 1 + 3 ≤ Y 2 + 4) ∧ Z (8 ≤ 3) ,
we could express concisely the change as a delta δ1 = (X ≤ (7 ≤ Y )) ∧ Z , using these names to refer to unchanged subterms. If only we had annotated our initial term with the states of the verifier, e1 = (

X:N 1 + 3 ≤ Y :N 2 + 4) ∧ Z:B (8 ≤ 3) ,
we would have a simple process to verify e2 taking advantage of e1's derivation, in O(|δ2|): verify δ1 as a term, retrieving the sort of names from a stored map. This suggests a data structure for a repository of named, annotated, verified subexpressions: a monotonously growing map, from names, or metavariables, to terms and types, together with a head metavariable identifying the top of the expression: R ::= X, ∆ where ∆ : (X → M : A) .

A metalanguage to encode derivations

What language are terms M and types A written into? Terms should encode our expressions with metavariables, and types A should encode the whole state of the batch verifier (here the sort). An obvious choice is to take M ::= (e with metavariables) and A ::= B | N, but switching to another language, we'd have to redefine another repository language. Moreover, this choice is no longer expressive enough when introducing binders. Another more modular choice for this is the metalanguage LF [START_REF] Harper | A framework for defining logics[END_REF]: it allows to specify syntax and rules of an object language as a signature Σ, and check terms against this signature with a generic algorithm. We'll use an increasing fragment of it. The so-called intrinsic style of LF signature for our expression language is: The encoded expressions are however very verbose: each term constructor takes as argument all these annotations. We can nonetheless make these information implicit in terms (but explicit in types) and let a reconstruction algorithm infer them, as in [START_REF] Necula | Efficient representation and validation of proofs[END_REF]. This reconstruction is language-dependent, user-provided but does not impair the safety of the system for the whole term is still checked afterwards.

tp : *
LF promotes the use of lambda-tree syntax to represent binders: instead of encoding the syntax first-order, it uses the λ binder built in LF to encode binders in the object language. This style of encoding has the advantage of making the manipulation of the environment (weakening, exchange. . . ) implicit in the deltas, but raises new challenges for the delta language and the verification process: how to share a subterm underneith a lambda? How to efficiently verify that such a delta is well-typed?

Expressivity

Aside from enabling to encode a large class of deductive systems safely and generically, the metalanguage approach allows to express incrementality features usually implemented in an ad-hoc manner, simply by adding new constants to the signature.

Version control Suppose we want to implement an undo system, storing successive versions of a closed expression of sort bool and able to rollback to a previous version. We add constants version : * , vnil : version, vcons : exp nil bool → version → version to the signature. The empty repository is now represented as vnil. Each time we have pushed a full expression M , and if S was the previous head (a version called its ancestor), we push vcons M S. This gives us a data structure for an undo stack, and a commit algorithm. But the sharing inherent to our repositories lets us actually represent trees of versions, by sharing common stack tails, each list head being a branch. Reconciling two branches' changes into a unique head is called merging in version control system's terminology: a merge is a version with several ancestors. We can represent merges by revising our previous addition to the signature into version : * , ancestors : * , anil : ancestors, acons : version → ancestors → ancestors, vcons : exp nil bool → ancestors → version This defines a data structure to represent (acyclic) graphs of versions; it is the exact data structure of repository used by version control systems Git, Monotone and Mercurial (see e.g. [START_REF] Chacon | Git community book. The Git Community[END_REF]) except that where they have directories and text files we have arbitrary typed terms.

Top-down construction While our system is based on bottom-up term construction, we can encode top-down construction common to some programming environments (e.g. Agda) and tactic-based proof assistants (e.g. Coq). The user constructs terms by successively filling holes with terms containing other holes. To add (linear) holes to our expressions, add constant hole : ΠE : env. ΠA : tp. exp E A to the signature. To instantiate a hole with an expression, commit the substituted term preserving sharing of subterms.

Architecture

We can implement this system following a layered architecture.

The kernel is the component in charge of verifying terms against a signature and a repository, and updating this repository. It supports two basic operations:

• push Σ (R, M ) checks a small part M of a larger term against Σ in R, synthetizes its type A, chooses a fresh metavariable X for M and returns R[X → M : A] and X.

• pull Σ (R, X) returns the term M associated with X in R recursively: all metavariables are unfolded to their definitions.

The slicer is the component in charge of slicing a term M into many terms, pushing them to the repository to enable future sharing, and adding version markers. It supports operations:

• commitΣ(R, M ) pushes vcons M (acons X anil) to R in several push() operations, where X is the current head.

• merge Σ (R, M, Y ) pushes vcons M (acons X (acons Y anil)) to R. Note that it doesn't actually perform the merge, it simply commits a previously computed merge node with value M .

The reconstructor performs the reconstruction of the derivation (an M ) from the initial expression (an e), given the derivations for its metavariables (an R), and the expected type (exp nil bool), and commits M .

Finally, the compressor computes a delta e ′ from a metavariablefree expression e by recognizing equal subterms in R. This can be achieved by hash-consing.

  , nat : tp, bool : tp, exp : tp → nat, atom : N → exp nat, plus : exp nat → exp nat → exp nat, and : exp bool → exp bool → exp bool, leq : exp nat → exp nat → exp boolIn this style, both the encoding of an expression and its sort are terms in the metalanguage, but the sort appears in the type of the encoded expression. As an example, the repository associated with expression e1 isThe dependent nature of types in LF allows to express more complex languages. We can for example add functions, applications and variables to our expressions in a purely first-order style (using de Bruijn indices for variables) if we annotate them not only with sorts but with an environment of free variables:

	T,	  	X → plus 1 3 : exp nat Y → plus 2 4 : exp nat Z → leq 8 3 : exp bool T → and (leq X Y ) Z : exp bool	  

exp : env → tp → * , atom : ΠE : env. N → exp E nat, var : ΠE : env. ΠA : tp. var E A → exp E A, leq : ΠE : env. exp E nat → exp E nat → exp E bool, lam : ΠE : env. ΠA, B : tp. exp (cons A E) B → exp E (arr A B) . . .


Hagit Attiya

Armando Castañeda
email: armando.castaneda@inria.fr

A non-topological proof for the impossibility of k-set agreement

Keywords: Set agreement, Shared memory, Wait-freedom

In the k-set agreement task each process proposes a value, and it is required that each correct process has to decide a value which was proposed and at most k distinct values must be decided. Using topological arguments it has been proved that k-set agreement is unsolvable in the asynchronous wait-free read/write shared memory model, when k < n, the number of processes. This paper presents a simple, non-topological impossibility proof of k-set agreement. The proof depends on two simple properties of the immediate snapshot executions, a subset of all possible executions, and on the well known graph theory result stating that every graph has an even number of vertices with odd degree (the handshaking lemma).

Introduction

In a breakthrough result, Fischer, Lynch and Paterson proved [START_REF] Fischer | Impossibility of Distributed Consensus with One Faulty Process[END_REF] that it is impossible to solve consensus in the asynchronous message passing system in which at most one process, which is unknown in advance, can crash. Herlihy [START_REF] Herlihy | Wait-free synchronization[END_REF] and Loui and Abu-Amara [START_REF] Loui | Memory requirements for agreement among unreliable asynchronous processes[END_REF] extended this impossibility result to the asynchronous wait-free read/write shared memory model, where wait-free means that in each execution all processes but one can fail by crashing. Recall that in the consensus task, each process proposes a value, and it is required that every correct process decides on a value proposed by some process and no two correct processes decide distinct values.

Later, in order to study the border between solvable and unsolvable tasks in presence of asynchrony and failures, Chaudhuri [START_REF] Chaudhuri | More Choices Allow More Faults: Set Consensus Problems in Totally Asynchronous Systems[END_REF] introduced a natural generalization of consensus, called k-set agreement; in this task, each process proposes a value and it is required that each correct process decides on a value proposed by a process and at most k ≥ 1 distinct values are decided. For k = 1, k-set agreement is exactly consensus, and for k = n, the number of processes in the system, k-set agreement is trivial, since every process can decide on its proposal. The paper shows that k-set agreement can be solved by a t-resilient asynchronous algorithm, when t < k. An algorithm is t-resilient, 1 ≤ t ≤ n -1, if it solves the problem even in executions where up to t processes crash. This means that if the number of failures is strictly smaller than the number of possible decision values, then k-set agreement is solvable. Chaudhuri [START_REF] Chaudhuri | More Choices Allow More Faults: Set Consensus Problems in Totally Asynchronous Systems[END_REF] also conjectured that k-set agreement is unsolvable if t ≥ k. For the case k = 1, this conjecture matches the impossibility of solving consensus, namely, 1-set agreement, with a single crash failure [START_REF] Herlihy | Wait-free synchronization[END_REF][START_REF] Loui | Memory requirements for agreement among unreliable asynchronous processes[END_REF]. Notice that for the the wait-free case, i.e., t = n -1, this conjecture says that only the trivial n-set agreement task has a wait-free solution.

Chaudhuri's conjecture was proved by Borowsky and Gafni [START_REF] Borowsky | Generalized FLP Impossibility Result for t-Resilient Asynchronous Computations[END_REF], Herlihy and Shavit [START_REF] Herlihy | The Topological Structure of Asynchronous Computability[END_REF] and Saks and Zaharoglou [START_REF] Saks | Wait-Free k-Set Agreement Is Impossible: The Topology of Public Knowledge[END_REF]. Indeed, these three papers discovered a strong relationship between distributed computing and topology and used this topological approach for proving the conjecture of Chaudhuri. Later, Attiya and Rajsbaum [START_REF] Attiya | The Combinatorial Structure of Wait-Free Solvable Tasks[END_REF] and Herlihy and Rajsbaum [START_REF] Herlihy | Algebraic Spans[END_REF] presented two other topological impossibility proofs of k-set agreement. Although these proofs are not extremely complicated, they use concepts and results that are not widely known by the distributed computing community; the kind of arguments they use vary from combinatorial and algebraic to continuous arguments.

This paper presents a simple, non-topological impossibility proof for k-set agreement. This proof does not demand from the reader any previous knowledge of topology at all. Very roughly, the proof considers the immediate snapshot (IS) executions [START_REF] Attiya | The Combinatorial Structure of Wait-Free Solvable Tasks[END_REF][START_REF] Borowsky | Generalized FLP Impossibility Result for t-Resilient Asynchronous Computations[END_REF][START_REF] Borowsky | Immediate Atomic Snapshots and Fast Renaming[END_REF][START_REF] Saks | Wait-Free k-Set Agreement Is Impossible: The Topology of Public Knowledge[END_REF] of an algorithm, a subset of all possible executions, and constructs a graph, whose vertices are the IS executions, and whose edges connect two IS executions (vertices) only if they satisfy certain indistinguishability conditions. Then, using the well known handshaking lemma, stating that every graph has an even number of vertices with odd degree, the proof concludes that there must be at least one execution in which at least k + 1 values are decided.

We believe that it is valuable to have several proofs of this important result, since they provide different perspectives on it. In particular, the proof we present in this paper gives an operational insight into the impossibility of set agreement. Such a perspective cannot be easily obtained from the known topological impossibility proofs for k-set agreement.

We stress that this paper does not argue that the use of topology for proving the impossibility of k-set agreement is "artificial", namely, that topology has been used before as a "trick" for proving the result. The reader has not to understand this paper in that way. The fundamental reason why k-set agreement is not solvable is topological, and more precisely, it has to do with Sperner's lemma [10, p. 36]. We strongly encourage the reader to see the connections between the proof we present here and Sperner's lemma. Moreover, we believe that the topological approach to distributed computing must be studied and extended, since it has been extensively and successfully used in the past for proving a variety of results (see, for example, [START_REF] Castañeda | New Combinatorial Topology Upper and Lower Bounds for Renaming[END_REF][START_REF] Gafni | Three-Processor Tasks Are Undecidable[END_REF][START_REF] Gafni | Subconsensus Tasks: Renaming is Weaker Than Set Agreement[END_REF][START_REF] Herlihy | Set Consensus Using Arbitrary Objects (Preliminary Version)[END_REF][START_REF] Herlihy | A Classification of Wait-free Loop Agreement Tasks[END_REF][START_REF] Hoest | Toward a Topological Characterization of Asynchronous Complexity[END_REF]), and it is unlikely that all these results have non-topological proofs.

The paper is organized as follows. Section 2 describes the asynchronous waitfree read/write shared memory model. Section 3 presents the subset of IS executions, which is used for proving the impossibility of k-set agreement in Section 4. Finally, Section 5 provides an operational perspective of this proof.

Model of computation

This section describes the standard asynchronous wait-free read/write shared memory model, considered in this paper, following [START_REF] Attiya | The Combinatorial Structure of Wait-Free Solvable Tasks[END_REF][START_REF] Attiya | Distributed Computing: Fundamentals, Simulations and Advanced Topics[END_REF]. System and executions. A system consists of n asynchronous sequential processes p 1 , . . . , p n . Each process is a deterministic state machine with a (possibly infinite) set of local states S and two subsets of S called initial states and output states, respectively. The processes communicate by using a shared memory with a finite number of single-writer multi-reader atomic registers. No assumption is made regarding the size of the registers, thus we can assume that process p i has a single register r i to which it can write its entire state. Process p i has two atomic operations available to it: write i (v) that writes the value v into r i , and read i (j) that returns the current value in r j . A step is performed by a single process p i , which executes one of its two available operations, read i or write i , performs some local computation and then changes its local state.

A configuration of the system consists of the local states of the processes and the content of the registers. An initial configuration is a configuration in which all local states are initial states and all registers are set to a distinguished value ⊥. An output configuration is a configuration in which all local states are output states.

An execution of the system is a, possibly infinite, alternating sequence of configurations and steps α = C 0 , s 0 , C 1 , s 1 , C 2 , . . ., where C 0 is an initial configuration and C +1 is the result of applying the step s to C , for ≥ 0. The view of a process p i in α, denoted α|p i , is the sequence of p i 's local states in configurations C 0 , C 1 , . . .. The participating set of an execution α, denoted ps(α), is the set of processes that take at least one step in the execution.

Two executions α and α are indistinguishable for a set of processes P , denoted α ∼ P α , if all processes in P have the same view in both executions, namely, ∀p i ∈ P, α|p i = α |p i . In the following section we are interested in pairs of executions α and α that are distinguishable to exactly one process, that is, there is a process p i such that α|p i = α |p i and α ∼ P α , where P = {p 1 , . . . , p n } \ {p i }.

In this case, we write α ∼ ¬pi α .

Algorithms. The state machine of a process p i models a local algorithm A i that determines p i 's next step. An algorithm A is a collection of local algorithms A 1 , . . . , A n .

Each process has two distinguished components, input and output, that allow the system to model decision tasks. The input component never changes and cannot contain the distinguished value ⊥. The output component contains initially ⊥, and once a process reaches a local state in which a non-⊥ value is written in it, the output component never changes. When that happens, we say that the process decides. The output states are the states with non-⊥ output values. If a process decides v in an execution α, we say v is decided in α.

A view of a process p i in a finite execution α is final, if p i decides in α. A final view of p i in α is minimal if none of its prefixes is final. In other words, the minimal final view of p i in α is the prefix of the view of p i up to the first configuration in which p i decides. A finite execution α is minimal final if the view of each process in ps(α) is a minimal final; in particular, each participating process decides in α. For a minimal final execution α, dec(α) is the set of all the values that are decided in α, and for a process p i ∈ ps(α), dec(α, ¬p i ) is the set dec(α) \ {v}, where v is the value that p i decides in α. Note that if two distinct processes p i and p j decide on the same value v, then dec(α, ¬p i ) = dec(α, ¬p j ).

An algorithm A is wait-free if in each execution of A, every process executes a finite number of steps or decides. Therefore, a process must decide if it executes an infinite number of steps. We only consider wait-free algorithms.

An algorithm is full-information if a process writes its entire local state in every write operation. We say that an algorithm is in standard-form if processes proceed in a sequence of asynchronous rounds. In a round, every process first executes a write operation and then asynchronously reads all registers. Note that if there is a wait-free algorithm solving some task, then there is a, possibly inefficient, full-information and standard-form wait-free algorithm solving this task. Since efficiency is not an issue in this paper, we only consider full-information and standard-form algorithms.

k-set agreement. In k-set agreement [START_REF] Chaudhuri | More Choices Allow More Faults: Set Consensus Problems in Totally Asynchronous Systems[END_REF], 1 ≤ k ≤ n, each process p i proposes a value has to decide on a value, such that the following properties hold.

Termination: Each process executes a finite number of steps or decides. Validity: A decided value is a proposed value. k-Agreement: At most k different values are decided.

We now define a trivial task T that will be used in the impossibility proof of k-set agreement. Indeed, in Section 4 we shall see that every wait-free algorithm that solves T possesses a property which implies that there is no algorithm that solves k-set agreement for k < n.

In the task T each process p i proposes a value and each process has to decide a value such that the termination and validity properties of k-set agreement are satisfied. Obviously, T is wait-free solvable: Each process can just decide it proposal, or each process can decide the smallest proposed value it sees in the shared memory. The following lemma is immediate from the definition of k-set agreement and T . Lemma 1. Any wait-free algorithm that solves k-set agreement for some k, 1 ≤ k ≤ n, also solves T .

Immediate snapshot executions

Consider a full-information and standard-form wait-free algorithm. The immediate snapshot executions of this algorithm form a subset of all its possible executions. The executions in this set have a structure that makes them easier to analyze.

An immediate snapshot (IS) execution [START_REF] Attiya | The Combinatorial Structure of Wait-Free Solvable Tasks[END_REF][START_REF] Borowsky | Generalized FLP Impossibility Result for t-Resilient Asynchronous Computations[END_REF][START_REF] Borowsky | Immediate Atomic Snapshots and Fast Renaming[END_REF][START_REF] Saks | Wait-Free k-Set Agreement Is Impossible: The Topology of Public Knowledge[END_REF] is modeled by a sequence of non-empty sets of processes α = s 1 , . . . , s l , . . .. Processes in s l first perform, one by one, a write operation and then read all registers. Intuitively, the processes execute a concurrent write followed by a concurrent atomic snapshot of the shared memory. If p i ∈ s l , then we say that p i is active in the l-th set of α.

Since we only consider wait-free algorithms, we can restrict our attention to minimal final IS executions, namely, each process executes computation steps until it decides. Indeed, each process decides in the last round in which it is active. We sometimes write α as a concatenation of sequences of sets, i.e., α = α 1 α 2 , where α 1 = s 1 s 2 . . . s and α 2 = s +1 s +2 . . . s t .

For example, α = {p, q} {r} denotes an IS execution made of 2 sets. Processes p and q are active in the first set and r is active in the second one. Observe that p and q see each other, but do not see r because it executes steps of computation after p and q read the whole memory.

Although IS execution are well-structured they still have uncertainty, as the following example shows. In addition to the execution α described in the previous paragraph, consider the IS execution α = {p} {q} {r}. Note that p only sees itself in α while sees itself and q in α. The reader can verify that the views of q and r are the same in α and α . Therefore, α ∼ ¬p α . For a sequence α = s 1 s 2 . . . s t of sets of processes and a process p i , we write p i / ∈ α if p i / ∈ s for every , 1 ≤ ≤ t, . Alternatively, we say that p i does not appear in α. Also, for p i and r ≥ 1, we let {p i } r denote the sequence containing r times the set {p i }.

Formally, we say that a process p i is unseen in an IS execution α = s 1 s 2 . . . s t if and only if there exists , 1 ≤ ≤ t -1, such that p i / ∈ s x , 1 ≤ x ≤ and s y = {p i }, < y ≤ t. Therefore, if p i is unseen in α, then α = α {p i } r , for some r ≥ 1 and α , such that p i / ∈ α . Intuitively, p i is unseen in α since every step of p i occurs after all other processes decided. A process p i is seen in an IS execution α if it is not unseen in α.

Lemmas 2 and 3 below are from [START_REF] Attiya | The Combinatorial Structure of Wait-Free Solvable Tasks[END_REF]. They capture two properties about the uncertainty in minimal final IS executions. They will be used in the impossibility proof of k-set agreement presented in the following section. Lemma 2 is Lemma 3.3 in [START_REF] Attiya | The Combinatorial Structure of Wait-Free Solvable Tasks[END_REF] and Lemma 3 is a restatement of Lemma 3.4 in [START_REF] Attiya | The Combinatorial Structure of Wait-Free Solvable Tasks[END_REF].

Lemma 2. If a process p i is unseen in a minimal final IS execution α, then there is no minimal final IS execution α such that α ∼ ¬pi α .

Lemma 3. Let α be a minimal final IS execution in which a process p i is seen. Then there is a unique minimal final IS execution α such that α ∼ ¬pi α .

Let A be a wait-free algorithm. For any given collection C of inputs to the processes, let S be the set containing all minimal final IS executions of A in which the processes start with inputs C. For a subset P of processes, let P S P (S) be the set containing all executions in S with participating set P . If there is no ambiguity, we write P S P instead of P S P (S).

For a proper subset of processes P and a process p / ∈ P , the next lemma shows that there is a one-to-one correspondence between the executions in P S P and the executions in P S P ∪{p} in which p is unseen. Lemma 4. For every proper subset of processes P and a process p i / ∈ P , the following properties hold:

1. For every execution α ∈ P S P there is a unique execution α ∈ P S P ∪{pi} such that p i is unseen in α and α is equal to the maximal prefix of α in which p i does not appear. 2. For every execution α ∈ P S P ∪{pi} such that p i is unseen in α, P S P contains the maximal prefix α of α in which p i does not appear.

Proof. First let us consider an execution α ∈ P S P . Since A is asynchronous waitfree, α can be extended to a minimal final execution α with ps(α ) = P ∪ {p i }, namely, α = α {p i } r , for some r ≥ 1. Thus α ∈ P S P ∪{pi} . Note that p i is unseen in α because by hypothesis p i / ∈ α. In addition, α is the maximal prefix of α in which p i does not appear. Moreover, α is unique because A is deterministic. Now let us consider an execution α ∈ P S P ∪{pi} such that p i is unseen in α. We have that α = α {p i } r , for some r ≥ 1 and p i / ∈ α . Note that α is the maximal prefix of α in which p i does not appear. Moreover, α ∈ P S P because, by hypothesis, each process that appears in α executes steps of computation until it decides, namely, it is a minimal final IS execution with ps(α ) = P .

Impossibility of k-set agreement

This section is devoted to proving the impossibility of the k-set agreement task in the asynchronous wait-free read/write shared memory model (Theorem 1). The core of the proof is Lemma 6, roughly showing that every wait-free algorithm solving the task T (defined in Section 2) maintains an invariant concerning the number of its executions in which distinct processes decide distinct values. Indeed this lemma can be regarded as the operational counterpart of the Sperner's lemma [10, p. 36]. Then, using Lemma 1 and the invariant in Lemma 6, we conclude that k-set agreement is not wait-free solvable.

Let A be a wait-free algorithm that solves T . Consider n distinct input values v 1 , . . . , v n and let S be the set containing all minimal final IS executions of A in which process p i has input v i , 1 ≤ i ≤ n.

Recall that P S P is the set of all executions in S with participating set P . The next simple lemma directly follows from the validity property of T , and it is used in the proof of Lemma 6 below. Lemma 5. For every subset of processes P and for every execution α ∈ P S P , dec(α) contains only the inputs of processes in P .

When P = {p 1 , . . . , p t }, 1 ≤ t ≤ n, we write P S t instead of P S P . Lemma 6. For all t, 1 ≤ t ≤ n, P S t contains exactly an odd number of executions α 1 , . . . , α 2q+1 , q ≥ 0, such that dec(α j ) = {v 1 , . . . , v t }, 1 ≤ j ≤ 2q + 1.

Intuitively, the proof of Lemma 6 proceeds by constructing a graph G using the executions in P S t as vertices and putting an edge between two executions α, α ∈ P S t if and only if at most one process distinguishes between them and at least t -1 distinct values are decided in α and α . The graph G also contains an "imaginary" vertex v * , which is defined in such a way that it has odd degree. This guarantees that G contains at least one vertex with odd degree. All other vertices of G with odd degree, if they exist, correspond to the executions of P S t in which the values v 1 , . . . , v t are decided. Let M be the set containing all vertices of G with odd degree except v * . Using the well known handshaking lemma, stating that every graph has an even number of vertices with odd degree, 3 the proof finally concludes |M ∪ {v * }| is even, hence |M | is odd, which proves the lemma.

Proof (of Lemma 6). We proceed by induction on t. For t = 1, P S 1 only contains p 1 's solo execution, that is, P S 1 only contains α = {p 1 } r , for some r ≥ 1. Obviously, p 1 must decide v 1 in α, which proves the base of the induction. Now suppose that the lemma holds for t, 1 ≤ t ≤ n -1. We prove it holds for t + 1.

We define a graph G = (V, E) whose vertices are the executions in P S t+1 , plus an additional vertex v * , that is, V = P S t+1 ∪ {v * }. The edges of G are defined as follows (recall that v i is the input of process p i ).

-For every pair of executions α, α ∈ P S t+1 , (α, α ) ∈ E if and only if there is a process p i such that α ∼ ¬pi α and dec(α,

¬p i ) = {v 1 , . . . , v t }; hence, dec(α , ¬p i ) = {v 1 , . . . , v t }.
-For every execution α ∈ P S t+1 , (v * , α) ∈ E if and only if p t+1 is unseen in α and dec(α, ¬p t+1 ) = {v 1 , . . . , v t }.

Fig. 1 depicts an example of the graph G constructed in the inductive step t = 2 for a one-round algorithm for three processes p, q and r. In the algorithm, a process decides its proposal if it sees less than 2 processes. Otherwise, if it sees that its proposal is not the largest one, then decides the smallest proposal, and it decides the second smallest proposal in any other case. In Fig. 1 the inputs for p, q and r are 1, 2 and 3, respectively, and process r corresponds to p t+1 . In each execution, above each process it appears the value that the process decides in that execution. Observe that there is an edge between executions α = {p} {q, r} and α = {p, q, r} because, first, α ∼ ¬p α (p sees no other process than itself in α while it sees q and r in α ), and second, q and r decide 1 and 2, respectively, in α. Also there is an edge between v * and α = {p, q} {r} because r is unseen in α and p and q decide 1 and 2. Finally, note that there is no edge between α = {p, q, r} and α = {r} {p, q} because although α ∼ ¬r α , both p and q decide 1 in α.

For the rest of the proof, let deg(v) denote the degree of a vertex v of G. Below, we prove the following properties about the degrees of the vertices in G.

1. deg(v * ) is odd.
3 This result is a consequence of Euler's observation that for every graph G = (V, E),

P v∈V deg(v) = 2 |E|.

For all α ∈

P S t+1 = V \ {v * }: (a) If dec(α) = {v 1 , . . . , v t+1 }, then deg(α) = 1. (b) If dec(α) = {v 1 , . . . , v t }, then deg(α) = 2. (c) Otherwise, deg(α) = 0.
These properties, can be use to derive the induction step, together with the next well-known result of graph theory.

Handshaking Lemma. Every graph has an even number of vertices with odd degree. The vertices of G with odd degree are exactly M ∪ {v * }, where M is the set that contains every execution α ∈ P S t+1 such that dec(α) = {v 1 , . . . , v t+1 }. Thus, by the Handshaking Lemma, |M ∪ {v * }| is even, hence |M | is odd. We now prove the properties of the degrees. deg(v * ) is odd. Consider an execution α ∈ P S t . By Lemma 4(1), there is a unique execution α ∈ P S t+1 such that p t+1 is unseen in α and α is equal to the maximal prefix of α in which p t+1 does not appear. Conversely, by Lemma 4(2), for every execution α ∈ P S t+1 such that p t+1 is unseen in α, P S t contains the maximal prefix α of α in which p t+1 does not appear.

By the induction hypothesis, we have that P S t contains exactly an odd number of executions α 1 , . . . , α 2q+1 , q ≥ 0, such that dec(α j ) = {v 1 , . . . , v t }, 1 ≤ j ≤ 2q + 1. Thus for every α j , 1 ≤ j ≤ 2q + 1, there is a unique execution α j ∈ P S t+1 such that p t+1 is unseen in α j and α j is a prefix of α j . Hence, (v * , α j ) ∈ E, since dec(α j , ¬p t+1 ) = {v 1 , . . . , v t } because dec(α j ) = {v 1 , . . . , v t }. Moreover, these are all the edges adjacent to v * because, as explained above, there is a one-to-one correspondence between the executions of P S t and the executions of P S t+1 in which p t+1 is unseen. Therefore, deg(v * ) is odd.

For every execution α ∈ P S t+1 , if dec(α) = {v 1 , . . . , v t+1 }, then deg(α) = 1.

Since |dec(α)| = |{v 1 , . . . , v t+1 }| = t + 1 and |ps(α)| = |{p 1 , . . . , p t+1 }| = t + 1, it follows that for every v ∈ {v 1 , . . . , v t+1 }, there is exactly one process in α that decides v. Let p denote the process that decides v t+1 in α. Thus, dec(α, ¬p) = {v 1 , . . . , v t }. We identify two subcases: p is unseen in α or p is seen in α.

If p is unseen in α, then, by Lemma 4(2), P S P contains the maximal prefix α of α in which p does not appear, where P = {p 1 , . . . , p t+1 } \ {p}. Observe that dec(α ) = {v 1 , . . . , v t }. Lemma 5 and the assumption that each p i has a distinct input v i , imply that P = {p 1 , . . . , p t+1 } \ {p} = {p 1 , . . . , p t }, hence p = p t+1 . Therefore, p t+1 is unseen in α and dec(α, ¬p t+1 ) = {v 1 , . . . , v t }, because as explained above dec(α, ¬p) = {v 1 , . . . , v t }. By definition of G, (v * , α) ∈ E.

We claim that (v * , α) is the only edge that is adjacent to α. First, there is no execution α ∈ P S t+1 such that α ∼ ¬q α with q = p t+1 , by Lemma 2. Second, for every process q ∈ {p 1 , . . . , p t }, dec(α, ¬q) = {v 1 , . . . , v t } because for each v ∈ {v 1 , . . . , v t+1 } there is exactly one process in α that decides v, and q decides on a value in {v 1 , . . . , v t }. These two observations imply that there is no α ∈ P S t+1 such that (α, α ) ∈ E, and hence deg(α) = 1.

For the second subcase, namely, p is seen in α, there is only one execution α ∈ P S t+1 such that α ∼ ¬q α , by Lemma 3. Then (α, α ) ∈ E, because dec(α, ¬p) = {v 1 , . . . , v t }.

The edge (α, α ) is the only edge that is adjacent to α: We have that for every q ∈ {p 1 , . . . , p t }, dec(α, ¬q) = {v 1 , . . . , v t } because for each v ∈ {v 1 , . . . , v t+1 } there is exactly one process in α that decides v, and q decides a value of {v 1 , . . . , v t }. Therefore, there does not exist a α ∈ P S t+1 such that α = α and (α, α ) ∈ E. Hence we get deg(α) = 1.

For every α ∈ P S t+1 , if dec(α) = {v 1 , . . . , v t }, then deg(α) = 2. Since |dec(α)| = |{v 1 , . . . , v t }| = t and |ps(α)| = |{p 1 , . . . , p t+1 }| = t + 1, we get that there must be a value v ∈ {v 1 , . . . , v t } such that there are two distinct processes q 1 , q 2 ∈ {p 1 , . . . , p t+1 } that decide v in α. Therefore, for each i ∈ {1, 2}, dec(α, ¬q i ) = {v 1 , . . . , v t }. Also observe that v is the unique value of {v 1 , . . . , v t } that has that property.

We identify three subcases: q 1 is unseen and q 2 is seen in α, q 1 is seen and q 2 is unseen in α, and both q 1 and q 2 are seen in α. Note that it is impossible that both q 1 and q 2 are unseen.

Consider first the subcase q 1 is unseen and q 2 is seen in α. The argument is similar to the one in the previous case. If q 1 is unseen in α, then, by Lemma 4(2), P S P contains the maximal prefix α of α in which q 1 does not appear, where P = {p 1 , . . . , p t+1 } \ {q 1 }. Observe that dec(α ) = {v 1 , . . . , v t }. Thus, by Lemma 5 and the assumption that each p i has a distinct input v i , we get P = {p 1 , . . . , p t+1 } \ {q 1 } = {p 1 , . . . , p t }, and hence q 1 = p t+1 . Therefore, p t+1 is unseen in α and dec(α, ¬p t+1 ) = {v 1 , . . . , v t }, because dec(α, ¬q 1 ) = {v 1 , . . . , v t }. Hence (v * , α) ∈ E.

For q 2 , by Lemma 3, there is an execution α ∈ P S t+1 such that α ∼ ¬q2 α . Then (α, α ) ∈ E, because dec(α, ¬q 2 ) = {v 1 , . . . , v t }.

If |dec(γ 1 )| = k + 1, then P only contains γ 1 . Otherwise, |dec(γ 1 )| = |D| = k and the proof looks for an execution γ 2 such that there is a process p such that γ 1 ∼ ¬p γ 2 , and hence dec(γ 2 , ¬p) = D. If there is no such execution γ 2 then P only contains γ 1 , otherwise γ 2 is appended to P and the procedure continues by considering γ 2 instead of γ 1 .

In the end we get a path P = γ 1 , γ 2 , . . . , γ s , such that s ≥ 1 and for each i, 1 ≤ i ≤ s -1, there is a process p such that γ i ∼ ¬p γ i+1 and dec(γ i , ¬p) = D. What is important to notice is that the last execution (vertex) γ s of P holds either |dec(γ s )| = k + 1, or |dec(γ s )| = |D| = k and p k+1 is unseen in γ s . In the second case we have that the maximal prefix α of γ s in which p k+1 does not appear, belongs to S. Therefore, in some sense, the path P "matches" α (the maximal prefix of γ 1 in which p k+1 does not appear) to α . For example, in the graph in Fig. 1, the sequence of IS executions {p q} {r}, {q} {p} {r} matches {p q} to {q} {p}. However, only an even number of execution of S can be matched in this way, and since |S| is odd, we get that there must be a path that matches an α ∈ S to an execution in which k + 1 values are decided. In Fig. 1, the path that starts at {p} {q} {r} and ends at {q} {r} {p}, matches {p} {q} to {q} {r} {p}.

Finally, an execution γ with |dec(γ)| = k + 1, that is not matched to an execution in S, is matched to an execution γ with |dec(γ )| = k + 1. In Fig. 1, {q r} {p} is matched to {r} {q} {p}.

Fig. 1 .

 1 Fig.1. Graph associated with a 3-process 1-round algorithm.

Acknowledgments:

The second author would like to thank Michel Raynal and Julien Stainer for useful discussions and comments on earlier versions of this paper.

We claim that (v * , α) and (α, α ) are the unique edges adjacent to α. First, for q 1 , there is no execution α ∈ P S t+1 such that α ∼ ¬q1 α , by Lemma 2. Second, for q 2 , there is no α = α such that α ∼ ¬q2 α , by Lemma 3. And third, for every process q ∈ {p 1 , . . . , p t+1 } distinct from q 1 and q 2 , dec(α, ¬q) = {v 1 , . . . , v t } because q decides on a value in {v 1 , . . . , v t } and, as mentioned above, there is no other process in {p 1 , . . . , p t+1 } that decides the same value as q. Therefore, deg(α) = 2.

The subcase in which q 1 is seen and q 2 is unseen in α is symmetric to the previous one.

For the third subcase, that is, q 1 and q 2 are seen in α, for each i ∈ {1, 2} there is an execution

As in the first subcase, it can be easily proved that there is no extra edge that is adjacent to α. Hence deg(α) = 2.

Otherwise, deg(α) = 0. We have two subcases: |dec(α)| < t, or |dec(α)| = t and dec(α) = {v 1 , . . . , v t }. In both subcases, for every process p ∈ {p 1 , . . . , p t+1 }, dec(α, ¬p) = {v 1 , . . . , v t }, hence it follows from the definition of G that deg(α) = 0.

Theorem 1. There is no wait-free algorithm that solves k-set agreement for k < n.

Proof. Suppose that there is a wait-free algorithm A that solves k-set agreement, for some k, 1 ≤ k ≤ n -1. By Lemma 1, A solves T . Consider n distinct input values v 1 , . . . , v n and let S be the set containing all minimal final IS executions of A in which process p i has input v i , 1 ≤ i ≤ n. Consider the set P S k+1 (S), namely, the set containing all executions in S with participating set p 1 , . . . , p k+1 . By Lemma 6, P S k+1 (S) contains an execution α such that |dec(α)| = k + 1. But this contradicts the fact that A solves k-set agreement, since the k-agreement property means that in all executions α ∈ P S k+1 (S), |dec(α)| ≤ k.

An operational perspective

From an operational perspective we can think of the proof of Lemma 6, and hence the impossibility proof of k-set agreement, in the following way.

The induction hypothesis of the proof states that there is an odd number of minimal final IS executions α 1 , . . . , α 2q+1 , q ≥ 0, such that for each α ∈ S = {α 1 , . . . , α 2q+1 }, ps(α) = {p 1 , . . . , p k } and dec(α) = D = {v 1 , . . . , v k }, where v i is the input of p i , 1 ≤ i ≤ k. Namely, k processes decide k distinct values in α. As explained in the proof, each α ∈ E can be extended to a minimal final IS execution γ 1 such that ps(γ 1 ) = {p 1 , . . . , p k+1 } and p k+1 is unseen in γ 1 . Thus, α is the maximal prefix of γ 1 in which p k+1 does not appear, hence p k+1 decides after all processes p 1 , . . . , p k decide in γ 1 . Moreover, dec(γ 1 , ¬p k+1 ) = D because dec(α) = D. Let us fix α and γ 1 .

Then, taking advantage of the uncertainty related to IS execution, what the proof essentially does is to produce a path P in the graph G that starts in γ 1 .


Martine A M C Baven-Pronk

Minneke J Coenraad

Henk R Van Buuren

Robert A De Man

Karel J Van Erpecum

Mieke M H Lamers

Joost P H Drenth

Aad A P Van Den Berg

Ulrich H Beuers

Jannie Den Ouden

Johannes ; Brouwer

Reinier

Graaf Gasthuis

Aad P Van Den Berg

Ger H Koek

Carin M J Van Nieuwkerk

Gerd Bouma

Johannes T Brouwer

Bart Van Hoek
email: b.van_hoek@lumc.nl

Prof. dr B Van Hoek

Mycophenolate mofetil: role in

Keywords: autoimmune hepatitis and overlap syndromes Auto-immune Hepatitis, Primary sclerosing cholangitis, Primary biliary cirrhosis, Overlap Syndrome, Mycophenolate Mofetil AIH= Autoimmune hepatitis AZA = Azathioprine IAHG

come

Background and Aims: Treatment failure occurs in 20% of autoimmune hepatitis patients on prednisolone and azathioprine (AZA). There is no established second line treatment. This retrospective observational study was conducted to assess the efficacy of mycophenolate mofetil as second line treatment after AZA-intolerance or AZA-nonresponse in autoimmune hepatitis and overlap syndromes.

Methods: Consecutive patients from the Dutch Autoimmune Hepatitis Group cohort, consisting of 661 patients , with autoimmune hepatitis or overlap syndromes, AZAintolerance or AZA-nonresponse, and past or present use of mycophenolate mofetil were included. Primary endpoint of mycophenolate mofetil treatment was biochemical remission.

Secondary endpoints were biochemical response (without remission), treatment failure and prevention of disease progression.

Results: Forty-five patients treated with mycophenolate mofetil were included. In autoimmune hepatitis remission or response was achieved in 13% and 27% in the AZAnonresponse group compared to 67% and 0% in the AZA-intolerance group (P = 0.008). In overlap-syndromes remission or response was reached in 57% and 14% in the AZAnonresponse group and 63% and 25% of the AZA-intolerance group (NS). 33% had sideeffects and 13% discontinued mycophenolate mofetil. Overall 38% had treatment failure; this was 60% in the autoimmune hepatitis AZA-nonresponse group. Decompensated liver cirrhosis, liver transplantations and death were only seen in the autoimmune hepatitis AZAnonresponse group (P < 0.001).

Conclusion:

Mycophenolate mofetil induced response or remission in a majority of patients with autoimmune hepatitis and azathioprine-intolerance and with overlap syndromes, irrespective of intolerance or nonresponse for azathioprine. In autoimmune hepatitis with azathioprine nonresponse mycophenolate mofetil is less often efective.

Introduction

Autoimmune hepatitis (AIH) is a chronic inflammatory liver disease characterized by hypergammaglobulinemia, auto-antibodies and interface hepatitis. [START_REF] Czaja | Current concepts in autoimmune hepatitis[END_REF][START_REF] Alvarez | International Autoimmune Hepatitis Group Report: review of criteria for diagnosis of autoimmune hepatitis[END_REF][START_REF] Krawitt | Autoimmune hepatitis[END_REF] . No single test exists to confirm AIH and a scoring system was devised by the International Autoimmune Hepatitis Group (IAHG) in 1993 which was revised in 1999 and simplified in 2008 [START_REF] Alvarez | International Autoimmune Hepatitis Group Report: review of criteria for diagnosis of autoimmune hepatitis[END_REF][START_REF] Hennes | Simplified criteria for the diagnosis of autoimmune hepatitis[END_REF][START_REF] Johnson | Meeting report: International Autoimmune Hepatitis Group[END_REF] . The incidence of AIH among Caucasian Northern Europeans ranges from 0.1 to 1.9/100.000/years and its prevalence is 16.9/100.000/year [START_REF] Czaja | Current concepts in autoimmune hepatitis[END_REF][START_REF] Boberg | Prevalence and epidemiology of autoimmune hepatitis[END_REF] .

If left untreated as many as 35% of the patients with severe disease die within six months and of the remaining patients 40% develop cirrhosis [START_REF] Soloway | Clinical, biochemical, and histological remission of severe chronic active liver disease: a controlled study of treatments and early prognosis[END_REF][START_REF] Czaja | AASLD practice guidelines: Diagnosis and Treatment of Autoimmune Hepatitis[END_REF] .

Randomized controlled trails published between 1973 and 1985 have established the role of prednisolone (PRED) alone and in combination with azathioprine (AZA) in the treatment of AIH [START_REF] Soloway | Clinical, biochemical, and histological remission of severe chronic active liver disease: a controlled study of treatments and early prognosis[END_REF][START_REF] Cook | Controlled prospective trial of corticosteroid therapy in active chronic hepatitis[END_REF][START_REF] Summerskill | Prednisone for chronic active liver disease: dose titration, standard dose, and combination with azathioprine compared[END_REF][START_REF] Murray-Lyon | Controlled trial of prednisone and azathioprine in active chronic hepatitis[END_REF][START_REF] Tage-Jensen | Azathioprine versus prednisone in non-alcoholic chronic liver disease (CLD). Relation to a serological classification[END_REF][START_REF] Stellon | Randomised controlled trial of azathioprine withdrawal in autoimmune chronic active hepatitis[END_REF][START_REF] Lamers | Treatment options for autoimmune hepatitis: A systematic review of randomized controlled trials[END_REF] . Although these trails have their limitations, as shown in a recently published review, current treatment is based upon these data and about 80% of the patients achieve remission within 3 years [START_REF] Lamers | Treatment options for autoimmune hepatitis: A systematic review of randomized controlled trials[END_REF] . The immediate consequence is that about 20% of the patients cannot tolerate PRED and/or AZA or only have a partial response or treatment failure 15, 16 . There is no established second line treatment for these patients.

In the past 15 years several immunosuppressive drugs, including ciclosporin, tacrolimus, methothrexate, 6-mercaptopurine and 6-thioguanine have been investigated as possible second line treatment, mainly in small case series or single case-reports. The groups are too small to define the utility of these agents [START_REF] Larsen | Low-dose tacrolimus ameliorates liver inflammation and fibrosis in steroid refractory autoimmune hepatitis[END_REF][START_REF] Alvarez | Short-term cyclosporine induces a remission of autoimmune hepatitis in children[END_REF][START_REF] Fernandes | Cyclosporine therapy in patients with steroid resistant autoimmune hepatitis[END_REF][START_REF] Aqel | Efficacy of tacrolimus in the treatment of steroid refractory autoimmune hepatitis[END_REF][START_REF] Burak | Successful treatment of refractory type 1 autoimmune hepatitis with methotrexate[END_REF][START_REF] De Boer | Promising treatment of autoimmune hepatitis with 6-thioguanine after adverse events on azathioprine[END_REF][START_REF] Pratt | The successful treatment of autoimmune hepatitis with 6-mercaptopurine after failure with azathioprine[END_REF] .

In the last decade ten case series describe the use of mycophenolate mofetil (MMF) in a total of 121 adult patients and patients, concludes that MMF could be a good alternative but mainly in patients who do not tolerate AZA. Only one study included the AIH-overlap syndromes with primary sclerosing cholangitis (PSC) and primary biliary cirrhosis (PBC) [START_REF] Richardson | Mycophenolate mofetil for maintenance of remission in autoimmune hepatitis in patients resistant to or intolerant of azathioprine[END_REF][START_REF] Devlin | Mycophenolate mofetil for the treatment of autoimmune hepatitis in patients refractory to standard therapy[END_REF][START_REF] Chatur | Transplant immunosuppressive agents in nontransplant chronic autoimmune hepatitis: the Canadian association for the study of liver (CASL) experience with mycophenolate mofetil and tacrolimus[END_REF][START_REF] Czaja | Empiric therapy of autoimmune hepatitis with mycophenolate mofetil: comparison with conventional treatment for refractory disease[END_REF][START_REF] Inductivo-Yu | Mycophenolate mofetil in autoimmune hepatitis patients not responsive or intolerant to standard immunosuppressive therapy[END_REF][START_REF] Hlivko | A single center review of the use of mycophenolate mofetil in the treatment of autoimmune hepatitis[END_REF][START_REF] Hennes | Mycophenolate mofetil as second line therapy in autoimmune hepatitis?[END_REF][START_REF] Wolf | Mycophenolate mofetil for autoimmune hepatitis: a single practice experience[END_REF][START_REF] Aw | Mycophenolate mofetil as rescue treatment for autoimmune liver disease in children: a 5-year follow-up[END_REF][START_REF] Sharzehi | Mycophenolate mofetil for the treatment of autoimmune hepatitis in patients refractory or intolerant to conventional therapy[END_REF] . Because of the low prevalence of overlap syndromes little is known about the preferred treatment in this patient category.

Usually the AIH-component in overlap syndromes is treated as AIH [START_REF] Rust | Overlap syndromes among autoimmune liver diseases[END_REF] .

The

Results

Forty-nine patients with current or past use of MMF were selected from the 661 Dutch AIH Group cohort. One had to be excluded because the AIH score was too low, three because not all the information required for this study was available. The remaining 45 patients were divided into two main groups: AZA-non-responders (N = 22) and AZA-intolerance (N = 23).

Subsequently both groups were divided into subgroups according to whether they had AIH or AIH-overlap syndrome (Figure 1). All patients with AIH-PBC overlap syndrome and one out of four patients with AIH-PSC overlap syndrome received ursodeoxycholic acid treatment in addition to immunosuppression.

Side effects of AZA before switching to MMF were gastro-intestinal complains (nine), rash (eight), fever (four), hepatitis (three), leucopenia (two), pancreatitis (two), arthralgia (one), myalgia (one), elevated amylase (one) and haemolytic anaemia (one). Some patients reported multiple side effects. At the time of data collection 29 out of 45 (64%) patients still used MMF (Table 3).

Reasons for discontinuing MMF were non-response (seven (16%), five in the AZA-nonresponse group), intolerance (six (13%), four in the AZA-intolerance group), patients initiative (two) and unknown (one). Fifteen out of 45 (33%) patients had side-effects of MMF which were gastro-intestinal complaints (five), rashes or skin carcinomas (three), fatigue or concentration problems (three), alopecia (two), infections (two), leucopenia (one), palpitations (one) and ischemic colitis (one). Some patients reported multiple side effects.

Table 4 shows the number of patients and percentages of treatment failure, response, remission, relapses and disease progression with MMF treatment as defined after three months (A) and at the end of follow-up (B). Before starting MMF 78% of all patients had a response on AZA and PRED. Remissions on AZA and PRED before MMF were only seen in the intolerance group. After starting MMF 17 (38%) out of 45 patients had a treatment failure.

Twelve of these patients stopped using MMF, six because of side-effects. Twenty-one out of 45 (47%) patients achieved a remission while using MMF. In 13 of these 21 patients IgG levels normalized, in four IgG levels stayed elevated and in four IgG levels were unknown. Comparing the AZA-non-response versus the AZA-intolerance group remission rates (P = 0.0017) and relapse rates (P=0.028) are significantly higher in the AZA-intolerance group. Although not statistically significant, treatment failure was twice as high in de AZAnon-response group compared to the AZA intolerance group. In both groups, one patient progressed to cirrhosis while using MMF. Decompensated liver cirrhosis, liver transplantations and death were only seen in the AZA-non-response group (p<0.01).

Comparing the AIH-AZA-non-response versus de AIH-AZA-intolerance group remission rates are higher in de AIH-AZA-intolerance group (P = 0.008). Although not significant, treatment failure is twice as high in the AIH-AZA-non-response group compared to the AIH-AZA-intolerance group. Decompensated liver cirrhosis, liver transplantations and death were only seen in the AIH-AZA-non-response group. The AIH-AZA-non-response group has significantly less remissions compared to the other subgroups combined (P = 0.002) (Figure 2). The percentages of patients reaching remission, response or treatment failure with MMF in the four patient groups are shown in figure 3. Currently, most experience with the use of MMF is in the organ transplant setting.

MMF has a more favorable side-effect profile than many other immunosuppressives [START_REF] Dharancy | Mycophenolate mofetil monotherapy for severe side effects of calcineurin inhibitors following liver transplantation[END_REF][START_REF] Dandel | Maintenance immunosuppression with mycophenolate mofetil: long-term efficacy and safety after heart transplantation[END_REF] .

The last decade ten small case series described the use of MMF in AIH and the overall opinion was that it could be used as a second line treatment [START_REF] Richardson | Mycophenolate mofetil for maintenance of remission in autoimmune hepatitis in patients resistant to or intolerant of azathioprine[END_REF][START_REF] Devlin | Mycophenolate mofetil for the treatment of autoimmune hepatitis in patients refractory to standard therapy[END_REF][START_REF] Chatur | Transplant immunosuppressive agents in nontransplant chronic autoimmune hepatitis: the Canadian association for the study of liver (CASL) experience with mycophenolate mofetil and tacrolimus[END_REF][START_REF] Czaja | Empiric therapy of autoimmune hepatitis with mycophenolate mofetil: comparison with conventional treatment for refractory disease[END_REF][START_REF] Inductivo-Yu | Mycophenolate mofetil in autoimmune hepatitis patients not responsive or intolerant to standard immunosuppressive therapy[END_REF][START_REF] Hlivko | A single center review of the use of mycophenolate mofetil in the treatment of autoimmune hepatitis[END_REF][START_REF] Hennes | Mycophenolate mofetil as second line therapy in autoimmune hepatitis?[END_REF][START_REF] Wolf | Mycophenolate mofetil for autoimmune hepatitis: a single practice experience[END_REF][START_REF] Aw | Mycophenolate mofetil as rescue treatment for autoimmune liver disease in children: a 5-year follow-up[END_REF][START_REF] Sharzehi | Mycophenolate mofetil for the treatment of autoimmune hepatitis in patients refractory or intolerant to conventional therapy[END_REF] . However, two series indicated that there was a difference between patients who were intolerant for AZA and those who were AZA-non-responders [START_REF] Hennes | Mycophenolate mofetil as second line therapy in autoimmune hepatitis?[END_REF][START_REF] Sharzehi | Mycophenolate mofetil for the treatment of autoimmune hepatitis in patients refractory or intolerant to conventional therapy[END_REF] . This study is the largest on the use of MMF in AIH so far. It is the only study that compares both AZA-intolerance versus AZA-non-response and includes AIH-overlap syndromes.

All patients in the current cohort were treated with PRED and AZA before starting MMF. Here some expected differences between the AZA-intolerance and AZA-non-response 2). Usually intolerance is seen within the first half year, which is why in the AZA-intolerance group it is not possible to increase the dose of AZA and lower the dose of PRED.

Six patients were treated with PRED, AZA and MMF. In all these patients MMF was added because they did not respond sufficiently to PRED and AZA despite long term treatment (minimum of 100 months). In our opinion the additional effect after adding MMF thus can be contributed to MMF en we therefore did not exclude these patients. Although four of these patients had a response or remission we do not recommend this triple therapy.

The number of relapses on MMF is higher in the AZA-intolerance group than in the AZA-non-response group (P =0.028). The explanation for this is that in order to have a relapse, first there must be a response or remission. In the AZA-non-response group there are fewer responses and remissions and more treatment failures on MMF. Apparently AZA-nonresponse predicts non-response to MMF in most patients. However, in AIH-overlap patients in both groups, AZA-intolerance and AZA-non-response, similar response and remission rates on MMF were seen, keeping in mind that both groups are very small, while the doses of PRED used in the overlap-AZA-non-response group were not significantly higher. Therefore in AIH-overlap syndrome patients AZA-non-response does not predict a non-response to MMF, while in AIH patients it does. The differences between AZA-non-response and AZAintolerant patients were apparent when comparing the AIH-AZA-intolerance group to the AIH-AZA-non-response group (Table 4). The AIH-AZA-non-response group has the lowest remission rate (13%) and highest treatment failure (60%) on MMF treatment of all subgroups.

There are no apparent differences in patient characteristics between the AIH-AZA-nonresponse group and the other subgroups, except possibly more cirrhosis at presentation than in the AIH-AZA-intolerance patients. As in the other smaller case series a limitation of the current report is its retrospective nature. AZA-non-response is a conclusion of the treating physician. In some cases treatment with AZA and PRED may have been insufficient in dose or length according to current guidelines [START_REF] Manns | Diagnosis and management of autoimmune hepatitis[END_REF] . Also there were patients who did not achieve a response or remission on AZA and PRED who were already lowering the PRED dose and then were switched to MMF.

Subsequently some of these patients did not achieve a response or remission on MMF with low dose PRED and were labeled as treatment failures. In some of these cases there was never a proper remission induction with sufficiently high PRED dose after switching to MMF. It was also quite difficult to compare the use of PRED before and after starting MMF. One of the main reasons for this was the increased use of budesonide as an alternative of PRED. As induction therapy budesonide appears superior to PRED in a recent study [START_REF] Manns | Azathioprine With Budesonide Induces Remission More Effectively Than With Prednisone in Patients With Autoimmune Hepatitis[END_REF] . However, according to a meta-analysis of previous randomized controlled trials and the current AASLD guidelines PRED with or without AZA should be used to induce remission, while AZA with or without PRED currently is the standard in remission maintenance treatment in AIH and AIH-overlap syndrome patients [START_REF] Lamers | Treatment options for autoimmune hepatitis: A systematic review of randomized controlled trials[END_REF][START_REF] Manns | Diagnosis and management of autoimmune hepatitis[END_REF] .

Out of the ten published MMF case series eight did not separate AZA-intolerance and AZA-non-response patients [START_REF] Richardson | Mycophenolate mofetil for maintenance of remission in autoimmune hepatitis in patients resistant to or intolerant of azathioprine[END_REF][START_REF] Devlin | Mycophenolate mofetil for the treatment of autoimmune hepatitis in patients refractory to standard therapy[END_REF][START_REF] Chatur | Transplant immunosuppressive agents in nontransplant chronic autoimmune hepatitis: the Canadian association for the study of liver (CASL) experience with mycophenolate mofetil and tacrolimus[END_REF][START_REF] Czaja | Empiric therapy of autoimmune hepatitis with mycophenolate mofetil: comparison with conventional treatment for refractory disease[END_REF][START_REF] Inductivo-Yu | Mycophenolate mofetil in autoimmune hepatitis patients not responsive or intolerant to standard immunosuppressive therapy[END_REF][START_REF] Hlivko | A single center review of the use of mycophenolate mofetil in the treatment of autoimmune hepatitis[END_REF][START_REF] Wolf | Mycophenolate mofetil for autoimmune hepatitis: a single practice experience[END_REF] . Only one of these eight studies included AIH-overlap syndrome patients, but responses were not reported separately [START_REF] Wolf | Mycophenolate mofetil for autoimmune hepatitis: a single practice experience[END_REF] . In two of these eight studies MMF is used to induce remission. One is a case series of five patients and concludes that MMF can be used to induce and maintain remission [START_REF] Devlin | Mycophenolate mofetil for the treatment of autoimmune hepatitis in patients refractory to standard therapy[END_REF] . One is a study with eight patients receiving MMF who were compared to 17 patients receiving high dose corticosteroids. The conclusion of this study was that MMF cannot be used to induce remission [START_REF] Czaja | Empiric therapy of autoimmune hepatitis with mycophenolate mofetil: comparison with conventional treatment for refractory disease[END_REF] . Four of the eight studies describe the use of MMF in combination with corticosteroids and one describes the use of MMF with or without tacrolimus. These previous studies report a remission rate of 71-84%, which is high compared to our findings. The other studies reports side-effects in 6-34% of patients, which is comparable to our findings [START_REF] Richardson | Mycophenolate mofetil for maintenance of remission in autoimmune hepatitis in patients resistant to or intolerant of azathioprine[END_REF][START_REF] Chatur | Transplant immunosuppressive agents in nontransplant chronic autoimmune hepatitis: the Canadian association for the study of liver (CASL) experience with mycophenolate mofetil and tacrolimus[END_REF][START_REF] Hlivko | A single center review of the use of mycophenolate mofetil in the treatment of autoimmune hepatitis[END_REF][START_REF] Wolf | Mycophenolate mofetil for autoimmune hepatitis: a single practice experience[END_REF] .

In our opinion the study of Hennes et al is best comparable to our study in terms of size and design. The remission rate in the AZA-non-response group, percentage of treatment failure, side effects and patients who had to stop MMF because of side effects were comparable. Compared to our data (67% remission rate) this other study reached a remission rate of 43% in the AZA-intolerance group. The difference is mainly explained by differences in definition, since the other study did not use the definitions of the AASLD-guideline but stated its own, more strict definitions [START_REF] Manns | Diagnosis and management of autoimmune hepatitis[END_REF] . In contrast to that study the current study also looked at MMF in AIH-overlap syndromes and 86% of these patients had a response and/or remission with MMF [START_REF] Hennes | Mycophenolate mofetil as second line therapy in autoimmune hepatitis?[END_REF] . In our opinion the similarity of the results of this study and the study of Hennes et al suggests that the findings are an accurate reflection of the use of MMF as a second line treatment in the real world. Both studies are retrospective but describe relatively large numbers of patients being treated with MMF.

In conclusion, this study shows that MMF with PRED is an excellent alternative treatment in patient with AIH who do not tolerate AZA (remission rate 67%). In addition our data show that MMF can induce remission in 60% of patients with AIH-overlap syndromes, irrespective if they were intolerant or non-responsive to AZA. However, the majority of patients with AIH and a non-response on AZA fail treatment with MMF. Since twothirds of these AIH patients with non-respsonse to AZA progressed to decompensated liver disease,

Legends to tables

Table 1. General characteristics of the study population.

  MMF for auto-immune hepatitis and overlap syndromesBaven-Pronk 10 Two out of 45 (4%) patients (both AIH-AZA-intolerance) were on MMF monotherapy, they were both in remission.

FifteenDiscussion

  AIH-overlap patients were included in this study, four PSC-AIH-overlap and 11 PBC-AIH-overlap (Figure1). Three PBC-AIH-overlap patients (two AZA-non-response and one AZA-intolerance) had a treatment failure on MMF. Two PBC-AIH-overlap patients (one AZA-non-response and one AZA-intolerance) and one PSC-AIH-overlap patient (AZAintolerance) had a response. Six PBC-AIH-overlap patients (three AZA-non-response and three AZA-intolerance) and three PSC-AIH-overlap patients (one AZA-non-response and two AZA-intolerance) had a remission. There were no significant differences between the overlap-AZA-intolerance and the overlap-AZA-non-response group.Our data indicate that MMF is a valuable second line treatment in AIH-AZAintolerant patients and in all AIH-overlap syndrome patients, irrespective if these patients were intolerant or non-responsive to AZA. However, in AIH-AZA-non-response patients treatment failure on MMF is frequent and in this group other therapies probably should be considered first.

  -AIH-overlap (AIH remission rate 75%) and PBC-AIH-overlap (AIH remission rate 55%) patients often do very well on MMF but the individual groups are too small to look at differences between PSC and PBC overlap subgroups regarding the effect of MMF.

Figure 1 .

 1 Figure 1. Patient distribution according to reasons for starting MMF and underlying disease in the patients derived from the 661 AIH and AIH-overlap patients in the Dutch AIH cohort.

Figure 2 .Figure 3 .

 23 Figure 2. Percentage of patients achieving remission and time to achieve remission with MMF in the four subgroups:

AZATable 3 . 22 AIH

 322 details on dose (five) or length (two) of the initial treatment were missing * Significant difference between AZA-intolerance and AZA-non-response (P<0.001), AIH-AZAintolerance and AIH-AZA-non-response (P=0.001) and Overlap-AZA-intolerance and Overlap-AZA-non-response (P=0.019) **Significant difference between AZA-intolerance and AZA-non-response (P=0.002) and AIH-AZAintolerance and AIH-AZA-non-response (P=0.005) ***Significant difference between AZA-intolerance and AZA-non-response (P=0.006) and AIH-AZA-intolerance and AIH-AZA-non-response (P=0.039) Data on treatment with MMF per group AZA-intolerance N = 23 AZA-non-responders N = MMF for auto-immune hepatitis and overlap syndromes Baven-Pronk 25 stable disease, but follow up was only 5 months. $ In both groups one patient had a treatment failure according to definition, continued using MMF and had a response. They were counted as a remission/response on MMF. *****Significant difference between AZA-intolerance and AZA-non-response (P=0.038) and AIH-AZA-intolerance and AIH-AZA-non-response (P=0.009) ******Other therapies were corticosteroids, either monotherapy or combined with AZA and one patient using no medication anymore. # Progression of liver disease defined as to progression to cirrhosis, decompensated cirrhosis, liver transplantation and death was significantly more prevalent in the AZA-non-response group versus the AZA-intolerance group (P=0.001) and in the AIH-AZA-non-response versus de AIH-AZA-intolerance group (P<0.001) Patient distribution according to reasons for starting MMF and underlying disease in the patients derived from the 661 AIH and AIH-overlap patients in the Dutch AIH cohort. 191x111mm (96 x 96 DPI) Percentage of patients achieving remission and time to achive remission on MMF in the four subgroups: .....AIH-AZAintolerance; ---overlap-AZAintolerance; ___overlap-AZAnonresponse; -.-. AIH-AZAnonresponse 166x133mm (96 x 96 DPI) Percentage of patients achieving remission (light), response (gray) or with treatment failure (dark) on MMF. AIH-INT: AIH with intolerance for AZA; AIH-NR: AIH with non-response to AZA; Overlap-INT: Overlap syndrome with intolerance for AZA; Overlap-NR: Overlap syndrome with non-response to AZA. Decompensated cirrhosis, liver transplantation and death only occurred in the AIH-NR group (in 60%)(p<0.01). Remission in AIH-NR vs AIH-NT: p=0.008; Remission AIH-NR vs other groups: p=0.002; Remission NR vs INT: p=0.002; Relapse NR vs INT: p=0.03. 254x190mm (96 x 96 DPI)

  aim of this retrospective multicentre observational study was to investigate whether MMF is a good second line treatment in patients with AIH or AIH-overlap syndromes who fail or do not tolerate AZA and whether this is true for all subgroups, namely AZA-intolerance versus AZA-non-response and AIH versus AIH-overlap syndromes. To determine the progression of the disease at the time of data collection all modalities (radiology, pathology, endoscopy and letters, whatever gave the most recent information) were used. Follow up is from start of MMF treatment till may 2009 and differs per patient.Fisher's exact test, Mann-Withney test, independent samples T-test and Log rank test were used with p<0.05 as the level of statistical significance.

	(presence of ascitis, hepatic encephalopathy or oesophageal varices), liver transplantation or
	F o r The Dutch AIH Group represents a cohort of identified AIH an AIH-overlap patients, Patients and Methods including AIH-PBC and AIH-PSC, consisting of 661 patients from academic and non-academic centres. From this cohort those patients with AIH according to the IAHG criteria (definite and probable) 2 and all patients with AIH-overlap syndromes according to the Paris criteria 35, 36 with past and present use of MMF before May 2009 were included. Intolerance was defined as stopping AZA because of AZA related side effects. Non-response was defined as failure to achieve or maintain remission, as determined by the treating physician. The response to MMF in identified AIH and AIH-overlap patients was determined by chart review. Treatment failure, response, remission and relapse were defined F o r death. F o r
	P e e r according to established criteria in the AASLD guideline 37 : Treatment failure: a rise in or P P stable AST and/or ALT three months after starting MMF or intolerance for MMF, defined as e e stopping MMF because of MMF related side effects. Response: a drop in AST and/or ALT below twice the upper limit of the reference range three months after starting MMF or a fifty e r e r
	R percent fall in AST and/or ALT one month after starting MMF. Remission: a normalisation of AST and/or ALT after starting MMF. Relapse: a rise in AST and/or ALT of more than R R
	e threefold the upper limit after a response or remission. A patient can fall into a category only e e
	v i e once. So, if a patient has a treatment failure there cannot be a response or remission and vice versa. All the data was collected and processed by the same person (MACMP) and verified v i e v i e
	(BvH).	w The primary endpoint was defined as biochemical remission while using MMF. w w
	Secondary endpoints were defined as biochemical response or treatment failure while using
	MMF and prevention of progression of the disease, defined as decompensated cirrhosis

Table 1

 1 treated with budesonide before switching to MMF. After switching to MMF two continued using budesonide. Most patients were subsequently treated with MMF and PRED (details in Table3). Seven patients (1 Overlap-AZA-intolerance, 2 AIH-AZA-nonresponse and 4 AIH-AZA-intolerance) were treated with budesonide while on MMF. Two AIH-AZA-non-response patients had a treatment failure, the other five had a remission on MMF. In patients treated with MMF the AZA was discontinued in almost all cases, except in three AIH and three AIH-overlap syndrome patients, all non-responders. Of these six patients two AIH patients had a treatment failure, one AIH and one Overlap patient had a response and two Overlap patients had a remission.

	MMF for auto-immune hepatitis and overlap syndromes	Baven-Pronk
	intolerance) were
	F o r
	P
	e
	e r
	R
	e
		v i e
		w
		9

shows the patient characteristics, including age at diagnosis. At the time of MMF treatment the youngest patient was 20 years of age. As shown in table 1, disease duration was equally distributed over the groups and not a confounding factor. Follow-up biopsies were scarce. Six patients had a liver biopsy before they were switched to MMF.

Twenty-two patients (equally divided over the subgroups) ever had a second liver biopsy either during AZA/PRED or during MMF/PRED treatment. Though not significant, cirrhosis -as determined by liver biopsy, CTscan or presence of varices-was more prevalent in the AIH-AZA-non-response group.

All patients were treated with PRED and AZA before starting MMF (details in Table

2

). Three patients (1 AIH-AZA-non-response, 1 AIH-AZA-intolerance and 1 Overlap-AZA

Table 2 .

 2 Data on initial treatment with PRED and AZA per group.

Table 3 .

 3 Data on treatment with MMF per group.

Table 4 .

 4 Overview of treatment failure, response, remission and disease progression with MMF treatment as defined after three months (A) and at the end of follow-up (B). .

		AIH-AZA-intolerance
		Overlap-AZA-intolerance
		Overlap-AZA-non-response
		AIH-AZA-non-response
	+	End of follow up

Table 1 .

 1 General characteristics of the study population

		AZA-intolerance N = 23	AZA-non-responders N = 22
		AIH	Overlap syndrome	AIH	Overlap syndrome
		N = 15	N = 8	N = 15	N = 7
	Gender (male/female)	2/13	2/6	4/11	0/7
	AIH Score	16 (12-21)	12 (9-20)	16 (12-21)	13 (6-17)
	Age at diagnosis (year)	38 (10-71)	36 (16-72)	35 (11-61)	46 (25-59)
	Disease duration (year)	8 (1-22)	10 (2-20)	9 (3-21)	10 (3-23)
	IgG/gamma globuline	10/15 (67%)	6/7 (86%)	12/13 (92%)	6/7 (86%)
	elevated at diagnosis
	ANA	10/15 (67%)	4/8 (50%)	10/14 (71%)	6/7 (86%)
	ASMA	11/13 (85%)	5/7 (71%)	11/14 (79%)	4/6 (67%)
	SLA	1/1 (100%)	0/0 (0%)	0/0 (0%)	0/0 (0%)
	LKM	0/4 (0%)	0/1 (0%)	0/2 (0%)	0/2 (0%)
	AMA	0/10 (0%)	3/7 (43%)	1/10 (10%)	4/7 (57%)
	Liver biopsy at diagnosis	14 (93%)	8 (100%)	15 (100%)	7 (100%)
	Interface hepatitis	14/14 (100%)	6/8 (75%)	13/14 (93%)	6/7 (86%)
	Plasma cell infiltrate	10/14 (71%)	7/8 (88%)	13/14 (93%)	7/7 (100%)
	Biliary changes	3/14 (21%)	4/8 (50%)	3/14 (21%)	7/7 (100%)
	Cirrhosis at diagnosis	2/15 (13%)	4/8 (50%)	9/15 (60%)	2/7 (29%)
	IgG/gamma globuline	5/10 (50%)	4/5 (80%)	5/8 (63%)	4/6 (67%)
	elevated at start MMF
	Liver biopsy at start MMF	1/15 (7%)	2/8 (25%)	1/15 (7%)	2/7 (29%)
	Cirrhosis before MMF	3/15 (20%)	5/8 (63%)	11/15 (73%)	5 (71%)
	Median (Range), Number positive/Number measured or known (Percentage)

Table 2 .

 2 Data on initial treatment with PRED and AZA per group

&One patient was excluded because she had treatment failure on MMF, continued it and still had

Acknowledgements

This article has been discussed within the Dutch Autoimmune Hepatitis Group. Apart from the above mentioned authors the Dutch Autoimmune Hepatitis Group has the following members: J.F. Monkelbaan, MF, Ph.D, Department of Gastroenterology and Hepatology, University Medical Center Utrecht, Utrecht, The Netherlands; B. Verwer MD and N. van Gerven MD, Department of Gastroenterology and Hepatology, Free University Medical Center, Amsterdam, The Netherlands; H.W. Verspaget PhD, Department of Gastroenterology and Hepatology, Leiden University Medical Center, Leiden, The Netherlands.