Robin Hirsch

Demonic operators

Joint work with Szabolcs Mikulás and Tim Stokes

Given two binary relations r, s we may define their demonic composition

r*s = {(x, y): ∃z ((x, z)∈r and (z, y)∈s) and ∀w ((x, w)∈r → w∈dom(s)}.

If s is left-total, or if r is a partial function, then demonic composition coincides with ordinary composition. One motivation comes from reasoning about total correctness for non-deterministic programs - the demonic composition r*s includes a pair (x, y) of states, if there is a computation of r followed by a computation of s going from x to y, but moreover every computation of r from x leads to a state where s can be executed.

A second demonic operator is demonic join. The demonic join of two binary relations r, s is the binary relation whose domain is the intersection of the domains of r and s, and is the same as r∪s when left-restricted to this domain. Demonic refinement may be defined from demonic join. We will look for finite axiomatisations of the representation classes of various signatures including demonic operators and relations.

For example, we show that the representation class for the signature with demonic composition and ordinary inclusion is not finitely axiomatisable, whereas the representation class for the signature with demonic composition and demonic refinement is finitely axiomatisable. I may also consider demonic signatures including the domain operator.