Théorie des types intuitionniste - Intuitionistic type theory

La théorie des types intuitionniste (également connue sous le nom de théorie des types constructive , ou théorie des types de Martin-Löf ) est une théorie des types et un fondement alternatif des mathématiques . La théorie des types intuitionniste a été créée par Per Martin-Löf , un mathématicien et philosophe suédois , qui l'a publiée pour la première fois en 1972. Il existe plusieurs versions de la théorie des types : Martin-Löf a proposé des variantes intensionnelles et extensionnelles de la théorie et des premières versions imprédicatives , révélée inconsistante par le paradoxe de Girard , a cédé la place à des versions prédicatives . Cependant, toutes les versions conservent la conception de base de la logique constructive en utilisant des types dépendants.

Conception

Martin-Löf a conçu la théorie des types sur les principes du constructivisme mathématique . Le constructivisme exige que toute preuve d'existence contienne un « témoin ». Ainsi, toute preuve de "il existe un nombre premier supérieur à 1000" doit identifier un nombre spécifique qui est à la fois premier et supérieur à 1000. La théorie des types intuitionniste a atteint cet objectif de conception en intériorisant l' interprétation BHK . Une conséquence intéressante est que les preuves deviennent des objets mathématiques qui peuvent être examinés, comparés et manipulés.

Les constructeurs de types de la théorie des types intuitionniste ont été construits pour suivre une correspondance un à un avec les connecteurs logiques. Par exemple, le connecteur logique appelé implication ( ) correspond au type d'une fonction ( ). Cette correspondance est appelée l' isomorphisme de Curry-Howard . Les théories des types précédentes avaient également suivi cet isomorphisme, mais Martin-Löf a été le premier à l'étendre à la logique des prédicats en introduisant des types dépendants .

Théorie des types

La théorie des types intuitionniste a 3 types finis, qui sont ensuite composés à l'aide de 5 constructeurs de types différents. Contrairement aux théories des ensembles, les théories des types ne reposent pas sur une logique comme celle de Frege . Ainsi, chaque caractéristique de la théorie des types remplit une double fonction en tant que caractéristique à la fois des mathématiques et de la logique.

Si vous n'êtes pas familier avec la théorie des types et que vous connaissez la théorie des ensembles, voici un bref résumé : Les types contiennent des termes tout comme les ensembles contiennent des éléments. Les termes appartiennent à un et un seul type. Des termes comme et calculer (« réduire ») jusqu'à des termes canoniques comme 4. Pour en savoir plus, consultez l'article sur la théorie des types .

0 type, 1 type et 2 types

Il existe 3 types finis: Le 0 Type contient 0 termes. Le 1 type contient 1 terme canonique. Et le type 2 contient 2 termes canoniques.

Comme le type 0 contient 0 termes, il est également appelé type vide . Il est utilisé pour représenter tout ce qui ne peut pas exister. Il est également écrit et représente tout ce qui est indémontrable. (C'est-à-dire qu'une preuve de cela ne peut pas exister.) En conséquence, la négation est définie comme une fonction de celle-ci : .

De même, le type 1 contient 1 terme canonique et représente l'existence. On l'appelle aussi le type d'unité . Il représente souvent des propositions qui peuvent être prouvées et est donc parfois écrit .

Enfin, le 2 de type 2 contient des termes canoniques. Il représente un choix définitif entre deux valeurs. Il est utilisé pour les valeurs booléennes mais pas pour les propositions. Les propositions sont considérées comme du type 1 et il peut être prouvé qu'elles n'ont jamais de preuve (le type 0 ), ou peuvent ne pas être prouvées de toute façon. (La loi du milieu exclu ne s'applique pas aux propositions de la théorie des types intuitionniste.)

type constructeur

Les types contiennent des paires ordonnées. Comme pour les types de paires ordonnées typiques (ou 2-uplets), un type peut décrire le produit cartésien , , de deux autres types, et . Logiquement, une telle paire ordonnée contiendrait une preuve de et une preuve de , donc on peut voir un tel type écrit comme .

Les types sont plus puissants que les types de paires ordonnées typiques en raison du typage dépendant . Dans le couple ordonné, le type du deuxième terme peut dépendre de la valeur du premier terme. Par exemple, le premier terme de la paire peut être un nombre naturel et le type du second terme peut être un vecteur de longueur égale au premier terme. Un tel type s'écrirait :

En utilisant la terminologie de la théorie des ensembles, cela est similaire à des unions disjointes indexées d'ensembles. Dans le cas de couples ordonnés usuels, le type du second terme ne dépend pas de la valeur du premier terme. Ainsi le type décrivant le produit cartésien s'écrit :

Il est important de noter ici que la valeur du premier terme, , ne dépend pas du type du second terme, .

De toute évidence, les types Σ peuvent être utilisés pour construire des tuples à typage dépendant plus longs utilisés en mathématiques et les enregistrements ou structures utilisés dans la plupart des langages de programmation. Un exemple de 3-uplet à typage dépendant est constitué de deux entiers et d'une preuve que le premier entier est plus petit que le deuxième entier, décrit par le type :

Le typage dépendant permet aux types de jouer le rôle de quantificateur existentiel . La déclaration "il existe un de type , tel qui est prouvé" devient le type de paires ordonnées où le premier élément est la valeur de type et le deuxième élément est une preuve de . Notez que le type du deuxième élément (preuves de ) dépend de la valeur de la première partie de la paire ordonnée ( ). Son type serait :

type constructeur

Les types contiennent des fonctions. Comme pour les types de fonction typiques, ils se composent d'un type d'entrée et d'un type de sortie. Ils sont cependant plus puissants que les types de fonction typiques, dans la mesure où le type de retour peut dépendre de la valeur d'entrée. Les fonctions de la théorie des types sont différentes de la théorie des ensembles. En théorie des ensembles, vous recherchez la valeur de l'argument dans un ensemble de paires ordonnées. Dans la théorie des types, l'argument est remplacé par un terme, puis le calcul ("réduction") est appliqué au terme.

Par exemple, le type d'une fonction qui, étant donné un nombre naturel , renvoie un vecteur contenant des nombres réels s'écrit :

Lorsque le type de sortie ne dépend pas de la valeur d'entrée, le type de fonction est souvent simplement écrit avec un . Ainsi, est le type de fonctions des nombres naturels aux nombres réels. De tels Π-types correspondent à une implication logique. La proposition logique correspond au type , contenant des fonctions qui prennent des preuves-de-A et renvoient des preuves-de-B. Ce type pourrait être écrit de manière plus cohérente comme :

Les types sont également utilisés en logique pour la quantification universelle . L'énoncé "pour chaque type de , est prouvé" devient une fonction de type à preuves de . Ainsi, étant donné la valeur de la fonction génère une preuve valable pour cette valeur. Le genre serait

= type constructeur

=-types sont créés à partir de deux termes. Étant donné deux termes comme et , vous pouvez créer un nouveau type . Les termes de ce nouveau type représentent des preuves que la paire se réduit au même terme canonique. Ainsi, puisque les deux et calculent le terme canonique , il y aura un terme du type . En théorie intuitionniste des types, il existe une seule façon de faire des termes de =-types et c'est par réflexivité :

Il est possible de créer des types =, par exemple lorsque les termes ne se réduisent pas au même terme canonique, mais vous ne pourrez pas créer de termes de ce nouveau type. En fait, si vous pouviez créer un terme de , vous pourriez créer un terme de . Mettre cela dans une fonction générerait une fonction de type . Puisque c'est ainsi que la théorie des types intuitionniste définit la négation, vous auriez ou, finalement, .

L'égalité des preuves est un domaine de recherche active en théorie de la preuve et a conduit au développement de la théorie des types d'homotopie et d'autres théories des types.

Types inductifs

Les types inductifs permettent la création de types complexes et autoréférentiels. Par exemple, une liste chaînée de nombres naturels est soit une liste vide, soit une paire d'un nombre naturel et d'une autre liste chaînée. Les types inductifs peuvent être utilisés pour définir des structures mathématiques illimitées telles que des arbres, des graphiques, etc. En fait, le type des nombres naturels peut être défini comme un type inductif, étant ou successeur d'un autre nombre naturel.

Les types inductifs définissent de nouvelles constantes, telles que zéro et la fonction successeur . Comme n'a pas de définition et ne peut pas être évalué par substitution, des termes comme et deviennent les termes canoniques des nombres naturels.

Les preuves sur les types inductifs sont rendues possibles par induction . Chaque nouveau type inductif est livré avec sa propre règle inductive. Pour prouver un prédicat pour chaque nombre naturel, vous utilisez la règle suivante :

Les types inductifs dans la théorie des types intuitionniste sont définis en termes de types W, le type d' arbres bien fondés . Des travaux ultérieurs en théorie des types ont généré des types coinductifs, une induction-récursivité et une induction-induction pour travailler sur des types avec des types d'autoréférentialité plus obscurs. Les types inductifs supérieurs permettent de définir l'égalité entre les termes.

Types d'univers

Les types d'univers permettent d'écrire des preuves sur tous les types créés avec les autres constructeurs de types. Chaque terme du type d'univers peut être mappé à un type créé avec n'importe quelle combinaison de et le constructeur de type inductif. Cependant, pour éviter les paradoxes, aucun terme ne correspond à .

Pour écrire des preuves sur tous les "petits types" et , vous devez utiliser , qui contient un terme pour , mais pas pour lui-même . De même, pour . Il existe une hiérarchie prédicative d'univers, donc pour quantifier une preuve sur n'importe quel univers constant fixe , vous pouvez utiliser .

Les types d'univers sont une caractéristique délicate des théories des types. La théorie des types originale de Martin-Löf a dû être modifiée pour tenir compte du paradoxe de Girard . Des recherches ultérieures ont porté sur des sujets tels que les "super univers", les "univers Mahlo" et les univers imprédicatifs.

Jugements

La définition formelle de la théorie des types intuitionniste est écrite à l'aide de jugements. Par exemple, dans l'instruction "si est un type et est un type alors est un type" il y a des jugements de "est un type", "et" et "si... alors...". L'expression n'est pas un jugement ; c'est le type qui est défini.

Ce deuxième niveau de la théorie des types peut prêter à confusion, en particulier lorsqu'il s'agit d'égalité. Il y a un jugement d'égalité à terme, qui pourrait dire . C'est un énoncé que deux termes se réduisent au même terme canonique. Il existe également un jugement d'égalité de type, disons que , ce qui signifie que chaque élément de est un élément du type et vice versa. Au niveau du type, il y a un type et il contient des termes s'il y a une preuve qui et se réduisent à la même valeur. (Évidemment, les termes de ce type sont générés à l'aide du jugement d'égalité de terme.) Enfin, il existe un niveau d'égalité en anglais, car nous utilisons le mot « quatre » et le symbole « » pour désigner le terme canonique . Des synonymes comme ceux-ci sont appelés "définitivement égaux" par Martin-Löf.

La description des jugements ci-dessous est basée sur la discussion dans Nordström, Petersson et Smith.

La théorie formelle travaille avec des types et des objets .

Un type est déclaré par :

Un objet existe et est dans un type si :

Les objets peuvent être égaux

et les types peuvent être égaux

Un type qui dépend d'un objet d'un autre type est déclaré

et supprimé par substitution

  • , en remplaçant la variable par l'objet dans .

Un objet qui dépend d'un objet d'un autre type peut se faire de deux manières. Si l'objet est "abstrait", alors il est écrit

et supprimé par substitution

  • , en remplaçant la variable par l'objet dans .

L'objet dépendant de l'objet peut également être déclaré comme une constante dans le cadre d'un type récursif. Un exemple de type récursif est :

Ici, est un objet constant dépendant de l'objet. Il n'est pas associé à une abstraction. Les constantes comme peuvent être supprimées en définissant l'égalité. Ici, la relation avec l'addition est définie en utilisant l'égalité et en utilisant le filtrage de motifs pour gérer l'aspect récursif de :

est manipulé comme une constante opaque - il n'a pas de structure interne pour la substitution.

Ainsi, les objets et les types et ces relations sont utilisés pour exprimer des formules dans la théorie. Les styles de jugements suivants sont utilisés pour créer de nouveaux objets, types et relations à partir d'objets existants :

σ est un type bien formé dans le contexte Γ.
t est un terme bien formé de type σ dans le contexte Γ.
σ et τ sont des types égaux dans le contexte Γ.
t et u sont égaux judgmentally termes de type σ dans Γ de contexte.
Γ est un contexte bien formé d'hypothèses de typage.

Par convention, il existe un type qui représente tous les autres types. Il s'appelle (ou ). Puisque est un type, ses membres sont des objets. Il existe un type dépendant qui mappe chaque objet à son type correspondant. Dans la plupart des textes n'est jamais écrit. À partir du contexte de l'énoncé, un lecteur peut presque toujours dire s'il se réfère à un type ou s'il se réfère à l'objet qui correspond au type.

C'est le fondement complet de la théorie. Tout le reste est dérivé.

Pour mettre en œuvre la logique, chaque proposition se voit attribuer son propre type. Les objets de ces types représentent les différentes manières possibles de prouver la proposition. Évidemment, s'il n'y a pas de preuve pour la proposition, alors le type n'a pas d'objets en lui. Les opérateurs comme "et" et "ou" qui fonctionnent sur des propositions introduisent de nouveaux types et de nouveaux objets. Est donc un type qui dépend du type et du type . Les objets de ce type dépendant sont définis pour exister pour chaque paire d'objets dans et . Évidemment, si ou n'a pas de preuve et est un type vide, alors le nouveau type représentant est également vide.

Cela peut être fait pour d'autres types (booléens, nombres naturels, etc.) et leurs opérateurs.

Modèles catégoriques de la théorie des types

En utilisant le langage de la théorie des catégories , RAG Seely a introduit la notion de catégorie fermée localement cartésienne (LCCC) comme modèle de base de la théorie des types. Cela a été affiné par Hofmann et Dybjer en catégories avec familles ou catégories avec attributs sur la base de travaux antérieurs de Cartmell.

Une catégorie avec familles est une catégorie C de contextes (dans laquelle les objets sont des contextes, et les morphismes de contexte sont des substitutions), avec un foncteur T  : C opFam ( Set ).

Fam ( Set ) est la catégorie de familles d'Ensembles, dans laquelle les objets sont des paires d'un "ensemble d'indices" A et une fonction B : XA , et les morphismes sont des paires de fonctions f  : AA' et g  : XX' , tel que B' ° g = f ° B — en d'autres termes, f fait correspondre B a à B g ( a ) .

Le foncteur T affecte à un contexte G un ensemble de types, et pour chacun , un ensemble de termes. Les axiomes pour un foncteur exigent que ceux-ci jouent harmonieusement avec la substitution. La substitution est généralement écrite sous la forme Af ou af , où A est un type dans et a est un terme dans , et f est une substitution de D à G . Ici et .

La catégorie C doit contenir un objet terminal (le contexte vide), et un objet final pour une forme de produit appelée compréhension, ou extension de contexte, dans laquelle l'élément de droite est un type dans le contexte de l'élément de gauche. Si G est un contexte, et , alors il devrait y avoir un objet final parmi les contextes D avec des correspondances p  : DG , q  : Tm ( D,Ap ).

Un cadre logique, comme celui de Martin-Löf, prend la forme de conditions de fermeture sur les ensembles de types et de termes dépendant du contexte : qu'il y ait un type appelé Ensemble, et pour chaque ensemble un type, que les types soient fermés sous des formes de somme dépendante et produit, et ainsi de suite.

Une théorie telle que celle de la théorie prédicative des ensembles exprime des conditions de fermeture sur les types d'ensembles et leurs éléments : qu'ils doivent être fermés sous des opérations qui reflètent une somme et un produit dépendants, et sous diverses formes de définition inductive.

Extensionnel versus intensionnel

Une distinction fondamentale est la théorie de type extensionnelle vs intensionnelle . Dans la théorie des types extensionnelle, l'égalité définitionnelle (c'est-à-dire computationnelle) n'est pas distinguée de l'égalité propositionnelle, qui nécessite une preuve. En conséquence, la vérification de type devient indécidable dans la théorie des types extensionnelle car les programmes de la théorie peuvent ne pas se terminer. Par exemple, une telle théorie permet de donner un type au combinateur Y , un exemple détaillé de ceci peut être trouvé dans Nordstöm et Petersson Programming in Martin-Löf's Type Theory . Cependant, cela n'empêche pas la théorie des types extensionnels d'être une base pour un outil pratique, par exemple, NuPRL est basé sur la théorie des types extensionnels.

En revanche, dans la théorie des types intensionnelle, la vérification de type est décidable , mais la représentation des concepts mathématiques standard est un peu plus lourde, car le raisonnement intensionnel nécessite l'utilisation de setoïdes ou de constructions similaires. Il existe de nombreux objets mathématiques communs, avec lesquels il est difficile de travailler ou qui ne peuvent être représentés sans cela, par exemple, les nombres entiers , les nombres rationnels et les nombres réels . Les entiers et les nombres rationnels peuvent être représentés sans setoïdes, mais cette représentation n'est pas facile à utiliser. Les nombres réels de Cauchy ne peuvent pas être représentés sans cela.

La théorie des types d'homotopie permet de résoudre ce problème. Il permet de définir des types inductifs supérieurs , qui définissent non seulement des constructeurs de premier ordre ( valeurs ou points ), mais des constructeurs d'ordre supérieur, c'est-à-dire des égalités entre éléments ( chemins ), des égalités entre égalités ( homotopies ), à l' infini .

Implémentations de la théorie des types

Différentes formes de théorie des types ont été implémentées en tant que systèmes formels sous-jacents à un certain nombre d' assistants de preuve . Alors que beaucoup sont basés sur les idées de Per Martin-Löf, beaucoup ont des caractéristiques supplémentaires, plus d'axiomes ou un arrière-plan philosophique différent. Par exemple, le système NuPRL est basé sur la théorie des types informatiques et Coq est basé sur le calcul des constructions (co)inductives . Les types dépendants figurent également dans la conception des langages de programmation tels que ATS , Cayenne , Epigram , Agda et Idris .

Théories de type Martin-Löf

Per Martin-Löf a construit plusieurs théories de types qui ont été publiées à différentes époques, certaines d'entre elles beaucoup plus tard que lorsque les prépublications avec leur description sont devenues accessibles aux spécialistes (entre autres Jean-Yves Girard et Giovanni Sambin). La liste ci-dessous tente de répertorier toutes les théories qui ont été décrites sous forme imprimée et d'esquisser les principales caractéristiques qui les distinguent les unes des autres. Toutes ces théories avaient des produits dépendants, des sommes dépendantes, des unions disjointes, des types finis et des nombres naturels. Toutes les théories avaient les mêmes règles de réduction qui n'incluaient pas la -réduction ni pour les produits dépendants ni pour les sommes dépendantes, sauf pour MLTT79 où la -réduction pour les produits dépendants est ajoutée.

MLTT71 a été la première des théories de type créées par Per Martin-Löf. Il est apparu dans une prépublication en 1971. Il avait un univers mais cet univers avait un nom en soi, c'est-à-dire qu'il s'agissait d'une théorie des types avec, comme on l'appelle aujourd'hui, "Type in Type". Jean-Yves Girard a montré que ce système était incohérent et la prépublication n'a jamais été publiée.

MLTT72 a été présenté dans un preprint de 1972 qui a maintenant été publié. Cette théorie avait un univers V et aucun type d'identité. L'univers était « prédicatif » dans le sens où le produit dépendant d'une famille d'objets de V sur un objet qui n'était pas dans V comme, par exemple, V lui-même, n'était pas supposé être dans V. L'univers était à la Russell, c'est-à-dire qu'on écrirait directement "T∈V" et "t∈T" (Martin-Löf utilise le signe "∈" au lieu du moderne ":") sans le constructeur supplémentaire tel que "El".

MLTT73 a été la première définition d'une théorie des types publiée par Per Martin-Löf (elle a été présentée au Logic Colloquium 73 et publiée en 1975). Il existe des types d'identité qu'il appelle « propositions », mais comme aucune distinction réelle entre les propositions et le reste des types n'est introduite, la signification de ceci n'est pas claire. Il y a ce qui acquiert plus tard le nom de J-éliminateur mais pourtant sans nom (voir pp. 94-95). Il y a dans cette théorie une suite infinie d'univers V 0 , ..., V n , ... . Les univers sont prédicatifs, à la Russell et non cumulatifs ! En fait, le corollaire 3.10 à la p. 115 dit que si A∈V m et B∈V n sont tels que A et B sont convertibles alors m  =  n . Cela signifie, par exemple, qu'il serait difficile de formuler l'univalence dans cette théorie - il y a des types contractibles dans chacun des V i mais on ne sait pas comment les déclarer égaux puisqu'il n'y a pas de types d'identité reliant V i et V j pour ij .

MLTT79 a été présenté en 1979 et publié en 1982. Dans cet article, Martin-Löf a présenté les quatre types de jugement de base pour la théorie des types dépendants qui est depuis devenue fondamentale dans l'étude de la méta-théorie de tels systèmes. Il y a également introduit les contextes en tant que concept distinct (voir p. 161). Il existe des types d'identité avec le J-éliminateur (qui figurait déjà dans MLTT73 mais n'y portait pas ce nom) mais aussi avec la règle qui rend la théorie « extensionnelle » (p. 169). Il existe des types W. Il existe une séquence infinie d'univers prédicatifs qui sont cumulatifs .

Bibliopolis : il y a une discussion d'une théorie des types dans le livre Bibliopolis de 1984 mais elle est quelque peu ouverte et ne semble pas représenter un ensemble particulier de choix et donc il n'y a pas de théorie des types spécifique qui lui est associée.

Voir également

Remarques

Les références

Lectures complémentaires

Liens externes