L'algèbre géométrique ou algèbre de Clifford offre un cadre algébrique intuitif pour la représentation d'objets géométriques et leurs transformations géométriques. Cette algèbre est le résultat de la généralisation de l'algèbre de Grassmann et des quaternions de Hamilton. Le développement de son utilisation pour les problèmes en géométrie discrète et en vision par ordinateur est relativement récent. Dans ce contexte, nous nous sommes intéressés à une implantation efficace de l'algèbre géométrique permettant une utilisation dans les espaces vectoriels de hautes dimensions. Nous avons notamment proposé un formalisme récursif de l'algèbre géométrique sur arbres préfixes en montrant que la définition récursive du produit obtenue vérifiait les propriétés de ce produit. Je montrerai les résultats obtenus en termes de complexité algorithmique. Ces résultats nous ont permis de développer la représentation et la transformation de surfaces quadratiques dans un espace vectoriel de haute dimension. Je montrerai les propriétés et les opérations géométriques possibles dans cet algèbre. En parallèle, nous avons montré que cette algèbre pouvait être utilisée en géométrie digitale pour la représentation des transformations digitales et notamment l'approximation de transformations rigides par des transformations digitales définies avec l'algèbre géométrique. Je montrerai enfin l'atout de cette algèbre pour un problème d'optimisation défini sur des nuages de points.
Dans le contexte de la géométrie discrète et du traitement d'image, la grille hexagonale est souvent considérée intéressante, mais difficile à représenter et à utiliser. Par conséquent, cette grille est moins populaire. Dans cet exposé, je passerai en revue le concept de la grille hexagonale dans le contexte de deux applications. La première est liée aux déplacements rigides discrets définis sur des grilles régulières et à la préservation de l'information sous une telle transformation. En effet, en général, les discrétisations de déplacements rigides ne sont pas bijectives. Néanmoins, certaines sont bijectives, et je vais discuter la caractérisation des rotations discrètes qui sont bijectives sur la grille hexagonale. En fin, je vais comparer les distributions des angles dont les rotations discrétisées sont bijectives dans les grilles hexagonale et carrée. Dans la deuxième partie de mon exposé, je me concentrerai sur les utilisations de la grille hexagonale dans l'architecture et la conception de bâtiments. Depuis un certain temps, on savait que les structures construites à partir de panneaux hexagonaux planaires, sont meilleures que les structures triangulaires en termes de stabilité structurelle et de répartition des contraintes physiques. Dans les structures triangulaires, de telles contraintes (par exemple causées par des chutes de neige) s'accumulent aux sommets. Au contraire, dans le cas des structures hexagonales, ces contraintes sont uniformément réparties sur la structure et transmises par les arêtes. Malheureusement, la conception de maillages hexagonaux planaires est un problème très difficile. Dans cet exposé, je vais passer en revue le problème de la conception de tels maillages hexagonaux planaires et décrire un processus automatique pour le remaillage de maillages triangulaires en maillages hexagonaux planaires.
Isomanifolds are the generalization of isosurfaces to arbitrary dimension and codimension, i.e. manifolds defined as the zero set of some multivariate multivalued smooth function $f: R^drightarrow R^{d-n}$. A natural (and efficient) way to approximate an isomanifold is to consider its Piecewise-Linear (PL) approximation based on a triangulation $mathcal{T}$ of the ambient space $R^d$. In this paper, we give conditions under which the PL-approximation of an isomanifold is topologically equivalent to the isomanifold. The conditions are easy to satisfy in the sense that they can always be met by taking a sufficiently fine and thick triangulation $mathcal{T}$. This contrasts with previous results on the triangulation of manifolds where, in arbitrary dimensions, delicate perturbations are needed to guarantee topological correctness, which leads to strong limitations in practice. We further give a bound on the Fr{'e}chet distance between the original isomanifold and its PL-approximation. Finally we show analogous results for the PL-approximation of an isomanifold with boundary.
An automata network (AN for short) is a finite digraph where each node holds a state, chosen among a finite set, that evolves in function of the states of its inbound neighbors. Time is discrete and all nodes evolve synchronously and in parallel, similarly to what happens in an cellular automaton. In other terms, the differences between a cellular automaton and an automata network is that the grid'' is an arbitrary finite digraph, and that different nodes may have different update functions. ANs have been used to model neural networks, dynamics of expression and inhibition of genes, distributed algorithms, and more. Although ANs look like a model of computation, they are not Turing-complete, for they lack unbounded memory. Still, they are subject to some kind ofRice theorems'', i.e., results along the lines of:``any nontrivial property of the function computed by an automata network is computationally hard to test''. In this talk, we will review several results that fit this pattern, as well as pieces of proof that hopefully may be reused in other contexts.
Le traitement d’images acquises sous éclairement non contrôlé s’avère fréquent dans de nombreuses applications. En effet, différentes conditions d’acquisitions contraignent la prise de vue comme le mouvement, un éclairement non uniforme, les changements d’opacité de l’objet, le bruit d’acquisition,etc... Ceci a pour conséquence de créer des variations inhomogènes de contraste dans les images. Peu de méthodes de traitement d’images prennent en compte ces variations. Afin de résoudre ce problème, un modèle adapté aux images peu contrastées, à savoir le Logarithmic ImageProcessing(LIP) sera présenté(Jourlin, 2016). Ce modèle est fondé sur la loi optique des transmittances, ce qui lui donne de très bonnes propriétés optiques pour traiter ces images. Grâce au modèle LIP, de nouvelles méthodes robustes à ces changements de contrastes seront introduites : à savoir, les métriques fonctionnelles d’Asplund(Noyel and Jourlin, 2020). Deux métriques seront étudiées : (i) la métrique d’Asplund LIP-multiplicative qui est robuste aux changements d’opacité (ou d’absorption) de l’objet modélisés par la loi multiplicative du modèle LIP, et (i) la métrique d’Asplund LIP-additive, qui est robuste aux variations d’intensité lumineuse (ou du temps d’exposition de la caméra) modélisées par la loi additive du modèle LIP. En pratique, ces métriques s’avèrent très utile pour la reconnaissance de forme grâce à des cartes de distances entre un gabarit de référence et une image. Ces cartes de distances d’Asplund seront reliées au corpus bien établi de la morphologie mathématique. Ceci permettra l’introduction d’un nouveau cadre de travail appelé morphologie mathématique logarithmique(Noyel, 2019). Je présenterai également des critères d’homogénéité de région à partir de contrastes logarithmique et qui sont robustes aux variations de contraste et très utiles pour la segmentation(Noyel and Jourlin, 2019). D’autres exemples d’analyses d’images dans de grandes banques de données seront montrés, notamment en imagerie médicale(Noyel et al., 2017) ou en analyse de texture pour les matériaux.
La conjecture de Nivat dit que toute configuration (coloration de la grille Z^2) de faible complexité (qui contient moins de mn motifs rectangulaires de taille mxn) est nécessairement périodique. Autrement dit, il est impossible des créer des configuration non périodique avec trop peu peu de motifs différents. En 2015, Michal Szabados et Jarkko Kari ont présenté une nouvelle manière d'approcher cette conjecture à l'aide d'outils algébriques. En représentant les configurations comme des séries formelles, ils parviennent à exploiter la structure de certains idéaux polynomiaux pour obtenir des résultats se rapprochant beaucoup de la conjecture de Nivat. Dans cet exposé je présenterai leur approche et leurs résultats, ainsi que les travaux que j'ai effectué avec Jarkko Kari dans la continuation de ceux de Michal Szabados. En particulier, je présenterai la preuve (ou au moins les grandes lignes) que la conjecture est vraie dans le cas de certains sous-shifts, ainsi que pour les configurations uniformément récurrentes (c'est à dire celles n'ayant pas de motifs isolés).
The speculative ambition of replacing the old theory of program approximation based on syntactic continuity with the theory of resource consumption based on Taylor expansion and originating from the differential λ-calculus is nowadays at hand. Using this resource sensitive theory, we provide simple proofs of important results in λ-calculus that are usually demonstrated by exploiting Scott’s continuity, Berry’s stability or Kahn and Plotkin’s sequentiality theory. A paradigmatic example is given by the Perpendicular Lines Lemma for the Böhm tree semantics, which is proved here simply by induction, but relying on the main properties of resource approximants: strong normalization, confluence and linearity.
TBA
(Joint work with P. LeFanu Lumsdaine.)
Lawvere theories and (coloured) operads provide particularly nice representations for suitable algebraic theories with a given set of sorts, as monoids in certain categories of collections.
We extend this to dependent type theories: For an inverse category C, we show how suitable “C-sorted type theories” may be viewed (1) as monoids in a category of collections, and (2) as generalised Lawvere theories in the sense of Berger–Melliès–Weber. Moreover, (essentially) every dependent type theory arises in this way.
Inverse categories are known from homotopy theory, where they (or their opposite categories) provide a good notion of a category of ``cells''. Examples are the category of semi-simplices, the category of globes, the category of opetopes, etc.
Hypergroups are objects like groups but with addition taking possibly many values. Likewise, hyperrings and hyperfields are objects similar to rings and fields, but with multivalued addition. Hyperfields provide a convenient tool in axiomatizing the algebraic theory of quadratic forms and in this talk we shall focus on three such applications. Firstly, we shall show how Witt equivalence of fields can be conveniently expressed in the language of hyperfields and will present some recent results on Witt equivalence of function fields over global and local fields. Secondly, we shall show how orderings of higher level can be defined for hyperrings and hyperfields, and, consequently, how they can be used to provide an axiomatic framework to study forms of higher order. Finally, we shall define the category of, so called, presentable fields and define their Witt rings, thus providing yet another machinery to study quadratic forms over fields. The results presented in this talk were obtained jointly with Murray Marshall and Krzysztof Worytkiewicz.
L'exposé se fera en deux temps. Dans la première partie (accessible à tous les membres de l'équipe), je présenterai le lambda-mu-calcul (pur et typé) de Parigot ainsi que ses propriétés et ses défauts. J'introduirai ensuite le lambda-mu-mu'-calcul (version De Groote) et je vous présenterai ses multiples propriétés de normalisation (sans rentrer dans les détails techniques). Dans la deuxième partie, je reprendrai quelques résultats techniques pour présenter les méthodes que nous avons utilisées pour les démontrer.
The μ-calculus with atoms, or nominal μ-calculus, is a temporal logic for reasoning about transition systems that operate on data atoms coming from an infinite domain and comparable only for equality. It is, however, not expressive enough to define some properties that are of interest from the perspective of system verification. To rectify this, we extend the calculus with tests for atom freshness with respect to the global history of transitions. Since global histories can grow arbitrarily large, it is not clear whether model checking for the extended calculus is decidable. We prove that it is, by showing that one can restrict attention only to locally relevant parts of the history.
L'exposé se fera en deux temps. Dans la première partie (accessible à tous les membres de l'équipe), je présenterai le lambda-mu-calcul (pure et typé) de Parigot ainsi que ses propriétés et ses défauts. J'introduirai ensuite le lambda-mu-mu'-calcul (version De Groote) et je vous présenterai ses multiples propriétés de normalisation (sans rentrer dans les détails techniques). Dans la deuxième partie, je reprendrai quelques résultats techniques pour présenter les méthodes que nous avons utilisées pour les démontrer.
TBA