Georges-Henri Cottet

Keywords:

à 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.

Forum "Math-for-Industry" 2013 November 4-8, 2013, Nishijin Plaza, Fukuoka, Japan Mathematics, Hybrid computing and HPC Georges-Henri COTTET CNRS and University Grenoble-Alpes, France HPC appears more and more as a key player in the field of numerical simulation and data processing. This trend comes of course with the desire to perform simulations that are closer and closer to real world situations, and with the development of clusters and platforms that provide access to hundreds to thousands CPU/GPU nodes.

The application domains encompass many fields, from fluid mechanics to biology and nano-sciences, in academic research as well as for industrial applications.

Concerning industrial applications, major groups have often already a good practice of HPC, with dedicated manpower and available in-house platforms. The access of SMEs to HPC is more problematic as they do not have the appropriate resources in hardware and manpower, and it is sometimes hard for them to have a clear idea of the gain they will obtain through HPC. In the first part of the talk, I will talk about a national initiative led by INRIA, GENCI and BPI, to promote the access of SMEs to HPC. This initiative provides support both in terms of market analysis, access to hardware and technical environment. It now involves middle-size HPC platforms that are distributed in French universities. This initiative will therefore give new opportunities to researchers, in particular mathematicians, to be connected to industrial collaborations.

HPC is actually not only a question of accessing hardware and adapting existing codes to massively parallel platforms. It also raises questions about mathematical and numerical models that optimize the emerging hardware and analyze the huge amount of data associated with these simulations, and software engineering to distribute algorithms on heterogeneous clusters. Mathematicians therefore can use HPC as a mean to access challenging industrial collaborations in which they can contribute through new methods and algorithms, in both scientific computing and statistics.

In the second part of the talk I will try to illustrate this point of view with ongoing research in Grenoble related to High Performance (hybrid) Computing for the direct numerical simulation of turbulent mixing. Turbulent mixing appears in many applications (environment, combustion, ..). The turbulent mixing of a scalar often induces a separation of the scales that appear in the flow and in the scalar. This feature makes turbulent mixing a natural candidate for hybrid computation, where difference computed quantities, the flow and the scalar in this example, are treated by different algorithms and, ultimately, distributed to different type of hardwares. We will describe such an hybrid approach, combining a spectral flow solver and a semi-lagrangian scalar solver, and running on massively parallel platforms. We will show how this numerical approach allows to capture the scalar up to the dissipative scales at a minimal cost.

Figure 1 .

 1 Figure 1. Vorticity (left) and scalar (middle) scales in a turbulent flow. Schmidt number=128. Right pictures : zoom of flow and scalar showing the scale gap between the vorticity (top) and the scalar (bottom).


Jean Gillibert

CATEGORY THEORY, LOGIC AND FORMAL LINGUISTICS: SOME CONNECTIONS, OLD AND NEW

Keywords:

We seize the opportunity of the publication of selected papers from the Logic, categories, semantics workshop in the Journal of Applied Logic to survey some current trends in logic, namely intuitionistic and linear type theories, that interweave categorical, geometrical and computational considerations. We thereafter present how these rich logical frameworks can model the way language conveys meaning.

A SEMINAR AND WORKSHOP ON CATEGORY THEORY, LOGIC AND LINGUISTIC

APPLICATIONS

The present issue of the Journal of Applied Logic gathers a selection of papers presented at a workshop Logic, categories, semantics held in Bordeaux in November 2010. This workshop was organised as a fitting conclusion to the activities of a weekly reading group a weekly reading group called Sheaves in logic and in geometry in 2009/2010 and Logic, categories, geometry in 2010/2011.

Those activities are common to the maths and computing departments of the University of Bordeaux (IMB-CNRS and LaBRI-CNRS). Although he did not contribute to this introduction, we must thank Boas Erez (IMB, Bordeaux) who was an enthusiastic participant and speaker in our reading group. We would like to thank for their scientific and financial support: our tow departments, (Institut de Mathématiques de Bordeaux, Laboratoire Bordelais de Recherche en Informatique), INRIA Bordeaux Sud-Ouest, the ANR project LOCI, and the project ITIPY (Aquitaine Region) and the French mathematical society (SMF).

Unfortunately, the material in this issue of the Journal of Applied Logic does not cover all the great talks we had the privilege to hear, but one can find published material that more or less cover these talks (and these references themselves include further references):

• Pierre Cartier (IHES, Bures) Sur les origines de la connexion entre logique intuitionniste, catégories et faisceaux, cf. [START_REF] Cartier | Logique, catégories et faisceaux[END_REF]; • Jean-Yves Girard (CNRS, IML, Marseille) Interdire ou réfuter? Le statut ambigu de la normativité, cf. [START_REF]Normativity in logic, Epistemology versus Ontology[END_REF]; • Paul-André Melliès (CNRS, PPS, Paris) Logical proofs understood as topological knots, cf. [START_REF] Melliès | Game semantics in string diagrams[END_REF]; • Michael Moortgat (Universiteit Utrecht) Continuation semantics for generalized Lambek calculi, cf. [START_REF] Moortgat | Proof nets for the Lambek-Grishin calculus[END_REF]; • Carl Pollard (Ohio State University, Columbus) Remarks on categorical semantics of natural language, cf. [START_REF] Pollard | Are (linguists') propositions (topos) propositions?[END_REF].

INTUITIONISTIC LOGIC

Type theory and categorical logic, which are at the hear of this issue, all rely on intuitionistic logic. Even linear logic, which is also discussed by two articles of this issue, may be viewed as a refinement of intuitionistic logic.

It is quite a challenge to explain briefly what intuitionistic logic is and how it relates to other logical trends. Regarding the historical development of logic, we refer to the standard [START_REF] Kneale | The development of logic[END_REF] and regarding a standard logic master course we refer the reader to the standard textbook [START_REF] Van Dalen | Logic and structure[END_REF] which includes a chapter on intuitionistic logic.

Logic is concerned with"truth", and let us vaguely say that "truth" holds or not of formulae that are formalisations of common language sentences, or of mathematical statements, and as such logic has at least two facets. A formula F can be true because it is correctly derived from formulae that are already established or assumed to be true, and this is the proof theoretical view of truth that started with Aristotle. The same formula F can also be true in all or in some situation once the symbols in the formula are properly interpreted: that's the model theoretical view of truth, which is much more recent. Besides these two well established viewpoints, there exists a slightly different view of "truth" with Ancient origins, dialectics which emerge from the interaction between proofs and refutations. Nowadays this view culminates in game theoretical semantics, and ludics, and the presentations by J.-Y. Girard and P.-A. Mellis during our workshop developed this interactive view. [START_REF]Normativity in logic, Epistemology versus Ontology[END_REF][START_REF] Melliès | Game semantics in string diagrams[END_REF] An important theorem, due to Gödel as an impressive number of the fundamental results logic, is that for first order classical logic, the two notions of truth coincide: a formula is true in any model if and only if it can be proved. This result admits a a more striking formulation as: a formula C can be derived from formulae H 1 , . . . , H n if and only if any model satisfying H 1 , . . . , H n satisfies C as well. Such a result holds for classical propositional logic and for classical first-order logic, also known as predicate calculus.

Intuitionistic logic comes from doubts that appeared during the crisis of the foundations of mathematics, between the XIX and XX centuries. These doubts concerned existential statements in infinite sets. For instance it is admittedly a bit strange, especially in an infinite universe, that ∃x(B(x) =⇒ ∀yB(y)), although it is absolutely correct in classical logic using principles like U =⇒ V ≡ ¬U ∨V , ¬¬A ≡ A, ¬∀xA(x) ≡ ∃x¬A(x). According to intuitionistic logic, tertium non datur, or any of the principles that are equivalent to it, like reductio ad absurdum or Pierce's law, should be left out from deduction principles.

When restricting ourselves to intuitionistic logic both facets of truth are modified:

• In order to maintain the completeness results, models need to be more complex: the usual models ought to be replaced with structured families of classical models, like Kripke models or (pre)sheaves, cf. section 3. • Intuitionistic proofs are more interesting: as opposed to classical proofs, they can be viewed as algorithms (as programs of a typed functional programming language) or as morphisms in a category (which is not a poset, i.e. with many morphisms from an object to another).

Each of these two aspects brings connections with category theory. The first one yields models of higher order intuitionistic logic, e.g. with (pre)sheaves of L -structures (classical models, roughly speaking). The second one yields models that interpret proofs as morphisms in a cartesian closed category.

A HISTORICAL CONNECTION BETWEEN LOGIC AND GEOMETRY: (PRE)SHEAVES, TOPOSES AND CATEGORICAL MODELS OF INTUITIONISTIC LOGIC

Pierre Cartier reminded us in the inaugural lecture of the workshop that the connection between intuitionistic logic and topos theory appeared in the sixties. We refer the reader to [START_REF] Cartier | Logique, catégories et faisceaux[END_REF] for a survey, and to [START_REF] Mac | Sheaves in geometry and logic: a first introduction to topos theory[END_REF] for a thorough treatment, and to [START_REF] Mac | Categories for the working mathematician[END_REF] for an excellent textbook on category theory.

Inspired by the work of Eilenberg and Mac Lane on categories, Lawvere started in 1964 to introduce a categorical approach to set theory, and Lambek was looking at categories as deductive systems, the 1972 book edited by Lawvere Toposes, Algebraic Geometry, and Logic gives a pretty good idea of the landscape at the end of the 60s. [START_REF]Toposes, algebraic geometry, and logic[END_REF] At the same time, Grothendieck was introducing groundbreaking concepts in order to define a topology on an algebraic variety that would play a similar role to the topology of the complex points, namely the étale topology. The first step in Grothendieck's construction is the notion of site, that is, a category endowed with a notion of covering that is reminiscent of open coverings in topology. The concept of site does not exactly capture the'topology" of a situation, since different sites can give rise to the same category of sheaves. Thus Grothendieck chose to take a category of sheaves of sets over a given site as a notion of generalized topological space, and he called such a category a topos But another important idea of Grothendieck was somehow more surprising: the étale site is just a step in the construction, the final notion to study is the category of sheaves of sets on the site, that he calls a topos. This category has many properties in common with the category of sets, and possesses a good notion of localisation. These radically new ideas were first developed by Grothendieck and his group in [START_REF]Théorie des topos et cohomologie étale des schémas[END_REF].

Taking into account this new approach, Lawvere and Tierney in [START_REF] William | Quantifiers and sheaves, Actes du congrès international des mathématiciens[END_REF] gave before 1970 a new definition of topos (elementary toposes), which does not refer to a site. One of the avantages of this theory is that each topos contains an object Ω, that plays the role of all possible truth values, and has the (internal) structure of a Heyting algebra. Hence intuitionist logic naturally appears as being the internal logic of the topos.

This connection with intuitionistic logic was formulated by Lawvere at the same time [START_REF] William | Quantifiers and sheaves, Actes du congrès international des mathématiciens[END_REF]. Shortly afterwards, Lawvere and Tierney in [START_REF]Toposes, algebraic geometry, and logic[END_REF] discovered that models of set theory corresponding to proofs of the independence of the axiom of choice and continuum hypothesis by Cohen's method of forcing [START_REF] Paul | Set theory and the continuum hypothesis[END_REF] were in fact elementary toposes see e.g. [START_REF] Mac | Sheaves in geometry and logic: a first introduction to topos theory[END_REF][START_REF] Borceux | Handbook of categorical algebra. 3: Categories of sheaves[END_REF].

On the other hand, the internal logic of the topos shed a new light on categories of sheaves. Namely, one can handle sheaves as if they were sets with elements but with respect to the internal language, but when reasoning about these elements one should follow should follow the rules of intuitionistic logic.

In order to fix ideas, let us recall that a category C is defined by the following data: (a) a class of objects; (b) a class of arrows (or morphisms) whose domain and codomain are objects of C ; (c) a partial binary operation on arrows called composition, required to be associative; (d) every object is endowed with an identity arrow. If for any objects A and B of C , the class Hom(A, B) of all morphisms from A to B is a set, the category is said to be locally small, and most of the useful categories are locally small. If the class of objects and of morphisms of C are sets, C is said to be small.

It is easy to define morphisms of categories, which for historical reasons are called functors.

A category can be seen as a directed graph with a composition operation on arrows. The most basic examples of categories are the category of sets, the category of groups, the category of K-vector spaces where K is a field, the category of topological spaces, etc. Roughly speaking, categories allow to handle most kind of structural questions in mathematics.

We will now focus our attention on sheaves, which are central in this story. Let X be a topological space. A presheaf of sets is a contravariant functor from the category of open subsets of X (a poset, actually) to the category of sets 1 .

A morphism of presheaves φ : A → B is given by a family of maps φ U : A(U) → B(U) (where U runs through all open subsets of X) that is compatible with restriction maps in the following sense: for any inclusion V ⊆ U between open subsets of X, the following diagram commutes

A(U) φ U ----→ B(U)     A(V ) φ V ----→ B(V )
where vertical maps are the restrictions induced by the inclusion V ⊆ U.

It is worth noticing that (pre)sheaves of L -structures of some theory T over a topological space -whose open sets can be viewed as a poset category that is a Heyting algebra -define a notion of model that is complete for intuitionistic logic. An L -structure is a set with an interpretation of the first order language L , and the morphisms between Lstructures, in particular the restrictions morphisms of the sheaf, are functions that preserves function symbols and the truth of atomic formulae -hence they are more general than the usual elementary morphisms of model theory which preserve the truth of all formulae. This construction due to Joyal is related to forcing and is a particular case of Kripke models [START_REF] Kripke | A completeness theorem in modal logic[END_REF] and therefore is known as Kripke-Joyal forcing. [START_REF] Boileau | La logique des topos[END_REF] The proof of completeness of (pre)sheaf models can be inferred from results in [START_REF] Troelstra | Constructivism in mathematics[END_REF]; recently, Ciardelli obtained a short and direct proof of this completeness result [START_REF] Ivano | A canonical model for presheaf semantics[END_REF].

A sheaf of sets is a presheaf F which satisfies the following condition: for any open subset U of X and any family (U i ) of open subsets of X such that U = ∪U i , there is an equaliser diagram

F (U) → ∏ i F (U i ) ⇉ ∏ j,k F (U j ∩U k )
(this means that the first map is injective and its image is exactly the set where the two other maps coincide 2 ).

In other words, a "compatible" family of local sections of F can be glued-in a unique way-into a global section of F i.e. a U-section of F . This is exactly what one needs in order to perform "local to global" yoga.

By definition, a morphism of sheaves is just the same as a morphism of presheaves. Hence the category of sheaves on X, that we denote by Sh(X), is a full subcategory of the category of presheaves. In order to describe its properties, we introduce the notion of cartesian closed category (CCC).

Definition 1. A category is said to be cartesian closed whenever:

(1) It has a terminal object here noted 1 (it can be noted T );

1 Explicitely, a presheaf A is a family of sets A(U) (where U runs through all open subsets of X) together with

restriction maps A(U) → A(V ) for any inclusion V ⊆ U between open subsets of X. Of course, these restriction maps can be composed, that is, if W ⊆ V ⊆ U then the restriction map A(U) → A(W ) is equal to the composition A(U) → A(V ) → A(W ). 2
The first map is induced by inclusions U i ⊆ U, and the two other maps are respectively induced by inclusions

U j ∩U k ⊆ U j and U j ∩U k ⊆ U k .
(

2) Any two objects A and B have a product written A × B; (3) Any two objects A and B have an exponential noted B A or A → B.

In more detail, 1 a terminal object is an object 1 such that for any object A there exists a unique arrow A → 1; 2 if A and B are two objects, the product A × B (if it exists) is an object such that, for all Y , there is a bijection Hom(Y, A) × Hom(Y, B) ≃ Hom(Y, A × B) which is natural in Y ; 3 if A and B are two objects, the exponential noted B A (if it exists) is an object such that, for all Y , there is a bijection Hom(Y × A, B) ≃ Hom(Y, B A ) which is natural in Y . Another limit is useful, equaliser: given tow morphisms f and g from A to B, an equaliser of f and g is a morphism e from C to A such that f • e = g • e and for any morphism

d from D to A with f • d = g • d there is a unique k from D to C such that e • k = d.
Let us check that Sh(X) is cartesian closed. The constant sheaf 1 defined by 1(U) = { * } for all U is clearly a terminal object in Sh(X). The product of two sheaves, as well as the equaliser of sheaf morphisms with the same domain and codomain exist, hence all finite limits exist in the category of sheaves. Finally, exponential objects exist: for any two sheaves A and B, we let B A be the sheaf U → Hom(A| U , B| U ), where F | U denotes the restriction of F to U3 .

More generally, the category Sh(X) inherits many properties from the category of sets, which is not surprising if we consider a sheaf as being a "continuous family of sets". This leads us to the next topic, namely elementary toposes.

Definition 2. According to Lawvere and Tierney, an elementary topos is a category E satisfying the following properties:

(1) E has finite limits;

(2) E has exponentials;

(3) E has a subobject classifier.

The first two conditions imply that a topos is a cartesian closed category. In fact, the main difference between CCC and toposes is the existence of a subobject classifier.

Let us recall that Ω is a subobject classifier if, for any object A of E, there is a natural isomorphism between subobjects of A and the set of maps A → Ω. More precisely, Ω comes with a canonical map 1 → Ω (where 1 is the terminal object of E) which satisfies the following universal property: for any monomorphism f : B → A there exists a unique morphism g :

A → Ω such that the square B ----→ 1 f     A g ----→ Ω is a fibered product or pullback (roughly speaking, B is the inverse image of 1 by g).
In the category of sets, Ω = {0, 1} (Boolean truth-values).

In the category of sheaves, the subobject classifier is defined as follows: for any open subset U of X, we let Ω(U) to be the set of all open subsets of U. Roughly speaking, an assertion inside the topos Sh(X) may have an intermediate truth value, which from the viewpoint of an open subset U is the open subset of U where the assertion is true.

In this issue, the paper Continuity and geometric logic by Steve Vickers emphasises the connection with topology by exploring geometric logic, that is many sorted logic with finite conjunctions and arbitrary disjunctions (also existential quantification). Given that axiom x:A ⊢ x:A z 1 :Z 1 ,..., z p :Z p ⊢ t:B exchange

(σ :permutation) z σ (1) :Z σ (1) ,..., z σ (p) :Z σ (p) ⊢ t:B z 1 :Z 1 ,..., z p :Z p , x:A, x:A ⊢ t:B contraction z 1 :Z 1 ,..., z p :Z p , x:A ⊢ t:B z 1 :Z 1 ,..., z p :Z p , ⊢ t:B weakening z 1 :Z 1 ,..., z p :Z p , x:A ⊢ t:B z 1 :Z 1 ,..., z p :Z p , x:A ⊢ t:B abstraction / hypothetical reasoning Γ, x:A ⊢ (λ x A .t):A → B z 1 :Z 1 ,..., z p :Z p , ⊢ f :A → B y 1 :Y 1 ,..., y k :Y k ⊢ u:A application / modus ponens z 1 :Z 1 ,..., z p :Z p , y 1 :Y 1 ,..., y k :Y k ⊢ f (u):B FIGURE 1.
The Curry-Howard isomorphism [START_REF] Howard | The formulae-as-types notion of construction[END_REF]. Upper case letters stand for propositions. On the left handside of "⊢" one only has type assignments for variables, like x : X. On the right hand side, before the ":" there is a lambda term which encodes the proofs. Leaving out terms, that are on the left hand side of ":" one get a standard natural deduction system for proposition logic as introduced by Gentzen. [START_REF] Gentzen | Untersuchungen über das logische Schließen I[END_REF][START_REF]Untersuchungen über das logische Schließen II[END_REF] These rules infer a sequent from one or two sequents a sequent being a sequence of hypotheses and a formula on the right hand side, Z 1 , .., Z p ⊢ C meaning:

(Z 1 & • • • Z p ) → C.
classical models of a geometric theory T are not complete, one has to look models of T inside a topos, and there exists a classifying topos whose category of T models is universal. This is a point-free manifestation of the "space of models of T ".

INTUITIONISTIC PROOFS, TYPED LAMBDA CALCULUS AND CARTESIAN CLOSED

CATEGORIES

A second link between intutionistic logic and category theory is the following. Proofs in (propositional) intuitionistic logic can be viewed as typed lambda terms, that are functional programs. The main idea is that a proof of A → B maps proofs of A to proofs of B, hence it is rather natural to interpret a formula (with ∧, →) by the sets of its proofs. Functions can be applied to arguments of the right type, and composed. To compute such a term, one substitutes the occurrences of the bound variable used to define the function with the argument of the function:

(λ x A . t B )(u A ) β t[x A : = u A ]
Values are normal terms i.e. terms that cannot be reduced any further.

In figure 4 we give the proof rules and the corresponding proof terms, that are simply typed lambda terms, a good reference being [START_REF] Girard | Proofs and types[END_REF] and [START_REF] Lambek | Introduction to higher order categorical logic[END_REF] on the categorical aspects.

Functions in this setting are algorithms (that always converge) that represent total recursive functions, the ones whose totality can be proved within the underlying logical system. They are defined intentionally, how could one view them as usual functions? Functions can be viewed as morphisms in a cartesian closed category, cf. definition 1 above -in this logical setting, B A is rather written A → B. Observe that the logical rules match categorical isomorphisms, for instance,

A → (B → C) ∼ = (A × B) → C
Closed terms (i.e. terms without free variables) of type U also can be viewed as maps from the terminal object 1 to U -this view is supported by the fact, that 1 = { * } in the category of set.

A function in the model interprets a function as a static notion (a "set" of pairs x, f (x) ) and not as a (functional) algorithm: indeed whenever a term/proof t reduces to t • its interpretation as a morphism in the category is the same.

Given that functions from A to B are definable by terms/proofs, the set Hom(A, B) should be countable. Therefore, "elements" in B A , that are arrows from in 1, should be countable as well, and this imposes a drastic restriction on the morphisms we consider in the category. The study of such models of intuitionistic proofs lead to linear logic as we shall see in section 6.

A result by Joyal (unpublished see e.g. [START_REF] Lambek | Introduction to higher order categorical logic[END_REF][START_REF]The blind spot -lectures on logic[END_REF]) shows that all proofs of a given formula are equivalent in classical logic. Although there also exists a logical, syntactical analogous result by Girard and Lafont (see figure 2), Joyal proved a category theoretical formulation of this statement:

Proposition 1. In a cartesian closed category interpreting classical logic between any two objects (formulae) A and B there is at most one morphism from A to B (at most one interpretation of proofs of A ⊢ B).

Proof. The interpretation of classical logic needs an initial object 0 (false) and a negation ¬A = (A → 0) which is involutive i.e. A ∼ = ((A → 0) → 0). To see that in such a situation there exists at most one arrow between any two objects, let us first see that in a CCC with an initial object 0 when there is a map from Z some object to 0, then Z is initial as well:

(1) If 0 is initial, then is 0 × Z is initial as well. Indeed, in a CCC , maps from 0 × Z to any object U are in bijection with maps from 0 to

U Z = [Z → U].
(2) If there exists an arrow f from Z to 0 then Z is isomorphic to 0 × Z and therefore Z is initial. Indeed, π 2 • f , Id Z = Id Z (by definition of π 2 ) and f , Id Z • π 2 = Id 0×Z because it goes from 0 × Z to itself, which is initial because of 1 above. Maps from A to B correspond to maps from A to ¬¬B ∼ = (B → 0) → 0 and thus to maps from A × (B → 0) to 0. But from 2 it follows that such a map is an isomorphism and there is precisely one such isomorphism since 0 is initial. This result, simple enough to be presented in this introduction, clearly shows that intuitionistic logic is the natural logic of the CCC interpretation of proofs -in the previous section we already saw that intuitionistic also is the logic of toposes which generalise set theory.

MARTIN-L ÖF TYPE THEORY AND IDENTITY TYPES

One may further refine the operations (exponential, product) on the simple types of Church [START_REF] Chruch | A formulation of the simple theory of types[END_REF] of the previous section 4 as linear logic defined in next section 6 does, or consider a wider set of types as Martin-Löf type theory does.

Actually, the most prominent feature of Martin-Löf type theory is that there are types which depend on terms as e.g. Vect(n) for n : N, the type of vectors of length n. Propositions are considered as types and, accordingly, predicates may be considered as dependent

δ 1 • • • ⊢ F weakening ⊢ F, K δ 2 • • • ⊢ F weakening ⊢ F, ¬K cut ⊢ F, F contr. ⊢ F FIGURE 2
. This proof defined from δ 1 and δ 2 -that are any two proofs of the same formula F --reduces to δ 1 or to δ 2 followed by the exactly the same rules. Hence any two proofs of the same formula are equivalent in classical logic.

types. The most important example of dependent types will be identity types as discussed subsequently.

Martin-Löf type theory provides the necessary technology to deal with the standard mathematical concept of a family of sets. Moreover a dependent type can be considered as as predicate; for example if we are given a dependent type B(x) with x : A (a family of types indexed by the type A), we can think of A as a set and B(x) as a family of sets, but in addition, if we consider B(x) as a predicate, given a hypothetical element a of A and a hypothetical b in A(a) we can think of b as a proof witness that shows the truth of B(a). The presence of dependent types forces us to consider the following judgements

Γ ⊢ Valid The context Γ is valid Γ ⊢ A in the context Γ, A is a type. Γ ⊢ A = B
the types A and B are equal Γ ⊢ t : A in the context Γ, t is of type A Γ ⊢ t = u : A t and u are equal terms of type A. This notion of equality is called judgemental and can be decided by normalisation. But it cannot be combined into propositions for which reason one introduces the notion of propositional equality. If t, s : A one may form the types Id A (t, s) whose elements will be proofs that t and s are equal. Reflexivity is given by the constructor r A (t) : Id A (t,t) for t : A. As usual in type theory a constructor is accompanied by an eliminator which in case of identity types happens to be called J and can be described as follows. Given a family of types x, y : A, z : Id A (x, y) ⊢ C and a term x, y : A, z : Id A (x, y) ⊢ d : C(x, y, z) one may consider the term x, y : A, z : Id A (x, y) ⊢ J((x)d, z) : C(x, y, z) whose meaning is provided by the reduction rule J((x)d, r A (t)) = d[t/x]. This is in accordance with functional programming where functions are defined by pattern matching aka structural recursion. This is how equality is represented in intensional type theory of [START_REF] Martin-Löf | An intuitionistic theory of types: predicative part[END_REF]. In [START_REF]Intuitionistic type theory[END_REF] judgemental and propositional equality get identified via a so-called equality reflection rule allowing one to conclude t = s : A from p : Id A (t, s). This, however, renders type checking undecidable and, therefore, has been abandoned. Current proof checkers as e.g. the widely used system Coq [START_REF] Bertot | Interactive theorem proving and program development. coq'art: The calculus of inductive constructions[END_REF] are based on intensional type theory. This is sometimes inconvenient but allows one to avoid the manipulation and storing of derivation trees for typing judgements as in the much older NuPrL system.

As said above in section 3, toposes admit an internal logic in form of intuitionistic higher order arithmetic. In this logic propositions are not represented as types but as subobjects of the terminal object 1. Accordingly, predicates on a type A are represented as monomorphisms into A. On the other hand, a good interpretation of Martin-Löf type theory needs a predicate on a type A to be represented by a morphism B → A which is more general than just a monomorphism, since we want the ability to distinguish between proof witnesses. Thus we need a a distinguished class of morphisms (often called display maps), which are subject to a few simple conditions, the most important of which being that the pullback of a display map with codomain A by any morphism with same codomain is again a display map. This corresponds to being able to substitute a term for a variable in a predicate. It is then possible to interpret the Π-types when a right adjoint always exists to that pullback functor. When this happens we have a display category with (dependent) products, and when all maps of the category can be used as display maps, we have a locally cartesian closed categories. There are many display categories with dependent products, but it turned out to be harder to find examples that have a good, nontrivial (i.e., non collapsed) versions of the intensional identity type. For example locally cartesian closed categories are guaranteed to give trivial identity types. The first good example was given by M. Hofmann and Th. Streicher in [START_REF] Hofmann | The groupoid interpretation of type theory, Twenty-five years of Martin-Löf type theory[END_REF], where types were interpreted as groupoids, display maps as fibrations of groupoids (very easy to define), and Id A (x, y) as the set of morphisms (necessarily isomorphisms) from x to y. This model was only nontrivial in dimension one, in the sense that iterating the identy type would land us on the old, trivial, nonintensional interpretation where identity is just the diagonal.

It was realized that if a model of dependent types has an intensional identity type, then we are very close to being able to do topology (especially, homotopy theory) in it. This is because in such an identity type, we can view an intuitive element of ID A (x, y) (a proof that x is equal to y) as a path from x to y, and we are able to do many constructions of homotopy theory, with the additional bonus of dependent products.

Thus inspirations for good models of identity types were bound to come from algebraic topology, and this is the case for the first completely non-degenerate model, where paths in higher dimensions (higher homotopies) do not collapse, and which was found independently by Streicher and Voevodsky around 2006 (see e.g. [START_REF] Voevodsky | A very short note on homotopy lambda calculus[END_REF][START_REF] Streicher | Identity types and weak omega-groupoids, Identity Types -Topological and Categorical Structure[END_REF]. The base category is the presheaf topos of simplicial sets, the most studied of all models in combinatorial topology, and families of types (i.e., display maps) are interpreted as Kan fibrations, which forces ordinary, non-dependent types to be Kan complexes. As expected, the identity type Id A (x, y) is the standard construction for the path object in the sense of the usual Quillen model structure on simplicial sets. [START_REF] Daniel | Homotopical algebra[END_REF] Another inspiration from topology, namely in the theory of fiber bundles, has led V. Voevodsky [START_REF]Homotopy type theory: univalent foundations of mathematics[END_REF] to propose the Univalence Axiom in what is now called Homotopy Type Theory (HoTT), which applies to universes, like those found in Coq and those defined by Martin-Löf, and can be viewed as the statement that in a "good" universe isomorphic types are equal.

The present issue contains two papers about categorical models of identity types, both having links to homotopy type theory:

• Franc ¸ois Lamarche in his paper Modelling Martin-Löf Type Theory in Categories proposes a simple model of Martin-Löf type theory that includes both dependent products and the identity types. • Thomas Streicher in the next paper describes A Model of Type Theory in Simplicial Sets in which the Voevodsky Univalence axiom holds. Although little work has been done in this direction, categorical models of type theory should be very appealing from the viewpoint of natural language semantics, to be evoked in section 7.

Indeed, natural language semantics, philosophy of language, analytic philosophy has always been interested in models (classical models, possibles worlds, situations) and nowadays, natural language semantics is often formalised and computed within type theoryas exemplified in the present issue, see section 7.

FROM A PARTICULAR CATEGORICAL INTERPRETATION TO LINEAR LOGIC

While Martin-Löf type theory discussed in previous section 5 extends the expressive power of simply typed theory with dependent types, one can also have a closer look at the intuitionistic logical connectives & and → from a computational perspective bearing in mind that an involutive negation like the one of classical logic brings many convenient and elegant properties. One thus discompose the connective of intuitonistic logic and finds a classical but constructive logic called linear logic. [START_REF] Girard | Linear logic[END_REF][START_REF]The blind spot -lectures on logic[END_REF].

Linear logic, present in two papers of the present issue, arose from the study of a particular cartesian closed category that interprets proofs of intuitionistic logic, namely coherence spaces and deserve some extra information: coherence spaces, which are discussed in the present issue regarding their relation to formal ontologies, see section 7.

A coherence space is basically a simple graph (possibly infinite, but without loops nor multiple edges) but entities that interpret terms or proofs in a coherence space are not its vertices but the cliques of this graph, i.e. its complete subgraphs. A stable map from A to B maps cliques of A to cliques of B, and it enjoys certain properties: monotony (a ⊂ b ⇒ F(a) ⊂ F(b)), preservation of directed unions (F(∪ ↑ a i ) = ∪F(a i )) and of intersections inside a clique (when a ∪ a ′ is a clique of A one has F(a ∩ b) = F(a) ∩ F(b)) The important point is that a stable function from a coherence space A to another one B can be viewed as a clique of a larger coherence space A → B, whose vertices are (a, β ) where β is a vertex of B and a a finite clique of A, such that β ∈ F(a) and a is minimal for this property -F being stable there always exists such a finite a, and one of them a is minimal and in fact the minimum. Two vertices (a, β ) and (a ′ , β ′ ) of A → B are said to be coherent whenever a ∪ a ′ is a clique of A implies that β and β ′ are coherent in B and when furthermore a and a ′ are distinct so are β and β ′ .

One then has a bijection between stable functions from A to B and the cliques of the coherence space A → B. There is also a product of coherence spaces, which is the disjoint union of the two graphs, plus edges between any vertex of A and any vertex of B.

The categorical product corresponds to the rule from Γ ⊢ A and Γ ⊢ B infer Γ ⊢ A&B, while the other product ⊗ corresponds to the rule from Γ ⊢ A and ∆ ⊢ B infer Γ, ∆ ⊢ A ⊗ B. These two conjunctions of linear logic cannot be distinguished in intuitionistic logic, because of the weakening and contraction rules given in figure 4.

Interpreting proofs in coherence spaces, where operation on coherence spaces correspond to logical connectives lead to linear logic. Indeed, besides the product described above there is another "product", which is not a categorical product, whose vertices are pairs of vertices, with an edge between (a, b) and (a ′ , b ′ ) whenever there is an edge {a, a ′ } and an edge {b, b ′ } in Ba = a ′ or b = b ′ is allowed as well, but not both since there are no loops in simple graphs.

Besides these pairs of conjunction, one discovers an involutive negation A ⊥ whose simple graph is the complement of the simple graph (simple graphs contain no loop). Using De Morgan laws it maps the two aforementioned conjunctions to two disjunctions respectively written ⊕ (additive disjunction) and ℘ (multiplicative disjunction).

There also exists a unary operator ! which relates linear logic (resource sensitive) to intuitionistic logic. The coherence space !A is defined as follows: its vertices are the finite cliques of A, and two vertices a and a ′ of !A, that is to say two finite cliques of A, are coherent in !A whenever the union a ∪ a ′ is a clique of A. This operator turns the additive conjunction & into the multiplicative conjunction ⊗: !(A&B) ≡!A⊗!B.

A kind of classical implication can be defined from the ℘ disjunction: A ⊥ ℘B, it is written as A ⊸ B, and the intuitionistic implication can be defined as:

A → B =!A ⊸ B
Linear logic was provided with a syntax, both with sequent calculus and with proofnets that identify proofs up to rule permutations. Propositional linear logic is also endowed with a truth value semantics phase semantics.

In this issue, the paper entitled Relational semantics for full linear logic by Dion Coumans, Mai Gehrke, Lorijn van Rooijen proposes a Kripke style semantics for full propositional linear logic, i.e. with, additives, multiplicatives and exponentials that allow the addition of proper axioms.

LINGUISTIC APPLICATIONS: COMPOSITIONAL SEMANTICS, LEXICAL SEMANTICS, AND KNOWLEDGE REPRESENTATION

Natural language semantics is usually expressed by first order (some times higher order) logic or predicate calculus, single sorted as Frege wished to, and computed according to Frege's compositionally principle: the meaning of the compound is a function of the meaning of its parts. [START_REF] Van Benthem | Handbook of logic and language[END_REF][START_REF]Formal semantics: The essential readings[END_REF][START_REF] Davis | Introduction (to "semantics, a reader[END_REF]. This is easily implemented in lambda calculus where anything is a function, as noticed by Montague in 1970 [START_REF] Montague | English as a formal language, Linguaggi nella Societa e nella Tecnica[END_REF]. Typed λ -terms for representing logical formulae are usually defined out of two base types, e for individuals (also known as entities) and t for propositions (which have a truth value). Logical formulae can be defined in this typed λ -calculus as first observed by Church in 1940 [START_REF] Chruch | A formulation of the simple theory of types[END_REF], but the combination of word meaning (partial formulae) according to the syntactic structure of the sentence is due to Montague. This early use of lambda calculus, where formulae are viewed as typed lambda terms, can not be merged with the more familiar view of typed lambda terms as proofs evoked in the section 4. The proof which such a typed lambda term corresponds to is simply the proof that the formula is well formed, e.g. that a two-place predicate is properly applied to two individual terms of type e and not to more or less arguements, nor to arguments of a different type etc. This initial vision of lambda calculus was designed for a proper handling of substitution in deductive systems à la Hilbert. One needs constants for the logical quantifiers and connectives: as well as predicates for the precise language to be described -a binary predicate like won has the type e → e → t.

A small example goes as follows. Assume that the syntactical analysis of the sentence "Some club defeated Leeds." is (some (club)) (defeated Leeds) where the function is always the term on the left. If the semantic terms are as in the lexicon in figure 3, placing the semantical terms in place of the words yields a large λ -term that can be reduced: λ P e→t λ Q e→t (∃ (e→t)→t (λ x e (&(P x)(Q x)))) λ x e (club e→t x) λ y e λ x e ((defeated e→(e→t) x)y) Leeds e ↓ β λ Q e→t (∃ (e→t)→t (λ x e (& t→(t→t) (club e→t x)(Q x))))

λ x e ((defeated e→(e→t) x)Leeds e ) ↓ β ∃ (e→t)→t (λ x e (&(club e→t x)((defeated e→(e→t) x)Leeds e )))

This λ -term of type t that can be called the logical form of the sentence, represents the following formula of predicate calculus (admittedly more pleasant to read):

∃x : e (club(x) & defeated(x, Leeds))

Thus defined, computational semantics looks a miracle. But this miracle does not account for selectional restriction (a "book" cannot "bark"), does not tell anything of the relations between predicates (a "book" can be "read"), nor of the correspondence of predicates with concepts (a book is both an informational and a physical entity), nor of the relation between the logical language for semantics and world knowledge and ontologies. Issues such as selectional restriction have been much discussed in type theoretical framework e.g. in [START_REF] Cooper | A record type theoretic account of copredication and dynamic generalized quantification[END_REF][START_REF] Asher | A type driven theory of predication with complex types[END_REF][START_REF] Bassac | Towards a Type-Theoretical Account of Lexical Semantics[END_REF][START_REF] Asher | Lexical meaning in context -a web of words[END_REF][START_REF] Luo | Contextual analysis of word meanings in type-theoretical semantics[END_REF].

In his paper Selectional Restrictions, Types and Categories, Nicholas Asher discusses the introduction of types as objects of a category (instead of a single e) endowed with categorical operations that go beyond the logical ones: he is thus able to correctly account for selectional restriction, felicitous and infelicitous copredications.

This framework in which one composes functions to compute meanings and ultimately the truth values in a given model is given a categorical formalisation by Anne Preller in her paper Natural Language Semantics in Biproduct Dagger Categories. Starting with pregroup grammars defined in an algebraic structure that can be viewed as non commutative linear logic in which ℘ = ⊗, she computes the meaning categories with extra operations, as finite dimensional vector spaces or two sorted functions over finite sets. She can then account of meaning with the usual set theoretic interpretations or with bags of words vectors used for text classification.

An underlying question, in relation to the interpretation of common nouns and to the bags of words approach is what a concept or a base type is, and the interrelations between base types. For instance one can say "a cat sleeps", because "animals" can "sleep" and "cats" are "animals". In the kind of model used in semantics ontological relations are quite common, but here is no specific structure to represent these ontological relations.

The paper entitled Formal ontologies and coherent spaces by Michel Abrusci, Christophe Fouqueré and Marco Romano exploits the structure of coherent spaces that we discussed in section 6 to give a formal account of the relation between entities and concepts, encoding properties of formal ontologies.

  Type theory as formalized by Martin-Löf gives us access to the construction of • the type (Πx : A)B(x) whose intuitive elements should be seen as functions f that map a term a : A to a term f (a) : B(a). In case B does not depend on x, the type (Πx : A)B(x) corresponds to the type A → B of simply typed lambda calculus. When we see dependent types as predicates, we now have access to the universal quantifier. • the type (Σx : A)B(x) whose elements should be seen are pairs (a, b) with a : A and b : B(a). If B(x) does not depend on x, the type (Σx : A)B corresponds to the type A × B of simply types lambda calculus, and we also have access to the existential quantifier when we think of a type as a predicate.

  Predicates and constants Constant Type defeated, . . . e → (e → t) won, voted, . . . (e → t) Liverpool, Leeds, . . . e . . . . . .

	word	semantic type u *
		semantics : λ -term of type u *
		x v the variable or constant x is of type v
	some	(e → t) → ((e → t) → t)
		λ P e→t λ Q e→t (∃ (e→t)→t (λ x e (& t→(t→t) (P x)(Q x))))
	club	e → t
		λ x e (club e→t x)
	defeated e → (e → t)
		λ y e λ x e ((defeated e→(e→t) x)y)
	Leeds	e
		Leeds
		FIGURE 3. A simple semantic lexicon
		Logical connectives and quantifiers
		Constant Type
		&, and t → (t → t)

∨, or t → (t → t) ⇒, implies t → (t → t) ∃ (e → t) → t ∀ (e → t) → t

This sheaf U → Hom(A| U ,B| U ) is often called "internal hom".

Thanks: We are indebted to Mai Gehrke, Alain Lecomte, Anne Preller, Steve Vickers, Gilles Zémor, and especially to Franc ¸ois Lamarche and Thomas Streicher for a quick but efficient rereading of this introduction, which they all contributed to improve. Remaining errors and confusions are ours.


Christian Förstel

Metochites and his Books between the Chora and the Renaissance

[paru dans : The Kariye Camii Reconsidered / Kariye Camii Yeniden, éd. Holger A. Klein, Robert Ousterhout, Brigitte Pitarakis, Istanbul: Istanbul Arastirmalari Enstitusu, 2011, pp.

241-266]

In a poem adressed to his protégé Nicephorus Gregoras, Theodore Metochites speaks of the fate of "his own compositions", as the title of the poem announces 1 . He says: « And I commend to your keeping all the books I have composed here and there which are the dearest of all things to me, and which I desire to remain unharmed into all ages » 2 . It would appear then that this wish has been fulfilled: with the notable exception of Metochites letters which were lost in the fire of the Escorial library in 1671 3 , his works have been preserved and have been the subject of many scholarly studies by philologists and historians since the mid-1950s.

Our interest here is in the history of the transmission of these texts from their composition until their arrival in the great Greek manuscript collections of the Renaissance. How is it that these texts which are so difficult to understand have been preserved whereas the political and cultural structures in which they were created have disappeared? In order to answer this question, we shall concentrate mainly on the two Paris manuscripts and shall make only occasional references to other manuscripts of Metochites.

The transmission of the writings of εetochites begins with their 'edition" by the Grand Logothete himself. He distinctly mentions, again in the poem to Gregoras, his solicitude for all of "these dearly beloved offspring" of his soul 4 : "I have taken great care for these books, even as for my own children" 5 . In a general way this remark could be applied to the entirety of the φhora"s library whose richness surpassed all other monastic libraries of Constantinople put together.

In the context of Poem IV however this remark concerns only εetochites"s own works and it is not simply rhetoric but is corroborated by what the manuscripts themselves tell us. τlmost all of εetochites"s works have come down to us in very careful copies, on parchment, written by one copyist with excellent calligraphy. This copyist was an eminent member of the imperial chancellery who wrote a great number of chrysobulls, very formal documents issued by the emperor and sealed with gold, of Andronicus II. In one of these official letters written in the name of Andronicus, a so-called « horkomatikos » chrysobull sent to Venice in 1324, the copyist gives his nameκ the 'imperial notary" εichael Klostomalles6 .

The collaboration of Klostomalles with Metochites was evidently very close: the manuscript on exhibit here shows this very wellέ Klostomalles was at εetochites"s disposition both before and after the latter"s fall from power as chief minister to Andronicus. The case is the same with the manuscript of the Miscellanea preserved in Paris which is also the work of Klostomalles. The monograms of Metochites which appear in two different places in the manuscript 7 prove that it was an official copy made when Metochites was Grand Logothete; thus it was copied between 1321 and 1328. In the margins of the manuscript Metochites has made several notes which apparently date from the last four years of his life. Recently doubts have been expressed about the authorship of these notes 8 but they are of such a personal nature that it seems unlikely that they could have been dictated. In Poem IV Metochites entrusts the care of his books to Gregoras, whom he calls 'the successor of his wisdom" 9 and also 'his highly qualified disciple" 10 , the care of his books. Gregoras says the same thing in his History 11 έ That ύregoras fulfilled his patron"s command is attested by the manuscripts themselves, since ύregoras"s activity is visible in most of themέ In the Paris manuscripts of the Poems and the Miscellanea as well as the Vatican manuscript of the Introduction to Astronomy Gregoras records in an identical way at the beginninng of the Pinax, or List of Contents, the name of the author : « Of the most learned Grand Logothete Theodore Metochites » 12 Gregoras also made remarks in the Vienna manuscript of the rhetorical works of Metochites. All these remarks were apparently added in the manuscripts in the φhora"s library where they were keptέ Almost all the copies of the Introduction to Astronomy contain remarks by Gregoras 13 , which demonstrate that this work was edited several times in the Chora. τfter εetochites"s death his spiritual heir watched over the books in the monastery where he lived « since he was a child » 14 and where he continued to reside as he himself tells us in his ώistoryέ υut what became of the library after ύregoras"s death, some thirty years after that of Metochites, in 1359 or 1361 ?

A generation later, around 1400, a good number of these manuscripts must have still been in the Chora, for it was there that John Chortasmenos, an imperial notary and great scholar of the early 15th century found the copy of the Introduction to Astronomy (Vatican.gr. 1365) in which he wrote two lines on the first folio: « this book belongs to the monastery of the Chora whose patron was the Great Logothete » 15 . At the top of the same page 7 For a comparision of the monograms in the manuscript and those of the dome of the monastery see I. Chortasmenos rewrote the name of Metochites beneath the note by Gregoras and identifies the authors of these two notes as if to call attention to his own affiliation with Gregoras 16 .

A considerable number of manuscripts of the Chora contain indications that they once belonged to the library of Manuel Chrysoloras, the trusted advisor and envoy of Manuel II Palaiologos. The common element is a bilinguial title, in Greek and Latin, at the very beginning of the manuscripts. Even if only one work of Metochites figures here 17 , this is evidence that the φhora"s library remained to a certain extent intact in φonstantinople until the reign of Manuel II.

The relation of the books of the Chora and the collection of Chrysoloras provides us also with a connexion to the Italian Renaissance. Initiator of the first systematic teaching of Greek in Italy from 1397, Chrysoloras had as his pupils the humanists of Florence, Pavia and Rome 18 . His influence was such that his arrival in Italy from Byzantium was straightaway seen as an event marking the beginnig of a new era 19 .

Since only one of the works of Metochites figures amongst the books which have until now been identified as belonging to the library of Chrysoloras, did the compositions of the Grand Logothete play a minimal role in the expansion of Greek studies in the West in the 15th century? If the answer was yes, our discussion should end here. Fortunately, the case is otherwise.

Three of the four 'official" manuscripts of the works of εetochites were in fact in Italy by the 15th or beginning of the 16th century. Above the title on the fist folio of the manuscript of the Poems is the following ex-libris in ύreekκ 'This is a book of δianoro" 20 . This must be the humanist Lianoro Lianori of Bologna who is known to have possessed a rather large collection of ύreek and δatin manuscriptsέ δianori"s biography is now well known thanks to a recent work on humanist circles in Bologna around the year 1450 21 . Born around 1425 Lianori was a student in Ferrara of Guarino of Verona, the great pedagogue of the Quatrocento who himself had been one of the first disciples of Manuel Chrysoloras in Florence at the very end of the fourteenth century. Also in Ferrara Lianori had been able to attend the courses of Theodore of Gaza, a close associate of Cardinal Bessarion, who also played an important role in the study of Greek in Italy and to whom we ow a number of Latin translations of the works of Aristotle executed as part of the great project of translation sponsored by Pope Nicholas V. Lianori was charged with the instruction of Greek at the Studio in Bologna from 1455 to 1459, before being called to the papal court by Pope Pius II, who granted him a number of benefices and the direction of several nunciaturae, first in Naples and then in Spain.

The 15 manuscripts known to have belonged to Lianori 22 , some of them copied by his hand, attest to his ecclectic tastes: here we find Homeric Poems, Hesiod, Aristophanes, 16 Euripides, Plutarch, Aesop, Synesius, Libanius, Aristotle and the grammar of Manuel Chrysoloras. To these we should add a rare treatise by Galen, the Exhortation to the Study of Medicine, from which Angelo Poiziano made excerpts in Florence in 1491. At the beginning of his notes θoliziano names as his source a 'book of δianoro of υologna" 23 . δianori"s library corresponds more or less to what we should expect of a humanist"s collectionέ With the exception of εetochites"s Poems and the φhrysoloras"s grammar, which was evidently intended for teaching, this library is exclusively composed of ancient texts.

In this collection the Poems of the Grand Logothete occupy a place apart. Where did Lianori get this manuscript? At the present state of our knowledge we cannot reply definitively to this question. But several hypotheses are possible. In 1465 Gaspare of Verona sold Lianori a number of Greek manuscripts. « Several days ago », Gaspare records in his history of the pontificate of Paul II, « Lianori bought from me almost all the poets who are now considered to be the most important amongst the Greeks 24 ». Was Metochites one of these poets whom Lianori acquired, and at great cost? This is not an impossibility, even if we have trouble in counting Metochites amongst the most important of Greek poets.

In any case the acquistion of the manuscript by Lianori must be placed at a certain distance from the capture of Constantinople by Mehmet II. On one of the first folios of the manuscript, just above the Pinax, a note concerns the beginning of the siege by the Ottomans: « In the year (of the world) 6961 [1453], on the fifth day of the month of April, in the first week after Easter, the impious Machamet came to lay siege before the queen of cities by land and by sea, bringing with him an army of 10.000 men together with the greatest number possible of war machines as well as a fleet, it too most abundant, in order to surround the city completely. 25 » This note was evidently written by a Greek and must have been made somewhere near the theatre of war, probably in Constantinople itself. If this is so, the manuscript would have remained in the capital from the time of its creation in the early fourteenth century until 1453.

But whatever may have happened to the manuscript before Lianori acquired it, of primary interest to us is the use which this humanist made of it. Apart from the ex-libris Lianori left no trace in it. Can we be sure that he read it? To tell the truth, δianori"s knowledge of ύreek was certainly not up to the level of the highly 'idiosyncratic" style of Metochites which, according to Gregoras, « stings the ear of the listener as the thorn of the rose wounds the palm of him who would pick it 26 ». It is most probable that our humanist was unable to understand the ύrand δogothete"s verses stuffed with archaisms, regardless of contemporary statements in praise δianori"s mastery of both Latin and Greek. Such praises surely reflect more the custom of the day than reality. In the words of a recent scholar, δianori"s reputation as a ώellenist would appear « unjustified » 27 .

But aside from linguistic competence, the reading of εetochites"s Poems requires great motivation; and it is not at all certain that a literary figure like Lianori, formed in the great centres of the humanist tradition, would really have wanted to read and understand an author who by reason of his style and the period in which he lived was so far removed from the Classical ideal so dear to the Humanists.

The deluxe edition of εetochites"s astronomical treatises had a history similar to that of the Poems at the end of the 14th or during the first half of the 15th century. This is the 23 T. Martínez Manzano, "Autógrafos", 24-25. 24 T. Martínez Manzano, "Autógrafos", 16-17. 25 The note is edited by J. M. Featherstone, Theodore Metochites's Poems, 13 and 154, pl. 3. 26 " ἀ ἀ αὶ ῶ ἐπ ὴ ἀ οὴ , α π ὴ ῶ πα ἡ π ὶ ὸ ο α α"κ Nicephori Gregorae Historia Romana, Corpus scriptorum historiae Byzantinae (Bonne 1829-1855), 1. 272, ll. 12-1δέ See also Ševčenko, Études sur la polémique, 35. 27 A. Onorato, Gli amici Bolognesi, XLIX. manuscript we left a short time ago in the hands of John Chortasmenos in the Chora. An autograph ex-libris at the end of this manuscript shows that it belonged to Pietro Bembo, a patrician of Venice born in 1470 who toward the end of his life became the cardinal of the Roman Church seen in the portraits by Titianέ υembo"s father, υernardo, had been Venitian ambassador in Florence. He had had close relations with the humanists in the entourage of Lorenzo the Magnificent, among them Marsilio Ficino and Angelo Poliziano, and he himself possessed a large library [START_REF] See | Umanesimo e patriziato a Venezia nel Quattrocento, II, Il circolo umnistico veneziano. Profilo[END_REF] . Imbued with humanist culture, Pietro Bembo soon became interested in Greek. From 1492 to 1494 he went to distant Messina in order to study Greek with Constantine Lascaris [START_REF] Wilson | Da Bisanzio all'Italia. Gli studi greci nell'Umanesimo italiano[END_REF] . On returning to Venice he had Aldus Manutius print the Greek grammar composed by Lascaris [START_REF] Lowry | The World of Aldus Manutius. Business and Scholarship in Renaissance Venice[END_REF] and Bembo himself wrote a treatise in favor of the study of Greek which he presented as a discourse before the Venitian Senate [START_REF] Bembo | Oratio pro litteris graecis[END_REF] .

In subsequent years Bembo appears to have turned his back rather quickly on Greek and to have devoted himself to his works in δatin and to the 'vulgar" language. As editor of the Divine Comedy and the Canzoniere of Petrarch for Aldus Manutius, Bembo played a major role in the diffusion of the language of Boccacio and Petrarch as a literary language far beyond the borders of Tuscany. Very close to the Florentine humanists in his conception of literature, Bembo has left few traces as a Hellenist. The Greek texts contained in his library are for the most part Classical or late Antique and were apparently connected with his study of Greek as a young man. The presence of the astronomical work of Metochites in his collection would thus appear the result of chance: there is no evidence that Bembo ever read this text attentively.

The manuscripts of εetochites"s Poems and Introduction to Astronomy created no echo in Renaissance Italyέ υut the case is different with the 'official" manuscript of the Miscellanea. This manuscript, now in Paris, was profusely annotated in the course of the 15th century by an Italian scholar whose notes are found in the margins of many Greek manuscripts. Until recently this scholar remained anonymous, but the presence of notes in the margins of the numerous manuscripts copied by the scribe Michael Apostolis has led to the identification of the author. An autograph copy of proverbs collected by Apostolis, now in Paris (Paris. gr. 3059), not only contains a great many notes by our scholar but also a dedication by τpostolis to the 'most famous and most learned δauro Quirini", patrician of Venice [START_REF] Rashed | Die Überlieferungsgeschichte der aristotelischen Schrift De generatione et corruptione[END_REF] . The later and well-documented history of the manuscript provides irrefutable proof that the person to whom the book is dedicated and the author of the notes are one and the same.

Who was Lauro Quirini? A Venetian noble born around 1420 who died between 1475 and 1479, he possessed numerous properties on Crete, where he passed a good part of his life. He was also, and above all, a good scholar of Greek and was greatly interested in philosophy, history and more generally ancient literature. In the philosophical sphere Quirini considered himself an Aristotelian, and he manifestly knew all the works of Aristotle, though he was also interested in post-Aristotelian philosophers, whether Peripatetics or Platonists, Greek, Latin or Arab [START_REF] Rashed | δ"averroïsme de δauro Quirini[END_REF] . Thus, in the margin of the Paris manuscript he cites a passage of Plotinus (III 5, 6.31) more than fifteen years before this extremely difficult text was made accessible in Latin by the translation and commentary of Ficino. Quirini was therefore one of the first Latins of the 15th century to have read Plotinus.

Quirini"s interest in ancient authors is well documented by the quantity of his notes in the margins of a great number of manuscripts. What about his interest in a late-Byzantine author like Metochites? In Quirini"s marginal notes in the Miscellanea we can distinguish three categories: notes which simply call attention to a passage, notes containing Quirini"s personal reactions to a passage and, finally, notes which echo Quirini"s own worksέ

To the first category belong the many cases in which Quirini marks a phrase or proverb. This interest in proverbs is perhaps connected with the work of Apostolis which was dedicated expressly to Quirini. Sometimes Quirini simply notes a difficult word and translates it into Latin.

Of more interest to us are the remarks of a more personal nature which appear here and there in the margins of the Miscellanea. One note of this type is found opposite the beginning of Treatise 10 which is entitled « Disrespect of Wise Men toward their Predecessors » and opens with a critique of Plato and Aristotle whom Metochites presents as particularly aggressive with regard to the philosophers who preceded them 34 έ Quirini"s reaction: "but it is a man's duty to correct the errors of others" [START_REF]Sed boni viri officium est errores hominum corrigere[END_REF] . This remark would appear above all a defence of Aristotle whom the platonic tradition presented as an ungrateful pupil of Plato.

But Quirini was not only interested in philosophy. He also gives particular attention to Metochites's historical and political remarks. In treatise 99, on the Constitution of Athens, Quirini devotes a long paragraph to the ancient domination of Crete over the greek islands. Before Thucydides and Aristotle, he says, we have the statement of Homer in the Odyssey concerning, "the land called Crete in the midst of the wine-dark sea" 36 . With this passage Quirini compares a verse of book three of the Aeneid: "Crete, the island of great Jove stretches forth in the middle of the sea (3.104)" [START_REF]Creta Iovis terra medio iacet insula ponti[END_REF] . Quirino"s comparision of the Odyssey with the Aeneid is not only perfectly justified from a philological point of view, but it also shows his interest for every thing which concerns Crete and its history.

Metochites deals with questions of a more contemporary nature in his long treatise on democracy (Misc. 96): democracy, by entrusting equal power to wise men as to stupid ones, to honest men as to those who are not, is an illness. The Ancients attest to this in many of their writings. We also find examples of this quite close at hand as in the Italian cities which "are administered democratically and find themselves in a bad position because of the inherent faults in this type of constitution". Metochites then cites as an example and proof of what he says the city of Genoa, which now finds itself in extreme danger because of its excessive democracy, whereas not so long ago it was renoumed as one of the most flourishing cities of the earth 38 . The history of Genoa is indeed marked by a sort of apogee in the second half of the thirteenth century before a recrudescence of the internal conflicts between Guelfs and Ghibellines which weakened the commercial and military position of the city in the Mediterranean world. The ideological presuppositions of this passage were interesting to Quirini because it concerns the recent history of the ennemy of Venice. He marks it twice with notes in the margin: "Italian cities" and "Genoa" 39 .

These examples show that Quirini read attentively all the treatises of Metochites in the Paris manuscript. Other of his notes suggest that Quirini even occasionnally used the Miscellanea as a source for his own writings. This seems probable to me for a passage of the treatise on democracy, where Metochites speaks of the fate of Themistocles who was at once hero of the Athenians' struggle against the Persians and victim of the democratic system: "And Themistocles, this man who was at once remarkable for his wisdom and his competence in the political and military domain, who was himself the principal author, in the face of the Persians, of the liberation of Athens and moreover of the Greeks in general, this man was forced to flee his homeland because of the defamation and calomny of Lykomedes and also because of the ignorance and incomprehension of the people who owed to him their enormous victory and success" 40 .

Here again, Quirini marks the passage in the manuscript and notes in the margin: "Themistocles this great man" 41 . Moreover Quirini takes up this theme in his treatise De republica which was composed around 1449-1450 and which was intended to glorify the perfection of the Venetian constitution. In the first book of this treatise Quirini speaks of the disadvantages of an active life: "A great many jealousies arrise in an active life in such a way that the best of men, the most just, those who have well served the republic, are forced to live a life in exile because of the ingratitude and jealousy of their fellow citizens. For who was more famous in the city of Athens, who more powerful than Themistocles? Themistocles, although he had liberated Greece from servitude in the Median wars, was nevertheless sent ignominiously into exile on account of jealousy" 42 .

One could cite many other examples of parallels between the Miscellanea and the works of Quirini. But is the resonance due simply to a shared preference for the history of antiquity as reported by Thucydides, Plutarch and others? Are these parallels between the Miscellanea and Quirini's works not simply a coincidence resulting from the fact that both authors borrowed from the same ancient authors? Has any passage of Quirini been taken directly from the Miscellanea?

In one case at least Quirini himself provides us with proof of borrowing by explicitly naming his source. The passage in question is found at the end of a long letter which Quirini wrote in the name of the Cretan nobility to Pope Pius II in 1464. Quirini pleads for the restauration of the Christian Roman Empire, which, he says, was once of very great extent, describing its borders first as they were reported by Appian and secondly in accordance with "this great Theodore of Constantinople" 43 . The editor of this text, Agostino Pertusi, had difficulty with the reference to Theodore of Constantinople whom he identified with Theodore the Lector, Church historian of the fifth-sixth century, although he admitted that the latter's work contained no passage similar to this one 44 . In fact Quirini meant Theodore Metochites even if the citation is not a litteral one.

This explicit reference to Metochites is very important, for it demonstrates that Quirini held Metochites in great esteem. The numerous parallels between his works and the Miscellanea attest to a conscious interest in one of the great figures of the late Byzantine Empireέ This interest is also confirmed by the presence of Quirini"s notes in another "venerable" manuscript of the works of Metochitesin one of the two volumes of the commentary on Aristotle which was certainly written during or shortly after Metochites's lifetime and in which Gregoras also added titles, the present manuscript Paris. gr.1935.

In conclusion, let us speak of one of the last owners of the manuscript before it entered the royal library in the 18th century. Jean Hurault de Boistaillé, ambassador of the French king in Constantinople and later in Venice, possessed not only the manuscript of the Miscellanea but also that of the Poems, both of which he had rebound at great cost in Paris. Hurault de Boistaillé possessed more than a hundred greek manuscripts most of which he acquired in Venice, the centre of the greek book trade at this time. His interest in Greek books would appear to date from the years 1558 to 1560 when he was french ambassador to the Suplime Porte. In Istanbul, Hurault acquired one of the master-pieces of Byzantine illumination, the so-called Paris-Psalter of the middle of the 10th century. He purchased several Hebrew manuscripts, as well as three in Arabic, either in Constantinople or in Venice 45 . By the collection of these manuscripts, this openminded ambassador made a significant contribution to the preservation of Byzantine culture. 45 See Dέόέ Jackson, "The ύreek εanuscripts of Jean ώurault de υoistaillé", StItalFCl, 2 (2004), 209-252, and M.-θέ δaffitte, "Une acquisition de la υibliothèque du roi au XVII e siècleκ les manuscrits de la famille ώurault", to be published in the Bulletin du Bibliophile, 2008.

39

  Paris. gr. 2003, f. 207. 40 Metochitae Miscellanea, 608. 41 « Themistocles magnus ille », Paris. gr. 2003, f. 204. 42 C. Seno, G. Ravegnani, « Il "De Republica" di δauro Quirini », in : Lauro Quirini Umanista. Studi e testi, ed. V. Branca, K. Krautter, P.O. Kristeller et al., Civiltà Veneziana, Saggi 23 (Firenze 1977), 143-144. 43 « Theodorus ille magnus Constantinopolitanus », see A. Pertusi, « Le Epistole storiche di Lauro Quirini sulla caduta di Costantinopoli e la potenza dei Turchi », in : Lauro Quirini, 256-257. 44 Pertusi, « Le Epistole », 195 n.

Ševčenko, « Theodore Metochites, the Chora, and the Intellectual Trends of His Time », in The Kariye Drami, 4 : Studies in the Art of the Kariye Djami and Its Intellectual Background (Bollington Series LXX

	), ed. P. A.
	Underwood (Princeton 1975), 39. For the monograms on the exterior of the monastery, see R.G. Ousterhout, The
	Architecture of the Kariye Camii in Istanbul, Dumbarton Oaks Studies 25 (Washington 1987), 35, Figs. 121, 131
	and 132.
	8 See P. A. Agapitos, K. Hult, O.L.Smith, Theodoros Metochites on Philosophic Irony and Greek History :
	Miscellanea 8 and 93 (Nicosia, Göteborg 1996), 18-20, and K. Hult, Theodore Metochites on Ancient Authors
	and Philosophy. Semeioseis gnomikai 1-26 & 71, Studia Graeca et Latina Gothoburgensia 65 (Göteborg 2002),
	xviii-xx. 9 " α ' ... ἐ ᾶ ο 10 " ὐ α ο πο ὺ ἀ οα ο "κ Ševčenko, Featherstone, 36, l. 200. .../ ... ο ο "κ Ševčenko, όeatherstone, βθ, lέ β-3. 11 Nicephori Gregorae Historiae Byzantinae, ed. I. Bekker, L. Schopen, CSHB (Bonn 1829-1855), 1, 309. 12 " ο ο ο ο ο ο ο ο ο ο ο ο ο ο ": Paris. gr. 1776, f. 1 (Featherstone, Theodore Metochites's θoems, 1εε, plέ δ) , θarisέ grέ βίίγ, fέ γ, Vaticanέ grέ 1γἄε, fέ 1 (Ševčenko, Études sur la
	polémique, pl. V a). 13 See B. Bydén, Theodore Metochites' Stoicheiosis Astronomike and the Study of Natural Philosophy and
	Mathematics in Early Palaiologan Byzantium, Studia Graeca et Latina Gothoburgensia 66 (Göteborg 2003),
	385-386.

14

Gregorae, Historiae,2. 1045.

15

" ο ῆ ἡ ο ἥ α · ἧ ἐ ὁ α ο ο ", see W. Turyn, The Byzantine Manuscript Tradition of the Tragedies of Euripides, Illinois Studies in Language and Literature 43 (Urbana, 1ιεἅ), γιγ, and Ševčenko, Études sur la polémique, 281.

  Iέ Ševčenko, « Observations sur les recueils des Discours et des Poèmes de Th. Métochite et sur la bibliothèque de Chora », Scriptorium 5 (1951), 443 λ Ševčenko, Études sur la polémique, 282 and pl. V a ; H. Hunger, Johannes Chortasmenos (ca. 1370-ca. 1436/37). Briefe, Gedichte und kleine Schriften, Wiener Byzantinistische Studien 7 (Wien, 1969), 24-25 ; see also the important recent study of D. Bianconi, « La biblioteca di Cora tra Massimo Planude e Niceforo Gregora. Una questione di mani », Segno e Testo 3 (2005), 406-407. 17 This is the Vaticanus gr. 2176 of the Introduction to Astronomy which has the bilingual title on f. I: see N. Zorzi, "I Crisolora: personnaggi e libri", in Manuele Crisolora e il ritorno del greco in Occidente, Atti del Convegno Internazionale, ed. R. Maisano, A. Rollo (Napoli 2002), 102, 108, 113. 18 On Manuel Chrysoloras, see now A. Rollo, "Problemi e prospettive della ricerca su Manuele Crisolora", in: Manuele Crisolora e il ritorno del greco in Occidente, 31-85.

19

See V. Fera, in : Manuele Crisolora e il ritorno del greco in Occidente, 11-18.

20

"αὕ ο Λ α ο ", see J.M. Featherstone, Theodore Metochites's Poems 'To Himself'. Introduction, Text and Translation, Byzantina Vindobonensia 23 (Wien 2000), 13 and 155, pl. 4. 21 A. Onorato, Gli amici Bolognesi di Giovanni Tortelli, Biblioteca Umanistica 5 (Messina 2003), XLVIII-LIII. 22 See T. Martínez Manzano, "Autógrafos griegos de Lianoro Lianori en la Biblioteca Universitaria de Salamanca", Scriptorium 58.1 (2004): 17-20.

ὴ πο ὺ ' ἀ α, κ Ševčenko, όeatherstone, γἄ-37, l. 211.

The identification of the copyist is due to Erich Lamberz: "Das Geschenk des Kaisers Manuel II. an das Kloster Saint-Denis und der 'Metochitesschreiber' Michael Klostomalles", in ΛΙΘΟΣΡΩΣΟΝ. Studien zur byzantinischen Kunst und Geschichte. Festschrift für Marcell Restle, ed. T. Borkopp, T. Steppan (Stuttgart, 2000), 155-165, and "Georgios Bullotes, Michael Klostomalles und die byzantinische Kaiserkanzlei unter Andronikos II. und Andronikos III. in den Jahren 1298-1329", in Lire et écrire à Byzance, Centre de recherche d'histoire et civilisation de Byzance 19, ed. B. Mondrain (Paris 2006), 44-47.