Les grammaires catégorielles abstraites (ou λ-grammaires)

Table des matières

1 Introduction
partie I – λ-calcul, typage et jeux
2 λ-calcul et typage
2.1 Syntaxe et opérations du λ-calcul non-typé
2.1.1 Syntaxe du λ-calcul non-typé
2.1.2 Règles de réécriture : α-conversion, β-réduction et η-conversion
2.2 Le λ-calcul simplement typé
2.2.1 Typage à la Curry
2.2.2 Typage à la Church
2.3 Propriétés du λ-calcul simplement typé
2.3.1 Termes η-longs pour un typage
2.3.2 Préservation de typage et β-réduction
2.3.3 Normalisation
2.3.4 Structures de termes et β-expansion
2.4 Logique intuitionniste et λ-calcul simplement typé
2.4.1 Logique minimale et correspondance de Curry-Howard
2.4.2 Unicité de démonstrations en logique minimale
2.5 Conclusion
3 Jeux et λ-calcul simplement typé
3.1 Typage et interaction
3.2 Arènes et typages
3.2.1 Arènes
3.2.2 Occurrences de types et sous-arènes
3.2.3 Curryfication, substitutions de types et morphismes d’arènes
3.3 Stratégies et λ-termes
3.3.1 Justification, innocence et jeux
3.3.2 Stratégies de typage
3.3.3 Préservation de stratégies gagnantes par substitutions de coups
3.3.4 Interprétation de stratégies comme λ-termes
3.3.5 Stratégies recouvrantes et principalité
3.4 Conclusion
3.5 Annexes
3.5.1 Démonstration du Théorème 3.3.4.1
3.5.2 Démonstration du Théorème 3.3.5.1
partie II – Linguistique formelle, λ-calcul et reconnaissance
4 Linguistique formelle et grammaires de λ-termes
4.1 Syntaxe : les langages faiblement sensibles au contexte
4.1.1 La hiérarchie de Chomsky
4.1.2 Les langages faiblement sensibles au contexte
4.1.3 Quelques formalismes MCS
4.2 Sémantique : la compositionnalité
4.2.1 Compositionnalité, logique et λ-calcul
4.2.2 De la syntaxe à la sémantique
4.2.3 Quantificateurs et typage
4.3 Les grammaires catégorielles abstraites
4.3.1 Des grammaires de λ-termes simplement typés
4.3.2 ACGs et formalismes grammaticaux
4.3.3 Une hiérarchie de langages
4.3.4 Traitement de certains phénomènes linguistiques
4.4 Conclusion
5 Programmation logique et analyse grammaticale
5.1 Algorithmes de reconnaissance grammaticale
5.1.1 L’algorithme de Cocke-Younger-Kasami
5.1.2 L’algorithme de Earley
5.2 Reconnaissance grammaticale et déduction logique
5.2.1 Un langage de programmation logique : Datalog
5.2.2 L’exemple des grammaires de clauses définies
5.3 Reconnaissance grammaticale et vérification de typage
5.3.1 Identifier des λ-termes par des typages
5.3.2 Construction de reconnaisseurs Datalog pour les ACGs du second-ordre
5.3.3 Réécriture par ensembles magiques supplémentaires et algorithme de Earley
6 Conclusion