Ordre partiel complet
Il existe plusieurs notions non équivalentes d'ordre partiel complet (complete partial order ou CPO).
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
Les ensembles partiellement ordonnés ne se comportent pas tous comme des ensembles de parties ordonnés 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[1].
Définitions
- Un d-CPO est un ensemble partiellement ordonné dont toutes les chaînes ont une borne supérieure. Cette définition équivaut à celle d'ensemble inductif strict avec plus petit élément (la borne supérieure de la chaîne vide)[2].
- La notion d'ω-CPO est définie de même mais en se limitant aux « ω-chaînes », c'est-à -dire aux suites croissantes[3]. La borne supérieure d'une suite croissante d0 ≤ d1 ≤ ... ≤ dn ≤ ...est notée ⨆{d0, d1, ...}, ou ⨆ndn.
Le plus petit élément d'un CPO, s'il existe, est noté ⊥.
Exemples
- Tout ensemble E muni de la relation identité est un ω-CPO (sans plus petit élément sauf si E est un singleton).
- L'ensemble des parties d'un ensemble, ordonné par l'inclusion, est un d-CPO (le plus petit élément est l'ensemble vide).
Notes et références
- (en) Glynn Winskel, The Formal Semantics of Programming Languages : An Introduction, The MIT Press, (lire en ligne), p. 69.
- (en) George Markowsky, « Chain-complete posets and directed sets with applications », Algebra Universalis, vol. 6, no 1,‎ , p. 53-68 (lire en ligne).
- Winskel 1993, p. 70.
Voir aussi
Cet article est issu de wikipedia. Text licence: CC BY-SA 4.0, Des conditions supplémentaires peuvent s’appliquer aux fichiers multimédias.