Definition. Pointed poset [math-XV49]

A poset $D$ is pointed if there is a least element $\bot_D$.

This turns out, is very important for computation; if we view type $A$ as a DCPO, then a function $A \to B$ has computation $A \to B_\bot$. The $B_\bot$ means result will be an element of $B$, or diverging.