Théorie du point fixe et programmation logique

Abstract

La théorie du point fixe est sujette à beaucoup d’applications en programmation logique. L’objectif de cette thèse est d’illustrer l’incidence de points fixes considérés dans des métriques peu ordinaires sur la recherche de modèles de programmes logiques. Elle est composée de deux parties: La première partie développe la théorie du point fixe dans les espaces ultramétriques généralisés à valeurs dans une algèbre de Heyting. Nous allons établir un théorème de type Banach dans les espaces ultramétriques dits hyperconvexes. Nous allons par la suite voir une extension de ce théorème aux applications multivoques prises sous certaines conditions et nous obtiendrons alors une forme semblable à la version multivoque du théorème de Banach considérée sur les espaces métriques ordinaires. La deuxième partie de cette thèse concerne une investigation des résultats de la première partie en programmation logique. La recherche de sémantiques déclaratives pour les programmes logiques revient à prouver l’existence de points fixes pour des opérateurs conséquents aux programmes et qui sont dans ce cas, l’opérateur de Van Emden-Kowalski dans le cas nondisjonctif et l’opérateur multivoque de Gelfond-Lifschitz dans le cas disjonctif. Nous montrons alors l’existence de modèles supportés pour les programmes logiques normaux dits localements stratifiés au sens de Przymusinski. La flexibilité de la méthode utilisée suggère une extension aux programmes disjonctifs. Nous montrons alors l’existence d’un ensemble de réponses pour les programmes dits disjonctifs semi-strictement décroissants. L’étude se fait en termes de fonctions niveaux.