Map Theory est une extension équationnelle du lambda-calcul non-typé conçue par Klaus Grue pour être une fondation commune de l'informatique et des mathématiques. Elle permet en particulier une interprétation complète du calcul des prédicats et de ZFC+FA, où ZFC est la théorie de Zermelo-Fraenkel, et FA est l'axiome de bonne fondation usuel. Toutes les notions primitives de la logique du premier ordre et de la théorie des ensembles, valeurs de vérité, connecteurs, quantificateurs, appartenance et égalité, y sont traduites par des termes du lambda-calcul enrichi de quelques constantes. De plus, Map Theory permet de représenter les types de données inductifs et de donner un sens calculatoire immédiat à tous les constructeurs ensemblistes usuels. La version initiale de Map Theory par K. Grue ne considère cependant que les ensembles (ou classes) bien-fondée relativement à la relation d'appartenance. Dans le cadre du renouveau d'intérêt pour l'antifondation induit par les developpements récents de l'informatique théorique, nous montrons dans notre thèse qu'il est possible d'élaborer une version antifondée de Map Theory qui prenne en compte l'existence des objets non-bien-fondés, et qui permette de raisonner sur ces objets par co-induction. Ce nouveau système ouvre la possibilité d'une représentation directe des types de données co-inductifs, et de la modèlisation des phènoménes et processus circulaires. Dans une première partie, nous présenterons l'axiomatisation MTA de ce nouveau système, et nous montrerons que ZFC+AFA, où AFA est l'axiome d'Antifondation de Aczel-Forti-Honsell, y est interprétable syntaxiquement. Dans la deuxième partie, nous montrerons la consistance de MTA relativement à ZFC+SI, où SI est l'axiome exprimant l'existence d'un cardinal fortement inaccessible.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00001298 |
| Date | 21 December 2001 |
| Creators | Vallée, Thierry |
| Publisher | Université Paris-Diderot - Paris VII |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0021 seconds