Abstract FR:

Notre but, dans cette these, est d'etudier le pouvoir de generation des grammaires categorielles en relation avec les algebres de demonstrations formelles induites par les systemes deductifs (particulierement le calcul de lambek sans produit et divers sous-calculs de celui-ci) par lesquels ces grammaires sont definies. Cette approche nous conduit a une methode systematique (incluant la preuve donnee par m. Pentus de la conjecture de chomsky) de reduction des grammaires categorielles a des grammaires hors-contexte faiblement equivalentes. Techniquement, nous representons les demonstrations formelles considerees dans un fragment d'un lambda-calcul bilateral et nous construisons alors des reductions au hors-contexte sous forme d'algorithmes de normalisation en des lambda-termes typables sur un ensemble fini