Théorie des domaines

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 ⊥.