Jeux de typage et analyse de lambda-grammaires non-contextuelles
Langue
fr
Thèses de doctorat
Date de soutenance
2012Spécialité
Informatique
École doctorale
École doctorale de mathématiques et informatique (Talence, Gironde)Résumé
Les grammaires catégorielles abstraites (ou λ-grammaires) sont un formalisme basé sur le λ-calcul simplement typé. Elles peuvent être vues comme des grammaires générant de tels termes, et ont été introduites afin de modéliser ...Lire la suite >
Les grammaires catégorielles abstraites (ou λ-grammaires) sont un formalisme basé sur le λ-calcul simplement typé. Elles peuvent être vues comme des grammaires générant de tels termes, et ont été introduites afin de modéliser l’interface entre la syntaxe et la sémantique du langage naturel, réunissant deux idées fondamentales : la distinction entre tectogrammaire (c.a.d. structure profonde d’un énoncé) et phénogrammaire (c.a.d représentation de la surface d’un énoncé) de la langue, ex- primé par Curry ; et une modélisation algébrique du principe de compositionnalité afin de rendre compte de la sémantique des phrases, due à Montague. Un des avantages principaux de ce formalisme est que l’analyse d’une grammaires catégorielle abstraite permet de résoudre aussi bien le problème de l’analyse de texte, que celui de la génération de texte. Des algorithmes d’analyse efficaces ont été découverts pour les grammaires catégorielles abstraites de termes linéaires et quasi-linéaires, alors que le problème de l’analyse est non-élémentaire dans sa forme la plus générale. Nous proposons d’étudier des classes de termes pour lesquels l’analyse grammaticale reste solvable en temps polynomial. Ces résultats s’appuient principalement sur deux théorèmes de typage : le théorème de cohérence, spécifiant qu’un λ-terme donné est l’unique habitant d’un certain typage ; et le théorème d’expansion du sujet, spécifiant que deux termes β-équivalents habitent les même typages. Afin de mener cette étude à bien, nous utiliserons une représentation abstraite des notions de λ-termes et de typages, sous forme de jeux. En particulier, nous nous appuierons grandement sur cette notion afin de démontrer le théorème de cohérence pour de nouvelles familles de λ-termes et de typages. Grâce à ces résultats, nous montrerons qu’il est possible de construire de manière directe, un reconnaisseur dans le langage Datalog, pour des grammaires catégorielles abstraites de -termes quasi-affines.< Réduire
Résumé en anglais
Abstract categorial grammars (or, equivalently, lambda-grammars) is formalism based on the simply-typed lambda-calculus. These grammars can be described as grammars of such terms and were introduced in order to bring a ...Lire la suite >
Abstract categorial grammars (or, equivalently, lambda-grammars) is formalism based on the simply-typed lambda-calculus. These grammars can be described as grammars of such terms and were introduced in order to bring a model of the syntax-semantics interface in natural language, based on two main ideas: the distinction between the tectogrammatical (i.e. the deep structure of an utterance) and phenogrammatical (i.e. the interpretation of this structure) levels in natural languages, which was expressed by Curry; and an algebraic modeling of the principle of compositionality in order to give account of the semantics of a sentence. an idea formalized by Montague. One of the main advantages of abstract categorial grammars is that both the problems of natural language parsing and generation can be tackled under the same problem: parsing abstract categorial grammars. Efficient algorithms were discovered for abstract categorial grammars of linear and almost linear lambda-terms, while it is known the recognition problem is decidable but non-elementary in general. This work focuses on the study of classes of terms for which parsing can still be solved in polynomial time. The results we give are mainly based on two theorems: the coherence theorem which specifies that a given lambda-term in the desired class must be the unique inhabitant of one of its typing; and the subject expansion theorem, which states that two beta-equivalent terms of the desired class must inhabit the same typings. In order to lead the study, we use an alternative representation of both simply-typed lambda-terms and their typings as games. In particular, we will use this representation in order to prove the coherence theorems for new classes of lambda-terms. Thanks to these results, we will show it is possible to build in a direct way, recognizers for grammars of almost affine lambda-terms as Datalog programs.< Réduire
Mots clés
Lambda-calcul
Linguistique formelle
Analyse et génération de langage
Datalog
Sémantique des jeux
Mots clés en anglais
Lambda calculus
Formal linguistic
Natural language parsing and generation
Datalog
Game semantics
Origine
Importé de STAR