Skip to Main content Skip to Navigation
Journal articles

Choice sequence and nonstandard extension of type theory

Résumé : Partant de son travail Mathematics of Infinity (1989), Martin-Löf a développé l'idée d'un lien conceptuel profond entre les notions de suite de choix et d'objet mathématique nonstandard. Précisément, il a défini une extension nonstandard de la théorie des types en ajoutant une série d'axiomes nonstandard conçue comme une sorte de suite de choix. Enfin, dans une communication de 1999, il a présenté les grandes lignes d'une théorie des types nonstandard plus générale et munie d'un fort contenu computationnel. Le présent travail est une tentative de donner un développement complet d'une théorie de ce genre. Cependant, dans le but de garder un fort contrôle sur la théorie résultante et notablement pour éviter quelques problèmes en rapport avec l'égalité définitionnelle, le champ des axiomes nonstandard est moins général que ceux proposés dans sa communication de 1999. L'étude présente est poussée jusqu'à l' introduction d'une notion de proposition externe qui joue le même rôle que les propriétés externes si utiles dans l'analyse nonstandard usuelle. Du fait que ce texte débute par une introduction à la théorie des types de Martin-Löf, il peut intéresser les mathématiciens non familiers avec ce sujet.
Document type :
Journal articles
Complete list of metadata

Cited literature [5 references]  Display  Hide  Download

https://hal.inria.fr/hal-01320619
Contributor : Coordination Episciences Iam <>
Submitted on : Tuesday, May 24, 2016 - 11:01:08 AM
Last modification on : Thursday, October 8, 2020 - 1:00:03 PM

File

vol.20.pp.237-265.pdf
Publisher files allowed on an open archive

Identifiers

  • HAL Id : hal-01320619, version 1

Collections

Citation

Guy Wallet. Choice sequence and nonstandard extension of type theory. Revue Africaine de la Recherche en Informatique et Mathématiques Appliquées, INRIA, 2015, 20, pp.237-265. ⟨hal-01320619⟩

Share

Metrics

Record views

156

Files downloads

1293