Finite Representability of Semigroups with Demonic Refinement
share
Composition and demonic refinement ⊑ of binary relations are defined by (x, y)∈ (R;S) ∃ z((x, z)∈ R∧ (z, y)∈ S) R⊑ S (dom(S)⊆ dom(R) ∧ R_dom(S)⊆ S) where dom(S)={x:∃ y (x, y)∈ S} and R_dom(S) denotes the restriction of R to pairs (x, y) where x∈ dom(S). Demonic calculus was introduced to model the total correctness of non-deterministic programs and has been applied to program verification. We prove that the class R(⊑, ;) of abstract (≤, ∘) structures isomorphic to a set of binary relations ordered by demonic refinement with composition cannot be axiomatised by any finite set of first-order (≤, ∘) formulas. We provide a fairly simple, infinite, recursive axiomatisation that defines R(⊑, ;). We prove that a finite representable (≤, ∘) structure has a representation over a finite base. This appears to be the first example of a signature for binary relations with composition where the representation class is non-finitely axiomatisable, but where the finite representations for finite representable structures property holds.
READ FULL TEXT