Samson Abramsky

Jonathan Zvesper

From Lawvere to Brandenburger-Keisler: interactive forms of diagonalization and self-reference

Introduction

Diagonal arguments lie at the root of many fundamental phenomena in the foundations of logic and mathematics. Recently, a striking form of diagonal argument has appeared in the foundations of epistemic game theory, in a paper by Adam Brandenburger and H. Jerome Keisler [START_REF] Brandenburger | An impossibility theorem on beliefs in games[END_REF]. The core Brandenburger-Keisler result can be seen, as they observe, as a two-person or interactive version of Russell's Paradox. This raises a number of fascinating questions at the interface of epistemic game theory, logic and theoretical computer science:

1. Is the Brandenburger-Keisler argument (henceforth: 'BK argument') just one example of a more general phenomenon, whereby mathematical structures and arguments can be generalized from a familiar 'one-person' form to a two-or multi-agent interactive form? 2. To address this question, a sharper understanding of the BK argument is needed. The argument hinges on a statement involving the modalities believes and assumes. The statement has the form Ann believes that Bob assumes that . . . which is not familiar as it stands. Where does this believes-assumes pattern come from? How exactly does it relate to the more familiar arguments in the one-person case? In particular, can it be reduced to a one-person argument? 3. Is there a natural multi-agent generalization of the BK argument? In particular, does it have a compositional structure, which allows a smooth generalization to any number of agents? 4. The main formal consequence of the BK argument is that there can be no belief model which is 'assumption-complete' with respect to a collection of predicates including those definable in the first-order language of the model. Brandenburger and Keisler also give a positive result, a construction of a topological model which is assumption-complete with respect to the positive fragment of first-order logic extended with the believes and assumes modalities. They raise the question of a more general perspective on the availability of such models.

We shall provide substantial answers to questions (2)-( 4) above in the present paper. These results also suggest that the Brandenburger-Keisler 'paradox' does offer a good point of entry for considering the more general question [START_REF] Abramsky | Retracing some paths in process algebra[END_REF].

The starting point for our approach is a classic paper by F. William Lawvere from 1969 [START_REF] Lawvere | Diagonal arguments and cartesian closed categories[END_REF], in which he gave a simple form of the (one-person) diagonal argument as a fixpoint lemma in a very general setting. This lemma lies at the basis of a remarkable range of results. Lawvere's ideas were amplified and given a very attractive presentation in a recent paper by Noson Yanofsky [START_REF] Noson | A universal approach to self-referential paradoxes and fixed points[END_REF].

Our contributions can be summarized as follows:

-We reformulate the core BK argument as a fixpoint lemma. This immediately puts it in the general genre of diagonal arguments, and in particular of the Lawvere fixpoint lemma. -The BK argument applies to (belief) relations, while the Lawvere argument applies to functions (actually, abstractly to arrows in a category). To put them on common ground, we give a novel relational reformulation of the Lawvere argument.

-We analyze the exact logical resources required for our fixpoint version of the BK argument, and show that it can be carried out in regular logic, the fragment of first-order logic comprising sequents φ ψ, where φ and ψ are built from atomic formulas by conjunction and existential quantification. Regular logic can be interpreted in any regular category, which covers a wide range of types of mathematical structure. The Lawvere argument can also be carried out in (a fragment of) regular logic. We can now recognize the Lawvere argument as exactly the one-person version of the BK argument, and interpret the key BK lemma as a reduction to the one-person Lawvere argument. -This analysis leads in turn to a smooth generalization of the BK argument to multi-agent belief models. The content of the believes-assumes pattern, or more generally the believes * -assumes pattern:

A 1 believes that A 2 believes that . . . A n believes that B assumes that . . . is that the Lawvere hypothesis of weak point surjectivity is propagated back along belief chains. -We furthermore give a compositional analysis of the believes-assumes pattern, which characterizes what we call 'belief-complete' relations in terms of this propagation property. This gives a rather definitive analysis for why the BK argument takes the form it does. -We then turn to the issue of the construction of assumption complete models. The categorical perspective allows us to apply general techniques from coalgebra and domain theory to the construction of such models.

The further contents of this paper are as follows. In Section 2, we review the setting for the BK argument, and give our formulation of it as a fixpoint lemma. In Section 3, we show how it can be formalized in regular logic. In Section 4, we introduce the Lawvere fixpoint lemma. In Section 5 we bring BK and Lawvere together, giving a relational reformulation of the Lawvere lemma, and showing how to reduce BK to this version of Lawvere, i.e. the two-person to the one-person argument. In Section 6, we give the multi-agent generalization, and in Section 7 the compositional analysis of belief-completeness, and hence of the believes-assumes pattern. In Section 8, we show how general functorial methods lead to the construction of assumption-complete models. Section 9 concludes with some further directions.

The Brandenburger-Keisler Argument

A (two-person) belief structure has the form (U a , U b , R a , R b ) where

R a ⊆ U a × U b , R b ⊆ U b × U a .
In the context of epistemic game theory, we think of U a and U b as type spaces for Alice and Bob:

-Elements of U a represent possible epistemic states of Alice in which she holds beliefs about Bob, Bob's beliefs, etc. Symmetrically, elements of U b represent possible epistemic states of Bob.

-The relations R a ⊆ U a ×U b , R b ⊆ U b ×U a specify these beliefs. Thus R a (x, y)
expresses that in state x, Alice believes that state y is possible for Bob. -We say that a state x ∈ U a believes P ⊆ U b if R a (x) ⊆ P . Modal logic provides a useful perspective on these notions, as shown by Eric Pacuit [START_REF] Pacuit | Understanding the Brandenburger-Keisler paradox[END_REF] (see also [START_REF] Brandenburger | An impossibility theorem on beliefs in games[END_REF]). Modally, 'x believes P ' is just x |= P a P where P a is the usual necessity operator defined with respect to the relation R a :

x |= P a φ ≡ ∀y. R a (x, y) ⇒ y |= φ.

-We say that x assumes P if R a (x) = P . This is x |= a P , where a is the modality defined by

x |= a φ ≡ ∀y. R a (x, y) ⇔ y |= φ.

A belief structure (U a , U b , R a , R b ) is assumption-complete [START_REF] Brandenburger | An impossibility theorem on beliefs in games[END_REF] with respect to a collection of predicates on U a and U b if for every predicate P on U b in the collection, there is a state x on U a such that x assumes P ; and similarly for the predicates on U a . (A predicate on a set U is just a subset of U .) 1Brandenburger and Keisler show in [START_REF] Brandenburger | An impossibility theorem on beliefs in games[END_REF] that this hypothesis, in the case where the predicates include those definable in the first-order language of this structure, leads to a contradiction. (They also show the existence of assumption complete models for some other cases.)

Our aim is to understand the general structures underlying this argument. Our first step is to recast their result as a positive one -a fixpoint lemma.

The BK Fixpoint Lemma

We are given a belief structure (U a , U b , R a , R b ). We assume that for 'all' (in some 'definable' class of) predicates p on U a there is x 0 such that:

R a (x 0 ) ⊆ {y | R b (y) = {x | p(x)}}. (1)
∃y. R a (x 0 , y).

Modally, these assumptions can be expressed as follows:

x 0 |= P a b p ∧ Q a .
Remark We can read (1) as saying: 'x 0 believes that (y assumes that p)', in the terminology of Brandenburger and Keisler.

Lemma 1 (Basic Lemma). From ( 1) and ( 2) we have:

p(x 0 ) ⇐⇒ ∃y.[R a (x 0 , y) ∧ R b (y, x 0 )].
Proof Suppose p(x 0 ). Take y as in ( 2), so R a (x 0 , y). Then by ( 1

), R b (y, x 0 ). Now consider y satisfying R a (x 0 , y) ∧ R b (y, x 0 ). By (1), from R a (x 0 , y) we have that R b (y) = {x | p(x)}. Hence from R b (y, x 0 ) we have that p(x 0 ).
Lemma 2 (BK Fixpoint Lemma). Under our assumptions, every unary propositional operator O has a fixpoint.

Proof Since p was arbitrary, we can define

q(x) ≡ ∃y.[R a (x, y) ∧ R b (y, x)] (3)
p(x) ≡ O(q(x)). (4)
(N.B. It is important that p is defined without reference to x 0 to avoid circularity.) These definitions combined with the equivalence given by the Basic Lemma immediately yield:

O(q(x 0 )) (4) ≡ p(x 0 ) ⇐⇒ ∃y.[R a (x 0 , y) ∧ R b (y, x 0 ) (3)
≡ q(x 0 ), so q(x 0 ) is a fixpoint for the operator O, as required.

Remarks Taking O ≡ ¬ yields the BK 'paradox'. (In fact ¬q(x) is equivalent to their 'diagonal formula' D in [START_REF] Brandenburger | An impossibility theorem on beliefs in games[END_REF]).

In general, since our assumptions (1) and ( 2) are relative to a class of predicates, this argument relies on q(x) and p(x) being in this class. Note that q(x) only involves conjunction and existential quantification. This leads to our analysis of the logical resources needed to carry out the BK argument.

We recall that regular logic is the fragment of (many-sorted) first-order logic comprising sequents of the form φ X ψ where φ and ψ are built from atomic formulas by conjunction (including the empty conjunction ) and existential quantification; and X is a finite set of variables which includes all those occurring free in φ and ψ. The intended meaning of such a sequent is

∀x 1 • • • ∀x n [φ ⇒ ψ]
where X = {x 1 , . . . , x n }. This is a common fragment of intuitionistic and classical logic. It plays a core rôle in categorical logic. A convenient summary of regular logic can be found in [START_REF] Butz | Regular categories and regular logic[END_REF]. We shall write X ψ for the sequent X ψ, and φ ψ for φ ∅ ψ. We shall assume a logical vocabulary containing the sorts U a and U b , and binary relation symbols R a : U a × U b and R b : U b × U a , together with a constant c : U a which will correspond to x 0 in the informal argument given in the previous section. Thus c is associated with the given predicate p, which will be represented by a formula in one free variable of sort U a .

The assumptions given in the informal argument can be expressed as regular sequents as follows.

(A1) R a (c, y) ∧ R b (y, x) {x,y} p(x) (A2) R a (c, y) ∧ p(x) {x,y} R b (y, x) (A3) ∃y. R a (c, y)
Here (A1) and (A2) correspond to assumption (1) in the informal argument, while (A3) corresponds to assumption [START_REF] Abramsky | A Cook's tour of the finitary non-well-founded sets[END_REF].

The formal version of Lemma 1 is as follows:

Lemma 3. From (A1)-(A3) we can infer the following sequents:

(F 1) p(c) q(c) (F 2) q(c) p(c) where q(x) ≡ ∃y.[R a (x, y) ∧ R b (y, x)].
A definable unary propositional operator will be represented by a formula context This is obtained directly from the previous lemma, taking p(x) ≡ O[q(x)]. The required sentence S is then q(c).

O[•],

Remarks

-Regular logic can be interpreted in any regular category [START_REF] Jaap Van Oosten | Basic category theory[END_REF][START_REF] Butz | Regular categories and regular logic[END_REF]: well-powered with finite limits and images, which are stable under pullbacks.These are exactly the categories which support a good calculus of relations. -The BK fixpoint lemma is valid in any such category. Regular categories are abundant -they include all (pre)toposes, all abelian categories, all equational varieties of algebras, compact Hausdorff spaces, and categories of Q-sets for right quantales Q. -If the propositional operator O is fixpoint-free, the result must be read contrapositively, as showing that the assumptions (A1)-(A3) lead to a contradiction. This will of course be the case if O = ¬[•] in either classical or intuitionistic logic. This yields exactly the BK argument. -In other contexts, this need not be the case. For example if the propositions (in categorical terms, the subobjects of the terminal object) form a complete lattice, and O is monotone, then by the Tarski-Knaster theorem there will indeed be a fixpoint. This offers a general setting for understanding why positive logics, in which all definable propositional operators are monotone, allow the paradoxes to be circumvented.

The Lawvere Fixpoint Lemma

We start off concretely working in Set. Suppose we have a function

g : X → V X
or equivalently, by cartesian closure:

ĝ : X × X → V
Think of V as a set of 'truth values': V X is the set of 'V-valued predicates'. Then g is showing how predicates on X can be represented by elements of X. In terms of ĝ: a predicate p : X → V is representable by x ∈ X if for all y ∈ X:

p(y) = ĝ(x, y)
Note that, if predicates 'talk about' X, then representable predicates allow X to 'talk about itself'. If g is surjective, then every predicate on X is representable in X. When can this happen? Proposition 1 (Lawvere Fixpoint Lemma). Suppose that g : X → V X is surjective. Then every function α :

V → V has a fixpoint: v ∈ V such that α(v) = v.
Proof Define a predicate p by

X × X ĝ -V X ∆ 6 p -V α ?
There is x ∈ X which represents p: then

p(x) = α(ĝ(∆(x))) = α(ĝ(x, x)) = α(p(x)) so p(x) is a fixpoint of α.
Remarks on the proof Note firstly that the proof is constructive. The crucial idea is that it uses two descriptions of p -one from its definition, one from its representation via ĝ. And since x represents p, p(x) is (indirect) self-application.

But does this make sense? Say that X has the fixpoint property if every endofunction on X has a fixpoint. Of course, no set with more than one element has the fixpoint property! Basic example: 2 = {0, 1}. The negation

¬0 = 1, ¬1 = 0
does not have a fixpoint. So the meaning of the theorem in Set must be taken contrapositively:

For all sets X, V where V has more than one element, there is no surjective map

X → V X

Two Applications

Cantor's Theorem Take V = 2. There is no surjective map X → 2 X and hence |P(X)| ≤ |X|.

We can apply the fixpoint lemma to any putative such map, with α = ¬, to get the usual 'diagonalization argument'. Russell's Paradox Let S be a 'universe' (set) of sets. Let ĝ : S × S → 2 define the membership relation:

ĝ(x, y) ⇔ y ∈ x
Then there is a predicate which can be defined on S, and which is not representable by any element of S. Such a predicate is given by the standard Russell set, which arises by applying the fixpoint lemma with α = ¬.

Abstract Version of the Basic Lemma

Lawvere's argument was in the setting of cartesian (closed) categories. Amazingly, it only needs finite products. 2Let C be a category with finite products. The terminal object (empty product) is written as 1. In Set it is any one-point set.

Definition 1 (Lawvere). An arrow f : A × A → V is weakly point surjective (wps) if for every p : A → V there is an x : 1 → A such that, for all y : 1 → A:

p • y = f • x, y : 1 → V
In this case, we say that p is represented by x.

Proposition 2 (Abstract Fixpoint Lemma). Let C be a category with finite products. If f : A × A → V is weakly point surjective, then every endomorphism

α : V → V has a fixpoint v : 1 → V such that α • v = v. Proof Define p : A → V by A × A f -V A ∆ A 6 p -V α ? Suppose p is represented by x : 1 → A. Then p • x = α • f • ∆ A • x def of p = α • f • x, x diagonal = α • p • x x represents p. So p • x is a fixpoint of α.
In [START_REF] Lawvere | Diagonal arguments and cartesian closed categories[END_REF], the Fixpoint Lemma is used to derive Gödel's First Incompleteness Theorem. Yanofsky's paper covers many more applications: semantic paradozes (Liar, Berry, Richard), the Halting Problem, existence of an oracle B such that P B = NP B , Parikh sentences, Löb's paradox, the Recursion theorem, Rice's theorem, von Neumann's self-reproducing automata, . . . All of these are 'one-person' results. The question of applying this argument to a two-person scenario such as the BK paradox has remained open.

How do we relate Lawvere to BK? As we have seen, the BK argument is valid in any regular category. This is pretty general. Nevertheless, BK needs a richer setting than Lawvere. To find common ground between them, we reformulate Lawvere, replacing maps by relations.

The rules of regular logic (just standard rules for this fragment of first-order logic) are sound in any regular category, and thus we can use logic to reason about relations in a wide variety of mathematical contexts. For further details, see [START_REF] Butz | Regular categories and regular logic[END_REF].

We shall write Sub : C op → Set for the subobject functor, which can be defined on any regular catgory. It sends an object A to the set of subobjects Sub(A), and acts by pullback on morphisms: notation is f → f * .

Given a formula φ of regular logic, with free variables X = x 1 : A 1 , . . . , x n : A n , where each A i is interpreted as an object of a regular category C, the standard categorical semantics [START_REF] Butz | Regular categories and regular logic[END_REF] assigns a subobject φ ∈ Sub(A 1 × • • • × A n ) as the intepretation of φ.

Relational Reformulation of Lawvere

As a first step, we reformulate Lawvere's notion of weak point surjectivity in relational terms.

To see how to do this, imagine the Lawvere wps situation ĝ : X × X → Ω is happening in a topos, and Ω is the subobject classifier. In the case of Set, Ω is just 2, and we are appealing to the familiar identification P(X) = 2 X of subsets with characteristic functions. Then this map ĝ corresponds to a relation R --X × X Such a relation is weakly point surjective (wps) if for every subobject p --X there is x : 1 → X such that, for all y : 1 → A: R(x, y) = p(y)

or in logical terms R(x, y) ⇐⇒ p(y).

In fact, a weaker notion suffices to prove the Fixpoint Lemma (cf. [START_REF] Soto-Andrade | Self-reference and fixed points: a discussion and an extension of Lawvere's theorem[END_REF]). We say that R is very weakly point surjective (vwps) if for every subobject p --X there is x : 1 → X such that: R(x, x) = p(x) .

What is a 'propositional operator' ?

To find the right 'objective' -i.e. language independent -notion, once again we consider the topos case, and translate out of that into something which makes sense much more widely.

In a topos, a propositional operator is an endomorphism of the subobject classifier α : Ω → Ω (In more familiar terms: an operator on the lattice of truth values, as e.g. in Boolean Algebras with Operators.) This corresponds to the endomorphism of V in Lawvere's original formulation. Note that by Yoneda, since Sub ∼ = C(-, Ω), such endomorphisms of Ω correspond bijectively with endomorphisms of the subobject functor -i.e. natural transformations τ : Sub =⇒ Sub.

Thus this is the right semantic notion of 'propositional operator' in general. Naturality corresponds to commuting with substitution.

The Relational Lawvere Lemma

Lemma 5 (Relational Lawvere fixpoint lemma). If R is a vwps relation on X in a regular category 3 , then every endomorphism of the subobject functor τ : Sub =⇒ Sub has a fixpoint.

Note that a fixpoint K1 =⇒ Sub from the constant functor valued at the terminal object is determined by its value at Sub(1).

Proof

We define a predicate P (x) ≡ τ (R(x, x)), so P = τ X (∆ * X (R)). By vwps, there is c : 1 → X such that:

P (c) = c * ( P ) = c, c * (R) = R(c, c) . Then P (c) = c * ( P ) = c * (τ X (∆ * X (R)) = τ 1 (c * • ∆ * X (R)) = τ 1 ((∆ X • c) * (R)) = τ 1 ( c, c * (R)) = τ 1 (c * ( P )) = τ 1 ( P (c) ).
considered here. Powerful general methods are available for finding such fixpoints, as solutions of domain equations [START_REF] Abramsky | Domain theory[END_REF] or final coalgebras [START_REF] Jan | Universal coalgebra: a theory of systems[END_REF].

The problem can be phrased as follows, in the setting of the strategy-based belief models of [START_REF] Brandenburger | An impossibility theorem on beliefs in games[END_REF]. We are given strategy sets S a , S b for Alice and Bob respectively. We want to find sets of types T a and T b such that

T a ∼ = P(U b ), T b ∼ = P(U a ) (5)
where U a = S a × T a and U b = S b × T b are the sets of states for Alice and Bob. Naively, P is powerset, but in fact it must be a restricted set of subsets (extensions of predicates) defined in some more subtle way, or such a structure would be impossible by mere cardinality considerations. Thus a state for Alice is a pair (s, t) where s is a strategy from her strategyset and t is a type. Given an isomorphism α : T a ∼ = -P(U b ), we can define a relation R a : U a + -U b by: R a ((s, t), (s , t )) ≡ (s , t ) ∈ α(t). Note that (s, t) assumes α(t). Because α is an isomorphism, the belief model (U a , U b , R a , R b ) is automatically assumption complete with respect to P(U a ) and P(U b ).

In fact, having isomorphisms α :

T a ∼ = -P(U b ), β : T b ∼ = -P(U a
) is more than is strictly required for assumption completeness. It would be sufficient to have retractions

T a £ P(U b ), T b £ P(U a )
i.e. maps r a : T a → P(U b ), s a : P(U b ) → T a such that r a • s a = id P(U b ) , and similarly for T b and P(U a ). 4 However, we shall emphasize the situation where we do have isomorphisms, where we can really speak of canonical solutions.

We shall now generalize this situation so as to clarify what the mathematical form of the problem is. Suppose that we have a category C, which we assume to have finite products, and a functor P : C → C. We are given objects S a and S b in C. Hence we can define functors F a , F b : C → C:

F a (Y ) = P(S b × Y ), F b (X) = P(S a × X).
Intuitively, F a provides one level of beliefs which Alice may hold about states which combine strategies for Bob with 'types' from the 'parameter space' Y ; and symmetrically for F b . Now we define a functor F : C × C → C × C on the product category:

F (X, Y ) = (F a (Y ), F b (X)).
To ask for a pair of isomorphisms as in ( 5) is to ask for a fixpoint of the functor F : an object of C × C (hence a pair of objects of C, (T a , T b )) such that

(T a , T b ) ∼ = F (T a , T b ).
This situation has been extensively studied in Category Theory and Theoretical Computer Science [START_REF] Jan | Universal coalgebra: a theory of systems[END_REF][START_REF] Barr | Terminal coalgebras in well-founded set theory[END_REF][START_REF] Abramsky | Domain theory[END_REF]. In particular, the notion of final coalgebra provides a canonical form of solution. Once again, previous work has focussed on 'oneperson' situations, although the tools needed for two-or multi-agent forms of solution -essentially the ability to solve simultaneous equations -are already in hand. Indeed, final coalgebras subsume what are known as terminal models in the game-theoretic literature on type spaces. What amount to terminal sequence constructions of final coalgebras have been used in the literature on Harsanyi type spaces [START_REF] Harsanyi | Games with incomplete information played by "Bayesian" players, I-III. Part I. The basic model[END_REF] to construct what are known as universal models. Heifetz and Samet gave the first construction of a universal type space in the category of measurable spaces [START_REF] Heifetz | Topology-free typology of beliefs[END_REF], following other work in more restricted contexts. Subsequently, Moss and Viglizzo made explicit use of coalgebraic ideas in [START_REF] Moss | Final coalgebras for functors on measurable spaces[END_REF]. Thus these well-developed methods from Theoretical Computer Science can be used to address the following question raised by Brandenburger and Keisler:

We end by noting that, to the best of our knowledge, no general treatment exists of the relationship between universal, complete, and terminal models (absent specific structure). Such a treatment would be very useful.

Our contribution here is to set the discussion in a wider context, emphasizing the construction of interactive belief models which are assumption complete.

The topic deserves a fuller treatment than is possible here. We shall content ourselves with giving some examples where known results on the existence of final coalgebras can be applied to yield assumption complete models.

Application to Assumption-Complete Models

We begin by noting that standard results allow us to lift one-person to two-(or multi-)agent constructions. Suppose we have endofunctors G 1 , G 2 : C → C. We can define a functor

G : C × C → C × C :: G(X, Y ) = (G 1 (Y ), G 2 (X)).
Note that this directly generalizes our definition of F from F a and F b . We have

G = (G 1 × G 2 ) • twist. It is standard that if G 1
and G 2 satisfy continuity or accessibility hypotheses which guarantee that they have final coalgebras, so will G.

Note that the final sequence for G will have the form

(1, 1) ← (G 1 (1), G 2 (1)) ← (G 1 (G 2 (1)), G 2 (G 1 (1)) ← • • • ← ((G 1 • G 2 ) k (1), (G 2 • G 1 ) k (1)) ← • • •
This 'symmetric feedback' is directly analogous to constructions which arise in Geometry of Interaction and the Int construction [START_REF] Abramsky | New foundations for the geometry of interaction[END_REF][START_REF] Abramsky | Retracing some paths in process algebra[END_REF][START_REF] Abramsky | Concurrent games and full completeness[END_REF]. It is suggestive of a compositional structure for interactive belief models. We shall now consider three specific settings where the general machinery we have described can be applied to construct assumption complete models as final coalgebras. In each case we must specify the ambient category C, and the functor P.

Sets We firstly consider Set, the category of sets and functions. Our candidate for P is a variant of the powerset functor. We take P(X) = P κ (X), the collection of all subsets of X of cardinality less than κ, where κ is an inaccessible cardinal. 5It is standard that, for any sets S a , S b , the functors F a and F b are accessible, and hence so is the functor

F = (F a × F b ) • twist : C × C → C × C. Hence we get a final coalgebra γ : (T a , T b ) ∼ = -(P κ (S a × T b ), P κ (S b × T a )).
This yields an assumption complete belief model, as previously discussed.

Note that the terminal sequence for this functor is always transfinite, as analyzed in detail in [START_REF] Worrell | Terminal sequences for accessible endofunctors[END_REF]. Even in the case κ = ω (finite subsets), ω + ω stages are required for convergence to the final coalgebra.

Stone Spaces Another convenient setting for final coalgebra is the category of Stone spaces, i.e. totally disconnected compact Haussdorff spaces [START_REF] Abramsky | A Cook's tour of the finitary non-well-founded sets[END_REF][START_REF] Kupke | Stone coalgebras[END_REF]. By Stone duality, this category is dual to the category of Boolean algebras. Our candidate for P here is the Vietoris powerspace construction [START_REF] Michael | Topologies on spaces of subsets[END_REF]. In [START_REF] Abramsky | A Cook's tour of the finitary non-well-founded sets[END_REF], one can find essentially a treatment of the one-person case of the situation being considered here. The final coalgebra constructed here is closely related to the model built in a more concrete fashion in [START_REF] Brandenburger | An impossibility theorem on beliefs in games[END_REF]. We get stronger properties (isomorphism rather than surjection) and a clearer relation to general theory.

In this case, the final coalgebra is reached after ω stages of the terminal sequence, because of continuity properties of the functor.

Algebraic Lattices As a final example, we venture into the realm of Domain theory [START_REF] Gierz | Continuous Lattices and Domains[END_REF][START_REF] Abramsky | Domain theory[END_REF]. We work in the category of algebraic lattices and Scott-continuous maps (those preserving directed joins). We have two convenient choices for P: the lower and upper powerdomain constructions, both well-studied in Domain theory. In the first case, we take the lattice of Scott-closed subsets of an algebraic lattice, ordered by inclusion. In the second, we take the subsets which are compact in the Scott topology, and upwards closed in the partial ordering, ordered by reverse inclusion. In either case, we obtain a continuous functor, which converges to the final coalgebra in ω stages of the terminal sequence.

Closure under logical constructions We have constructed models which are assumption complete in a semantic sense, with respect to the predicates specified by the functor P. A further issue is how expressive these collections of predicates are; this can be made precise in terms of which logical constructions they are closed under, and hence which logics can be interpreted. Brandenburger and Keisler show that their topological belief model is closed under conjunction, disjunction, existential and universal quantification, and constructions corresponding to the assumes and believes modalities. The same arguments show that our model in Stone spaces is closed under these constructions. Similar arguments show that the model in Set is also closed under these constructions. In this case, closure under the believes modality requires that if a set S has cardinality less than κ, so does its powerset. This follows from the inaccessibility of κ. Finally, the models in algebraic lattices are also closed under these constructions, with the proviso that appropriate order-theoretic saturation (upwards or downwards closure) must be applied in some cases.

These models also allow for various forms of recursive definition. We leave a detailed account to an extended version of this paper.

Further Directions

There are a number of natural directions to be pursued. One is to a more comprehensive account of the construction of belief models and type spaces, taking full advantage of the use of categorical methods, and of developments in coalgebraic logic. Another is to a finer analysis of the use of completeness hypotheses in justifying solution concepts for games. Finally, we would like to pursue the broader agenda of understanding the mathematical structure of interaction, and the scope of interactive versions of logical and mathematical phenomena which have previously only been studied in 'one-person' versions.

Wider perspective: applied coalgebra We also wish to put this work in a wider perspective, emphasizing in particular the rôle which we believe that coalgebra can play, as a wide-ranging theory of systems encompassing reflexive forms of behaviour, going far beyond the direct applications in computer science which have mainly been studied to date. Coalgebraic representations of physical systems are discussed in [START_REF] Abramsky | Coalgebras, Chu spaces, and representations of physical systems[END_REF]. Potential further applications in biology and economics are currently under investigation.

Lemma 4 .

 4 which is a closed formula built from atomic formulas, plus a 'hole' [•]. We obtain a formula O[φ] by replacing every occurrence of the hole by a formula φ. The formal version of the Fixpoint Lemma is now stated as follows: Under the assumptions (A1)-(A3), every definable unary propositional operator O[•] has a fixpoint, i.e. a sentence S such that S O[S], O[S] S.

Related forms of completeness assumption are used in the analysis of various solution concepts in games in[START_REF] Battigalli | Strong belief and forward-induction reasoning[END_REF][START_REF] Brandenburger | Admissibility in games[END_REF].

In fact, even less suffices: just monoidal structure and a 'diagonal' satisfying only point naturality and monoidality.

In fact, it suffices to assume that the category is and has finite limits.

Brandenburger and Keisler ask only for surjections, but they are working in a setting where surjections can always be split.

Alternatively, and essentially equivalently, we can follow Peter Aczel[START_REF] Aczel | A final coalgebra theorem[END_REF], and work over the ('superlarge') category of classes, taking P(A) to be the class of sub-sets of a class A.

Acknowledgements

This research was supported by the EPSRC grant EP/F067607/1 and by ONR. An extended abstract of an earlier version of this paper was presented at the LOFT 2010 conference. Discussions with Adam Brandenburger and Viktor Winschel are gratefully acknowledged.

Our Basic Lemma can now be restated as follows:

Lemma 6. If R a and R b satisfy the BK assumptions (A1)-(A3), then R is vwps.

Hence the relational Lawvere fixpoint lemma applies! As an immediate Corollary, we obtain: Lemma 7 (BK Fixpoint Lemma). If R a and R b satisfy the BK assumptions (A1)-(A3), then every endomorphism of the subobject functor has a fixpoint.

Multi-Agent Generalization of BK

A multiagent belief structure in a regular category is

where we write R :

We now formulate Generalized BK Assumptions for such a belief cycle: For each subobject p --A, there is some c :

These assumptions can be written straightforwardly as regular sequents.

Multiagent BK Fixpoint Lemma We can define the relation

Lemma 8 (Generalized Basic Lemma). Under the Generalized BK assumptions, R is vwps.

Hence the Relational Fixpoint Lemma applies. Note that in the one-person case n = 0, assumption completeness coincides with weak point surjectivity.

In modal terms:

One-person BK is (relational) Lawvere! The force of the BK argument is that the (very) wps property propagates back along belief chains.

In particular, this produces the 'believes-assumes' construction of BK, or the generalized version believes * -assumes, in which 'believes' is iterated n times followed by an 'assumes'.

Compositional Analysis

We shall briefly consider the issue of compositional gluing of belief relations with given completeness properties. For simplicity, we shall conduct our discussion concretely, in terms of relations on sets. To incorporate the idea of relativization to a set of predicates, we shall assume that each set A is given together with a set P(A) ⊆ P(A) \ {∅} of (non-empty) predicates on A.

Suppose we are given a relation R : A + -B. We say that R is assumptioncomplete (with respect to P) if for every p ∈ P(B), for some x ∈ A, for all y ∈ B: R(x, y) ⇔ p(y).

This is just wps again, of course. We say that it is belief-complete if for all y ∈ B: R(x, y) ⇒ p(y).

and also ∃y.R(x, y). Modally, this corresponds to

x |= Pp ∧ Q .

Now suppose we have relations

Lemma 9 (Composition Lemma). Suppose that:

1. R ab is belief-complete with respect to P(B).

2. R bc is assumption-complete with respect to P(C).

For each p ∈ P(C), bc p ∈ P(B).

Then the composition R ac = R ab ; R bc : A + -C is assumption-complete with respect to P(C).

Note the need for the comprehension assumption (3). We now prove a kind of converse to the Composition Lemma, which characterises belief-completeness, and shows why the BK assumptions and the believesassumes pattern arise in this context.

Theorem 1 (Compositional Characterization). A relation R :

A + -B is belief complete with respect to P(B) if and only if, for every S : B + -C such that 1. S is assumption complete with respect to P(C) 2. S p ∈ P(B) for every p ∈ P(C) the composition R; S : A + -C is assumption complete with respect to P(C).

Proof The left to right implication is Lemma 9.

For the converse, we suppose that R is not belief-complete for some p ∈ P(B). We let C = {0, 1}, and define S to be the characteristic function of p. We take P(C) = {q}, where q = {1}. Note that q = p, and that S is assumption complete with respect to P(C) -indeed, any element of p, which by our general assumption on predicates is non-empty, assumes q.

We claim that R; S is not assumption complete for q. Indeed, for any x ∈ A, if R(x) = ∅, then R; S(x) = ∅, and so x does not assume q. The only other possibility, since by assumption R is not belief complete with respect to p, is that for some y ∈ p, R(x, y). In this case, R; S(x, 0), and so x does not assume q.

Remark The proof of the Compositional Characterization Theorem assumes that we have the freedom to choose any collection of predicates we like on a given set. It would be useful to have a more general formulation and result.

Functorial Constructions of Assumption-Complete Models

We now turn to the question of constructing belief models which are assumption complete with respect to a natural class of predicates. The categorical perspective is well-suited to this task. Indeed, leaving aside model-theoretic subtleties, we can identify the problem as essentially one of finding fixpoints for certain 'powerset-like' functors. This 'recursion in the large' at the level of types, to support 'recursion in the small' at the level of programs, is a familiar theme in Theoretical Computer Science [START_REF] Abramsky | Domain theory[END_REF]. If we think of recursion as enabling selfreference, in formulas rather than programs, we see the link to the ideas being


Guillaume Noyel
email: guillaume.noyel@i-pri.org

Michel Jourlin

Michel Smans

Rebecca Thomas

Simon Iles

Gavin Bhakta

Andrew Crowder

David Owens

Peter Boyle

Thomas Adams

Enhancing Eye Fundus Images for Diabetic Retinopathy Screening

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

A ABSTR BSTR BSTR BSTR BSTRA ACT CT CT CT

Many eye fundus images present strong variations of contrast which can be a limitation to the diagnosis of the retinopathy. Either some lesions are not taken into account or only a limited part of the domain of the image can be read. Graders have to manually adjust the contrast, which is tedious and not easily reproducible.

We have developed an automatic system, which standardises the colour contrast across the whole domain of the image. The method is consistent with the physical principles or image formation and ensures that the colour aspect of lesions such as micro-aneurysms or anatomical structures such as veins are similar. It is more powerful than the existing grey level methods.

We have tested our approach on several thousand images acquired in good or in harsher conditions. Some were bright while others were dark. Expert graders have checked the enhanced images. Diagnosis becomes more obvious and the grading more comfortable.

Another limitation for the diagnosis is that images of the same patient acquired for di erent examinations cannot be directly superimposed. Indeed, the eye of the patient is never in the exact same position, the image is a projection of a 3D scene into the plane of the sensor, the optics of the camera creates a radial deformation and the colour of the image may have changed.

We have developed an automatic method to superimpose eye fundus images acquired in the same position (nasal or macular). It is based on contrast standardisation, matching of salient points and a deformation model taking into account two radial distortions.

We have performed tests for 69 patients with pairs of retinal examinations acquired in good conditions at an interval of one year with and without the same camera. A similar test has been performed on 5 patients with 20 pairs acquired in harsher conditions. A minimum of 96% of pairs were correctly superimposed. This is an important step towards the longitudinal analysis of large public health databases.

C CONTR ONTR ONTR ONTR ONTR ONTRA AST ST ST ENH ENH ENH ENHA ANCEMENT NCEMENT NCEMENT NCEMENT NCEMENT NCEMENT NCEMENT NCEMENT NCEMENT NCEMENT

Figure 1 illustrates the improvement brought by our method of standardizing the colour contrast across the entire Figure 1 illustrates the improvement brought by our method of standardizing the colour contrast across the entire Figure 1 illustrates the improvement brought by our method of standardizing the colour contrast across the entire Figure 1 illustrates the improvement brought by our method of standardizing the colour contrast across the entire Figure 1 illustrates the improvement brought by our method of standardizing the colour contrast across the entire Figure 1 illustrates the improvement brought by our method of standardizing the colour contrast across the entire Figure 1 illustrates the improvement brought by our method of standardizing the colour contrast across the entire image. image. image.

The enhanced colour images allow a more comfortable grading and a more obvious diagnostic. The enhanced colour images allow a more comfortable grading and a more obvious diagnostic. The enhanced colour images allow a more comfortable grading and a more obvious diagnostic. The enhanced colour images allow a more comfortable grading and a more obvious diagnostic. The enhanced colour images allow a more comfortable grading and a more obvious diagnostic. The enhanced colour images allow a more comfortable grading and a more obvious diagnostic. The enhanced colour images allow a more comfortable grading and a more obvious diagnostic. The enhanced colour images allow a more comfortable grading and a more obvious diagnostic. The enhanced colour images allow a more comfortable grading and a more obvious diagnostic. The enhanced colour images allow a more comfortable grading and a more obvious diagnostic.

Figure 1. Contrast enhancement by our colour method

Original images Enhanced

exam of the same patient with a year of interval acquired in harsh conditions (strong variation of contrast in the original images)

Original images Enhanced images

I I I IM MA A A A A A A A A AGE GE GE GE GE GE GE GE SUPER SUPER SUPER SUPER SUPER SUPER SUPER SUPER SUPER SUPER SUPER SUPER SUPER SUPER SUPERI IMPOS MPOS MPOS MPOS MPOS MPOS MPOS MPOS MPOS MPOS MPOS MPOS MPOS MPOS MPOS MPOSI IT T T T T TI ION ON ON ON ON ON ON ON ON

RESULTS AND CONCLUSIONS

Our automatic method will allow an easier follow-up of patients with diabetic retinopathy.

Figure 2

 2 Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).

  Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).

  Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).

  Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).

  Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).

  Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).

  Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).

  Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).

  Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).

  Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).

  Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).

  Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).

  Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).

  Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).

  Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).

  Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).

  Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).Figure 2 details (with false colours) the two corrections needed for a proper superimposition (position and distortion).

Figure 2 .Figure 3

 23 Figure 2. Naive and correct superimposition of pairs of eye fundus images Figure 2. Naive and correct superimposition of pairs of eye fundus images Figure 2. Naive and correct superimposition of pairs of eye fundus images Figure 2. Naive and correct superimposition of pairs of eye fundus images Figure 2. Naive and correct superimposition of pairs of eye fundus images Figure 2. Naive and correct superimposition of pairs of eye fundus images Figure 2. Naive and correct superimposition of pairs of eye fundus images Figure 2. Naive and correct superimposition of pairs of eye fundus images Figure 2. Naive and correct superimposition of pairs of eye fundus images Figure 2. Naive and correct superimposition of pairs of eye fundus images Figure 2. Naive and correct superimposition of pairs of eye fundus images Figure 2. Naive and correct superimposition of pairs of eye fundus images Figure 2. Naive and correct superimposition of pairs of eye fundus images Naive superimposition showing the di erence in size and position of the images (False colours are used)

Figure 3 .

 3 Figure 3. Correct superimpositions of pairs of eye fundus images

© iPRI -International Prevention Research Institute, 95 Cours Lafayette, 69006 Lyon, France | Tel: +33472171199 | Web: www.i-pri.org | Email: info@i-pri.org -Poster ref: 072/2017/05/15

t t t t t w w w w w w w w w w ww w w w w w w w w w ww w w w w w w w w w w w. . . . . . . . . . .