On étudie dans cette thèse la relation entre les catégories finies et les matrices carrées positives, ensuite on arrive à étudier l'état de l'ensemble Cat(M) : s'il est vide ou non et déterminer ses bornes si c'est possible.
(suite de l'exposé précédent) On propose une sémantique de jeux pour le langage concurrent CCS (Milner), dont l'ingrédient principal est une catégorie de ``parties'' suffisamment générale pour contenir à la fois une notion de partie en monde clos (quand les joueurs ne peuvent pas interagir avec le monde extérieur) et une notion de vue (ce qu'un joueur retient d'une partie). Les stratégies sont définies sur les vues, puis sont munies (1) d'une opération d'extension à toutes les parties et (2) d'une opération de recollement, qui permet de faire jouer une équipe contre une autre. Ces deux opérations permettent de définir une équivalence de test équitable, analogue à celle donnée indépendamment pour CCS par Cleaveland et al d'une part et Brinksma et al d'autre part, qui compare les stratégies selon leurs réactions à des tests. On donne une traduction de CCS en termes de stratégies et on donne des résultats de comparaison de la sémantique induite avec la bisimilarité faible et avec l'équivalence de test équitable originale.
(disponible prochainement)
Dans cet exposé, on étudie les ensembles de degrés Turing associés aux pavages générés par un jeu de tuile. En particulier, on prouve qu'il existe un quasi-isomorphisme entre n'importe quelle classe Pi01 de {0,1}^N et un pavage. Pour cela, on introduit une construction permettant d'avoir du calcul tout en ayant un nombre dénombrable de pavages.
On propose une sémantique de jeux pour le langage concurrent CCS (Milner), dont l'ingrédient principal est une catégorie de ``parties'' suffisamment générale pour contenir à la fois une notion de partie en monde clos (quand les joueurs ne peuvent pas interagir avec le monde extérieur) et une notion de vue (ce qu'un joueur retient d'une partie). Les stratégies sont définies sur les vues, puis sont munies (1) d'une opération d'extension à toutes les parties et (2) d'une opération de recollement, qui permet de faire jouer une équipe contre une autre. Ces deux opérations permettent de définir une équivalence de test équitable, analogue à celle donnée indépendamment pour CCS par Cleaveland et al d'une part et Brinksma et al d'autre part, qui compare les stratégies selon leurs réactions à des tests. On donne une traduction de CCS en termes de stratégies et on donne des résultats de comparaison de la sémantique induite avec la bisimilarité faible et avec l'équivalence de test équitable originale.
The categorical presentation of the standard model of the geometry of interaction –namely the free compact closure of sets and partial injections Int(PInj)– fails to be a denotational semantics of MELL. The work of Melliès, Tabareau & Tasson on the formula for a free exponential modality gives us insights into the reasons of this failure: absence of free pointed objects, absence of equalizers of some groups of permutations... We will present generic constructions which successively add the algebraic structure needed to compute this formula, and show that the usual model of GoI wrapped in these successive layers defines a denotational semantics of MELL.
Le théorème de Feit-Thompson (1963) est un résultat historique de théorie des groupes finis. En effet, il permet de comprendre la structure de tous les groupes finis simples d'ordre impair et constitue ainsi une étape importante dans la classification des groupes finis simples qui est considérée comme achevée depuis les années 80. Néanmoins cette classification a un statut controversé car elle résulte de la compilation d'un nombre considérable de publications hétérogènes et parfois encore mal comprises. La preuve du théorème de Feit-Thompson est elle-même imposante, par sa taille et par la variété des résultats sur lesquels elle repose (théorie des groupes, algèbre linéaire, théorie de Galois, caractères,...). Elle est un défi pour les assistants à la preuves, logiciels permettant de représenter énoncés et preuves mathématiques sous la forme de termes logiques, vérifiables mécaniquement par un ordinateur. Dans cet exposé, qui ne présuppose aucune connaissance préalable en théorie des groupes, nous essaierons de montrer quels problèmes sont posés par une telle formalisation, par la représentation des objets mathématiques mis en jeu en théorie des types et en particuliers les solutions qui ont été trouvées pour faire vérifier (une partie conséquente de) cette preuve par l'assistant à la preuve Coq.
Nous proposons une méthode de calcul de proximité entre textes, appelée mesure de voisinage. Cette mesure est basée sur la présence de mots communs, de synonymes et de mots cooccurrents. Nous comparons cette mesure à la similarité cosinus, utilisée en Recherche d'Informations, au travers de trois bases de données différentes. Nous avons développé un prototype, nommé ALHENA, utilisé dans le domaine de la veille stratégique anticipative (VAS). L'expérimentation menée sur la valorisation du CO2 a montré l'utilité du prototype dans le processus de VAS, face au problème de la surcharge d'information notamment occasionnée par l'usage de l'Internet.
Recently, A. Polonsky has shown that the range property fails for H. We give here some conditions on a term F that imply that its range has cardinality either 1 or infinity. L'exposé sera accessible à tous les membres de l'équipe.
We exhibit a model structure on 2-Cat. A certain class of homotopies in this model structure turns out to be in 1-to-1 correspondence with strong simulations among labeled transitions systems, formalising the geometric intuition of simulations as deformations. The correspondence still holds in the cubical setting, characterising simulations of higher-dimensional transition systems (HDTS).
Finiteness spaces were introduced by Ehrhard as a model of linear logic, which relied on a finitess property of the standard relational interpretation and allowed to reformulate Girard's quantitative semantics in a simple, linear algebraic setting. I will review recent results obtained in a joint work with Christine Tasson, providing a very simple and generic construction of finiteness spaces: basically, one can ``transport'' a finiteness structure along any relation mapping finite sets to finite sets. Moreover, this construction is functorial under mild hypotheses, satisfied by the interpretations of all the positive connectives of linear logic. Recalling that the definition of finiteness spaces follows a standard orthogonality technique, fitting in the categorical framework established by Hyland and Schalk, I will show that the features of transport do not stand on the same level as the orthogonality category construction; rather, they provide a simpler and more direct characterization of the obtained structure, in a webbed setting. PS: Although I have slides (in english) ready for this presentation, it is best enjoyed in its chalk and blackboard version so I will stick to the latter.
The epistemic logic used for n-agent systems is the modal logic $S5_n$. In this talk I will briefly look at the Kripke semantics of this, how it relates to simple models of multiagent systems, and then will explore some ideas that make some tentative steps in the direction of modelling the flow information and knowledge in such systems. (The last part will raise more problems and questions than it answers but that is the fun of it!!! Since the paper below was written, directed homotopy has been developed more and it remains to be seen if it can be used to describe evolving multi-agent systems. I will discuss this beyond the prepared slides, if there is time.) (As I have slides in English, I will give the talk in that language.) Ref: Interpreted systems and Kripke models for multiagent systems from a categorical perspective, Theoretical Computer Science, 323 (2004) pp. 235-266.
Let $(X,G)$ be a space of orderings, let $G_0$ be a subgroup of index $2$ in $G$, $-1 in G_0$, and let $X_0$ denote the set of restrictions $X restriction G_0$ of elements of $X$ (viewed as characters on $G$) to characters on $G_0$. We search for necessary and sufficient conditions on $G_0$ for $(X_0,G_0)$ to be a quotient of $(X,G)$. In particular, we discuss the case when $(X,G)$ is the space of orderings of the field $Q(x)$. The talk is intended for a broad audience and all definitions necessary to follow the exposition will be explained in details. This is joint work with Murray Marshall.
Les « systèmes d'interaction » étaient à l'origine un moyen de représenter une notion de « jeux » en théorie des types. On obtient de cette manière une catégorie de jeux et de simulations qui modélise la logique linéaire différentielle. De manière assez surprenante, la dynamique ne joue aucun rôle dans la définition de composition des stratégies ! Cette notion de jeux existe sous des noms différents : « containers » (Ghani, Altenkirch, Hancock, ...) ou « foncteurs polynomiaux » (Hyland, Kock, Gambino, ...). Ce qui change ici est la notion de morphisme, plus générale que dans la littérature existante. Après une petite introduction, je montrerais les liens entre ces polynômes (point de vue intentionnel) et les foncteurs associés (point de vue extensionnel). Je construirais ensuite le modèle de (D)ILL en insistant sur l'interprétation en termes de jeux et les similarités formelles avec le modèle « dégénéré » des transformateurs de prédicats. Je ne ferais probablement aucune preuve, mais je mentionnerais quand même l'outil important, à savoir le langage interne des catégories localement cartésiennes fermées (càd la théorie des types dépendants)...
On muni les tuples d'ensembles d'entiers (X1, ..., Xn) de l'ordre suivant : (X1, ..., Xn) < (Y1, ..., Yn) si les Xs ont plus de « sections non-ordonnées » que les Ys. L'équivalence engendré par ce préordre est très simple, mais la preuve, bien qu'élémentaire, l'est moins (il s'agit d'un petit casse-tête amusant...). Je caractériserais cette équivalence (avec la preuve) ainsi que les liens entre cet ordre et l'inclusion toute simple. La preuve utilise la notion de fonction booléenne strictement croissante, qui semble ne pas apparaitre souvent dans la littérature. Je montrerais quelques unes de leurs propriétés. Pré-requis : notion d'ordre, de permutation, de quotient. (niveau L1)
Nous considérons le problème d'ajustement suivant : étant donné un ensemble de N points dans une image numérique en dimension d (i.e. Z^d), trouver un hyperplan discret qui contient le plus grand nombre possible de points. En utilisant un modèle discret pour l'hyperplan, nous montrerons que nous pouvons générer tous les ensembles de consensus possibles pour ajuster le modèle, et présenterons une méthode exacte pour d=2,3 dont la complexité en temps est O(N^d log N) et celle en espace est O(N). Ces complexités ont naturellement motivé l'amélioration. Nous avons ensuite observé que le problème est 3SUM-difficile pour d=2 de sorte qu'il ne peut probablement pas être résolu exactement avec une complexité meilleure que O(N^2), et il est conjecturé que la complexité optimale en dimension d est en fait O(N^d). Nous proposons donc deux méthodes approximatives de complexité linéaire en temps.
Between the important thing, when we deal with a type or a formula A of a system of typing that satisfies the strong normalization S.N., is to build a set of terms that satisfies 'a term in the set corresponding to A is equivalent to say that t is of type A. Unfortunally it is impossible to have this equivalency because of S.N., so the work take another formulation to escape this problem and it becomes 'a term in the set corresponding to A is equivalent to say that t is in relation with t' which is of type A'. many studies having this form where been published for many systems and relations. My work will be around the simply typed system in lambda mu calculus.
La définition des différentes K-théories suit le schéma suivant. Etant donné un objet C, on lui associe d'abord une catégorie AC qui est « structurée » (symétrique monoïdale, exacte, Waldhausen, …). On applique ensuite une « machine » de K-théorie sur AC pour obtenir finalement le spectre de K-théorie de l'objet C. Par exemple, on associe à un anneau R sa catégorie de modules projectifs de type fini pour obtenir la K-théorie usuelle de R. Dans ma thèse, je me suis intéressé à la première étape de ce processus. Plus précisément, je me suis posé les questions suivantes. Quels types d'objets admettent une notion intéressante de K-théorie ? Quelles catégories structurées devrait-on associer à ces objets pour obtenir une information K-théorique à leur sujet ? Finalement, comment cette correspondance prend-elle en compte les morphismes de ces objets ? Je vais décrire un cadre conceptuel qui permet de traiter de manière unifiée de nombreux exemples et qui apporte de nouveaux outils pour les étudier. Je prendrai l’exemple de la K-théorie des schémas comme fil conducteur.
We present here a strongly normalizable extension of second order functional arithmetics (AF2) with subtyping, that allows to program with recursive types in the pure lambda-calculus (i.e., without constant). It assigns types to the Scott encoding of algebraic datatypes and to the recursor on those types. Thus, it answers the open question of finding a strongly normalizing type system which allows to program on Scott numerals. One of the key features of the system is to have no more typing rules than AF2. The new rules are only subtyping rules. The first-order layer is used to prove the correction of extracted programs. It is also worth noticing that in this system union type (both finite and infinite) are definable and still the system enjoys subject-reduction.
Spatial computing aims at providing a scalable framework where computation is distributed on a uniform computing medium and communication happen locally between nearest neighbors. We study the particular framework of cellular automata, using a regular grid and synchronous update. As a first step towards generic computation, we propose to develop primitives allowing to structure the medium around a set of particles. We consider three problems of geometrical nature: moving the particles on the grid in order to uniformize the density, constructing their convex hull, constructing a connected proximity graph establishing connection between nearest particles. The last two problems are considered for multidimensional grid while uniformization is solved specifically for the one dimensional grid. The work approach is to consider the metric space underlying the cellular automata topology and construct generic mathematical object based solely on this metric. As a result, the algorithms derived from the properties of those objects, generalize over arbitrary regular grid. We implemented the usual ones, including hexagonal, 4 neighbors, and 8 neighbors square grid. All the solutions are based on the same basic component: the distance field, which associates to each site of the space its distance to the nearest particle. While the distance values are not bounded, it is shown that the difference between the values of neighboring sites is bounded, enabling encoding of the gradient into a finite state field. Our algorithms are expressed in terms of movements according to such gradient, and also detecting patterns in the gradient, and can thus be encoded in finite state of automata, using only a dozen of state.