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.
In this talk, we discuss how to model in a finite way the semantics of resource-allocating interactive programs. Surprisingly, in doing so, the notion of behavioural symmetry arises from the framework, and is necessary to recover canonical models. Behavioural symmetry expresses properties relating the semantics of a program and the available resources at each state, e.g. ``the distinguished variables x and y have the same observable effect, and swapping them does not affect the semantics of the program''. Labelled transition systems (LTSs) have been successfully used to model the semantics of interactive programming languages. Their natural equivalence relation, the so-called bisimilarity, is a fundamental tool for the study of such languages. However, when resources (e.g. memory locations) can be allocated and de-allocated along transitions, bisimilarity becomes a non-standard notion (cf. the pi-calculus). The categorical abstraction of coalgebras generalises LTSs and has an associated, general definition of behavioural equivalence, coinciding with bisimilarity for LTSs. Presheaves generalise classical sets; elements of presheaves have intensional features such as interfaces, or resources, and operations on them. By using coalgebras in a category of presheaves, bisimilarity in the presence of resource allocation is recovered from the standard categorical definition. However, the obtained transition systems become infinite state machines because of fresh resources. An equivalence between categories of presheaves and of families recovers a finite representation for memory-bound programs. An associated notion of symmetry is necessary for the equivalence to hold, and for final systems (=canonical models) to exist, giving rise to behavioural symmetry.
Cet exposé, faisant suite au précédent sur les préfaisceaux, est une introduction aux faisceaux, un autre important outil catégorique dérivé des premiers. Je rappellerai le lemme de Yoneda, puis définirai les notions de crible, topologie de Grothendieck et enfin faisceau, en m'appuyant sur des exemples et contre-exemples. Si le temps le permet, je survolerai le théorème du faisceau associé, qui construit un faisceau à partir d'un préfaisceau arbitraire (si Christophe est là, on parlera de PML). Enfin, peut-être, je raconterai en deux mots mon travail avec Damien Pous, qui repose sur une description en termes de faisceaux des stratégies dites ``innocentes'' en sémantique des jeux.
En 1998, Pestov montra que le groupe G des automorphismes des rationnels (vus comme ensemble ordonné) est extrêmement moyennable, c'est-à-dire que toute action continue de G sur tout espace topologique compact admet un point fixe. Pour ce faire, il démontra que la propriété énoncé ci-dessus est équivalente au théorème de Ramsey fini. Ce résultat constitue le point de départ des travaux de Kechris, Pestov et Todorcevic, qui établirent en fait qu'il s'agit là d'un phénomène général liant théorie de Ramsey pour certaines classes de structures finies (classes de Fraïssé) et moyennabilité extrême pour certains groupes topologiques. Le but de cet exposé sera de présenter la correspondance de Kechris-Pestov-Todorcevic ainsi que certaines de ces conséquences.
Cet exposé est une introduction aux préfaisceaux, un important outil catégorique. Je reprendrai du début: catégories, foncteurs, transformations naturelles, en considérant de nombreux exemples petits et gros. Je concluerai par le lemme de Yoneda en donnant l'exemple des graphes.
IR' is a powerful principle for in the context of dependent type-theory, for defining simultaneously a set U *inductively*, with a function T : U -> D *recursively*. D may belarge', eg the type of Sets, and a paradigm example is a universe of (codes for) sets. I will try to motivate and illustrate this principle. Using containers (a particular kind of endofunctor on Set), one can distill out the essence of IR in an extremely compact, memorable form. I will try to give a tour of the distillery.
Dans cet exposé, nous montrerons comment utiliser la combinatoire des mots et la théorie des automates afin d'étudier certaines propriétés arithmétiques des séries de Laurent à coefficients dans un corps fini. En particulier, à l'aide d'une méthode inspirée par un article d'Adamczewski et Cassaigne, nous donnerons une majoration générale de l'exposant d'irrationalité des séries algébriques. Nous illustrerons cette approche à l'aide de quelques exemples.
I shall dust off some work by Bohm, on arithmetical features of combinatory logic. The natural combinators for addition, multiplication, exponentiation and nihilation of Church satisfy some pleasing algebraic laws resembling those of ordinal arithmetic. But they also satisfy and some other ''wild'' laws (resembling nothing arithmetical) in virtue of which they are combinatorially complete. Because of that, they support a notion of logarithm (with respect to a ''base''). I may add some remarks on ''exponentiality'', which says that two ''numbers'' are the same if they have the same behaviour as exponents.
Tout le monde aime les automates cellulaires, tout le monde aime les fractales, et l'on sait bien que celles-ci peuvent être produits par ceux-là. Par exemple, le triangle de Sierpinski, comme il s'agit du triangle Pascal modulo 2, est le diagramme espace-temps limite d'un automate cellulaire correspondant à la relation C(n+1,k+1)=C(n,k)+C(n,k+1). Plus généralement, il est connu que si l'alphabet a une structure d'anneau commutatif et que l'automate cellulaire est un morphisme d'anneaux - on parle alors d'automate cellulaire linéaire - une structure fractale va émerger de ses diagrammes espace-temps. Remplaçons maintenant l'anneau par un simple groupe - non, pas un groupe simple, un simple groupe abélien fini. J'expliquerai pourquoi, à mon sens, c'est dans ce cas plus général qu'on devrait parler d'automate cellulaire linéaire, et non pas seulement dans le cas des anneaux comme on le fait habituellement ; et surtout, je tâcherai de faire comprendre pourquoi leurs diagrammes espace-temps ont aussi des propriétés fractales.
Le size-change termination principle'' est un test (correct mais forcément incomplet) pour décider la terminaison de programmes mutuellement récursifs. Ce test, dû à A. ben Amram, N.D. Jones et C.S. Lee est particulièrement simple et élégant, tout en étant relativement puissant et modulaire. Il s'agit essentiellement d'une opération de clôture transitive sur le graphe d'appels des fonctions et la preuve de correction repose sur le théorème de Ramsey infini. Quand le langage des définitions récursives est un langage avec constructeurs / destructeurs à la ML, il y a une notion naturelle de taille : le nombre de constructeurs dans une valeur. Dans ce contexte, on peut généraliser le test pour conserver plus d'information que la seule taille des arguments. Ceci permet notamment d'ignorer certains chemins du graphe d'appels qui ne correspondent à aucune suite concrète d'appels. Par contre, la preuve de correction du nouveau principe est plus complexe que l'originale. Après une rapide présentation du test original, je décrirais cette extension et donnerai certaines idées de la preuve de correction. Comme le test est implanté (en Caml) pour le langage PML, je donnerais également des exemples (etcontre exemples'') pour permettre de se faire une idée des définitions acceptées (et refusées).
Je présenterai un modèle localisé de la logique linéaire multiplicative basé sur des graphes à partir duquel il est possible d'obtenir une catégorie *-autonome ainsi que de définir une notion de vérité. Je montrerai également qu'une restriction de ce modèle à une certaine classe de graphes se plonge dans la géométrie de l'interaction hyperfinie de Girard. Ceci permet d'appréhender de manière purement combinatoire le cadre utilisant des éléments d'analyse fonctionnelle avancés introduit par Girard. J'expliquerai enfin comment adapter ce modèle pour l'étendre à la logique linéaire multiplicative-additive, et discuterai d'une extension aux exponentielles.
TBA
Les courbes frontières définissent les régions ou les formes du plan de manière compacte et descriptive. Il est bien connu que les formes doivent être étudiées à différentes échelles. Ceci a conduit au développement des pyramides régulières et irrégulières pour l'analyse des formes et la compréhension des scènes. Cependant, il n'existe pas une description analytique de la multi-résolution d'une forme numérique, contrairement au célèbre espace-échelle (scale-space) dans le monde continu. En outre, les primitives géométriques telles que les lignes, les cercles ou les polynômes ont une grande importance dans le contexte de la géométrie numérique. Les morceaux des droites numériques sont un bon moyen pour estimer les tangentes et les arcs discrets approchent la courbure. Il est donc nécessaire de les garder dans l'analyse multi-échelle des frontières numériques. Un des objectifs de cette thèse est de donner des nouveaux résultats analytiques sur la multi-résolution des droites 4-connexes et des segments de droites 4-connexes. Figueiredo est le premier qui a étudié le comportement des droites 8-connexes lors du changement de la résolution de la grille. Dans le présent travail, nous considérons une droite 4-connexe pour laquelle une description analytique est fournie lorsque la résolution de la grille est modifiée par un facteur arbitraire. En plus, nous montrons que leurs couvertures sont des droites 4-connexes. Comme les formules analytiques des segments de droite sont un problème beaucoup plus difficile, nous proposons un parcours indirect pour la multi-résolution d'un DSS en utilisant le fait qu'un segment est un morceau fini d'une droite discrète. Etant donné un DSS, nous construisons deux droites dont l'intersection le contient et dont la partie connexe principale a les mêmes caractéristiques arithmétiques, ainsi que le même nombre de motifs. Notons que nous proposons de nouveaux résultats combinatoires des intersections de droites. Nous déterminons la multi-résolution du segment en examinant la multi-résolution de l'intersection de ces deux droites. Nous donnons une nouvelle description analytique de cet ensemble avec les inégalités arithmétiques. Nous abordons également le problème du calcul des caractéristiques exactes d'un sous-segment d'une droite 4-connexe qui a des caractéristiques connues. Nous présentons deux nouveaux algorithmes SmartDSS et ReversedSmartDSS qui résolvent ce problème. Leur principe est de se déplacer dans l'arbre de Stern-Brocot de la fraction soit de manière haut-bas ou bas-haut. Dans le pire cas, leur complexité est meilleure que l'algorithme de reconnaissance DSS classique. Les deux algorithms peuvent dès lors servir à calculer efficacement la multi-résolution d'un segment. Les bruits tout au long des contours numériques ne sont pas vraiment détectés, mais plutôt annulés par l'épaississement des segments de droites 4-connexes. De plus, l'épaisseur est réglée par un utilisateur et aussi définie globalement pour le contour. Pour surmonter ce problème, nous proposons une stratégie originale pour détecter localement à la fois la quantité de bruit et les épaisseurs significatives de chaque point de contour. Ce travail se base sur les propriétés asymptotiques de segments flous d'épaisseurs différentes, et forme une alternative à l'approche multi-résolution de la détection du bruit.
La classe des mots C∞, ou facteurs lisses, est la classe des mots finis qui sont arbitrairement dérivables. Ils ont été défini par Dekking pour décrire l'ensemble des facteurs du fameux mot de Kolakoski, le mot infini point fixe du codage par plages. Nombre de conjectures sur le mot de Kolakoski et ses facteurs restent ouvertes. Nous introduisons une nouvelle représentation des mots C∞ basée sur un codage de ces mots sur un alphabet à trois lettres. Ceci permet de classifier les mots C∞ en classes d'équivalence. Ces classes d'équivalence peuvent être représentées sur un graphe infini dont nous étudions les propriétés. Nous démontrons que ce graphe peut être décrit inductivement par une fonction récursive dont la définition est totalement indépendante du contexte des mots C∞.
B. Kerautret et J.-O. Lachaud ont proposé en 2009 un estimateur de bruit local sur les contours discrets 2D. Leur méthode consiste en une analyse multi-échelle des longueurs des segments maximaux en chaque point du contour. L'étude de la courbe du profil multi-échelle et la connaissance du comportement asymptotique de ces longueurs permettent, entre autre, de détecter du bruit en chaque point du contour ainsi que l'échelle significative. Nous proposons d'étendre cette méthode à la détection de bruit local sur les contours discrets tridimensionnels. Pour cela, nous nous orientons vers une analyse multi-échelle des plans discrets maximaux couvrant chaque point du contour. Nous choisissons dans un premier temps d'étudier le critère de l'aire discrète et nous espérons observer un comportement asymptotique caractéristique. Ces travaux sont actuellement en cours.