Thèse numérisée par la Direction des bibliothèques de l'Université de Montréal.

Le but de cette thèse est de construire un fragment de grammaire du français rendant compte de la syntaxe de l'infinitif dans le cadre des grammaires d'arbres polychromes (GAP).<br />La thèse se compose de deux parties. La première concerne l'étude des problèmes que pose l'infinitif. L'infinitif, comme un verbe, a des compléments et le constituant qu'il forme avec ses compléments peut être lui aussi un complément d'un verbe, d'un nom, d'un adjectif. Ce que les grammaires traditionnelles traduisent en parlant d'une double nature : il possède à la fois des propriétés nominales et verbales. D'où une difficulté spécifique pour faire entrer la syntaxe de l'infinitif dans un modèle formel qui puisse se prêter au traitement automatique. Nous appelons constituant infinitif l'unité composée d'un verbe infinitif et de ses compléments. Il est expliqué pourquoi ce terme est préféré à celui de « proposition subordonnée infinitive ».<br />La seconde partie aborde l'analyse syntaxique des constituants infinitifs en GAP et s'organise autour des contextes dans lesquels apparaît l'infinitif (un verbe, un nom, un adjectif). Le choix d'une représentation en GAP permet de mettre à l'épreuve ce formalisme et de montrer l'intérêt qu'il y a de séparer les fonctions syntaxiques des catégories. Ainsi peut-on rendre compte des cas où un constituant d'une catégorie non nominale occupe une position en général occupée par un nom.<br />Ce travail aura permis, en s'intéressant à la question de la syntaxe de l'infinitif, en partant d'une réinterrogation de certaines études en provenance des grammaires traditionnelles, de parvenir à l'enrichissement d'un formalisme élaboré dans la perspective du TAL.

The research work presented in this manuscript is of algorithmic kind: it is mainly composed of polynomial, fixed parameter and approximation algorithms, while hardness results are also mentioned.<br /> <br />This work is about building and comparing labelled trees. These objects find application in different areas, but notoriously in phylogenetics, where they represent evolutionary relationships of organisms or sequences.<br /><br />Most of this work can be considered as investigating solutions to so-called \emph{supertree} problems. Supertrees are large trees built by a dynamic programming approach from smaller trees. For instance, the latter are gene trees from which a comprehensive tree on many living species is to be built, such as the \emph{Tree of Life}. <br /><br />First definitions are introduced, then a part of the manuscript is dedicated to quartet tree building methods. The next part details tree comparison methods, mainly variants of the maximum agreement subtree method. Next follows a part on supertree problems in all generality. <br />The manuscript ends with a report of the research plan for the next few years. <br /><br />Several journal papers illustrating the material described in this manuscript are adjoined in appendix.

L'ingénierie du logiciel doit concilier, d'une part, la modularité requise par les phases de développement et de maintenance et, d'autre part, l'efficacité indispensable dans la mise en oeuvre des applications. Ce dilemme nécessite des méthodes et des techniques de transformation permettant d'accroître l'efficacité des programmes modulaires. La déforestation, qui consiste à éliminer les structures intermédiaires apparaissant lors de la composition des différentes parties d'un programme, a suscité beaucoup d'intérêt, notamment en grammaires attribuées et en programmation fonctionnelle. En dépit de la diversité des formalismes utilisés, cette thèse compare les différentes techniques existantes et s'inspire de leurs atouts pour développer une nouvelle méthode de déforestation plus générale. Tout d'abord, une extension naturelle des grammaires attribuées est introduite pour permettre de représenter une plus large classe de programmes fonctionnels. Les grammaires attribuées dynamiques peuvent se passer de la présence physique d'un arbre pour guider les calculs et les transformations, mais bénéficient des méthodes classiques d'évaluation des grammaires attribuées. Ensuite, les principales méthodes fonctionnelles de déforestation (algorithme de Wadler, règle d'élimination foldr/build, normalisation des folds, fusion d'hylomorphismes) sont étudiées et comparées avec la composition descriptionnelle des grammaires attribuées. Les limitations de chaque méthode sont établies et permettent de déterminer les atouts nécessaires pour ces transformations de programmes. Finalement, une nouvelle méthode de déforestation est proposée. La composition symbolique utilise la puissance du formalisme des grammaires attribuées et incorpore un mécanisme d'évaluation partielle. Cette technique générale peut être appliquée sur des grammaires attribuées ou sur des programmes fonctionnels et permet de déforester des programmes pour lesquelles les méthodes existantes restaient impuissantes.

Cette thèse vise à définir des techniques pour mieux exploiter les connaissances du domaine dans l’objectif de rendre compte de la réalité de systèmes qualifiés de complexes et critiques. La modélisation est une étape indispensable pour effectuer des vérifications et exprimer des propriétés qu’un système doit satisfaire. La modélisation est une représentation simplificatrice, mais réductionniste de la réalité d’un système. Or, un système complexe ne peut se réduire à un modèle. Un modèle doit s’intégrer dans sa théorie observationnelle pour rendre compte des anomalies qu’il peut y contenir. Notre étude montre clairement que le contexte est la première problématique à traiter car principale source de conflits dans le processus de conception d’un système. L’approche retenue dans cette thèse est celle d’intégrer des connaissances du domaine en associant le système à concevoir à des formalismes déclaratifs qualifiés de descriptifs appelés ontologies. Notre attention est portée au formalisme Event-B dont l’approche correct-par-construction appelée raffinement est le principal mécanisme dans ce formalisme qui permet de faire des preuves sur des représentations abstraites de systèmes pour exprimer/vérifier des propriétés de sûreté et d’invariance. Le premier problème traité concerne la représentation et la modélisation des connaissances du contexte en V&V de modèles. Suite à l’étude des sources de conflits, nous avons établi de nouvelles règles pour une extraction de connaissances liées au contexte par raffinement pour la V&V. Une étude des formalismes de représentation et d’interprétation logiques du contexte a permis de définir un nouveau mécanisme pour mieux structurer les modèles Event-B. Une deuxième étude concerne l’apport des connaissances du domaine pour la V&V. Nous définissons une logique pour le formalisme Event-B avec contraintes du domaine fondées sur les logiques de description, établissons des règles à exploiter pour l’intégration de ces connaissances à des fins de V&V. L’évaluation des propositions faites portent sur des études de cas très complexes telles que les systèmes de vote dont des patrons de conception sont aussi développés dans cette thèse. Nous soulevons des problématiques fondamentales sur la complémentarité que peut avoir l’intégration par raffinement des connaissances du domaine à des modèles en exploitant les raisonnements ontologiques, proposons de définir de nouvelles structures pour une extraction partiellement automatisée / This thesis aims at defining techniques to better exploit the knowledge provided from the domain in order to account for the reality of systems described as complex and critical. Modeling is an essential step in performing verifications and expressing properties that a system must satisfy according to the needs and requirements established in the specifications. Modeling is a representation that simplifies the reality of a system. However, a complex system can not be reduced to a model. A model that represents a system must always fit into its observational theory to account for any anomalies that it may contain. Our study clearly shows that the context is the first issue to deal with as the main source of conflict in the design process of a system. The approach adopted in this thesis is that of integrating knowledge of the domain by associating the system to design with declarative formalisms qualified of descriptive ones that we call ontologies. We pay a particular attention to the Event-B formalism, whose correct-by-construction approach called refinement is the main mechanism at the heart of this formalism, which makes it possible to make proofs on abstract representations of systems for expressing and verifying properties of safety and invariance. The first problem treated is the representation and modeling of contextual knowledge in V&V of models. Following to the study looked at the different sources of conflict, we established new definitions and rules for a refinement context knowledge extraction for Event-B V&V. A study of logical formalisms that represent and interpret the context allowed us to define a new mechanism for better structuring Event-B models. A second study concerns the contribution that domain knowledge can make to the V&V of models. We define a logic for the Event-B formalism with domain constraints based on the description logic, and we define rules to integrate domain knowledge for model V&V. The evaluation of the proposals made deal with very complex case studies such as voting systems whose design patterns are also developed in this thesis. We raise fundamental issues about the complementarity that the integration of domain knowledge can bring to Event-B models by refinement using ontological reasoning, and we propose to define a new structures for a partially automated extraction on both levels, namely the V&V

Après les « lois mathématiques » (19ème siècle) et les « modèles mathématiques » (années 1930), les sciences dites « non-exactes » recourent aux simulations numériques (années 1950) puis informatiques (années 1970). À cela, plusieurs raisons : la complexité des objets, l'évolution de la référence que représente la physique avec ses nouveaux formalismes, l'évolution conjointe des techniques de calcul (matérielles et formelles), enfin l'émergence de l'ordinateur et des langages évolués. Or, la modélisation puis la simulation imposèrent des réévaluations du rôle épistémique dévolu aux formalismes depuis la mécanique rationnelle. Pour livrer un pan d'histoire des sciences et des techniques de modélisation, une histoire intégrative et compréhensive est nécessaire. Avec cet angle de vue, sensible aux philosophies de l'époque, aux ontologies des acteurs, comme aux contraintes techniques des formalismes, des instruments et des institutions, on peut voir trois grandes époques dans le destin récent des formalisations des plantes : un déracinement par rapport à la classique supposition d'un fondement dans le réel des lois mathématiques (1922-1937) ; une dispersion des formalismes et une expansion des modèles théoriques et pragmatiques (1938-1967) ; enfin une convergence des formalismes et des axiomatiques autour des infrastructures informatiques pluriformalisées (à partir de 1967). Notre thèse historique et épistémologique est celle-ci : l'ordinateur, après avoir amplifié la dispersion des formalismes, tend à la neutraliser en offrant un nouveau terrain d'expérimentation. Le rejet des représentations fidèles (iconoclasme) des actuelles épistémologies est à rectifier en profondeur.

Depuis 2001 j'ai développé au sein de l'équipe Oasis des travaux de recherche sur la sémantique des applications à base d'objets distribués, appliquant dans le contexte d'un vrai langage, et d'applications de taille réelle, mes recherches précédentes dans le domaine des algèbres de processus. Les différents aspects de ce travail touchent naturellement à la sémantique comportementale, et à la définition de procédures de génération de modèles prenant en compte les différentes facettes de la programmation d'applications distribuées, mais aussi, en amont, à l'analyse statique de code et aux techniques d'abstraction de modèles, et en aval aux outils de vérification de propriétés comportementales. Je montre dans ce mémoire la complexité de ces recherches et la grande variété des techniques requises. Nous avons mis en place une méthode cohérente basée sur un modèle sémantique très flexible, le modèle pNets (parameterized Networks of automata), qui nous offre un bon compromis entre décidabilité, complexité, et utilisabilité. Cette approche nous a permis de définir une sémantique comportementale pour différents aspects des applications à base d'objets ou de composants distribués, mais aussi une notion d'abstraction vers des modèles abstraits finis, permettant d'utiliser des outils de vérification de type " model-checking ". L'ensemble de ces aspects a donné lieu à la réalisation de prototypes, dans la plateforme VerCors, et à des cas d'étude de grande taille.

Parmi les différentes formes de raisonnement étudiées dans le contexte de l'intelligence artificielle, le raisonnement qualitatif permet d'inférer de nouvelles connaissances dans le contexte d'informations imprécises, incomplètes et dépourvues de valeurs numériques. Il permet par exemple de déduire de nouvelles informations à partir d'un ensemble d'informations spatiales telles que « la France est frontalière de l'Allemagne », « la Suisse est à l'est de la France », « l'Italie est en Europe » et « le Luxembourg est proche de la France ». Il peut également être utilisé pour résoudre des abstractions de problèmes quantitatifs difficiles à résoudre, afin par exemple d'accélérer la résolution de ces problèmes.De nombreux formalismes de raisonnement qualitatif ont été proposés dans la littérature. Ils ne se focalisent cependant que sur un seul aspect du monde, alors que la majorité des applications requièrent la prise en compte d'informations hétérogènes. Afin de répondre à ces besoins, plusieurs combinaisons et extensions de formalismes qualitatifs, comme le raisonnement spatio-temporel et le raisonnement multi-échelle, ont récemment été proposées dans la littérature. Le raisonnement spatio-temporel permet de raisonner dans le contexte d'informations spatiales et temporelles interdépendantes. Le raisonnement multi-échelle permet de raisonner avec des informations de précisions différentes, et en particulier de lever des incohérences apparentes.Dans cette thèse, nous nous intéressons au raisonnement multi-échelle, au raisonnement spatio-temporel et aux combinaisons de formalismes qualitatifs.Nous proposons d'étendre le raisonnement qualitatif temporel multi-échelle pour prendre en compte le fait que les intervalles de temps peuvent être perçus comme des instants à certaines échelles de précision, de formaliser intégralement ce raisonnement et d'étudier la décision de la cohérence dans ce contexte ainsi que sa complexité. Nous montrons en particulier que ce formalisme permet de décider la cohérence et que le problème de décision de la cohérence est NP-complet, même dans le cas le plus simple.En outre, nous proposons un cadre général permettant de raisonner sur les séquences temporelles d'informations qualitatives, une forme de description spatio-temporelle. Ce cadre permet notamment de raisonner dans le contexte d'évolutions complexes. Par exemple, les entités considérées peuvent avoir des caractéristiques préservées au cours du temps, évoluer de manière dépendante les unes par rapport aux autres, tout en ayant un comportement potentiellement irréversible et différent selon leur nature. De plus, dans ce cadre, le raisonnement est plus performant computationnellement que les approches de l'état de l'art. Nous étudions en particulier la décision de la cohérence dans le contexte spécifique de régions mobiles de taille constante, et montrons que ce cadre permet effectivement de décider la cohérence.De surcroît, nous proposons un cadre formel unifiant plusieurs formes d'extensions et de combinaisons de formalismes qualitatifs, incluant le raisonnement multi-échelle et les séquences temporelles. Ce cadre permet de raisonner dans le contexte de chacune de ces combinaisons et extensions, mais également d'étudier de manière unifiée la décision de la cohérence et sa complexité. Nous établissons en particulier deux théorèmes complémentaires garantissant que la décision de la cohérence est polynomiale, et nous les utilisons pour prouver que plusieurs fragments de séquences temporelles sont traitables.Nous généralisons également la définition principale de formalisme qualitatif afin d'inclure des formalismes qualitatifs exclus des définitions de la littérature, importants dans le cadre des combinaisons. / In this thesis, we are interested in qualitative multi-scale reasoning, qualitative spatio-temporal reasoning and combinations of qualitative formalisms.We propose to extend the multiscale temporal reasoning to take into account the fact that time intervals can be perceived as instants at certain scales of precision, to fully formalize this reasoning and to study its consistency problem. We show in particular that this formalism decides consistency and that the consistency problem is NP-complete, even in the simplest case.In addition, we propose a general framework for reasoning on temporal sequences of qualitative information, a form of spatio-temporal description. This framework allows for reasoning in the context of complex evolutions. For example, the considered entities may have characteristics preserved over time, evolve in a dependent manner with respect to each other, while having a potentially irreversible and different behavior depending on their nature. Moreover, in this context, reasoning is computationally more efficient than state-of-the-art approaches. In particular, we study the consistency problem in the specific context of constant-size moving regions, and show that this framework actually decides consistency.Furthermore, we propose a formal framework unifying several forms of extensions and combinations of qualitative formalisms, including multi-scale reasoning and temporal sequences. This framework allows one to reason in the context of each of these combinations and extensions, but also to study in a unified way the consistency problem. In particular, we establish two complementary theorems guaranteeing that the consistency problem is polynomial, and we use them to prove that several fragments of temporal sequences are tractable.

Nous étudions l’analyse asymptotique en relativité générale sous deux aspects: le peeling et le scattering (diffusion) conforme. Le peeling est construit pour les champs scalaires linéaire et non-linéaires et pour les champs de Dirac en espace-temps de Kerr (qui est non-stationnaire et à symétrie simplement axiale), généralisant les travaux de L. Mason et J-P. Nicolas (2009, 2012). La méthode des champs de vecteurs (estimations d’énergie géométriques) et la technique de compactification conforme sont développées. Elles nous permettent de formuler les définitions du peeling à tous ordres et d’obtenir les données initiales optimales qui assurent ces comportements. Une théorie de la diffusion conforme pour les équations de champs sans masse de spîn n/2 dans l’espace-temps de Minkowski est construite.En effectuant les compactifications conformes (complète et partielle), l’espace-temps est complété en ajoutant une frontière constituée de deux hypersurfaces isotropes représentant respectivement les points limites passés et futurs des géodésiques de type lumière. Le comportement asymptotique des champs s’obtient en résolvant le problème de Cauchy pour l’équation rééchelonnée et en considérant les traces des solutions sur ces bords. L’inversibilité des opérateurs de trace, qui associent le comportement asymptotique passé ou futur aux données initiales, s’obtient en résolvant le problème de Goursat sur le bord conforme. L’opérateur de diffusion conforme est alors obtenu par composition de l’opérateur de trace futur avec l’inverse de l’opérateur de trace passé. / This work explores two aspects of asymptotic analysis in general relativity: peeling and conformal scattering.On the one hand, the peeling is constructed for linear and nonlinear scalar fields as well as Dirac fields on Kerr spacetime, which is non-stationary and merely axially symmetric. This generalizes the work of L. Mason and J-P. Nicolas (2009, 2012). The vector field method (geometric energy estimates) and the conformal technique are developed. They allow us to formulate the definition of the peeling at all orders and to obtain the optimal space of initial data which guarantees these behaviours. On the other hand, a conformal scattering theory for the spin-n/2 zero rest-mass equations on Minkowski spacetime is constructed. Using the conformal compactifications (full and partial), the spacetime is completed with two null hypersurfaces representing respectively the past and future end points of null geodesics. The asymptotic behaviour of fields is then obtained by solving the Cauchy problem for the rescaled equation and considering the traces of the solutions on these hypersurfaces. The invertibility of the trace operators, that to the initial data associate the future or past asymptotic behaviours, is obtained by solving the Goursat problem on the conformal boundary. The conformal scattering operator is then obtained by composing the future trace operator with the inverse of the past trace operator.