Localic sup-lattices and tropological systems. (Q1427786)

Approaches to process semantics using quantales and modules over them were developed by the second author of this paper and S.~Abramsky, and (in a slightly different way) by the first author. In these approaches, although the `set' of actions is taken to be a quantale, the set of states remains an untopologized set. In order to give a fully constructive account of these structures, it is necessary not merely to topologize the state set but to replace it with a locale (or `pointless space'): this is done in the present paper. The authors begin by recalling how the `classical' duality for sup-lattices may be constructivized by using localic sup-lattices instead of topological ones, and then go on to indicate how the same approach may be applied to the `tropological systems' introduced by the first author as a setting for process semantics. This enables them to rewrite the `third completeness' results of Abramsky and the second author in constructive form.