Finite representability of semigroups with demonic refinement
Robin Hirsch, Jaš Šemrl · Algebra Universalis · 2021
Abstract The motivation for using demonic calculus for binary relations stems from the behaviour of demonic turing machines, when modelled relationally. Relational composition (; ) models sequential runs of two programs and demonic refinement ( $$\sqsubseteq $$ ⊑ ) arises from the partial order given by modeling demonic choice ( $$\sqcup $$ ⊔ ) of programs (see below for the formal relational definitions). We prove that the class $$R(\sqsubseteq , ;)$$ R ( ⊑ , ; ) of abstract $$(\le , \circ )$$ ( ≤ , ∘ ) structures isomorphic to a set of binary relations ordered by demonic refinement with composition cannot be axiomatised by any finite set of first-order $$(\le , \circ )$$ ( ≤ , ∘ ) formulas. We provide a fairly simple, infinite, recursive axiomatisation that defines $$R(\sqsubseteq , ;)$$ R ( ⊑ , ; ) . We prove that a finite representable $$(\le , \circ )$$ ( ≤ , ∘ ) 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 representation property holds for finite structures.