arXiv subjects

Jaš Šemrl

Publications and source records attributed to Jaš Šemrl.

6 recordsLinked to original sources

arXiv2024

Minimal signatures with undecidability of representability by binary relations

A semigroup of binary relations (under composition) on a set $X$ is \emph{complemented} if it is closed under the taking of complements within $X\times X$. We resolve a 1991 problem of Boris Schein by showing that the class of finite unary semigroups that are representable as complemented semigroups of binary relations is undecidable, so composition with complementation forms a minimal subsignature of Tarski's relation algebra signature that has undecidability of representability. In addition we prove similar results for semigroups of binary relations endowed with unary operations returning the kernel and cokernel of a relation. We generalise to signatures which may include arbitrary, definable operations and provide a chain of weaker and weaker signatures, each definable in the previous signature, each having undecidability of representability, but whose limit signature includes composition only, which corresponds to the well known, decidable and finitely axiomatised variety of semigroups. All these results are also proved for representability as binary relations over a finite set.

math.LO↗

arXiv2023

Representable and diagonally representable weakening relation algebras

A binary relation defined on a poset is a weakening relation if the partial order acts as a both-sided compositional identity. This is motivated by the weakening rule in sequent calculi and closely related to models of relevance logic. For a fixed poset the collection of weakening relations is a subreduct of the full relation algebra on the underlying set of the poset. We present a two-player game for the class of representable weakening relation algebras akin to that for the class of representable relation algebras. This enables us to define classes of abstract weakening relation algebras that approximate the quasivariety of representable weakening relation algebras. We give explicit finite axiomatisations for some of these classes. We define the class of diagonally representable weakening relation algebras and prove that it is a discriminator variety. We also provide explicit representations for several small weakening relation algebras.

cs.LO↗

arXiv2021

Finite Representation Property for Relation Algebra Reducts

The decision problem of membership in the Representation Class of Relation Algebras (RRA) for finite structures is undecidable. However, this does not hold for many Relation Algebra reduct languages. Two well known properties that are sufficient for decidability are the Finite Axiomatisability (FA) of the representation class and the Finite Representation Property (FRP). Furthermore, neither of the properties is stronger that the other, and thus, neither is also a necessary condition. Although many results are known in the area of FA, the FRP remains unknown for the majority of the reduct languages. Here we conjecture that the FRP fails for a Relation Algebra reduct if and only if it contains both composition and negation, or both composition and meet. We then show the right-to-left implication of the conjecture holds and present preliminary results that suggest the left-to-right implication.

math.LO↗

arXiv2021

Domain Range Semigroups and Finite Representations

Relational semigroups with domain and range are a useful tool for modelling nondeterministic programs. We prove that the representation class of domain-range semigroups with demonic composition is not finitely axiomatisable. We extend the result for ordered domain algebras and show that any relation algebra reduct signature containing domain, range, converse, and composition, but no negation, meet, nor join has the finite representation property. That is any finite representable structure of such a signature is representable over a finite base. We survey the results in the area of the finite representation property.

cs.LO↗

arXiv2021

Demonic Lattices and Semilattices in Relational Semigroups with Ordinary Composition

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

cs.LO↗

arXiv2020

Finite Representability of Semigroups with Demonic Refinement

Composition and demonic refinement $\sqsubseteq$ of binary relations are defined by \begin{align*} (x, y)\in (R;S)&\iff \exists z((x, z)\in R\wedge (z, y)\in S) R\sqsubseteq S&\iff (dom(S)\subseteq dom(R) \wedge R\restriction_{dom(S)}\subseteq S) \end{align*} where $dom(S)=\{x:\exists y (x, y)\in S\}$ and $R\restriction_{dom(S)}$ denotes the restriction of $R$ to pairs $(x, y)$ where $x\in 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(\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.

cs.LO↗