Définir le fini : deux formalisations d'espaces de dimension finie

Florian Faissole 1
1 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Résumé : Les espaces de dimension finie permettent de décrire mathématiquement certaines méthodes numériques comme la méthode des éléments finis. Leur formalisation est nécessaire pour certifier que ces méthodes sont correctes et plus précisément qu'elles sont convergentes. Dans cet article, nous présentons deux méthodes pour formaliser les espaces de dimension finie en Coq, dans un cadre de topologie générale. Les deux approches utilisent des mécanismes différents et ne présentent pas les mêmes avantages et inconvénients. La première repose sur l'extension, à l'aide de structures canoniques, de la hiérarchie algébrique de la bibliothèque Coquelicot. Elle permet aisément de montrer que les espaces R n sont de dimension finie et plus généralement que le produit cartésien d'espaces de dimension finie est de dimension finie. La seconde repose sur l'utilisation de sous-espaces en tant que prédicats sur l'espace total. Elle permet d'extraire des propriétés topologiques sur des sous-espaces de dimension finie d'un espace de dimension infinie, comme la fermeture des sous-espaces de dimension finie des espaces de Hilbert. Nous proposons par ailleurs une étude comparative de ces deux approches.
Type de document :
Communication dans un congrès
JLFA 2017 - Journées Francophones des Langages Applicatifs, Jan 2018, Banyuls-sur-mer, France. pp.1-6, 2018, 29èmes Journées Francophones des Langages Applicatifs
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01654457
Contributeur : Florian Faissole <>
Soumis le : lundi 4 décembre 2017 - 08:49:38
Dernière modification le : jeudi 11 janvier 2018 - 06:25:27

Fichier

jfla.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01654457, version 1

Citation

Florian Faissole. Définir le fini : deux formalisations d'espaces de dimension finie. JLFA 2017 - Journées Francophones des Langages Applicatifs, Jan 2018, Banyuls-sur-mer, France. pp.1-6, 2018, 29èmes Journées Francophones des Langages Applicatifs. 〈hal-01654457〉

Partager

Métriques

Consultations de la notice

33

Téléchargements de fichiers

5