Proof Nets and Generation for Type-Logical Grammars
Réseaux de preuve et génération pour les grammaires de types logiques
Résumé
The study of the connection between syntax and semantics that type logical grammars set has given priority to parsing-from syntax to semantics. This thesis underlines how generation-from semantics to syntax-can also benefit from this close connection.
It relies on the logical study of these grammatical models and points out the use of linear logic and its proofnets. Around Lambek calculus, an intuitionistic non-commutative fragment of linear logic, we study the behavior of the extensions of this calculus as syntactic models, in particular with pomset calculus. For instance, we show that a fragment of this latter generates the same language class as tree adjoining grammars.
On the other hand, the appropriateness of syntax, with the notion of proof, to Montague's semantics, with lambda-terms, appears in the Curry-Howard correspondence. Using proofnets enables us to show that for Lambek calculus and linear semantic representations, with at least one constant, the generation problem is decidable and that these grammars are intrinsically reversible. We characterize the semantic forms that enable polynomial syntactic realization, so that we can propose a full generation method in this framework.
These results, and their implementation as well, use the underlying proof theory, in particular the graph presentation of proofnets. Thus, we get a uniform framework for parsing and generation. For the objective of taking non-linear semantic terms into account thanks to exponential connectives of linear logic, we give a new syntax and a new correctness criterion for proofnets with exponentials as graphs.
L'étude de la relation entre syntaxe et sémantique qu'établissent les grammaires de types logiques a essentiellement privilégié le sens de l'analyse - syntaxe vers sémantique. Cette thèse souligne le profit que la génération - sémantique vers syntaxe - tire de l'étroitesse de cette relation. Elle s'appuie sur l'étude logique des ces modèles grammaticaux et met en avant l'utilisation de la logique linéaire et de ses réseaux de preuve. Autour du calcul de Lambek, un fragment intuitionniste de la logique linéaire non commutative, nous étudions le comportement des extensions de ce calcul en tant que modèles syntaxiques, notamment avec le calcul ordonné. Nous montrons par exemple qu'un fragment de ce dernier permet d'engendrer la même classe de langage que les grammaires d'arbres adjoints. D'autre part, l'adéquation de la syntaxe, portée par la notion de preuve, à la sémantique de Montague, portée par la notion de lambda-terme, s'illustre dans la correspondance de Curry-Howard. L'utilisation des réseaux de preuve nous permet de montrer que, pour le calcul de Lambek et pour des représentations sémantiques linéaires avec une constante au moins, le problème de génération est décidable et que ces grammaires sont intrinsèquement réversibles. Nous caractérisons les formes sémantiques permettant une réalisation syntaxique polynomiale. Aussi pouvons-nous proposer une méthode complète de génération dans ce cadre. Ces résultats, de même que l'implémentation dont ils ont fait l'objet, exploitent la théorie de la démonstration sous-jacente et en particulier les réseaux de preuve sous forme de graphes. Nous obtenons ainsi un cadre uniforme pour l'analyse et la génération. Pour le conserver, dans l'optique d'une prise en compte sémantique de termes non linéaires grâce aux connecteurs exponentiels de la logique linéaire, nous donnons une nouvelle syntaxe et un nouveau critère de correction pour les réseaux avec exponentiels sous forme de graphes.
Fichier principal
INPL_T_2001_POGODALLA_Sylvain.pdf (4.11 Mo)
Télécharger le fichier
soutenance-these.pdf (275.53 Ko)
Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)