Academic literature on the topic 'Logique du second ordre'

La definissabilite logique sur les structures finies s'est beaucoup developpee ces dernieres annees principalement en raisons des nombreuses connexions qui existent entre ce domaine et la theorie de la complexite algorithmique. Dans cette optique, cette these s'interesse a l'etude du pouvoir d'expression de fragments particulierement significatifs de la logique existentielle du second ordre. On montre tout d'abord que, dans cette logique, toute formule dont la quantification au second ordre porte sur un nombre quelconque de fonctions unaires est logiquement equivalente, sur les structures finies, a une formule ou une seule relation binaire est quantifiee. On raffine ensuite ce resultat de plusieurs manieres. Celui-ci reste vrai si la relation binaire est restreinte a une relation symetrique, un ordre partiel ou meme une relation bipartie. De plus, on montre que l'on peut conserver le nombre de quantificateurs universels dans le prefixe du premier ordre. Ce dernier resultat nous permet de donner une nouvelle caracterisation logique de nlin (temps lineaire non deterministe). En utilisant un theoreme d'ajtai, on donne ensuite un resultat de separation en montrant que la parite du nombre d'aretes d'un graphe n'est pas definissable avec des fonctions unaires au second ordre mais qu'elle l'est avec une seule relation binaire. Enfin, on presente un nouveau theoreme de hierarchie sur les spectres prenant en compte a la fois l'arite des predicats et le nombre de quantificateurs universels

Ce travail de thèse étudie le systeme af2 de j. L. Krivine, qui est une extension du système f de j. Y. Girard. Dans af2, on peut obtenir un programme calculant une fonction, en exprimant les types de données algébriques (booléens, entiers, liste d'entiers)et en écrivant une démonstration de la totalité de la fonction. La classe a des types de données algébriques à la particularité suivante : un terme normal est typable d'un type d. A ssi il est dans l'interprétation de d, pour la sémantique de réalisabilité. Le but était de construire des classes (selon la sémantique adaptée des parties saturées) plus larges de types ayant cette particularité. Ces types nous les avons appelés types complets, puisque la sémantique considérée est complète pour ces types. Nous avons montré que les types a quantificateurs positifs (les quantifications du second ordre n'apparaissent pas en position negative) dans af2 sont des types complets pour la sémantique des parties saturées par -équivalence. Comme on avait besoin dans la démonstration de la conservation de type par -réduction (en effet, le système af2 n'a pas cette propriété) et comme la clôture par expansion faible de tête est une notion plus faible que celle de clôture par -équivalence, on était intéressé à étendre ce résultat a un modèle sature par expansion faible de tête. Ceci nous a amené à construire une classe plus restreinte de types (les bons types positifs), pour lesquels la -réduction est préservée et qui sont complets pour la sémantique des parties saturées par expansion faible de tête. Une deuxième façon pour avoir la préservation de types par -réduction était d'étendre af2 a un système de typage af2s qui a seulement trois règles de typage et parametre par une relation de sous typage. Nous avons montré que af2s n'est autre que af2 auquel on ajoute la préservation de type par -réduction comme règle de typage. Ensuite nous avons montré dans af2s, que les types a quantificateurs positifs sont complets pour la sémantique des parties stables par expansion faible de tête. Dans le dernier chapitre on a donné une définition d'un type de données du système f par des types entree-sortie qui servent à caractériser les domaines et codomaines des fonctions que l'on cherche à programmer. Nous avons montre que les types à quantificateurs positifs sont des types entrée et sortie, que tout type entrée est un type sortie. La réciproque est démontrée dans des cas particuliers, ou on impose des restrictions sur la règle d'élimination des quantificateurs du second ordre. La thèse conclut avec d'autres résultats, en particulier sur les opérateurs de mise en mémoire de j. L. Krivine.

Dans cette thèse on s'intéresse aux formes de "circularité" qui apparaissent dans la théorie de la preuve de la logique du second ordre et de son contrepartie constructive, le Système F.Ces "circularités", ou "cercles vicieux" (Poincaré 1900), sont analysées sur la base d'une distinction entre deux points de vue distincts et irréductible (à cause des théorèmes d'incomplétude): le premier ("le pourquoi", Girard 1989) concerne la cohérence et l'Hauptsatz et demande des méthodes infinitaires (i.e. non élémentaires) de preuve. Le deuxième ("le comment", Girard 1989) concerne le contenu computationnel et combinatoire des preuves, donné par la correspondance entre preuves et programmes, et ne demande que de méthodes élémentaires de preuve.Dans la première partie de la thèse, dévouée au "pourquoi", les arguments philosophiques traditionnels sur les "cercles vicieux" sont confrontés avec la perspective qui émerge de la démonstration de l' Hauptsatz pour la logique de second ordre (obtenue par Girard avec la technique des candidats de réductibilité).Dans la deuxième partie de la thèse, dévouée au "comment", deux approches combinatoires aux cercles vicieux sont proposés: la première se basant sur la théorie du polymorphisme paramétrique, la deuxième sur l'analyse géométrique du typage qui vient de la théorie de l'unification<br>In this dissertation several issues concerning the proof-theory of second order logic and its constructive counterpart (System F, Girard 1971) are addressed. The leitmotiv of the investigations here presented is the apparent "circularity'' or "impredicativity'' of second order proofs. This circularity is reflected in System F by the possibility to type functions applied to themselves, in contrast with Russell's idea that typing should rather forbid such ``vicious circles'' (Poincare 1906). A fundamental methodological distinction between two irreducible (because of incompleteness) approaches in proof theory constitutes the background of this work: on the one hand, "why-proof theory'' ("le pourquoi'', Girard 1989) addresses coherence and the Hauptsatz and requires non-elementary ("infinitary'') techniques; on the other hand, "how-proof theory'' ("le comment'', Girard 1989) addresses the combinatorial and computational content of proofs, given by the correspondence between proofs and programs, and is developed on the basis of elementary ("finitary'') techniques. }In the first part of the thesis, dedicated to "why-proof theory'', the traditional philosophical arguments on "vicious circles'' are confronted with the perspective arising from the proof of the Hauptsatz for second order logic (first obtained in Girard 1971 with the technique of reducibility candidates).In the second part of the thesis, dedicated to "how-proof theory'', two combinatorial approaches to "vicious circles'' are presented, with some technical results: the first one based on the theory of parametric polymorphism, the second one on the geometrical analysis of typing coming from unification theory

De l'etude conjointe, en theorie des modeles finis, du probleme de decision, du pouvoir d'expression et de l'existence d'une loi a-1 pour une meme logique, est apparu des connexions significatives. Ainsi, les resultats de kolaitis et vardi, d'une part, et de pacholski et szwast, d'autre part, ont revele une remarquable equivalence : une classe prefixe avec l'egalite est decidable si et seulement si le fragment existentiel de la logique du second ordre correspondant admet une loi 0-1. Les deux resultats principaux de cette these, qui repondent a des problemes ouverts, consiste a montrer que cette equivalence n'est pas preservee pour la logique du premier ordre a deux variables et pour la classe prefixe sans l'egalite de godel. En effet, ces deux logiques sont decidables et pourtant leur fragment existentiel de la logique du second ordre respectif n'admet pas de loi. Les contre-exemples s'obtiennent a partir de variantes de la propriete de noyau dans les graphes. On montre que celles-ci n'admettent pas de probabilite asymptotique. Ces resultats requiert une bonne maitrise des techniques probabilistes utilisees dans l'etude des graphes aleatoires.

Ce travail a pour propos la synthèse de programmes à partir de preuves constructives dans un cadre logique spécifique: l'arithmétique fonctionnelle du second ordre. Une première étape consiste à proposer une transcription du système de règles initial exprime en déduction naturelle, en un système de séquents plus adapte au traitement automatique du développement de preuves. Pour mécaniser la recherche de preuves, nous définissons un ensemble de tactiques que nous prouvons correctes vis-à-vis du cadre logique de référence de façon à garantir l'adéquation du système de preuves obtenu. Parmi ces tactiques, nous nous concentrons sur les plans de preuve, tactiques particulières capables de développer complètement une preuve ou une classe de preuves. La partie centrale de notre travail consiste en une étude des mécanismes d'induction dont la mise en œuvre est nécessaire pour l'obtention de programmes définis récursivement. Nous montrons des liens entre forme d'induction, spécification du programme, définition des types de données, et réussite de la construction de la preuve. Pour tirer profit de cette étude, nous proposons une procédure de choix d'induction et un plan de preuve générique qui permet d'obtenir des programmes aussi variés que la fonction d'Ackermann, la fonction Fibonacci ou le tri d'une liste par arbre binaire. Ces travaux ont fait l'objet de l'implantation d'un système baptise SKIL (Synthesizing Knowledge in Intuitionistic Logic)

Dans les deux parties qui composent cette thèse, nous utilisons des automates pour résoudre de manière décentralisée certains problèmes de graphes, i. E. Les automates n'ont pas une vision globale du graphe qu'ils parcourent, et chaque automate prend des décisions locales en utilisant l'information présente sur le nœud qu'il occupe. Nous étudions l'impact de cette information sur le nombre d'automates ou la mémoire (états, tableau blanc) nécessaires pour la résolution du problème. Dans la première partie, nous considérons des méthodes de génération d'algorithmes linéaires qui ont été proposées dans la littérature pour résoudre les problèmes exprimés en logique du second ordre monadique sur les graphes de largeur arborescente ou de largeur de clique bornée. Bien que linéaire, les constantes multiplicatives de ces algorithmes générés peuvent cependant être très grandes, rendant ainsi difficile leur utilisation. Nous avons néanmoins implémenté une méthode de génération basée sur les automates, et montré que les algorithmes obtenus pour un certain nombre de propriétés sont utilisables en pratique. Dans la deuxième partie, nous considérons le problème de la capture répartie. Dans un graphe donné, le but est qu'une équipe, utilisant un nombre minimum de chercheurs qui calculent eux-mêmes leur stratégie, capture un fugitif arbitrairement rapide et invisible. Nous étudions notamment le compromis entre le nombre de chercheurs et la quantité d'informations à leur fournir sur l'environnement pour capturer le fugitif<br>In both parts of this thesis, we use automata to solve in a decentralised manner some graphs problems, i. E. The automata do not have a global vision of the graph in which they move, and each automaton makes local decisions using the information available on the node on which it stands. We study the impact of this information on the number of automata or the memory (state, whiteboard) that are necessary for the resolution of the problem. In the first part, we consider some methods of generation of linear algorithms that have been proposed in the literature to solve the problems expressed in monadic second order logic on graphs of bounded treewidth or of bounded cliquewidth. Although the generated algorithms are linear, the multiplicative constant of these algorithms can be very large, making them difficult to use. We have nevertheless implemented a method of generation based on the automata, and we have proved that, for a certain number of properties, the algorithms obtained are usable in practice. In the second part, we consider the problem of distributed graph searching. In a given graph, the goal is that a team, using a minimum number of searchers who calculate their own strategy, capture a fugitive arbitrarily fast and invisible. We study the compromise between the number of searchers and the quantity of information to provide on the environment to capture the fugitive

Les automates distribués sont des machines à états finis qui opèrent sur des graphes orientés finis. Fonctionnant comme des algorithmes distribués synchrones, ils utilisent leur graphe d'entrée comme un réseau dans lequel des processeurs identiques communiquent entre eux pendant un certain nombre (éventuellement infini) de rondes synchrones. Pour la variante locale de ces automates, où le nombre de rondes est borné par une constante, Hella et al. (2012, 2015) ont établi une caractérisation logique par des formules de la logique modale de base. Dans le cadre de cette thèse, nous présentons des caractérisations logiques similaires pour deux classes d'automates distribués plus expressives.La première classe étend les automates locaux avec une condition d'acceptation globale et la capacité d'alterner entre des modes de calcul non-déterministes et parallèles. Nous montrons qu'elle est équivalente à la logique monadique du second ordre sur les graphes.En nous restreignant à des transitions non-déterministes ou déterministes, nous obtenons également deux variantes d'automates strictement plus faibles pour lesquelles le problème du vide est décidable.Notre seconde classe adapte la notion standard d'algorithme asynchrone au cadre des automates distribués non-locaux. Les machines résultantes sont prouvées équivalentes à un petit fragment de la logique de point fixe, et plus précisément, à une variante restreinte du μ-calcul modal qui autorise les plus petits points fixes mais interdit les plus grands points fixes. Profitant du lien avec la logique, nous montrons aussi que la puissance expressive de ces automates asynchrones est indépendante du fait que des messages puissent être perdus ou non.Nous étudions ensuite la décidabilité du problème du vide pour plusieurs classes d'automates non-locaux. Nous montrons que le problème est indécidable en général, en simulant une machine de Turing par un automate distribué qui échange les rôles de l'espace et du temps. En revanche, le problème s'avère décidable en LOGSPACE pour une classe d'automates oublieux, où les nœuds voient les messages reçus de leurs voisins, mais ne se souviennent pas de leur propre état. Finalement, à titre de contribution mineure, nous donnons également de nouvelles preuves de séparation pour plusieurs hiérarchies d'alternance de quantificateurs basées sur la logique modale<br>Distributed automata are finite-state machines that operate on finitedirected graphs. Acting as synchronous distributed algorithms, they use their input graph as a network in which identical processors communicate for a possibly infinite number of synchronous rounds. For the local variant of those automata, where the number of rounds is bounded by a constant, Hella et al. (2012, 2015) have established a logical characterization in terms of basic modal logic. In this thesis, we provide similar logical characterizations for two more expressive classes of distributed automata.The first class extends local automata with a global acceptance condition and the ability to alternate between non deterministic and parallel computations. We show that it is equivalent to monadic second-order logic on graphs. By restricting transitions to be non deterministic or deterministic, we also obtain two strictly weaker variants for which the emptiness problem is decidable.Our second class transfers the standard notion of asynchronous algorithm to the setting of non local distributed automata. There sulting machines are shown to be equivalent to a small fragment of least fixpoint logic, and more specifically, to a restricted variantof the modal μ -calculus that allows least fixpoints but forbids greatest fixpoints. Exploiting the connection with logic, we additionally prove that the expressive power of those asynchronous automata is independent of whether or not messages can be lost.We then investigate the decidability of the emptiness problem forseveral classes of nonlocal automata. We show that the problem isundecidable in general, by simulating a Turing machine with adistributed automaton that exchanges the roles of space and time. Onthe other hand, the problem is found to be decidable in logspace for a class of forgetful automata, where the nodes see the messages received from their neighbors but cannot remember their own state. As a minor contribution, we also give new proofs of the strictness of several set quantifier alternation hierarchies that are based on modallogic

Dans la première partie de ce manuscrit nous étudions les fonctions rationnelles, c'est-à-dire définies par des transducteurs unidirectionnels. Notre objectif est d'étendre aux transductions les nombreuses correspondances logique-algèbre qui ont été établies concernant les langages, notamment le célèbre théorème de Schützenberger-McNaughton-Papert. Dans le cadre des fonctions rationnelles sur les mots finis, nous obtenons une caractérisation à la Myhill-Nerode en termes de congruences d'indice fini. Cette caractérisation nous permet d'obtenir un résultat de transfert, à partir d'équivalences logique-algèbre pour les langages vers des équivalences pour les transductions. En particulier nous montrons comment décider si une fonction rationnelle est définissable en logique du premier ordre. Sur les mots infinis, nous pouvons également décider la définissabilité en logique du premier ordre, mais avec des résultats moins généraux.Dans la seconde partie nous introduisons une logique pour les transductions et nous résolvons le problème de synthèse régulière : étant donnée une formule de la logique, peut-on obtenir un transducteur bidirectionnel déterministe satisfaisant la formule ? Les fonctions réalisées par des transducteurs bidirectionnels déterministes sont caractérisés par plusieurs modèles différents, y compris par les transducteurs MSO, et ont ainsi été nommées transductions régulières. Plus précisément nous fournissons un algorithme qui produit toujours une fonction régulière satisfaisant une spécification donnée en entrée.Nous exposons également un lien intéressant entre les transductions et les mots avec données. Par conséquent nous obtenons une logique expressive pour les mots avec données, pour laquelle le problème de satisfiabilité est décidable<br>In the first part of this manuscript we focus on the study of rational functions, functions defined by one-way transducers.Our goal is to extend to transductions the many logic-algebra correspondences that have been established for languages, such as the celebrated Schützenberger-McNaughton-Papert Theorem. In the case of rational functions over finite words, we obtain a Myhill-Nerode-like characterization in terms of congruences of finite index. This characterization allows us to obtain a transfer result from logic-algebra equivalences for languages to logic-algebra equivalences for transductions. In particular, we show that one can decide if a rational function can be defined in first-order logic.Over infinite words, we obtain weaker results but are still able to decide first-order definability.In the second part we introduce a logic for transductions and solve the regular synthesis problem: given a formula in the logic, can we obtain a two-way deterministic transducer satisfying the formula?More precisely, we give an algorithm that always produces a regular function satisfying a given specification.We also exhibit an interesting link between transductions and words with ordered data. Thus we obtain as a side result an expressive logic for data words with decidable satisfiability