|
Ensemble, type et catégorie : l’architecture conceptuelle de la théorie constructive des types| old_uid | 785 |
|---|
| title | Ensemble, type et catégorie : l’architecture conceptuelle de la théorie constructive des types |
|---|
| start_date | 2006/03/06 |
|---|
| schedule | 11h-13h |
|---|
| online | no |
|---|
| summary | La notion de type a été introduite par Russell afin de reconstruire les mathématiques sur une base plus solide que celle offerte par la théorie cantorienne. Mais qu’est-ce qu’un type ? La réponse est loin d’être claire. Le domaine de signifiance d’une fonction propositionnelle, nous dit-on ; soit, mais qu’est-ce à dire ? Dans la théorie ramifiée, on peut considérer que c’est un ensemble. Mais Ryle, non sans raison, nous a aussi invités à voir dans les types des catégories. C’est le passage de l’ensemble à la catégorie qui est responsable de l’imprédicativité de la théorie des types simples.
Je voudrais montrer comment la théorie constructive des types de Martin-Löf permet de clarifier la situation. A cette fin, j’exposerai les deux versions (lower, higher level) sous lesquelles cette théorie a été présentée.
La remarquable vertu pédagogique du niveau inférieur tient à sa grande proximité avec la logique : il suffit en quelque sorte d’enrichir les règles de déduction naturelle par l’introduction d’une notation pour les preuves. En vertu de l’isomorphisme de Curry-Howard-de Bruijn, qu’on appellera encore non pas, comme d’ordinaire, principe de la proposition comme type, mais de la proposition comme ensemble, la logique se transforme immédiatement en une théorie des ensembles. De même, la thèse centrale de l’intuitionnisme devient : la proposition est l’ensemble de ses preuves. A ce premier stade, la théorie constructive des types n’est donc pour l’essentiel qu’une théorie des
ensembles.
La théorie de niveau supérieur exploite, elle, la distinction entre type et ensemble. Le point de départ est à chercher cette fois du côté non de Gentzen, mais de Church, c’est-à-dire directement du côté de la théorie des types. L’originalité de la théorie constructive consiste
alors dans l’introduction de types non seulement fonctionnels, mais dépendants. A ce second niveau, la distinction entre type-ensemble et type-catégorie devient claire. Pour qu’il y ait ensemble, il faut des règles spécifiant comment ses éléments sont formés; la différence entre éléments canoniques et éléments non canoniques joue alors un rôle capital. Rien de tel dans le cas des catégories puisqu’il suffit de saisir ce qu’est un objet d’une catégorie donnée..Je m’arrêterai pour finir sur une conséquence remarquable de cette
situation. Elle conduit en effet à distinguer deux concepts de fonction, selon qu’une fonction est définie par les règles de formation des types ( (x : ?) ?), ou par les règles de formation des ensembles ( (?x : A) B(x)) : selon les cas, le rapport entre abstraction
fonctionnelle et application fonctionnelle change. |
|---|
| responsibles | Barberousse, Tessier Cardon |
|---|
| |
|