Guy Wallet - Choice sequence and nonstandard extension of type theory

arima:1995 - Revue Africaine de Recherche en Informatique et Mathématiques Appliquées, September 17, 2015, Volume 20 - 2015 - Special issue - Colloquium in Honor of Éric Benoît - https://doi.org/10.46298/arima.1995
Choice sequence and nonstandard extension of type theoryArticle

Authors: Guy Wallet 1

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.


Volume: Volume 20 - 2015 - Special issue - Colloquium in Honor of Éric Benoît
Published on: September 17, 2015
Submitted on: February 20, 2015
Keywords: Choice sequence, type theory, constructive nonstandard analysis.,Suite de choix, théorie des types, analyse nonstandard constructive,[INFO] Computer Science [cs],[MATH] Mathematics [math]

Consultation statistics

This page has been seen 289 times.
This article's PDF has been downloaded 365 times.