 |
 |
 |
 |
 |
|
|
|
|
|
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.
Abstract
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.
