Finite Representability of Semigroups with Demonic Refinement

DOI10.1007/S00012-021-00718-5MaRDI QIDQ6349131arXivFDO

Authors Robin Hirsch, Jaš Šemrl

Publication date 15 September 2020

Published in arXiv

Full work available at URL https://doi.org/10.1007/S00012-021-00718-5

Mathematics Subject Classification ID

Cylindric and polyadic algebras; relation algebras (03G15) Ordered semigroups and monoids (06F05)

arXiv classification

cs.LOmath.LO

Abstract: Composition and demonic refinement $sqsubseteq$ of binary relations are defined by �egin{align*} (x, y)in (R;S)&iff exists z((x, z)in Rwedge (z, y)in S) Rsqsubseteq S&iff (dom(S)subseteq dom(R) wedge R estriction_{dom(S)}subseteq S) end{align*} where $dom(S)=x:existsy(x,y)inS$ and $Restrictio{n}_{dom(S)}$ denotes the restriction of $R$ to pairs $(x,y)$ where $xindom(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(sqsubseteq,;)$ of abstract $(leq,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 $(leq,circ)$ formulas. We provide a fairly simple, infinite, recursive axiomatisation that defines $R(sqsubseteq,;)$. We prove that a finite representable $(leq,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 representations for finite representable structures property holds.

This page was built for publication: Finite Representability of Semigroups with Demonic Refinement

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6349131)