Cette séance est consacrée au modèle booléen V^B de ZF, dont la construction est paramétrée par une algèbre de Boole complète B dans le modèle initial. Au programme: rappels de théorie des ensembles (classes et hiérarchie de Veblen), définition de la hiérarchie des B-ensembles, effondrement extensionnel, mélange de B-ensembles, principe du maximum et plénitude, conservation des propriétés Sigma_1, satisfaction des axiomes de ZFC.
Je présenterai ce qu'est une paramétrisation conforme d'une surface et son intérêt pour la géométrie discrète, en particulier la géométrie digitale, pour le plaquage de texture et le calcul des grandeurs géométriques d'une surface ou d'une courbe (normale, courbure...). Je discuterai de diffusion discrète, du laplacien discret dans le cadre des maillages et dans le cadre voxellique. La théorie de l'analyse conforme discrète qui est associée partage de nombreux points avec la théorie des surfaces de Riemann continue.
Les automates cellulaires ont cette riche dualité de pouvoir être à la fois considérés comme des systèmes dynamiques à temps et espace discret et comme des objets combinatoires simples proches des modèles de calcul de type machine. Cette dualité permet d'établir facilement des résultats de calculabilité et de complexité concernant la dynamique de ces objets. Dans cet exposé, nous abordons une propriété dynamique élémentaire : l'existence d'une période temporelle commune à toutes les configurations du système. Sans surprise, nous établissons l'indécidabilité de cette propriété. Pour établir ce résultat, les outils maintenant classiques liant pavages et automates cellulaires ne fonctionnent pas. C'est donc l'occasion d'exhiber de nouveaux outils adaptés et de redécouvrir d'anciens résultats sur les machines de Turing. Nous aborderons les notions de mortalité et de périodicité dans ce modèle de calcul, l'art et la manière de programmer dans un cadre réversible et nous montrons que le problème de l'immortalité des machines de Turing reste indécidable dans le cadre réversible. Ces travaux sont issus d'une collaboration avec J. Kari (Univ. Turku, Finlande)
Cet exposé commence par la présentation rapide de la règle Minorité stochastique et de ses particuliarités. Ensuite, je présenterai une application de cette règle pour modéliser la formation de quasi-cristaux.
Considérons un graphe où chaque sommet reçoit la couleur noire ou blanche. Une arête contient une erreur si elle relie deux sommets de la même couleur. Minorité est une dynamique stochastique minimisant rapidement l'énergie. Sous cette dynamique, un sommet, chosi aléatoirement et uniformément parmi l'ensemble des sommets, peut changer d'état si au moins la moitié des arêtes qui lui sont adjacentes sont erronées. Cette dynamique est sensible à la topologie du graphe et son analyse fine s'est révélée compliquée.
En physique, dans les annnées 70, il était conjecturé que toutes les structures ordonnées soient périodiques. En 1984, un contre-matériaux fût découvert et reçu le nom de quasi-cristal. Dès 1974, Penrose avait présenté un structure théorique ordonnée et apériodique. Le but de notre projet est de présenter un modèle pour expliquer la formation d'une telle structure. Pour cela, nous considérons le modèle des pavages par coupe et projection (qui contient le pavage de Penrose). En définissant une notion d'erreur et d'énergie sur ces pavages, la règle Minorité procédant par flips permet de converger rapidement expérimentalement vers une structure ordonnée qui selon la famille de pavages par coupe et projection considérée est soit périodique, soit apériodique. Je présenterai nos résultats expérimentaux ainsi que notre analyse de cette dynamique pour les pavages 2 vers 1 (mots sur deux lettres).
Les systèmes d'acquisition de données image en deux ou trois dimensions fournissent généralement des données organisées sur une grille régulière, appelées données discrètes. Que ce soit pour la visualisation ou l'extraction de mesures, la géométrie discrète définit les outils mathématiques et géométriques pour de nombreuses applications. Dans cet exposé, je présenterai comment adapter divers algorithmes de la géométrie discrète aux grilles irrégulières isothétiques. Ce modèle de grille permet de représenter de manière générique les structurations d'images en pixels ou voxels de taille et de position variables : les grilles anisotropes, très répandues en imagerie médicale, les décompositions hiérarchiques telles que quadtree/octree, les techniques de compression comme le run length encoding, etc. Plus précisément, je présenterai l'extension à cette représentation de plusieurs méthodologies largement étudiées pour analyser les formes discrètes: la reconstruction d'objets binaires complexes, la transformée en distance et l'extraction d'un axe médian. Je montrerai enfin comment ces outils sont employés dans diverses applications : la distinction de caractères ambigus dans un outil de reconnaissance de plaques minéralogiques, l'approximation dynamique de courbes implicites planaires et l'analyse d'objets discrets bruités.
Cette séance est consacrée au modèle booléen V^B de ZF, dont la construction est paramétrée par une algèbre de Boole complète B dans le modèle initial. Au programme: rappels de théorie des ensembles (classes et hiérarchie de Veblen), définition de la hiérarchie des B-ensembles, effondrement extensionnel, mélange de B-ensembles, principe du maximum et plénitude, conservation des propriétés Sigma_1, satisfaction des axiomes de ZFC.
Parmi les nombreuses structures ordonnées liées aux espaces topologiques, les treillis continus occupent une place importante. Ils constituent par exemple les espaces topologiques de Kolmogorov injectifs. Nous nous proposons ici de présenter ces treillis d'un point de vue algébrique au travers de la notion de monade et d'adjonction de Galois. La définition originelle d'espace topologique donnée par Hausdorff en 1914 apparaît alors de façon naturelle, et nous permet de jeter un regard neuf sur le résultat d'injectivité mentionné ci-dessus.
Voir la page dédiée.
TBA
Nous construisons une structure de modeles de Quillen pour la categorie des omega-categories strictes, a partir d'un ensemble de cofibrations generatrices et d'une classe d'equivalences faibles. Toute omega-categorie est fibrante par rapport a cette structure, alors que les omega-categories cofibrantes sont precisement les libres.
Cet exposé est divisé en deux parties distinctes présentant deux sujets de recherche autour de la Logique Linéaire. Bien qu'abordés il y a longtemps, ces sujets présentent toujours des questions ouvertes intéressantes. L'exposé pose plus de questions qu'il ne donne de réponses.
Le premier sujet concerne la notion de structure en Logique Linéaire. De nombreuses extensions de la Logique Linéaires ont été proposées dans le passé pour introduire une forme de structure qui dépasse celle de multi-ensemble: logique cyclique, logique non commutative, calcul de Lambek non associatif (qui en fait prédate la Logique Linéaire)... Un cadre général, appelé ``Logiques Linéaires Colorées'', a été proposé pour capturer les mécanismes communs à toutes ces extensions, et permettant d'en construire d'autres à l'infini, respectant automatiquement les propriétés essentielles d'élimination de la Coupure et de focalisation (ce travail montre d'ailleurs que ces deux propriétés sont intimement liées). La question ouverte est de comprendre quels critères supplémentaires permettent de séparer, dans cette infinité potentielle de systèmes, le bon grain de l'ivraie, avec l'idée sous-jacente que la Logique devrait avoir un caractère de nécessité, et ne pas laisser place à l'arbitraire.
Le deuxième sujet concerne un paradigme de programmation fondé non pas sur la réduction des coupures dans les réseaux de preuves mais sur la construction de réseaux de preuves en Logique Linéaire. La construction de réseaux, comme la réduction, peut se faire en parallèle, mais, contrairement à la réduction, il y a des séquentialisations irréductibles, qu'exprime la nécessité de respecter le critère de correction. Le paradigme résultant est très proche de celui, plus pragmatique, des systèmes transactionnels, issus du monde des bases de données, mais dont les mécanismes sont aujourd'hui présents dans les couches intergicielles de toutes les grandes applications réparties. Un mécanisme de construction incrémental de réseaux de preuves a été proposé dans le passé dans le cadre du fragment strictement multiplicatif de la Logique Linéaire. Les questions ouvertes sont ici de savoir si ce mécanisme est optimal pour le fragment visé d'une part et d'autre part s'il peut être étendu à des fragments plus larges, voire au système complet.
Deuxième séance du groupe de lecture sur le livre de Kohlenbach ``Applied Proof Theory''.
Developing effective reasoning techniques for languages with higher- order constructs is a challenging problem, made even more challenging with the presence of concurrency and mobility. In this talk I will present a practical and effective reasoning methodology for such a language, which employs first-order reasoning and handles examples in a straightforward manner. There are two significant aspects to this theory. The first is that higher-order inputs are treated in a first- order manner, hence eliminating the need to reason about arbitrarily complicated higher-order contexts, or to use up-to context techniques, when establishing equivalences between processes. The second is that we use augmented processes to record directly the knowledge of the observer. This has the benefit of making ordinary first-order weak bisimulation fully abstract w.r.t. contextual equivalence. It also simplifies the handling of names, giving rise to a truly propositional Hennessy-Milner characterisation of higher-order contextual equivalence. I will illustrate the simplicity of the approach with example equivalences and inequivalences, and use it to show that contextual equivalence in a higher-order setting is a conservative extension of the first-order pi-calculus.
La séance précédente était consacrée aux algèbres de Boole et aux notions de filtre, d'idéal et d'ultrafiltre. Cette séance sera consacrée à la définition de la notion de modèle Booléen (en insistant sur les problèmes soulevés par cette définition) et à l'étude de ses propriétés: validité, complétude, etc. Je présenterai les principales constructions attachées aux modèles booléens: produit, quotient, ultraproduit, ultrapuissance. Je terminerai en montrant comment la théorie peut être appliquée à la construction des modèles de l'analyse non standard.
Voir la page dédiée.
En combinatoire des mots et plus précisément dans l'étude des mots unidimensionnels, la notion de mot de retour a joué un rôle important, en particulier dans la caractérisation des mots sturmiens. Ces mots servant de représentation pour les droites discrètes, il est tout naturel de se poser la question d'une caractérisation en dimension supérieure, en particulier dans le cas des plans discrets. En dimension 2, on vient à considérer des mots bidimensionnels. Les notions habituelles doivent donc être adaptées. Nous verrons que le passage à la dimension 2 provoque de vrais problèmes vis à vis de définitions simples en dimension 1.
Je présente un lambda calcul codant une logique intuitionniste du second ordre et permettant de programmer un ou-parallèle''. Ce calcul a les propriétés suivantes :préservation de type'', forte normalisation'' etunicité de représentation des données''. Il permet aussi d'écrire des programmes avec une sorte d'exception. Il est inspire du lambda-mu-{++}-calcul que j'ai introduit en 2002.
En 1962, Cohen a résolu le premier problème de Hilbert en montrant que l'hypothèse du continu est indécidable dans la théorie des ensembles de Zermelo-Fraenkel. La technique qu'il a introduite pour établir ce résultat non trivial - le forcing - est devenue aujourd'hui un outil standard en théorie des modèles. Cette technique a permis d'établir de nombreux autres résultats de cohérence relative (ou d'indépendance), comme par exemple la cohérence de l'axiome de Solovay: « toute partie de R est mesurable au sens de Lebesgue » dans une théorie des ensembles sans axiome du choix (mais avec choix dépendant).
Dans cet exposé introductif au forcing, je me propose de présenter la théorie des modèles booléens, une variante du forcing (introduite par Scott, Solovay et Vopenska dans les années 1960) qui permet de faire essentiellement les mêmes constructions que Cohen, mais dans un cadre qui est plus facile à saisir au premier abord. J'introduirai les notions de base (algèbres de Boole, ultrafiltres, modèles booléens, quotient, produit, ultraproduit et ultrapuissance) tout en illustrant mon propos par quelques exemples de constructions, notamment en lien avec l'« analyse non standard ».
La preuve de l'indépendance de l'hypothèse du continu à l'aide de ces outils fera l'objet de l'exposé suivant.
In 2003, Hofmann and Jost introduced a type system that uses a potential-based amortized analysis to infer bounds on the resource consumption of (first-order) functional programs. This analysis has been successfully applied to many standard algorithms but is limited to bounds that are linear in the length of the input.
Here we extend this system to polynomial resource bounds. An automatic amortized analysis is used to infer these bounds for functional programs without further annotations if a maximal degree for the bounding polynomials is given. The analysis is generic in the resource and can obtain good bounds on heap-space, stack-space and time usage. Furthermore, the analysis can be used to infer polynomial relations between the input and the output sizes of a function in the sense of sized types.
Travail en collaboration avec Jan Hoffmann.
The wire calculus is a process algebra for modelling truly concurrent systems with explicit network topologies. It benefits from using categorical operators for coordination of processes: the tensor product and sequential composition of monoidal categories. The dynamics are handled by operators inspired by Milner's CCS and Hoare's CSP: unary prefix operation, binary choice and a standard recursion construct. The operational semantics is a labelled transition systems derived using SOS rules. After presenting the formal definition of the calculus I will discuss some basic results and give several examples.