Ce manuscrit présente une réflexion sur la terminaison des systèmes de réécriture d'ordres supérieurs. Nous nous concentrons sur une méthode particulière, la terminaison à base de tailles. La terminaison à base de tailles utilise le typage pourdonner une approximation syntaxique à la taille d'un élément du langage. Notre contribution est double: premièrement, nous permettons d'aborder de manière structurée le problème de la correction des approches à base de taille. Pour ce faire, nous montrons qu'elle peut être traitée par une version de la méthode des annotations sémantiques. Cette dernière utilise des annotations sur les termescalculés à partir de la sémantique des sous-termes dans un certain prémodèle équationnel. Nous montrons la correction de notre approche par annotations sémantiques, ainsi que du critère qui permet de traiter le système annoté, et nous construisons un prémodèle pour le système qui correspond intuitivement à lasémantique du système de réécriture. Nous montrons alors que le système annoté passe le critère de terminaison. D'un autre côté nous modifions l'approche classique de la terminaison à base de tailles et montrons que le système modifiépermet une analyse fine du flot de contrôle dans un langage d'ordre supérieur. Ceci nous permet de construire un graphe, dit graphe de dépendance approxime, et nous pouvons montrer qu'un critère syntaxique sur ce graphe suffit à montrer la terminaison de tout terme bien typé / The present manuscript is a reflection on termination of higher-order rewrite systems. We concentrate our efforts on a particular approach, size-based termination. This method uses typing to give a syntactic approximation to the size of an element of the language. Our contribution is twofold: first we give a structured approach to proving the correctness of size-based termination. To do this, we show that it is possible to apply a certain version of semantic labelling. This technique uses annotations on terms computed using the semantics of subterms in a certain equational premodel. We show correctness of our labelling framework and of the criterion that allows us to prove termination of the labelled system, and we build a premodel of the rewrite system that intuitively corresponds to the rewrite system. We show that the system labelled using these semantics passes the termination criterion. Furthermore we show that a modification of the classical size-types approach allows us to perform a fine control-flow analysis in a higher-order language. This allows us to build an approximated dependency graph, and show that if a certain syntactic criterion issatisfied by the graph, then all well-typed terms are terminating

Alors que la complexité des fonctions d'ordre 1 est bien définie et étudiée, il n'existe pas de notion satisfaisante à tout ordre. Une telle théorie existe déjà à l'ordre 2 et permet de définir une classe analogue aux fonctions calculables en temps polynomial usuelles. Cela est tout particulièrement intéressant dans le domaine de l'analyse récursive où l'on peut représenter, entre autres, les nombres et les fonctions réelles par des fonctions d'ordre 1. On peut alors remarquer un lien fort entre calculabilité et continuité, et aussi rapprocher la complexité avec certaines propriétés analytiques, ce que nous illustrons dans le cas des opérateurs réels. Nous prouvons cependant que, du point de vue de la complexité, les fonctions d'ordre 1 ne permettent pas de représenter fidèlement certains espaces mathématiques. Ce résultat appuie tout particulièrement la nécessité d'une théorie de la complexité d'ordre supérieur. Nous développons alors un modèle de calcul basé sur la sémantique des jeux, où l'application de deux fonctions est représentée par la confrontation de deux stratégies dans un jeu. En définissant la taille de telles stratégies, nous pouvons déduire une notion robuste et pertinente de complexité pour ces stratégies et donc pour les fonctions d'ordre supérieur. Nous définissons aussi une classe de fonctions calculables en temps polynomial qui paraît être un bon candidat pour définir une classe de complexité raisonnable à tout ordre / While first order complexity is well defined and studied, higher order lacks a satisfactory notion of complexity. Such a theory already exists at order 2 and provides a complexity class analogue to usual polynomial time computable functions. This is already especially interesting in the domain of computable analysis, where real numbers or real functions for example can be represented by first order functions. In particular, there is a clear link between computability and continuity, and we also illustrate in the case of real operators that complexity can be related to some analytical properties. However, we prove that, from a complexity point of view, some mathematical spaces can not be faithfully represented by order 1 functions and require higher order ones. This result underlines that there is a need to develop a notion of complexity at higher types which will be, in particular but not only, useful to computable analysis. We have developed a computational model for higher type sequential computations based on a game semantics approach, where the application of two functions is represented by the game opposing two strategies. By defining the size of such strategies, we are able to define a robust and meaningful notion of complexity at all types, together with a class of polynomial time computable higher order functionals which seems to be a good candidate for a class of feasible functionals at higher types

Ce manuscrit présente une réflexion sur la terminaison des systèmes de réécriture d'ordres supérieurs. Nous nous concentrons sur une méthode particulière, la terminaison à base de tailles. La terminaison à base de tailles utilise le typage pour donner une approximation syntaxique à la taille d'un élément du langage. Notre contribution est double: premièrement, nous permettons d'aborder de manière structurée le problème de la correction des approches à base de taille. Pour ce faire, nous montrons qu'elle peut être traitée par une version de la méthode des annotations sémantiques. Cette dernière utilise des annotations sur les termes calculés à partir de la sémantique des sous-termes dans un certain prémodèle équationnel. Nous montrons la correction de notre approche par annotations sémantiques, ainsi que du critère qui permet de traiter le système annoté, et nous construisons un prémodèle pour le système qui correspond intuitivement à la sémantique du système de réécriture. Nous montrons alors que le système annoté passe le critère de terminaison. D'un autre coté nous modifions l'approche classique de la terminaison à base de tailles et montrons que le système modifié permet une analyse fine du flot de contrôle dans un langage d'ordre supérieur. Ceci nous permet de construire un graphe, dit graphe de dépendance approximé, et nous pouvons montrer qu'un critère syntaxique sur ce graphe suffit à montrer la terminaison de tout terme bien typé.

L'évaluation précise de la surface équivalente radar (SER) large bande de cibles complexes et de grande dimension est réalisée par des méthodes numériques rigoureuses. Parmi celles-ci, la méthode des différences finies dans le domaine temporel (FDTD) est bien adaptée pour effectuer ce calcul de SER sur une large bande de fréquence et obtenir une signature temporelle de la cible. Le schéma de Yee, schéma FDTD historique pour la simulation de propagation d'ondes électromagnétiques en régime transitoire, souffre de deux points faibles cruciaux: la dispersion numérique imposant une finesse de maillage; et l'approximation de la géométrie curviligne par un maillage cartésien avec des marches d'escalier détériorant la qualité des résultats. Les schémas FDTD d'ordre supérieur en espace ont été investigués pour la réduction de l'effet de la dispersion numérique. Dans cette thèse, le schéma Conservative Modified FDTD(2,4) a été développé dont les performances, en précision et en ressources, sont très intéressantes pour le calcul de SER. Liés au problème de l'approximation de la géométrie curviligne, le traitement des bords de plaques métalliques reste une difficulté non résolue pour les schémas FDTD(2,4) à stencil élargi. Les techniques conformes sont des approches développées pour le schéma de Yee, lesquelles ont été étudiées pour les schémas FDTD(2,4) afin de prendre en compte correctement la géométrie curviligne. Nous proposons une nouvelle approche reposant sur le modèle des fils obliques pour la modélisation des éléments surfaciques métalliques. Des applications SER de cibles montrent que celle-ci est prometteuse. / Rigorous numerical methods are used to compute an accurate wideband radar cross section (RCS) evaluation of large complex targets. Among these, finite differences in time domain method is appropriated for the wideband characteristic and also to obtain a transient responses of the target. The Yee scheme, known historically as an FDTD scheme for Maxwell equations, is hindered by two crucial weak points: numerical dispersion which imposes a high mesh resolution; and staircase approximation of curve geometry which deteriorates results quality. High-order space differential operator for FDTD schemes have been investigated to limit numerical dispersion errors. In this thesis, the Conservative Modified FDTD(2,4) scheme has been developed and its performance has shown very accurate results with reasonable workload for RCS computation. Relating to curve geometry modeling problem, metallic edges modeling is still an unsolved problem for FDTD(2,4) schemes with enlarged stencil. Conformal techniques have been developed for the Yee scheme and has been studied for FDTD(2,4) to accurately model curve geometry. We propose a new approach based on oblique thin wire model to model metallic surfaces. RCS computations of several targets have shown that this method is promising.

L'objectif de cette thèse est de développer une sémantique d'ordre supérieur pour l'information quantique. S'appuyant sur les travaux de master (M.Sc.) de l'auteur, nous étudions un lambda-calcul pour le calcul quantique avec contrôle classique. Le langage comporte deux aspects. Le premier, émanant du théorème dit de « no-cloning » de l'information quantique, est le besoin de distinguer entre les données duplicables et celles non-duplicables. Pour tenir compte de la duplicabilité à l'ordre supérieur, nous utilisons un système de types inspiré par la logique linéaire, logique sensible à la notion de ressource. Le deuxième aspect important est l'effet de bord probabiliste émanant de la mesure, seule opération permettant de récupérer une information classique à partir de données quantiques. Cet effet de bord nous oblige à choisir une stratégie de réduction pour pouvoir être en mesure de définir une sémantique opérationnelle. Nous résolvons le problème de la sémantique dénotationnelle de deux façons. D'abord, en restreignant l'étude du langage au fragment strictement linéaire. Ce faisant, on supprime le besoin de distinguer entre structure duplicable et structure non-duplicable. Il est alors possible de se concentrer sur la description des caractéristiques du calcul quantique. En utilisant la catégorie des fonctions strictement positives (CPM), nous construisons un modèle dénotationnel « fully-abstract », c'est-à-dire caractérisant exactement l'équivalence opérationnelle du fragment strictement linéaire. L'étude du langage au complet est plus compliquée. Pour tenir compte de l'aspect probabiliste du langage, nous utilisons une méthode développée par Moggi et construisons un modèle distinguant la notion de résultat, ou valeur, de la notion de calcul (« computational model »). Pour traiter la distinction entre donnée duplicable et donnée non-duplicable, nous adaptons la notion de catégorie linéaire développée par Bierman, où la notion de duplication est interprétée comme une comonade avec des propriétés particulières. Le modèle issu de ce travail est ce que nous avons appelé une catégorie linéaire pour la duplication. Dans un dernier temps, le langage est restreint en ne considérant que la notion d'effet de bord et la distinction éléments duplicables – éléments non-duplicables pour obtenir un lambda-calcul linéaire générique. Dans ce contexte, nous montrons que la notion de catégorie linéaire de duplication est une interprétation « full and complete » pour le langage.

Cette thèse aborde le problème de l´introduction d´une connaissance a priori sur la géométrie de l´objet à détecter dans le cadre général de la reconnaissance de formes dans une image. L´application choisie pour illustrer ce problème est la détection de réseaux de linéiques dans des images satellitaires et aériennes. Nous nous placons dans le cadre des contours actifs et nous introduisons une nouvelle classe de contours actifs d´ordre supérieur. Cette classe permet la création de nouveaux modèles rendant possible l´incorporation d´informations géométriques fortes définissant plutôt qu´une forme spécifique, une famille générale de formes. Nous étudions un cas particulier d´énergie quadratique qui favorise des structures à plusieurs bras de largeur à peu près constante et connectés entre eux. L´énergie étudiée ainsi que des termes linéaires de longueur et d´aire sont utilisés comme termes d´a priori pour les modèles d´extraction de linéiques que nous proposons. Plusieurs termes d´attache aux données sont proposés dont un terme quadratique permettant de lier la géométrie du contour et les propriétés de l´image. Un modèle d´extraction permettant de gérer les occultations est également présenté. Pour permettre la minimisation de l´énergie, nous développons un cadre méthodologique utilisant les courbes de niveau. Les forces non locales sont calculées sur le contour extrait avant d´être étendues sur tout le domaine considéré. Finalement, afin de résoudre certaines difficultés rencontrées avec les contours actifs standards ainsi que les nouveaux modèles, nous proposons d´utiliser des modèles de champs de phase pour modéliser les régions. Cette méthodologie offre une alternative avantageuse aux techniques classiques et nous définissons des modèles d´extraction de linéiques similaires aux contours actifs d´ordre supérieur dans ce cadre. La pertinence de tous les modèles proposés est illustrée sur des images satellitaires et aériennes réelles.

Les diagrammes de phases d'ordre supérieur à quatre ne peuvent pas être dessinés dans l'espace à deux dimensions d'une représentation, sans transformation numérique des coordonnées.Le mémoire présente une codification originale de la loi des phases conduisant à une classification biunivoque des domaines de variance et à une nouvelle méthode de représentation (dite "séquentielle") des diagrammes de phases isothermes et isobares. Le principe en est: à un point expérimental dans l'espace de N constituants correspondent ENTIER(N/2) points appelés "séquences" dans la représentation bidimensionnelle.Le cheminement par évaporation isotherme et isobare est également décrit en termes de réactions chimiques et de bilan de matière calculé avec la méthode des moindres carrés, non habituelle pour ce type de problème; et les règles de la géométrie appliquées à l'espace de tous les constituants.La méthode a été appliquée aux saumures marines considérées comme des systèmes thermodynamiques quaternaires.

Dans cette thèse, nous nous attachons à étudier des classes de graphes infinis et leurs propriétés, Notamment celles de vérification de modèles, d'accessibilité et de langages reconnus.Nous définissons une notion d'arbres de piles ainsi qu'une notion liée de réécriture suffixe, permettant d'étendre à la fois les automates à piles d'ordre supérieur et la réécriture suffixe d'arbres de manière minimale. Nous définissons également une notion de reconnaissabilité sur les ensembles d'opérations à l'aide d'automates qui induit une notion de reconnaissabilité sur les ensembles d'arbres de piles et une notion de normalisation des ensembles reconnaissables d'opérations analogues à celles existant sur les automates à pile d'ordre supérieur. Nous montrons que les graphes définis par ces systèmes de réécriture suffixe d'arbres de piles possèdent une FO-théorie décidable, en montrant que ces graphes peuvent être obtenu par une interprétation à ensembles finis depuis un graphe de la hiérarchie à piles.Nous nous intéressons également au problème d'algébricité des langages de traces des systèmes à compteurs et au problème lié de la stratifiabilité d'un ensemble semi-linéaire. Nous montrons que dans le cas des polyèdres d'entiers, le problème de stratifiabilité est décidable et possède une complexité coNP-complète. Ce résultat nous permet ensuite de montrer que le problème d'algébricité des traces de systèmes à compteurs plats est décidable et coNP-complet. Nous donnons également une nouvelle preuve de la décidabilité des langages de traces des systèmes d'addition de vecteurs, préalablement étudié par Schwer / In this thesis, we study classes of infinite graphs and their properties,especially the model-checking problem, the accessibility problem and therecognised languages.We define a notion of stack trees, and a related notionof ground rewriting, which is an extension of both higher-order pushdownautomata and ground tree rewriting systems. We also define a notion ofrecognisability on the sets of ground rewriting operations through operationautomata. This notion induces a notion of recognisability over sets of stacktrees and a normalisation of recognisable sets of operations, similar to theknown notions over higher-order pushdown automata. We show that the graphsdefined by these ground stack tree rewriting systems have a decidableFO-theory, by exhibiting a finite set interpretation from a graph defined bya higher-order automaton to a graph defined by a ground stack tree rewritingsystem.We also consider the context-freeness problem for counter systems, andthe related problem of stratifiability of semi-linear sets. We prove thedecidability of the stratifiability problem for integral polyhedra and that itis coNP-complete. We use this result to show that the context-freeness problemfor flat counter systems is as well coNP-complete. Finally, we give a new proofof the decidability of the context-freeness problem for vector additionsystems, previously studied by Schwer

Cette thèse concerne le problème de désocclusion d'images, au moyen des équations aux dérivées partielles. Dans la première partie de la thèse, la désocclusion est modélisée par un problème de Cauchy qui consiste à déterminer une solution d'une équation aux dérivées partielles avec des données aux bords accessibles seulement sur une partie du bord de la partie à recouvrir. Ensuite, on a utilisé des algorithmes de minimisation issus de la théorie des jeux, pour résoudre ce problème de Cauchy. La deuxième partie de la thèse est consacrée au choix des paramètres de régularisation pour des EDP d'ordre deux et d'ordre quatre. L'approche développée consiste à construire une famille de problèmes d'optimisation bien posés où les paramètres sont choisis comme étant une fonction variable en espace. Ceci permet de prendre en compte les différents détails, à différents échelles dans l'image. L'apport de la méthode est de résoudre de façon satisfaisante et objective, le choix du paramètre de régularisation en se basant sur des indicateurs d'erreur et donc le caractère à posteriori de la méthode (i.e. indépendant de la solution exacte, en générale inconnue). En outre, elle fait appel à des techniques classiques d'adaptation de maillage, qui rendent peu coûteuses les calculs numériques. En plus, un des aspects attractif de cette méthode, en traitement d'images est la récupération et la détection de contours et de structures fines. / Image inpainting refers to the process of restoring a damaged image with missing information. Different mathematical approaches were suggested to deal with this problem. In particular, partial differential diffusion equations are extensively used. The underlying idea of PDE-based approaches is to fill-in damaged regions with available information from their surroundings. The first purpose of this Thesis is to treat the case where this information is not available in a part of the boundary of the damaged region. We formulate the inpainting problem as a nonlinear boundary inverse problem for incomplete images. Then, we give a Nash-game formulation of this Cauchy problem and we present different numerical which show the efficiency of the proposed approach as an inpainting method.Typically, inpainting is an ill-posed inverse problem for it most of PDEs approaches are obtained from minimization of regularized energies, in the context of Tikhonov regularization. The second part of the thesis is devoted to the choice of regularization parameters in second-and fourth-order energy-based models with the aim of obtaining as far as possible fine features of the initial image, e.g., (corners, edges, … ) in the inpainted region. We introduce a family of regularized functionals with regularization parameters to be selected locally, adaptively and in a posteriori way allowing to change locally the initial model. We also draw connections between the proposed method and the Mumford-Shah functional. An important feature of the proposed method is that the investigated PDEs are easy to discretize and the overall adaptive approach is easy to implement numerically.

L'objectif de cette thèse est de développer et de valider des approches robustes d'extraction semi-automatique de réseaux routiers en zone urbaine dense à partir d'images satellitaires optiques à très haute résolution (THR). Nos modèles sont fondés sur une modélisation par champs de phase des contours actifs d'ordre supérieur (CAOS). Le probléme est difficile pour deux raisons principales : les images THR sont intrinsèquement complexes, et certaines zones des réseaux peuvent prendre une topologie arbitraire. Pour remédier à la complexité de l'information contenue dans les images THR, nous proposons une modélisation statistique multi-résolution des données ainsi qu'un modèle multi-résolution contraint a priori. Ces derniers permettent l'intégration des résultats de segmentation de résolution brute et de résolution fine. De plus, dans le cadre particulier de la mise à jour de réseaux routiers, nous présentons un modèle de forme a priori spécifique, dérivé d'une ancienne carte numérique issue d'un SIG. Ce terme spécifique a priori équilibre l'effet de la connaissance a priori générique apportée par le modèle de CAOS, qui décrit la forme géométrique générale des réseaux routiers. Cependant, le modèle classique de CAOS souffre d'une limitation importante : la largeur des branches du réseau est contrainte à d'être similaire au maximum du rayon de courbure des branches du réseau, fournissant ainsi un modèle non satisfaisant dans le cas de réseaux aux branches droites et étroites ou aux branches fortement incurvées et larges. Nous résolvons ce problème en proposant deux nouveaux modèles : l'un contenant un terme additionnel, nonlocal, non-linéaire de CAOS, et l'autre contenant un terme additionnel, nonlocal, linéaire de CAOS. Ces deux termes permettent le contrôle séparé de la largeur et de la courbure des branches, et fournissent une meilleure prolongation pour une même largeur. Le terme linéaire a plusieurs avantages : d'une part il se calcule plus efficacement, d'autre part il peut modéliser plusieurs largeurs de branche simultanément. Afin de remédier à la difficulté du choix des paramètres de ces modèles, nous analysons les conditions de stabilité pour une longue barre d'une largeur donnée décrite par ces énergies, et montrons ainsi comment choisir rigoureusement les paramètres des fonctions d'énergie. Des expériences sur des images satellitaires THR et la comparaison avec d'autres modèles démontrent la supériorité de nos modèles.