Demonic Lattices and Semilattices in Relational Semigroups with Ordinary\n Composition

Relation algebra and its reducts provide us with a strong tool for reasoning\nabout nondeterministic programs and their partial correctness. Demonic\ncalculus, introduced to model the behaviour of a machine where the demon is in\ncontrol of nondeterminism, has also provided us with an extension of that\nreasoning to total correctness.\n We formalise the framework for relational reasoning about total correctness\nin nondeterministic programs using semigroups with ordinary composition and\ndemonic lattice operations. We show that the class of representable demonic\njoin semigroups is not finitely axiomatisable and that the representation class\nof demonic meet semigroups does not have the finite representation property for\nits finite members.\n For lattice semigroups (with composition, demonic join and demonic meet) we\nshow that the representation problem for finite algebras is undecidable,\nmoreover the finite representation problem is also undecidable. It follows that\nthe representation class is not finitely axiomatisable, furthermore the finite\nrepresentation property fails.\n

Paper

Similar papers

© 2026 NYSGPT2525 LLC