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.