Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur GraphSearch.
Concept
Théorie des domaines
Résumé
La théorie des domaines est une branche des mathématiques dont le principal champ d'application se trouve en informatique théorique. Cette partie de la théorie des ensembles ordonnés a été introduite par Dana Scott pendant les années 1960, afin de fournir le cadre théorique nécessaire à la définition d'une sémantique dénotationnelle du lambda-calcul.
Les domaines sont des ensembles partiellement ordonnés. Dans la sémantique dénotationnelle du lambda-calcul, les éléments des domaines représentent les lambda-termes et le plus petit élément (quand on en munit le domaine) représente le résultat d'un calcul ne finissant pas, c'est l'élément dit « indéfini », noté ⊥ (prononcer « bottom »). L'ordre du domaine définit, dans l'idée, une notion de quantité d'information : un élément du domaine contient au moins toute l'information contenue dans les éléments qui lui sont inférieurs.
L'idée est ensuite de se ramener à des domaines particuliers où toute fonction monotone (croissante) a un plus petit point fixe. En général, on utilise des ordres partiels complets (complete partial order, ou CPO), c'est-à-dire des domaines qui possèdent un plus petit élément et où toute chaîne (partie strictement ordonnée) a une borne supérieure.
Ainsi, il devient aisé d'associer une sémantique au combinateur de point fixe Y, en le représentant par une fonction totale qui à une fonction associe un de ses points fixes s'il en existe et ⊥ sinon. Par là-même, donner un sens à une fonction définie « récursivement » (c'est-à-dire en fait, en tant que point fixe d'une fonctionnelle G) devient possible :
si f est la fonction qui à 0 associe 1 et à n > 0 associe n * f(n – 1),
on peut aussi définir f comme ceci : f = Y(G) (point fixe de G) où G est la fonction qui prend une fonction φ en entrée et rend la fonction qui à 0 associe 1 et à n > 0 associe n * φ(n – 1) (et à ⊥ associe ⊥, par définition de ⊥). G est monotone sur le domaine des fonctions de N⊥ dans N⊥ et, à ce titre, admet un point fixe (la fonction factorielle)
alors, on a un moyen de calculer f : en itérant G sur la fonction f0 = ⊥, c'est-à-dire la fonction qui à tout entier naturel et à ⊥ associe ⊥.
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.