Contenu du sommaire : La théorie constructive des types

Depuis la fin des années soixante, on a vu apparaître plusieurs logiciels destinés à traiter des connaissances mathématiques, en particulier des démonstrations formelles. La réalisation de tels logiciels pose de nouveaux problèmes, en particulier celui de la conception de cadres logiques dans lesquels les mathématiques puissent être formalisées en fait. Cela renouvelle la problématique des fondements des mathématiques, jusque-là davantage concentrée sur la potentialité de la formalisation que sur son actualité. Plusieurs raisons expliquent que les concepteurs de tels logiciels choisissent bien souvent de formaliser les mathématiques en théorie des types, plutôt qu'en théorie des ensembles.

Cet article montre une formalisation complète des grammaires à la Montague dans le cadre de GF (Grammatical Framework), une formalisation qui est en même temps une implémentation déclarative. Cette implémentation comprend toutes les opérations fondamentales du modèles PTQ de Montague : la construction des arbres d'analyse, la linéarisation des arbres en chaînes de caractères, et l'interprétation des arbres comme formules logiques. De plus, un algorithme d'analyse syntaxique est dérivé de toute grammaire représentée dans GF. Comme GF est une théorie constructive des types avec des types dépendants, la technique utilisée pour les grammaires classiques de Montague est généralisée au cas où l'isomorphisme de Curry-Howard est utilisé pour expliquer la référence anaphorique. D'autre part, GF impose une condition de compositionnalité qui est plus forte que celle du PTQ. Ceci empêche la formulation des règles dites "quantifying in" de Montague. Nous arrivons ainsi à des formulations alternatives de ces règles utilisant des combinateurs et des constituants discontinues. Le fragment PTQ est aussi présenté comme exemple de la modification d'une grammaire GF par remplacement de l'anglais par une autre langue de cible, le français. L'article conclut par une discussion sur les rôles complémentaires d'une syntaxe logique et d'une syntaxe linguistique.

Nous donnons une vue d'ensemble du développement historique de la théorie de la preuve et des principales techniques utilisées dans la théorie ordinale de la preuve. Nous soutenons que, dans une forme révisée du programme d'Hilbert, la théorie ordinale de la preuve doit être complétée par une seconde étape, à savoir le développement de théories constructives fortes et équiconsistantes. Comme partie d'un tel programme, nous présentons ensuite l'analyse, en théorie de la preuve, de la théorie des types de Martin-Löf avec un univers microscopique ne contenant que deux types finis. Nous examinons ensuite l'analyse de la théorie des types de Martin-Löf avec type W et un univers clos pour ce type, puis nous étendons la théorie des types par un univers de Mahlo et considérons son analyse en théorie de la preuve. Enfin, nous présentons le concept de définition inductive-récursive, qui étend de façon substantielle la notion de définition inductive. Nous introduisons une formalisation close, qui peut être employée en programmation générique, et expliquons ce que nous savons de sa force ordinale.