liamoc.net
my forest
1\import{dt-macros}
2\author{liamoc}
3\taxon{Definition}
4\title{Algebraicity}
5\p{A [cpo](dt-001D) is \em{algebraic} iff every element is the [lub](dt-0017) of its [compact](dt-003U) approximations. That is, a [cpo](dt-001D) #{D} is \em{algebraic} iff for all #{x \in D},
6\ol{
7\li{#{\downset{x} = \Set{ y \in \compact{D} \mid y \sqsubseteq x }} is [directed](dt-0010);}
8\li{#{x = \bigsqcup\downset{x}}}
9}
10\strong{Note}: It's common in semantics to consider only algebraic [cpos](dt-001D) with a \em{countable} set of [compact](dt-003U) elements. Such [cpos](dt-001D) are called \em{#{\omega}-algebraic}.}
11
12\p{ \strong{Aside}: Plotkin provides an equivalent definition of #{\omega}-algebraic [cpos](dt-001D) in which [directed sets](dt-0010) are replaced with [#{\omega}-chains](dt-000W) throughout. [Hutton](haskellhutt) claims this is less appealing, as the definition speaks of \em{an} [#{\omega}-chain](dt-000W) of [compact](dt-003U) approximations, rather than \em{the} [directed set](dt-0010) of such.}