Activités Recherche


Thèmes de recherche :

Les linguistes et les logiciens essaient de voir les grammaires comme des théories logiques. Si l'on compare cette approche avec celle de la linguistique traditionnelle, l'avantage de l'approche logique est que l'on peut y prouver d'importantes propriétés des grammaires telles que l'adéquation, la complétude et la consistence.

La logique linéaire (J-Y. Girard,1987) est une logique sensible aux ressources. Ce trait de base de la logique linéaire, qui de plus est essentiel pour des applications linguistique, est l'absence de règles de contraction et d'affaiblissement. Mais la règle de commutativité non limitée, n'est pas acceptable, elle non plus, d'un point de vue linguistique. Si on ne permet pas la règle de commutativité du tout, on restreint fortement le pouvoir expressif pour engendrer des langages naturels. La logique linéaire non commutative a été étudiée par M. Abrusci et P. Ruet. Des travaux (P. de Groote, par exemple) ont proposé des théories dans un cadre de logique linéaire non commutative permettant des applications linguistiques.
Myriam Quatrini et moi-même avons proposé un lambda calcul (dit mixte) qui d'une part est typé par des formules d'un calcul restreint de celui de M. Abrusci et P. Ruet et d'autre part permet de retrouver autant de preuves (lambda-termes) que d'interprétations sémantiques à la Montague attendues d'une phrase. Ce qui a donné lieu à une publication en 2007.

En 2002, Jean-Yves Girard a proposé la ludique, théorie qui fonde la logique sur des bases purement interactives. L’objet de base est le dessein qu’on peut voir comme une "(para-)preuve normale non typée", dont la structure est en couches alternées positif/négatif, conformément à ce que nous a appris la focalisation. Ces preuves ne portent pas sur des formules, mais sur des occurrences (ce qui reste des formules quand on a oublié le superflu…) et sont donc localisées. L’interaction fondamentale est celle d’une "preuve" et d’une "contre-preuve", qui peut diverger ou converger sur le démon, la para-preuve par excellence (on peut difficilement admettre d’avoir à la fois une preuve d’une formule et de sa négation, d’où le "para"). Cette dualité est le cœur de la ludique. Elle permet de définir des ensembles "réflexifs" (égaux à leurs bi-duaux) de desseins, les comportements, qui correspondent aux formules logiques. La théorie développée par Girard porte essentiellement sur les comportements, leur structure et leurs propriétés de complétude, et propose de dépasser la traditionnelle distinction syntaxe/sémantique en mettant en place un cadre nouveau où des phénomènes informatiques connus, comme le sous-typage, devraient recevoir un traitement logique satisfaisant.
En collaboration avec Myriam Quatrini, nous avons exploré l’interprétation des quantificateurs du premier ordre de la logique linéaire en ludique. Nous avons étudié les propriétés d’uniformité susceptibles de garantir un résultat de complétude et nous avons analysé le cas du second ordre avec Claudia Faggian. ce qui a donné lieu à deux articles parus en 2004 cités ci-dessous. 

De plus, les propriétés de la ludique soulignées ci-dessus (interaction, construction dynamique d'une preuve/dialogue) montre que cette théorie est un bon candidat pour la formalisation des dialogues. Au sein du projet Prélude de l'ANR, Alain Lecomte, Myriam Quatrini, Samuel Tronçon et moi-même avons constitué un groupe de travail dont les résultats ont été exposés dans plusieurs workshop et qui vont donner lieu à une publication.
En effet
Le thème fédérateur de cette équipe est la théorie de la démonstration, et plus particulièrement les liens que cette théorie entretient avec l'informatique. Dans cette étude, la logique linéaire est devenue un instrument essentiel qui a permis l’introduction de nouveaux concepts : réseaux de démonstration et d’interaction, géométrie de l’interaction, logique non commutative. La logique linéaire a également renouvelé les recherches en sémantique dénotationnelle, permettant des rapprochements avec des domaines plus classiques des mathématiques (espaces vectoriels topologiques en particulier). Enfin, la logique linéaire a donné de nouveaux outils dans le domaine de la recherche de preuves (programmation logique), et introduit de nouveaux problèmes de décidabilité et de complexité. Ces dernières années, les phénomènes de focalisation et la notion de formule polarisée ont pris une place centrale, donnant notamment naissance à la ludique, une approche interactive de la logique dans l’esprit des sémantiques de jeux.

Organisation du Séminaire de Logique

J'ai assuré l'organisation du  séminaire de l'équipe "Logique et Programmation" , dirigé par J.Y. Girard, au sein de l'I.M.L. (Institut de Mathématiques de Luminy, UMR 6206 de 1992 à 2007.

Organisation de Colloques
Les principaux thèmes abordés ont été : circuits "digitaux", le Pi-calcul, les machines à environnement, les réseaux de démonstration et d'interaction, la géométrie de l'interaction et l'exécution optimale, aspects logiques de la recherche de démonstrations. Vingt invités de renom international ont exposé leurs derniers résultats.
 
  • Janvier-Mars 2002, session résidentielle au CIRM : "Logique et Interaction".
  • une école thématique : "Logique et Complexité" où les deux thèmes suivant ont été abordés : "Complexité algorithmique" et "Aspects géométrique et physique du calcul".
  • des exposés sur le thème : "Géométrie des preuves et du calcul".
  • des exposés sur le thème : "Logique et Vérification".
  • Durant cette semaine, les applications de la logique , des plus anciennes (grammaires catégorielles) aux plus récentes (applications des réseaux d'interactions de la logique linéaire) ont été abordées.


    Participation à l'encadrement de thèses :
  • Participation, pour la partie théorique (logique), à l'encadrement de la thèse de Christine Campioni, soutenue en 1991 dont le sujet était le typage d'un langage fonctionnel à la Backus, langage conçu au GRTC-CNRS, Marseille. Ce travail a débouché sur un exposé au Colloque de l'ASL 89 (Berlin);  et à un article "Graph typified language used as a functional programming langage" ( n° 11-91, URA 225- Marseillle).
  • Rapporteur de la thèse de P. Sotiropoulos, thèse dirigée par G. G. Granger, professeur au Collège de France (thèse, soutenue le 5 janvier 1996). Cette thèse est une étude épistémologique de différents systèmes logiques pour leurs capacités à formaliser le concept dynamique d'un calcul


  • Publications

    1975 : M-R.. Donnadieu : " Théorème de construction de catégories d’aprés description de Lawvere "
    C.R.A.S., T.280 Fev. 75

    1975 : G. Blanc et M-R.. Donnadieu : " Axiomatisation de la catégorie des catégories "
    Cahiers de topologie et de géométrie différentielle. 1976

    1977 : M-R.. Donnadieu et  C. Rambaud : " Théorème de complétude dans les théories sur graphes orientés"
    C.R.A.S., T.284 Fev. 77

    1978 : M-R.. Donnadieu et C. Rambaud : " Théorie conditionnelle "
    C.R.A.S., T.286 - 1978

    1979 : M-R.. Donnadieu  : " Théories on categories and applications"
    Journal of Symbolic Logic. Vol 44 n°3 1979

    1981 : M-R.. Donnadieu : " Syntax of Conditional Theories"
    Actes of A.S.L. Summer Meeting - Colloque Herbrand -1981- Marseille

    1985 : M-R.. Donnadieu : " Logiques conditionnelles et sémantique des programmes "
    Actes du colloque " Logique et informatique Théorique ", CIRM Marseille

    1986 : M-R.. Donnadieu et C. Rambaud : " Conditional Theories"
    Studia Logica XLV3  pp 237-250 - 1986

    1989 : M-R.. Donnadieu et C. Ciampioni : " Typified Programs and Categories"
    Logic Colloquium Berlin 1989 of A.S.L.

    1991 : M-R.. Donnadieu et C. Ciampioni : " Graph- Typified Language used as a functional programming language"
    Prépublication n°11-91 de l’URA 225 (Marseille)

    2004 : Claudia Faggian, Marie-Renée Fleury-Donnadieu, Myriam Quatrini : "Introduction to uniformity in Ludics". A paraître en 2004 dans "Linear Logic in Computer Science", London
    Mathematical Society, Lectures Notes Series. Edited by T. Ehrhard,  J-Y. Girard, P. Scott.
    Cambridge University Press.

    2004 : Marie-Renée Fleury, Myriam Quatrini : "First order in Ludics".  Juin 2004,  MSCS (Mathematical Structures in Computer Science), Cambrige University Press

    2007 : Marie-Renée Fleury, Myriam Quatrini : "A mixed lambda-calculus".  Décembre 2007,  in Studia Logica (vol 87), Cambrige University Press.

     
     

    Page Principale