Institut de Mathématiques de Luminy

THÈSES 2001-2002


Dates soutenances Noms et titres Équipes Photos
26 novembre 2001 Sylvie RUETTE
Chaos en dynamique topologique, en particulier sur l'intervalle,
mesures d'entropie maximale.
(Chaos in topological dynamics, in particular on the interval, measures of maximal entropy)
DAC  
18 décembre 2001 Alexandra BRUASSE-BAC
La logique linéaire classique du second ordre.
(Second order indexed linear logic)
LDP
15 janvier 2002 Pierre-Paul ROMAGNOLI
Contribution à l'étude d'un principe variationnel local pour l'entropie topologique.
(A contribution to the study of a local Variational Principle for topological entropy)
DAC  
11 mars 2002 Olivier LAURENT
Étude de la polarisation en logique.
(A study of polarization in logic)
LDP  
30 avril 2002 Claudia FAGGIAN
Sur la dynamique de la ludique : une étude de l'interaction.
LDP  
24 mai 2002 Ali ABERKANE
Utilisation des graphes de Rauzy dans la caractérisation
de certaines familles de suites de faible complexité.
DAC  
26 juin 2002 Sylvain LIPPI
Théorie et pratique des réseaux d'interaction.
(Interaction nets)
LDP  


Sylvie RUETTE
(équipe DAC)

Titre : Chaos en dynamique topologique, en particulier sur l'intervalle, mesures d'entropie maximale.

Directeur de thèse : François BLANCHARD

Rapporteurs : Eli Glasner, Bernard Schmitt.

Jury : François Blanchard, Jérôme Buzzi, Albert Fathi, Bernard Host, Bernard Schmitt, Serge Troubetzkoy

Date : 26 novembre 2001

Université d'inscription : Aix-Marseille II

Résumé : Dans cette thèse, on s'intéresse aux propriétés liées au chaos et aux mesures d'entropie maximale (ou mesures maximales) pour certains systèmes, en particulier ceux sur l'intervalle.
Pour un système dynamique (X,T), une entropie non nulle est considérée comme une propriété chaotique. On montre qu'une entropie non nulle implique la présence de couples asymptotiques propres, c'est-à-dire des couples de points distincts (x,y) tels que la distance entre Tnx et Tny tend vers zéro quand n tend vers l'infini. Si T est de plus inversible, de nombreux couples asymptotiques pour T sont des couples de Li-Yorke pour l'inverse de T. Les preuves de ces résultats sont ergodiques.
Une chaîne de Markov topologique est l'ensemble des chemins sur un graphe orienté ; c'est un outil pour l'étude des mesures maximales. Un graphe connexe est transient, récurrent nul ou récurrent positif. On rappelle les liens entre ces classes et la possibilité d'étendre ou de restreindre le graphe sans changer l'entropie, et on montre qu'un graphe transient admet un surgraphe récurrent de même entropie. On sait qu'une chaîne de Markov transitive a une mesure maximale si et seulement si le graphe est récurrent positif. On donne un nouveau critère impliquant la récurrence positive et on montre l'existence de mesures presque maximales fuyant vers l'infini pour un graphe non récurrent positif.
Quand on se restreint aux systèmes sur l'intervalle, les diverses notions de chaos coïncident largement. On présente une synthèse des liens existant entre les différentes propriétés chaotiques.
Pour un système sur l'intervalle, la question d'existence d'une mesure maximale se ramène dans certains cas à l'étude d'une chaîne de Markov. Cela permet de donner une condition assurant l'existence d'une mesure maximale pour les transformations C1. Pour tout entier n, on construit des exemples de transformations de l'intervalle Cn et mélangeantes mais n'admettant aucune mesure maximale.

Mots-clés : systèmes dynamiques topologiques, transformations de l'intervalle, chaînes de Markov topologiques, mesures d'entropie maximale, chaos, entropie, couples asymptotiques.

Title : Chaos in topological dynamics, in particular on the interval, measures of maximal entropy.

Abstract :
In this thesis we are interested in the properties linked to chaos and in the existence of measures of maximal entropy (called maximal measures) for some systems, in particular for systems on the interval.
For a topological dynamical system (X,T), having a positive entropy is considered as a chaotic property. We show that a positive topological entropy implies the existence of proper asymptotic pairs, that is, pairs of distinct points (x,y) such that the distance between Tnx and Tny tends to zero when n goes to infinity. In addition, if T is invertible, many asymptotic pairs for T are Li-Yorke pairs for the inverse of T. The proofs of these results rely entirely on ergodic methods.
A topological Markov chain is the set of infinite paths on an oriented graph; these systems are a tool for the study of maximal measures. A connected oriented graph is either transient or null recurrent or positive recurrent. We recall the links between this classification and the fact that a graph can be extended or contracted without changing its entropy, and we show that any transient graph is included in a recurrent graph of equal entropy. It is known that a Markov chain on a connected graph G has a maximal measure if and only if G is positive recurrent. We give a new condition implying positive recurrence and we show the existence of almost maximal measures escaping to infinity for non positive recurrent graphs.
When one restricts to dynamical systems on the interval, the various notions of chaos mostly coincide. We survey the links between the different chaotic properties.
For an interval map, the question of existence of maximal measures reduces in some cases to the study of a Markov chain. This allows us to give a condition that ensures the existence of a maximal measure for C1 maps. For every integer n, we build an example of a Cn mixing interval map which has no maximal measure.

Keywords :
topological dynamical systems, interval maps, topological Markov chains, measures of maximal entropy, chaos, entropy, asymptotic pairs.

Fichier / File
(1,5 Mo)


Page personnelle (homepage) :
http://iml.univ-mrs.fr:80/~ruette/



Alexandra BRUASSE-BAC
(équipe LDP)

Titre : La logique linéaire classique du second ordre.

Directeurs de thèse : Jean-Yves GIRARD et Thomas EHRHARD

Rapporteurs : Pierre-Louis Curien et Martin Hyland.

Jury : Pierre-Louis Curien (PPS CNRS-Paris VII), Thomas Ehrhard (IML CNRS-Marseille) Jean-Yves Girard (IML CNRS-Marseille), Jean Goubault-Larrecq (ENS-Cachan), Martin Hyland (Université de Cambridge), Jacqueline Vauzeilles (LIPN-Paris XIII).

Date : 18 décembre 2001

Université d'inscription : Aix-Marseille II

Résumé : La logique linéaire indexée, introduite en 1999-2000 par Bucciarelli et Ehrhard est un système logique qui permet d'exprimer des problèmes de définissabilité dans le modèle relationnel de la logique linéaire. Par ailleurs, la sémantique des phases de ce système peut, résultat surprenant, être vue comme une sémantique dénotationnelle non uniforme de la logique linéaire. Les modèles ainsi construits furent, du reste, les premiers modèles dénotationnels non uniformes non triviaux connus de la logique linéaire.
Le but de cette thèse est d'étendre au second ordre la logique linéaire indexée. L'une des motivations de ce travail est que, le traitement sémantique des unités (tant additives que multiplicatives) restant insatisfaisant, il est souhaitable qu'on puisse utiliser des variables propositionnelles.
La première étape de ce travail consiste à définir un modèle relationnel de la logique linéaire du second ordre et donc une notion appropriée de foncteurs stables et d'objets de type variable. Sur ces bases, on peut alors construire un système appelé logique linéaire indexée du second ordre et noté LL2(I). Cette syntaxe fait clairement ressortir l'importance des questions de localisation, ce qui n'est pas sans rappeler les récents travaux de Girard sur la ludique.
Nous nous penchons ensuite sur la définition d'une sémantique des phases pour LL2(I). Tout comme dans la logique linéaire indexée, cette dernière n'est pas complète, mais on peut construire une extension de LL2(I) pour laquelle la complétude est atteinte. A partir de chaque modèle de phases, on obtient un modèle dénotationnel non uniforme de LL2 et on peut, par exemple, définir des espaces cohérents non uniformes pour la logique linéaire du second ordre.

Mots-clés : logique linéaire, second ordre, sémantique dénotationnelle, modèle relationnel, sémantique des phases, logique linéaire indexée.

Title : Second order indexed linear logic.

Abstract :
The indexed linear logic system, introduced in 1999-2000 by Bucciarelli and Ehrhard is a logical system in which it is possible to express definability problems for the relational model of linear logic. Moreover, the phase semantics of this system can, surprisingly, be seen as a non-uniform denotational semantics of linear logic. Besides, the models built in this way have been the first non trivial non-uniform denotational models of linear logic.
In the present thesis, we extend to second order the indexed linear logic system. One of our interests in this work is that, as the status of the multiplicative and additive units in denotational semantics is still not clear, itwas highly desirable to be able working with propositional variables.
In the first part of the present work, we define a relational model of second order linear logic (and thus asuitable notion of stable functors and of objects of variable type). On these basis, we then define a system called second order indexed linear logic (that we denote by LL2(I)). In this syntax, deep localization questions appear to be at stake (in fact, these problems seem to bear many similitudes with the recent work by Girard on ludics).
We then focus on the definition of a phase semantics for LL2(I). As it was already the case in LL(I) this semantics is not complete but one can define an extension of LL2(I) for which completeness is reached. Then we prove that, starting from any phase space model, the phase semantics of LL2(I) actually gives rise to a nonuniform denotational model of LL2. As an exemple, we define a non-uniform coherence spaces semantics for second order linear logic.

Keywords :
linear logic, second order, denotational semantics, relational model, phase semantics, indexed linear logic.

Fichier / File
(1 Mo)


Page personnelle :
http://iml.univ-mrs.fr:80/~bac/



Pierre-Paul ROMAGNOLI
(équipe DAC)

Titre : Contribution à l'étude d'un principe variationnel local pour l'entropie topologique.

Directeurs de thèse : François BLANCHARD et Alejandro MAASS.

Rapporteurs : P. Collet (CPT, Ecole Polytechnique), K. Petersen (U. of N. Carolina).

Jury : F. Blanchard (IML-CNRS), B. Host (U. de Marne-la-Vallée), A. Maass (U. du Chili), A. Martínez (U. du Chili).

Date : 15 janvier 2002 (à Santiago, Chili).

Universités d'inscription : Aix-Marseille II et Université du Chili (cotutelle).

Résumé : Cette thèse porte sur les relations entre dynamique topologique et théorie ergodique.
Pour un système dynamique topologique (X,T) le principe variationnel s'énonce ainsi : h_{top}(X,T) = \sup_\mu h_\mu(X,T), où le sup est pris sur l'ensemble des mesures T-invariantes. Jusqu'à maintenant toutes les preuves connues évitaient la comparaison entre l'entropie topologique d'un recouvrement ouvert et l'entropie mesurée de partitions associées. Nous donnons et étudions ici deux définitions différentes de l'entropie d'un recouvrement pour une mesure, et exploitons l'une d'elles pour obtenir un principe variationnel pour les recouvrements. Un calcul de l'une et l'autre entropie est effectué explicitement dans des cas particuliers.
Dans un autre chapitre, nous déterminons les couples d'entropie d'un système dynamique topologique induit en fonction de ceux du système initial.

Mots-clés : systèmes dynamiques topologiques, théorie ergodique, entropie, principe variationnel, recouvrements, partitions, systèmes induits.

Title : A contribution to the study of a local Variational Principle for topological entropy.

Abstract :
The questions addressed concern the relations between Topological Dynamics and Ergodic Theory.
The Variational Principle states that for a topological dynamical system (X,T) one has h_{top}(X,T) = \sup_\mu h_\mu(X,T), where the supremum is taken over all T-invariant measures. All previous proofs by-passed the question of comparing the topological entropy of an open cover and the measure-theoretic entropy of related partitions. Here two different definitions of the measure-theoretic entropy of a cover are given and explored, and a Variational Principle is obtained for each particular open cover for one of these definitions. Computations of the topological and measure-theoretic entropies of covers are made in particular cases.
In another chapter the set of entropy pairs of an induced topological dynamical system is described according to the entropy pairs of the original system.

Keywords :
topological dynamical systems, ergodic theory, entropy, Variational Principle, covers, partitions, induced systems.

Page personnelle (homepage) : http://www.dim.uchile.cl/Ppp_romagnoli.htm



Olivier LAURENT
(équipe LDP)

Titre : Étude de la polarisation en logique.

Directeurs de thèse : Jean-Yves GIRARD et Laurent REGNIER.

Rapporteurs : Olivier Danvy, Martin Hyland.

Jury : Samson Abramsky, Pierre-Louis Curien, Vincent Danos, Olivier Danvy, Jean-Yves Girard, Martin Hyland, Jean-Louis Krivine, Laurent Regnier.

Date : 11 mars 2002.

Université d'inscription : Aix-Marseille II.

Résumé : Issue des travaux sur la logique linéaire et l'analyse calculatoire de la logique classique, la notion de polarités semble jouer un rôle essentiel dans l'étude actuelle des systèmes logiques. La polarisation est une contrainte qui simplifie les objets tout en conservant une expressivité suffisante d'un point de vue informatique.
L'objet de cette thèse est d'étudier et d'exploiter cette nouvelle structure afin en particulier de mettre à jour les relations entre la logique classique et la logique linéaire (LL). L'introduction des polarités dans LL permet de mieux appréhender ce vaste système et de prolonger le développement de différents outils trop complexes en l'absence de cette contrainte. Nous définissons ainsi, pour la logique linéaire polarisée (LLP), des réseaux de preuve intégrant les connecteurs additifs de manière satisfaisante, une sémantique des jeux polarisés qui réconcilie jeux et dualité, une géométrie de l'interaction parallèle et d'autres sémantiques dénotationnelles basées sur des notions connues (espaces de corrélation, catégories de contrôle).
Il est important de montrer que malgré cette contrainte, LLP reste un système suffisamment expressif. Pour cela nous étudions en détail les traductions des différents systèmes de logique classique déterministe connus (LC, lambda-mu calcul, ...) aussi bien en appel par nom qu'en appel par valeur. De surcroît, les traductions obtenues pour ces systèmes sont plus simples que celles vers LL.
Enfin la souplesse de ces traductions nous permet d'analyser plus finement certaines propriétés de la logique classique tout comme LL permet d'analyser la logique intuitionniste. On peut ainsi étudier un équivalent linéaire des CPS-traductions.

Mots-clés : logique linéaire, logique classique, lambda calcul, polarités, réseaux de preuve, sémantique des jeux, géométrie de l'interaction.

Title : A study of polarization in logic.

Abstract :
Coming from the study of linear logic and from the computational analysis of classical logic, the notion of polarities seems to have a very important place in the recent study of logical systems. The polarization constraint simplifies objects without reducing the computational expressivity too much.
This thesis deals with the study of this new structure given by polarities in order to enlighten the relations between classical logic and linear logic (LL). The introduction of polarities in LL allows to better understand this complex system. In particular, we define for this polarized linear logic (LLP) : a notion of proof-nets dealing with the additive connectives, a polarized game semantics reconciliating games and duality, a parallel geometry of interaction and some other denotational semantics based on already known structures (correlation spaces, control categories).
An important point is that LLP is still expressive enough. We precisely study the translations of the various deterministic systems for classical logic (LC, µ-calculus, ...) both for call-by-name evaluation and for call-by-value. Moreover these translations are simpler than translations of the classical systems into LL.
These simplified translations allow to precisely analyse in LLP some properties of classical logic as LL allows to analyze intuitionistic logic. In particular it is possible to study a linear equivalent of CPS-translations.

Keywords :
linear logic, classical logic, lambda calculus, polarities, proof-nets, game semantics, geometry of interaction.

Fichier / File
(2,4 Mo - version provisoire)


Page personnelle (homepage) :
http://www.pps.jussieu.fr/~laurent/



Claudia FAGGIAN
(équipe LDP)

Titre : Sur la dynamique de la ludique : une étude de l'interaction.

Directeurs de thèse : .

Rapporteurs : .

Jury : .

Date : 30 avril 2002.

Université d'inscription : Aix-Marseille II.

Résumé : I.

Mots-clés : .

Title : On the dynamics of Ludics. A study of interaction.

Abstract :
This thesis is devoted to the study of interaction in ludics. Ludics, recently introudced by Girard ("Locus Solum", Mathematical structures in Computer Science, 11:301-506, 2001), is a new framework born from proof-theory and the analysis of formal proofs as programs, and establishing a middleground between syntax and semantics. It generalizes proofs into untyped tree structures called designs which interact through a normalization procedure. It gives a status to the notion of address (locus). Most importantly ludics is fondamentally interactive: all properties of designs are tested by designs, in a way which is internal to the system. In particular the notion of behaviour which corresponds to that of a type is defined internally.
We introduce in this thesis tools and algorithmic techniques to handle notions of ludics in an effective way and use them to solve in this setting problems on testing of programs (designs) and properties of types (behaviours).
We first develop an operational approach to the interaction of designs and give an abstract machine for normalization. We then deal with the issue of observability, the problem of determining whether a given design can be completely tested by another design. We show given a trace of interaction how to build the designs that produced it. The question of observability is in a second step re-examined in the typed setting of behaviours. We then study the decomposition of designs as (generalized) linear logic formulas. Finally we establish a correspondance between ludics and game semantics, mapping designs to strategies.

Keywords :
.

Fichier / File

 
1 M    799 k

Page personnelle (homepage) :
http://www.math.unipd.it/~claudia/



Ali ABERKANE
(équipe DAC)

Titre : Utilisation des graphes de Rauzy dans la caractérisation de certaines familles de suites de faible complexité.

Directeurs de thèse : Pierre ARNOUX et Julien CASSAIGNE.

Rapporteurs : Jean Berstel, Guy Melançon..

Jury : Jean-Paul Allouche, Pierre Arnoux, Jean Berstel, Valérie Berthé, Srecko Brlek, Julien Cassaigne, Guy Melançon, Gérard Rauzy.

Date : 24 mai 2002.

Université d'inscription : Aix-Marseille II.

Résumé : Pour étudier un mot infini u défini sur un alphabet fini A, on lui associe la fonction Pu, dite fonction de complexité de u, en notant Pu(n) le nombre de facteurs de longueur n du mot u.
Dans ce mémoire, on cherche à caractériser des classes de mots infinis définies par leur fonction de complexité, et notamment des classes de suites de faible complexité (proche de n + 1). Pour cela, on associe aussi au mot u une famille de graphes (n) appelés graphes de Rauzy, où n est le graphe orienté dont les sommets sont les facteurs de longueur n de u et où il existe un arc entre deux sommets si les facteurs associés se succèdent dans le mot infini u. Le premier chapitre contient une présentation générale des graphes de Rauzy et de leur évolution.
Le deuxième chapitre est réservé aux graphes de Rauzy des suites sturmiennes (les suites sturmiennes ont la plus basse complexité parmi les suites non ultimement périodiques). On montre que l'évolution infinie des graphes de Rauzy d'une suite sturmienne est une composition infinie d'évolutions finies de deux types différents.
Dans le troisième chapitre, on étudie des suites de complexité comprise entre n + k et 2n. On montre que, pour tout nombre réel a > 1, on peut construire une suite u telle que .
Dans le quatrième chapitre, on caractérise toutes les suites dont la complexité vérifie lim. Ce sont des suites qui ont, presque, le même comportement que les suites sturmiennes. On montre qu'à partir d'un certain rang, les graphes de Rauzy de ces suites ne subissent que trois types d'évolutions finies différents, avec une condition sur l'enchaînement de ces évolutions qui assure que la complexité reste faible.
Dans le dernier chapitre, on caractérise toutes les suites ayant la même complexité que celle de Thue-Morse (la suite de Thue-Morse est le point fixe de la substitution 0 —> 01 et 1 —> 10). On montre qu'il n'y a que deux orbites possibles de suites récurrentes ayant la complexité de Thue-Morse et on les définit clairement : la première orbite est celle de Thue-Morse et la deuxième orbite est celle de la suite double de Thue-Morse (c'est-à-dire l'image de la suite de Thue-Morse par le morphisme 0 —> 00 et 1 —> 11).

Mots-clés : .

Title : .

Abstract :
.

Keywords :
.

Fichier / File
( Mo - version provisoire)
 
1,2 M   1,3 M


Page personnelle (homepage) :
http://iml.univ-mrs.fr:80/~aberkane/



Sylvain LIPPI
(équipe LDP)

Titre : Théorie et pratique des réseaux d'interaction.

Directeur de thèse : Yves LAFONT.

Rapporteurs : Ian Mackie, Stephano Guerrini.

Jury : Roberto Amadio, Denis Bechet, Alain Colmerauer, Jean-Louis Krivine, Ian Mackie, Stephano Guerrini.

Date : 26 juin 2002.

Université d'inscription : Aix-Marseille II.

Résumé : Les réseaux d'interaction d'Yves Lafont sont un modèle de calcul distribué et un paradigme de programmation inspiré par la logique linéaire de Jean-Yves Girard. Le but de cette thèse est d'exploiter ce "double statut" et d'en faire l'étude d'un point de vue à la fois pratique (langage de programmation) et théorique (modèle de calcul). L'implantation d'un interprète à la fois efficace et suffisamment convivial pour être utilisé par un "programmateur novice" justifie le statut de langage de programmation. De plus, l'algorithme d'affichage utilisé tire profit de la syntaxe graphique des réseaux. La description d'un paradigme de programmation est usuellement accompagnée d'exemples de programmes "classiques" (manipulations sur les listes et les arbres, algorithmes de tri, analyse syntaxique...) qui permettent de comparer le paradigme avec d'autres et de mettre en valeur ses spécificités. En particulier, une des caractéristiques fondamentales des réseaux d'interaction est la gestion explicite de la duplication et de l'effacement ; il n'y a pas de glaneur de cellules dans l'implantation de l'interprète. Une étude détaillée de ces mécanismes permet de prouver que la duplication est intrinsèquement limitée à certains types de réseaux. De plus, nous prouvons que l'effacement sert uniquement à récupérer la mémoire non utilisée : il n'y a pas de contenu calculatoire dans le processus d'effacement. Une des utilisations traditionnelles des réseaux d'interaction est le codage d'un autre modèle de calcul : le lambda-calcul. Nous proposons une nouvelle approche qui consiste à implanter les stratégies de réductions usuelles du lambda-calcul (la réduction de tête, la réduction gauche) par un jeu réduit de règles d'interaction. On obtient ainsi une syntaxe graphique des lambda-termes qui permet de s'affranchir des problèmes de renommage des variables liées et de décomposer la bêta-réduction en plusieurs réductions locales.

Mots-clés : .

Title : Interaction nets.

Abstract :
Interaction nets introduced by Yves Lafont and inspired by Linear Logic of Jean-Yves Girard are a model of distributed computation and a programming paradigm. The aim of this thesis is to take advantage of this double status and to make a study both in a practical (programming language) and a theoretical (model of computation) point of view. The programming language status is justified by the implementation of an efficient and user-friendly interpreter. Moreover, a layout algorithm takes advantage of the graphical syntax. A new programming paradigm is usually introduced with examples of "classical programs" (list and tree processing, sorting algorithms, parsing,...) that highlight its specificities. In particular, one of the fundamental features of interaction nets is explicit memory allocation (i.e explicit duplication and erasing) ; there is no garbage collector in the implementation of the interpreter. A detailed study of those mechanisms reveals that duplication is intrinsically restricted to some classes of nets. Moreover, we prove that erasing can only recover unused memory : there is no computation in the process of erasing. Interaction nets are often used to encode another model of computation : lambda-calculus (left reduction, head reduction) with a reduced set of interaction rules. This way, we obtain a graphical syntax for lambda-terms that eliminates problems of alpha-conversion and give a decomposition of beta-reduction in several local reductions.

Keywords :
.

Fichier / File
( 2,2 Mo )


Page personnelle (homepage) :
http://www.cmi.univ-mrs.fr/~lippi/



Last update : july 1st, 2009, EL.