{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,12,22]],"date-time":"2023-12-22T18:32:40Z","timestamp":1703269960296},"reference-count":14,"publisher":"Oxford University Press (OUP)","issue":"5","license":[{"start":{"date-parts":[[2021,9,15]],"date-time":"2021-09-15T00:00:00Z","timestamp":1631664000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022,9,15]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>Demonic composition, demonic refinement and demonic union are alternatives to the usual \u2018angelic\u2019 composition, angelic refinement (inclusion) and angelic (usual) union defined on binary relations. We first motivate both the angelic and the demonic via an analysis of the behaviour of non-deterministic programs, with the angelic associated with partial correctness and demonic with total correctness, both cases emerging from a richer algebraic model of non-deterministic programs incorporating both aspects. Zarecki\u012d has shown that the isomorphism class of algebras of binary relations under angelic composition and inclusion is finitely axiomatized as the class of ordered semigroups. The proof can be used to establish that the same axiomatization applies to binary relations under demonic composition and refinement, and a further modification of the proof can be used to incorporate a zero element representing the empty relation in the angelic case and the full relation in the demonic case. For the signature of angelic composition and union, it is known that no finite axiomatization exists, and we show the analogous result for demonic composition and demonic union by showing that the same axiomatization holds for both. We show that the isomorphism class of algebras of binary relations with the \u2018mixed\u2019 signature of demonic composition and angelic inclusion has no finite axiomatization. As a contrast, we show that the isomorphism class of partial algebras of binary relations with the partial operation of constellation product and inclusion (also a \u2018mixed\u2019 signature) is finitely axiomatizable.<\/jats:p>","DOI":"10.1093\/jigpal\/jzab026","type":"journal-article","created":{"date-parts":[[2021,8,12]],"date-time":"2021-08-12T11:20:49Z","timestamp":1628767249000},"page":"886-906","source":"Crossref","is-referenced-by-count":3,"title":["The Algebra of Non-deterministic Programs: Demonic Operations, Orders and Axioms"],"prefix":"10.1093","volume":"30","author":[{"given":"Robin","family":"Hirsch","sequence":"first","affiliation":[{"name":"Department of Computer Science, University College , London WC1E 6BTE, UK"}]},{"given":"Szabolcs","family":"Mikul\u00e1s","sequence":"additional","affiliation":[{"name":"Department of Computer Science and Information Systems , Birkbeck College, London WC1E 7HX, UK"}]},{"given":"Tim","family":"Stokes","sequence":"additional","affiliation":[{"name":"Department of Mathematics, University of Waikato , Hamilton 3240, New Zealand"}]}],"member":"286","published-online":{"date-parts":[[2021,9,15]]},"reference":[{"key":"2022092120485040800_ref1","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1007\/s00012-011-0142-3","article-title":"Axiomatizability of positive algebras of binary relations","volume":"66","author":"Andr\u00e9ka","year":"2011","journal-title":"Algebra Universalis"},{"key":"2022092120485040800_ref2","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1016\/0022-0000(81)90005-2","article-title":"On correct refinement of programs","volume":"23","author":"Back","year":"1981","journal-title":"Journal of Computer and System Sciences"},{"key":"2022092120485040800_ref3","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1017\/S096012950000030X","article-title":"Demonic operators and monotype factors","volume":"3","author":"Backhouse","year":"1993","journal-title":"Mathematical Structures in Computer Science"},{"key":"2022092120485040800_ref4","first-page":"16","article-title":"Relational specifications in algebraic methods in logic and in computer science (Warsaw, 1991)","volume":"28","author":"Berghammer","year":"1993","journal-title":"Banach Center Publications"},{"key":"2022092120485040800_ref5","doi-asserted-by":"crossref","first-page":"120","DOI":"10.1007\/11828563_8","article-title":"Demonic algebra with domain","volume-title":"Relations and Kleene Algebra in Computer Science","author":"de Carufel","year":"2006"},{"key":"2022092120485040800_ref6","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1080\/00927870902887096","article-title":"Restriction semigroups and inductive constellations","volume":"38","author":"Gould","year":"2009","journal-title":"Communications in Algebra"},{"key":"2022092120485040800_ref7","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1007\/s00012-017-0432-5","article-title":"Constellations and their relationship with categories","volume":"77","author":"Gould","year":"2017","journal-title":"Algebra Universalis"},{"key":"2022092120485040800_ref8","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1093\/jigpal\/jzi012","article-title":"The class of representable ordered monoids has a recursively enumerable, universal axiomatisation but it is not finitely axiomatisable","volume":"13","author":"Hirsch","year":"2005","journal-title":"Logic Journal of IGPL"},{"key":"2022092120485040800_ref9","volume-title":"Relation Algebras by Games","author":"Hirsch","year":"2002"},{"key":"2022092120485040800_ref10","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1093\/jigpal\/5.2.209","article-title":"Axiomatising various classes of relation and cylindric algebras","volume":"5","author":"Hirsch","year":"1997","journal-title":"Logic Journal of IGPL"},{"key":"2022092120485040800_ref11","doi-asserted-by":"crossref","DOI":"10.1007\/s00012-021-00719-4","article-title":"Axioms for signatures with domain and demonic composition","volume-title":"Algebra Universalis","author":"Hirsch","year":"2021"},{"key":"2022092120485040800_ref12","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/3-540-45442-X_14","article-title":"From kleene algebra to refinement algebra","volume-title":"Mathematics of Program Construction","author":"von Wright","year":"2002"},{"key":"2022092120485040800_ref13","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1016\/j.scico.2003.09.002","article-title":"Towards a refinement algebra","volume":"51","author":"von Wright","year":"2004","journal-title":"Science of Computer Programming"},{"key":"2022092120485040800_ref14","first-page":"48","article-title":"The representation of ordered semigroups by binary relations [Russian]","volume":"6","author":"Zarecki\u012d","year":"1959","journal-title":"Izvestiya Vysshikh Uchebnykh Zavedeni\u012d Matematika"}],"container-title":["Logic Journal of the IGPL"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/jigpal\/article-pdf\/30\/5\/886\/45878692\/jzab026.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/jigpal\/article-pdf\/30\/5\/886\/45878692\/jzab026.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,21]],"date-time":"2022-09-21T21:06:16Z","timestamp":1663794376000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/jigpal\/article\/30\/5\/886\/6370329"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,9,15]]},"references-count":14,"journal-issue":{"issue":"5","published-online":{"date-parts":[[2021,9,15]]},"published-print":{"date-parts":[[2022,9,15]]}},"URL":"https:\/\/doi.org\/10.1093\/jigpal\/jzab026","relation":{},"ISSN":["1367-0751","1368-9894"],"issn-type":[{"value":"1367-0751","type":"print"},{"value":"1368-9894","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2022,10]]},"published":{"date-parts":[[2021,9,15]]}}}