Théorie des domaines

Un article de Wikipédia, l'encyclopédie libre.
Cet article est une ébauche concernant l’informatique.
Vous pouvez partager vos connaissances en l’améliorant. (Comment ?).

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 60, 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é \perp (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 existe, et \perp 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 à \perp associe \perp, par définition de \perp). On note que G est monotone sur le domaine des fonctions de ℕ\perp dans ℕ\perp, 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 = \perp, c'est-à-dire la fonction qui a tout entier naturel et à \perp associe \perp. f est la limite de la suite ainsi obtenue (et le plus petit point fixe de G).

La théorie des domaines permet aussi de donner un sens aux équations de domaine de type A = A \rightarrow A (A est l'ensemble des fonctions de A dans A !). Dans les mathématiques habituelles, ceci est absurde, à moins de donner un sens particulier à cette flèche. Par exemple \reals = \reals \rightarrow \reals paraît impossible, ne serait-ce que pour des raisons de cardinalité (Dans la théorie des cardinaux \reals est un infini strictement plus petit que \reals \rightarrow \reals); pourtant, si cette flèche ne représente que les applications continues de \reals dans \reals, on garde bien le même cardinal que \reals (en effet, une application continue de \reals dans \reals peut être définie par sa restriction à l'ensemble dénombrable Q, donc cet ensemble a le cardinal de \reals ^ \omega, donc de \reals).

En théorie des domaines, la notion de continuïté sur un ensemble A aura son équivalent : la continuïté selon Scott sur un domaine A. Une fonction est Scott-continue ssi elle est monotone sur A et que pour toute partie filtrante (partie où toute paire d'éléments a un majorant) B de A admettant une borne supérieure, on a sup(f(B)) = f(sup(B)). Cette définition sera souvent simplifiée pour le cas où A est un CPO : la fonction est continue ssi elle est monotone, et si pour toute chaîne B, on a sup(f(B)) = f(sup(B)).

Autres langues