From chains to directed sets [dt-000Z]
- with contributions from Liam O'Connor
While \omega -chains are technically sufficient for denotational semantics, for our purposes it is a little more convenient to think in terms of directed sets rather than chains.
DefinitionDirected set [dt-0010]
Formally, a non-empty subset Y \subseteq X of a poset (X,\sqsubseteq ) is directed iff: \forall x, y \in Y.\ \exists z \in Y.\ x \sqsubseteq z \land y \sqsubseteq z
Intuitively, directed sets are "going somewhere" — given two elements we can always find a "greater" one in the set.
ExamplePower sets are directed [dt-0011]
TheoremChain → Directed [dt-0012]
All non-empty chains are directed.
Proof.
Let C be a chain. Then, given two elements x,y \in C we know from totality that either x \sqsubseteq y or y \sqsubseteq x. If x \sqsubseteq y, then y is the upper bound, otherwise x is the upper bound.
DefinitionConsistent subset [dt-0013]
A subset Y \subseteq X of a poset X is consistent iff
\exists x \in X.\ \forall y \in Y.\ y \sqsubseteq x
Such an x is called an upper bound of Y.
TheoremAlternative characterisation of directedness [dt-0014]
A subset Y \subseteq X of a poset X is directed iff every finite subset of Y' \subseteq Y has an upper bound in Y.
Proof.
- ⇐: Every pair of elements x,y \in Y has an upper bound simply by taking the upper bound of the set \{x,y\}.
- ⇒: Given a finite set X = \{x_1,x_2,\dots , x_n\} , we can show it has an upper bound by an inductive process, first taking the upper bound of x_1 and x_2, and then taking the upper bound of that an x_3 and so on until we have an upper bound for the whole set. This induction works because the set X is finite.