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.
Type de document :
Article dans une revue
Revue Africaine de la Recherche en Informatique et Mathématiques Appliquées, INRIA, 2015, 20, pp.237-265
Liste complète des métadonnées

Littérature citée [5 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01320619
Contributeur : Coordination Episciences Iam <>
Soumis le : mardi 24 mai 2016 - 11:01:08
Dernière modification le : jeudi 9 février 2017 - 16:58:52

Fichier

vol.20.pp.237-265.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

93

Téléchargements de fichiers

143