Cours "Structures Mathématiques du Langage" (DEC-B36)
Master-2 Paris 8 / DEC-ENS, 2012-2013, lundi 14h - 16h30 (2eme semestre) salle Langevin, à partir du 4 Février

Présentation:
Cette année, le séminaire "Structures Mathématiques du Langage" portera essentiellement sur "Types, preuves et dialogue". Cette thématique s'enracine principalement dans les travaux qui, au XXème siècle, ont conduit à une réflexion sur les mathématiques constructives et sur la notion de preuve. Il existe deux voies d'accès à la logique : via la notion de valeur de vérité ou via la déduction naturelle. Cette deuxième voie a été explorée par des logiciens comme Gentzen (années trente) et Prawitz. Elle permet de définir facilement une logique particulière, la logique "intuitionniste", ainsi nommée car elle est au soubassement de l'intuitionnisme, une philosophie des mathématiques qui a été développée par J. Brouwer dans les années trente, censée répondre aux questions difficiles que rencontraient les mathématiques à la suite de la découverte des paradoxes liés à la manipulation de l'infini.
En philosophie, l'intuitionnisme a été repris et défendu par le philosophe anglais Michael Dummett. Il conduit à une conception profonde selon laquelle le sens d'une formule réside dans l'ensemble de ses preuves (Hypothèse dite "de Brouwer-Heyting-Kolmogorov").
A une époque plus récente (années soixante), on a pu établir une correspondance fondamentale entre les preuves et les programmes (au sens informatique du terme). Un programme informatique est un objet typé: si par exemple, on a un programme qui calcule la somme de deux entiers, on dit que le type de ce programme est N x N --> N (il n'accepte que des entiers et ne donne en sortie qu'un entier). Il se trouve que les types correspondent aux programmes comme les formules correspondent aux preuves, d'où l'association entre types et formules. On notera qu'en sémantique formelle, il en va de même pour les parties du discours, ainsi un verbe transitif est-il de type <e, <e, t>>, un nom propre de type e, un nom commun de type <e, t>, un GN quantifié de type <<e, t>, t> etc. Exporter au langage naturel la correspondance entre preuves et programmes revient donc à associer à toute déduction qu'un syntagme donné est d'un type donné, une sorte de programme (un lambda-terme) qui fait figure de représentation sémantique.
Dans les années soixante, J. Lambek a proposé un système analogue à la logique propositionnelle intuitionniste pour résoudre les questions d'analyse syntaxique. Ce système se distingue de la logique propositionnelle par le fait qu'il est sensible au nombre de fois où on utilise une formule dans une preuve, ainsi qu'à l'ordre dans lequel ces formules sont fournies. A cause de la correspondance entre preuves et programmes, ce calcul (appelé "calcul de Lambek") permet d'associer à toute dérivation syntaxique (= preuve qu'une phrase est bien formée), en guise de programme, une "représentation sémantique" dans le style de la sémantique de Montague.
Ce faisant, Lambek a été un précurseur d'un autre genre de logique, appelée "logique linéaire", inventé dans les années quatre-vingt par le logicien français Jean-Yves Girard. Cette logique a servi de base pour la construction de grammaires dites "de types logiques", notamment au travers des travaux de Glyn Morrill.
Les grammaires que l'on obtient ont beaucoup de points communs avec les grammaires minimalistes, un formalisme grammatical développé par Ed Stabler sur la base des principes minimalistes de N. Chomsky.
Parallèlement, les travaux dans la lignée de l'intuitionnisme ont conduit à des formalismes beaucoup plus riches et expressifs que la logique intuitionniste, comme la Théorie des Types de P. Martin-Löf (années quatre-vingt). Cette théorie a été utilisée par A. Ranta, dans les années quatre-vingt-dix, afin de rendre compte de phénomènes sémantiques en linguistique comme la question des donkey-sentences (phrases de Geach, comme "tout fermier qui possède un âne le bat", où la représentation en logique du premier ordre semble ne pas respecter le principe de compositionnalité). On retient comme idée de base que les connecteurs logiques manipulent des ensembles de preuves et que les quantificateurs portent à la fois sur des preuves et des éléments d'ensembles.
De nos jours, la Théorie des Types ("avec Records") est utilisée par des sémanticiens comme R. Cooper et J. Ginzburg pour formaliser notamment le dialogue.

Ce séminaire a pour but de parcourir ces notions en proposant une vision de la sémantique des langues naturelles (et de leur pragmatique) qui se distingue de la sémantique formelle habituelle en ce qu'elle est moins fondée sur la notion de condition de vérité.

Cours:

- sur Montague
- sur Lambek
- sur les catégories (revu et complété le 10 avril)
- sur les continuations (revu et complété le 10 avril)
- sur les types (nouveau par rapport à la version précédente)

(1er mars) : Une digression: les grammaires de types et la sémantique distributionnelle:

Une simplification, par rapport au calcul de Lambek (cf. ci-dessus) conduit aux grammaires de prégroupes. Les prégroupes constituent une catégorie fermée compacte... de même que les espaces vectoriels! D'où l'idée de relier les deux types de structures. Cela donne un calcul syntaxique qui s'interprète, au niveau sémantique, en termes de combinaisons de vecteurs et de matrices. Si on attribue à chaque mot un vecteur qui représente sa distribution dans un ensemble de contextes, et à chaque type de base, un espace vectoriel qui contient les vecteurs des mots de ce type, on obtient une sémantique distributionnelle (c'est-à-dire basée sur les distributions statistiques des mots). On lira:

1- un article de Lambek sur les prégroupes (2005)
2- un article de Clark, Coecke et Sadrzadeh : Towards a Compositional Distributional Model of Meaning (2008)
3- un article de Coecke, Grefenstette et Sadrzadeh plus complet : Lambek vs Lambek: Functorial Vector Space Semantics and String Diagrams for Lambek Calculus (2011)

18 mars : nous introduisons la théorie des catégories, afin de poursuivre vers la symétrisation du calcul de Lambek (logique "bilinéaire" ou logique linéaire non commutative) et les prégroupes.

- quelques exercices sur les catégories et le calcul de Lambek symétrique

25 mars : continuation sur les catégories et le calcul de Lambek symétrique, les prégroupes. Exposé sur "Prégroupes et sémantique distributionnelle".

8 avril : calcul de Lambek symétrique et sémantique des continuations. Continuations et monades.

article à lire pour le 15 avril: Chung-chieh Shan, Monads for Natural Language Semantics (Proceedings of ESSLLI Student session, 2001).

Rosetta : un article général sur les liens entre physique, topologie, théorie des catégories et logique (et pourquoi pas langage?) par John Baez

2 articles fondamentaux sur les continuations et la dualité call-by-name vs call-by-value, Wadler et Curien-Herbelin

22 avril (dernière séance) : Grammaires minimalistes et grammaires catégorielles multi-modales, voir l'article de Whilelmijn Vermaat (1999). Théorie des types et résolution du problème des "donkey-anaphora", voir le cours sur les types.

Lectures :

Michael Dummett, Eléments d'intuitionnisme, 1977 (qu'on peut trouver dans Philosophie de la logique, D. Bonnay et M. Cozic eds. ed. Vrin, 2009)
J-Y. Girard, Proofs and Types, Cambridge Tracts in Theoretical Computer Science, Cambridge, 1989,
W. A. Howard, The formulae-as-types notion of construction
D. Prawitz, Natural Deduction, a proof-theoretical study, Dover Pub. 1965,
J. Lambek, The Mathematics of Sentence Structure, 1958
R. Montague, The Proper Treatment of Quantification in Ordinary English, 1973,
A. Ranta, Type-Theoretical Grammar, Oxford University Press, 1994
H. Geuvers, Introduction to Type Theory
R. Cooper, Type Theory and Semantics in Flux, in Philosophy of Linguistics, R. Kempson, T. Fernando and N. Asher eds, North-Holland, 2012
G. Morrill, Logical Grammar, in Philosophy of Linguistics, R. Kempson, T. Fernando and N. Asher eds, North-Holland, 2012
H. Lasnik and J. Uriagereka, Structure, in Philosophy of Linguistics, R. Kempson, T. Fernando and N. Asher eds, North-Holland, 2012
E. Stabler, Derivational Minimalism, Logical Aspects of Computational Linguistics, Springer, LNAI n°1328, 1997
J. Ginzburg, The Interactive Stance, Oxford University Press, 2011
R. Cooper & J. Ginzburg, Negation in Dialogue, SEMDIAL 2011,
A. Lecomte, Meaning, Logic and Ludics, Imperial College press, 2011

Evaluation :
L'évaluation du séminaire se fera sous la forme d'exposés.