Poset

As already described here, the representation in the following categories contains
the whole order and not just one element (unlike PartialOrder in catdef.spad).

Poset Implementation

The poset domain is similar to the DirectedGraph domain, the difference is that the poset has, at most, one arrow from any given source to any given destination. We enforce this by coding the representation differently in the poset. The representation is a two dimensional array of boolean values which indicate whether or not a given source has and arrow to a given destination.

Also, unlike graph, the poset has reflexivity, antisymmetry and transitivity properties. these properties are not enforced by the representation. However there are some functions provided to enforce these properties:

DCPO Directed-Complete Partial Order

Complete partial orders are partial orders which are guaranteed to have meets
and/or joins depending on type of CPO. The terminology around this is not always
consistent so I will use the following terminology.

A DCPO, or directed-complete partial order, is a poset where joins (or supremum or
least upper bound) are defined. That is join is a complete or closed function, not a
partial function.
Often a DCPO is required to have a bottom element; then it is called a pointed
DCPO or a CPO.

Finite DCPOs are pointed DCPOs, we can get the bottom element just by taking the
join of all the elements, this is not true of infinite DCPOs.

As an example consider the integers, any finite set of integers has a minimum
element but the set of all integers does not (minus infinity is not an integer).

Another example, more applicable to topology, is subsets of line segments.

The examples below only model finite DCPOs. TODO: I want to model infinite DCPOs,
we obvously cant do this by using a list of all the elements (as below). We need
to define the elements, and their order, recursively.

Co-DCPO

Here we will call the dual notion of a directed complete poset a Co-DCPO alternativly
it is sometimes called a filtered complete partial order.

BiCPO

BiCPO is Join of Dcpo and CoDcpo, that is, it is both joins and meets are gauranteed
to exist.

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 


metadata block
see also:
Correspondence about this page

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2023 Martin John Baker - All rights reserved - privacy policy.