my forest
add link to chain completeness proof
+2
-2
+2
-2
trees/dt-001F.tree
+2
-2
trees/dt-001F.tree
···
1
1
\taxon{Aside}
2
2
\title{Other kinds of completeness}
3
3
\author{liamoc}
4
-
\p{In \ref{dt-001D} we defined cpos in terms of \em{directed completeness}. We may consider \em{chain completeness} instead, where, rather than require [lubs](dt-0017) for every [directed](dt-0010) subset of our [poset](dm-0004) #{A}, we require [lubs](dt-0017) for every [chain](dt-000V) #{X \subseteq A}. We know from \ref{dt-0012} that all [chains](dt-000V) are [directed](dt-0010), so every directed complete cpo is also chain complete. It is also known that every chain complete cpo is also directed complete, so the notions are \strong{equivalent}, although the proof is apparently non-trivial and buried in the literature.}
4
+
\p{In \ref{dt-001D} we defined cpos in terms of \em{directed completeness}. We may consider \em{chain completeness} instead, where, rather than require [lubs](dt-0017) for every [directed](dt-0010) subset of our [poset](dm-0004) #{A}, we require [lubs](dt-0017) for every [chain](dt-000V) #{X \subseteq A}. We know from \ref{dt-0012} that all [chains](dt-000V) are [directed](dt-0010), so every directed complete cpo is also chain complete. It is also known that every chain complete cpo is also directed complete, so the notions are \strong{equivalent}, although the proof is non-trivial, relying on transfinite induction (see [these lecture notes](https://www.cs.cornell.edu/courses/cs6110/2023sp/lectures/lecC.pdf) for details).}
5
5
\p{If we weaken our completeness requirement to require [lubs](dt-0017) only for the countable [#{\omega}-chains](dt-000W) and not necessarily all chains, we get what is called an \em{#{\omega}-cpo}. All [#{\omega}-chains](dt-000W) are [chains](dt-000V) and are therefore [directed](dt-0010), but not all [chains](dt-000V) are [#{\omega}-chains](dt-000W).}
6
-
\p{Working with just #{\omega}-cpos is common in [denotational semantics](dt-0001) practice, but working with [directed](dt-0010) completeness simplifies some of the properties we will discuss later.}
6
+
\p{Working with just #{\omega}-cpos is common in [denotational semantics](dt-0001) practice, but working with [directed](dt-0010) completeness simplifies some of the properties we will discuss later.}