Demonic operators and monotype factors

Abstract

This paper tackles the problem of constructing a compact, point-free proof of the associativity of demonic composition of binary relations and its distributivity through demonic choice. In order to achieve this goal, a definition of demonic composition is proposed in which angelic composition is restricted by means of a so-called ‘monotype factor’. Monotype factors are characterised by a Galois connection similar to the Galois connection between composition and factorisation of binary relations. The identification of such a connection is argued to be highly conducive to the desired compactness of calculation.