Puissance expressive des preuves circulaires

Fortier, Jérôme (2015). « Puissance expressive des preuves circulaires » Thèse. Montréal (Québec, Canada), Université du Québec à Montréal, Doctorat en mathématiques.

Fichier(s) associé(s) à ce document :

Prévisualisation	PDF Télécharger (28MB)

Résumé

Cette recherche vise à établir les propriétés fondamentales d'un système formel aux preuves circulaires introduit par Santocanale, auquel on a rajouté la règle de coupure. On démontre, dans un premier temps, qu'il y a une pleine correspondance entre les preuves circulaires et les flèches issues des catégories dites u-bicomplètes. Ces flèches sont celles que l'on peut définir purement à partir des outils suivants : les produits et coproduits finis, les algèbres initiales et les coalgèbres finales. Dans la catégorie des ensembles, les preuves circulaires dénotent donc les fonctions qu'on peut définir en utilisant les produits cartésiens finis, les unions disjointes finies, l'induction et la coinduction. On décrit également une procédure d'élimination des coupures qui produit, à partir d'une preuve circulaire finie, une preuve sans cycles et sans coupures, mais possiblement infinie. On démontre que l'élimination des coupures fournit une sémantique opérationnelle aux preuves circulaires, c'est-à-dire qu'elle permet de calculer les fonctions dénotées par celles-ci, par le moyen d'une sorte d'automate avec mémoire. Enfin, on s'intéresse au problème de la puissance expressive de cet éliminateur de coupures, c'est-à-dire à la question de caractériser la classe des expressions qu'il peut calculer. On démontre, par une simulation, que l'éliminateur des coupures est strictement plus expressif que les automates à pile d'ordre supérieur. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : preuves circulaires, logique catégorique, catégories u-bicomplètes, points fixes, algèbres initiales, coalgèbres finales, élimination des coupures, automates à pile d'ordre supérieur

Type:	Thèse ou essai doctoral accepté
Informations complémentaires:	La thèse a été numérisée telle que transmise par l'auteur.
Directeur de thèse:	Brlek, Srecko
Mots-clés ou Sujets:	Logique symbolique et mathématique, Catégories (Mathématiques), Théorème du point fixe, Théorie des preuves circulaires
Unité d'appartenance:	Faculté des sciences > Département de mathématiques
Déposé par:	Service des bibliothèques
Date de dépôt:	24 sept. 2015 15:09
Dernière modification:	24 sept. 2015 15:09
Adresse URL :	http://archipel.uqam.ca/id/eprint/7235

Modifier les métadonnées (propriétaire du document)

Statistiques