Set Domains

Reinhold Heckmann

Abstract

Set domains are intended to give semantics to a data type of sets together with a wide range of useful set operations. The classical power domain constructions are shown to be inappropriate for this purpose. Lower and upper domain do not support quantification, whereas Plotkin's domain does not contain the empty set. This is an immense defect, since the empty set is not only interesting in its own, but is also needed to define operations such as filtering a set through a predicate. Two constructions, the big and the small set domain, are proposed that support the desired set operations. The big domain is bounded complete, whereas the small one only respects Plotkin's SFP-property. Both constructions are free with respect to suitable algebraic theories.


Remark:   big set domain = sandwich power domain,   small set domain = mixed power domain.


[Paper.ps.gz (21p, 78k, reformatted)]


Reinhold Heckmann / heckmann@absint.com