Séminaire Linguistique Informatique



7 Mars 2011
Pierre Bourreau (Bordeaux 1 LaBRI - Signes)

TITRE: Une approche ludique de l'unicité de preuves en logique intuitionniste

L'avènement des grammaires de lambda-termes (de Groote2001, Muskens2001) en linguistique informatique a  permis d'unifier l'analyse et la génération du langage naturel sous une même méthode. Les premiers algorithmes ont été donnés dans Salvati03 pour les termes linéaires, puis dans Kanazawa07, pour les termes quasi-linéaires, une extension des termes linéaires.
Un des théorèmes centraux de la méthode utilisée par Salvati et Kanazawa est l'unicité entre un terme (quasi)-linéaire et son type principal. Cette relation a été démontrée pour les termes linéaires (Babaev-Soloviev1982) et pour les termes quasi-linéaires (Aoto-Ono1999), à travers des résultats qui révèlent l'importance de l'intéraction entre formules positives et formules négatives d'un typage. Cette intéraction est plus particulièrement étudiée dans la sémantique de jeux. Je présenterai donc une étude de cette relation d'unicité à travers une approche ludique du typage de lambda-termes simplement typés. Cette approche amène à une preuve concise du théorème de Aoto et Ono; de plus, je donnerai une nouvelle caractérisation du type principal d'un terme normal simplement typé, ainsi qu'une caractérisation des termes qui sont exactement caractérisés par le Aoto-Ono1991.