Ordre partiel complet

Un article de Wikipédia, l'encyclopédie libre.

Un ordre partiel complet (complete partial order ou CPO) est un ensemble partiellement ordonné dont toutes les chaînes ont une borne supérieure[1].

Cette définition équivaut à celle d'ensemble inductif strict avec plus petit élément.

La notion de CPO est utilisée pour résoudre les équations aux domaines, notamment quand on cherche une sémantique dénotationnelle pour un langage en informatique.

Motivation[modifier | modifier le code]

Les ensembles partiellement ordonnées ne se comportent pas tous comme des ensembles de parties, munies de l'ordre donnée par l'inclusion ⊆. En particulier, quand on a une suite croissante de sous-ensembles E0 ⊆ E1 ⊆ E2 ⊆ ..., on peut définir l'union infinie E0 ∪ E1 ∪ E2 ∪ ... La définition de CPO abstrait et formalise ce point[2].

Définition[modifier | modifier le code]

Formellement, (D, ⊑) est un CPO si c'est un ensemble partiellement ordonné tel que toute chaîne d0 ⊑ d1 ⊑ ... ⊑ dn ⊑ ... admet une plus petite borne supérieure. Cette plus petite borne supérieure est notée ⨆{d0, d1, ...}, ou ⨆ndn.

Un CPO sans bottom est un CPO qui admet un plus petit élément que l'on note ⊥ (bottom).

Exemples[modifier | modifier le code]

  • Tout ensemble muni de la relation identité est un CPO (sans bottom sauf si l'ensemble est de cardinal 1).
  • L'ensemble des parties d'un ensemble muni de la relation d'ordre ⊆ est un CPO avec bottom (le plus petit élément est l'ensemble vide).

Notes et références[modifier | modifier le code]

  1. Winskel 1993, p. 70.
  2. Winskel 1993, p. 69.

Bibliographie[modifier | modifier le code]

  • (en) Glynn Winskel, The Formal Semantics of Programming Languages : An Introduction, The MIT Press, .

Voir aussi[modifier | modifier le code]

Théorème du point fixe de Kleene