| dbo:abstract
|
- En mathématiques, logique et informatique, une théorie des types est une classe de systèmes formels, dont certains peuvent servir d'alternatives à la théorie des ensembles comme fondation des mathématiques. Ils ont été historiquement introduit pour résoudre le paradoxe d'un axiome de compréhension non restreint. En théorie des types, il existe des types de base et des constructeurs (comme par exemple, celui des fonctions ou encore celui du produit cartésien) qui permettent de créer de nouveaux types à partir de types préexistant. Une différence notable avec la théorie des ensembles et que chaque terme possède un type, ce qui est un jugement subjectif et non pas une proposition . En d'autres termes la question de savoir si un terme appartient ou non à un type n'est pas réputée objective. Des types sont utilisés dans certains langages de programmation, ce qui permet d'éviter des bugs. Toutefois, la théorie des types fait plus souvent références à l'étude des systèmes de types qui servent de fondation alternative aux mathématiques. Le λ-calcul typé d'Alonzo Church et ses extensions permettent de faire de la logique à différents ordres ; ainsi elles servent à formaliser le système F. Dans la même ligne, la théorie des types intuitionniste de Per Martin-Löf ainsi que le calcul des constructions inductif offrent d'autres perspectives. Ceux-ci sont notamment à la base d' (en) ou de Coq qui sont des assistants de preuve. (fr)
- En mathématiques, logique et informatique, une théorie des types est une classe de systèmes formels, dont certains peuvent servir d'alternatives à la théorie des ensembles comme fondation des mathématiques. Ils ont été historiquement introduit pour résoudre le paradoxe d'un axiome de compréhension non restreint. En théorie des types, il existe des types de base et des constructeurs (comme par exemple, celui des fonctions ou encore celui du produit cartésien) qui permettent de créer de nouveaux types à partir de types préexistant. Une différence notable avec la théorie des ensembles et que chaque terme possède un type, ce qui est un jugement subjectif et non pas une proposition . En d'autres termes la question de savoir si un terme appartient ou non à un type n'est pas réputée objective. Des types sont utilisés dans certains langages de programmation, ce qui permet d'éviter des bugs. Toutefois, la théorie des types fait plus souvent références à l'étude des systèmes de types qui servent de fondation alternative aux mathématiques. Le λ-calcul typé d'Alonzo Church et ses extensions permettent de faire de la logique à différents ordres ; ainsi elles servent à formaliser le système F. Dans la même ligne, la théorie des types intuitionniste de Per Martin-Löf ainsi que le calcul des constructions inductif offrent d'autres perspectives. Ceux-ci sont notamment à la base d' (en) ou de Coq qui sont des assistants de preuve. (fr)
|
| rdfs:comment
|
- En mathématiques, logique et informatique, une théorie des types est une classe de systèmes formels, dont certains peuvent servir d'alternatives à la théorie des ensembles comme fondation des mathématiques. Ils ont été historiquement introduit pour résoudre le paradoxe d'un axiome de compréhension non restreint. Des types sont utilisés dans certains langages de programmation, ce qui permet d'éviter des bugs. (fr)
- En mathématiques, logique et informatique, une théorie des types est une classe de systèmes formels, dont certains peuvent servir d'alternatives à la théorie des ensembles comme fondation des mathématiques. Ils ont été historiquement introduit pour résoudre le paradoxe d'un axiome de compréhension non restreint. Des types sont utilisés dans certains langages de programmation, ce qui permet d'éviter des bugs. (fr)
|
