Mathematical Structures in Computer Science

Research Article

Demonic operators and monotype factors

Roland Backhousea1 and Jaap van der Woudea1

a1 Department of Mathematics and Computing Science, Eindhoven University of Technology, P.O. Box 513, 5600 MB Eindhoven, The Netherlands

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.

(Received April 24 1992)

(Revised January 29 1993)