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.
Les différentes parties de mes travaux de thèse en géométrie discrète et géométrie algorithmique seront présentées durant cet exposé.
Partie 1 : Nous considérons tout d’abord le problème de l’approximation d’un nombre réel par un nombre rationnel de dénominateur borné. Soit a un nombre réel, soit b et b’ deux nombres entiers tels que b<b’, nous souhaitons déterminer le nombre rationnel r=p/q qui approxime au mieux a, tel que b <= q <= b’. La principale approche numérique connue utilise le développement en fraction continue du réel a. Géométriquement, ce problème revient à déterminer le point de la grille le plus proche de la droite d’équation y=ax compris dans un domaine vertical défini par {(x,y) | b <= x <= b’}. Nous proposons de calculer l’enveloppe convexe des points de la grille situés au dessus (resp. en dessous) de la droite et compris dans le domaine vertical. Notre algorithme atteint une complexité logarithmique en la largeur du domaine vertical. De plus, il est adaptatif puisque le nombre d’itérations en temps constant effectuées par notre algorithme est exactement égal au nombre de sommets des deux enveloppes convexes calculées.
Partie 2 : Par la suite, nous présenterons notre algorithme de reconnaissance de plans discrets. Nous rappelons qu’un ensemble de points S de Z^3 est appelé morceau de plan discret s’il est contenu dans la discrétisation d’un plan euclidien. Un tel algorithme est utilisé pour décider si un sous-ensemble de points d’un objet discret peut être remplacé par une facette dans une représentation polyédrique de l’objet. La méthode proposée décide si un sous-ensemble de points de Z^3 correspond à un morceau de plan discret en résolvant un problème de réalisabilité sur une fonction convexe en dimension 2, dite fonction épaisseur. Ainsi, notre méthode ne prend en compte que deux paramètres et elle utilise des techniques géométriques planaires pour déterminer si l’espace des solutions est vide. Notre algorithme s’exécute en O(n log D) dans le pire cas ou n correspond au nombre de points de l’ensemble S et D représente la taille d’une boite englobant S. Notre méthode s’avère également efficace en pratique et reconnaît un ensemble de 10^6 points en environ 10 itérations linéaires.
Partie 3 : Si le temps nous le permet, nous aborderons enfin une problématique un peu à part : calculer l’épaisseur d’un ensemble de points de Z^d dans le réseau entier de même dimension (épaisseur latticielle). L’épaisseur d’un ensemble de points K suivant une direction c de Z^d correspond à la quantité max{c.x | x \in K} - min{c.x | x \in K}. L’épaisseur latticielle de l’ensemble de points K correspond à l’épaisseur minimum pour toutes les directions du réseau. D’après une idée originale de Fabien FESCHET, nous avons mis en place un algorithme valable en toute dimension pour déterminer cette épaisseur. Cette méthode s’avère optimale puisque linéaire en temps dans le cas planaire. En dimensions supérieures, nous passons par une approche gloutonne qui s’avère efficace en pratique.
TBA
L'exposé sera pour un public de non spécialistes. J'essaierai de raconter ce qu'est un bon langage de programmation (selon moi) et donc ce qu'est PML. J'essaierai notamment d'expliquer les points suivants:
Je ferai un premier exposé de complexité de communication, et un deuxième sur nos résultats sur les applications entre cette théorie et les automates cellulaires. Il y aura un peu de machines de Turing, pas mal d'automates cellulaires, beaucoup de complexité de communication, et aussi des circuits logiques. La complexité de communication est une théorie très générale, et il y a plein d'applications en complexité (parallèle et séquentielle), mais aussi des choses plus appliquées comme le design de processeurs, des problèmes de graphes, etc. En plus, c'est un modèle de calcul qui n'a pas besoin de la thèse de Church.
Dans cet exposé, je présenterai une famille de polyominos appelés doubles carrés, ayant la propriété de paver le plan par translation de deux façons distinctes. Rappelons qu'un polyomino est un sous-ensemble de la grille discrète qui est 4-connexe (connecté verticalement et horizontalement) et sans trou (c'est-à-dire que son complément est également 4-connexe). Nous pouvons en particulier coder son contour par un mot sur un alphabet à quatre lettres {h, b, g, d} codant les déplacements 'haut', 'bas', 'gauche' et 'droite'. J'introduirai d'abord les définitions de la combinatoire des mots nécessaires à cet exposé ainsi que les notions de polyominos et de pavages. Ensuite, je survolerai rapidement les résultats connus et certaines conjectures intéressantes. J'enchaînerai en présentant quelques propriétés sur les chemins liées à une généralisation de la notion de palindrome et je terminerai en présentant une famille de tuiles liées à la suite de Fibonacci. L'exposé se déroulera en québécois...
Des entreprises comme Amazon, Google et Yahoo rendent maintenant disponibles une partie de leurs fonctionnalités sous la forme de services web; une application tierce peut communiquer avec ces services via Internet en échangeant des messages dont la structure et le contenu sont publics et formellement définis. Cependant, la documentation précise également une foule d'autres détails sur la manière dont ces services doivent être consommés, exprimés en langue naturelle et échappant à toute formalisation. Ce contexte nous a amené à développer LTL-FO+, une extension de la logique temporelle LTL incluant 1) une forme particulière de quantification du premier ordre; 2) une sémantique à 2, 3 ou 4 valeurs de vérité, selon le contexte. On verra que, contrairement à LTL, elle est appropriée pour exprimer des contraintes sur les séquences de messages propres aux applications web. On s'intéressera par la suite à son runtime monitoring; pour ce faire, nous présenterons BeepBeep, un outil permettant la vérification et l'application de formules LTL-FO+ en temps réel sur de vraies applications web. Finalement, on verra au moyen d'un exemple concret (si la connexion Internet le permet) comment BeepBeep: 1) empêche une application web mal programmée de commettre des erreurs; et 2) nous permet de découvrir que les services web d'Amazon ne respectent pas certains détails de leur propre documentation.
One of the purposes of quantum programming languages is to express quantum programs, however a possibly more important reason is to provide a framework for reasoning about the programs expressing quantum algorithms -- and hence about quantum computation in general.
Indeed, in classical computer science it is frequent to express the reasoning behind a program via several formally-defined logics. These logics provide important frameworks in which to reason and prove properties about the computational processes. Often they arise via the study of type systems for the language. Related to our motivation there is already a quantum logic, which was developed before quantum computing, and which is not known to have a clear relation to quantum programs and algorithms.
The Linear-Algebraic Lambda-Calculus extends the Lambda-Calculus with the possibility to make arbitrary linear combinations of terms a.t+b.u. We want to set up a type system for it which is capable of such handling vectorial notions, i.e. were types themselves form a vector space. This is needed at a practical level for instance in order to prove normalization and unitarity properties of terms. There is also the intriguing question as to what logical meaning we can give these `superposition types'.
Joint work with Pablo Arrighi.
We consider a graph having a single quantum system sitting at each node. The entire compound system evolves in discrete time steps by iterating a global evolution G. Moreover we require that this global evolution G be unitary, in accordance with quantum theory, and that this global evolution G be causal, in accordance with special relativity. By causal we mean that information can only ever be transmitted at a bounded speed, the speed bound being quite naturally that of one edge of the underlying graph per iteration of G. We show that under these conditions the operator G is local; i.e. it can be put into the form of a quantum circuit made up with more elementary, unitary gates -- each acting solely upon neighbouring nodes.
Joint work with Vincent Nesme and Reinhard Werner.
Rencontre annuelle du projet Types, au centre Paul Langevin à Aussois, du 12 au 15 mai.
Groupe de travail pour comprendre ce qu'on pourra de la théorie géométrique de la complexité à la Ketan Mulmuley. On se basera sur ses articles introductifs et les vidéos de ses conférences à l'Institute for Advanced Study en février 2009.
Nous considérons un graphe où les cellules sont caractérisées par un état qui est soit noir, soit blanc. À chaque pas de temps, une cellule, choisie aléatoirement, se met à jour et passe dans l'état minoritaire dans son voisinage. L'évolution globale de ce processus ne semble pas dépendre de la topologie du graphe: dans un premier temps des régions, pavées par des motifs dépendant de la topologie du graphe, se forment rapidement. Puis dans un deuxième temps, les frontières entre ces régions évoluent jusqu'à devenir relativement stables. Nous étudions ce processus sous différentes topologies: arbres, anneaux, grilles, cliques. Ceci nous permet de montrer que même si ce processus se comporte à priori globalement de la même manière sur n'importe quel graphe, modifier la topologie influence la façon dont les régions sont pavées (rayures, damiers), la structure et les mouvements des frontières entre les régions, l'ensemble limite, le temps de relaxation (le temps nécessaire pour que le processus atteigne une configuration de l'ensemble limite). Ainsi, Minorité entraîne des comportements riches et variés qui se révèlent difficile à analyser. Comprendre cette règle simple est néanmoins nécessaire avant de considérer des règles plus compliquées.
Les mots (finis ou pas, en dimension 1 ou supérieure) peuvent être vus comme des modèles de formules de la logique monadique du second ordre (MSO), une formule définissant alors un langage. Cette approche a été suivie avec succès en dimension 1 par Büchi et Elgot dans les années 60 : les langages ainsi définis sont exactement les langages rationnels. De plus toute formule MSO est dans ce contexte équivalente à une formule EMSO (quantification existentielle au second ordre suivie d'une formule au premier ordre).
Plus récemment, Giammarresi, Restivo, Seibert et Thomas ont reconsidéré ces résultats dans le cas des figures'', c'est à dire des mots bidimensionnels finis avec bords marqués : cette fois les formules EMSO définissent exactement les langagessofiques'' (projections de langages locaux), mais elles ne suffisent plus à capturer tous les langages définissable par une formule MSO.
L'objectif de cet exposé est de développer cette approche, en dimension 2, pour les sous-shifts (ensembles de configurations fermés topologiquement et invariants par décalages). Nous verrons alors que les sous-shifts sofiques (introduits par Weiss dans les années 70) ne correspondent pas aux sous-shifts définissables par formules EMSO. Nous donnerons néanmoins une caractérisation logique des sous-shifts sofiques et, inversement, nous donnerons une caractérisation ``combinatoire'' des ensembles de configurations définissables dans EMSO.
Je présente l'approche algébrique au lambda-calcul basée sur les algèbres de lambda abstraction et sur les algèbres de Boole, qui a permis d'étudier la structure du treillis des lambda théories et d'obtenir des résultats d'incomplétude pour le sémantique du lambda calcul. Depuis, je présente mon dernier résultat: la lambda théorie minimum extensionelle n'est pas la théorie d'une domaine de Scott réflexive.
Voir la page dédiée.
TBA