Showing 1–5 of 5 results for author: Mikulas, S

Finite Model Properties for Residuated Semigroups

Authors: Szabolcs Mikulás

Abstract: We have a quick look at various finite model properties for residuated semigroups. In particular, we solve Problem 19.17 from Relation Algebras by Games by Hirsch and Hodkinson. We have a quick look at various finite model properties for residuated semigroups. In particular, we solve Problem 19.17 from Relation Algebras by Games by Hirsch and Hodkinson. △ Less

Submitted 21 November, 2022; originally announced November 2022.

MSC Class: 03G25

The algebra of non-deterministic programs: demonic operators, orders and axioms

Authors: Robin Hirsch, Szabolcs Mikulás, Tim Stokes

Abstract: Demonic composition, demonic refinement and demonic union are alternatives to the usual "angelic" composition, angelic refinement (inclusion) and angelic (usual) union defined on binary relations. We first motivate both the angelic and demonic via an analysis of the behaviour of non-deterministic programs, with the angelic associated with partial correctness and demonic with total correctness, bot… ▽ More Demonic composition, demonic refinement and demonic union are alternatives to the usual "angelic" composition, angelic refinement (inclusion) and angelic (usual) union defined on binary relations. We first motivate both the angelic and 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. Zareckii has shown that the isomorphism class of algebras of binary relations under angelic composition and inclusion is finitely axiomatised as the class of ordered semigroups. The proof can be used to establish that the same axiomatisation 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 axiomatisation exists, and we show the analogous result for demonic composition and demonic union by showing that the same axiomatisation holds for both. We show that the isomorphism class of algebras of binary relations with the "mixed" signature of demonic composition and angelic inclusion has no finite axiomatisation. 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 "mixed" signature) is finitely axiomatisable. △ Less

Submitted 13 January, 2021; v1 submitted 25 September, 2020; originally announced September 2020.

Domain and range for angelic and demonic compositions

Authors: Marcel Jackson, Szabolcs Mikulas

Abstract: We give finite axiomatizations for the varieties generated by representable domain--range algebras when the semigroup operation is interpreted as angelic or demonic composition, respectively. We give finite axiomatizations for the varieties generated by representable domain--range algebras when the semigroup operation is interpreted as angelic or demonic composition, respectively. △ Less

Submitted 30 October, 2018; originally announced November 2018.

MSC Class: 08A02; ACM Class: F.3.1; F.3.2

Journal ref: Journal of Logical and Algebraic Methods in Programming 103 (2019) 62-78

The finite representation property for composition, intersection, domain and range

Authors: Brett McLean, Szabolcs Mikulás

Abstract: We prove that the finite representation property holds for representation by partial functions for the signature consisting of composition, intersection, domain and range and for any expansion of this signature by the antidomain, fixset, preferential union, maximum iterate and opposite operations. The proof shows that, for all these signatures, the size of base required is bounded by a double-expo… ▽ More We prove that the finite representation property holds for representation by partial functions for the signature consisting of composition, intersection, domain and range and for any expansion of this signature by the antidomain, fixset, preferential union, maximum iterate and opposite operations. The proof shows that, for all these signatures, the size of base required is bounded by a double-exponential function of the size of the algebra. This establishes that representability of finite algebras is decidable for all these signatures. We also give an example of a signature for which the finite representation property fails to hold for representation by partial functions. △ Less

Submitted 4 March, 2016; v1 submitted 9 March, 2015; originally announced March 2015.

Comments: 15 pages. Results extended from antidomain-containing signatures to domain-containing signatures

Journal ref: International Journal of Algebra and Computation, Volume 26, Issue 6 (2016) 1199-1216

The algebra of functions with antidomain and range

Authors: Robin Hirsch, Marcel Jackson, Szabolcs Mikulás

Abstract: We give complete, finite quasiequational axiomatisations for algebras of unary partial functions under the operations of composition, domain, antidomain, range and intersection. This completes the extensive programme of classifying algebras of unary partial functions under combinations of these operations. We look at the complexity of the equational theories and provide a nondeterministic polynomi… ▽ More We give complete, finite quasiequational axiomatisations for algebras of unary partial functions under the operations of composition, domain, antidomain, range and intersection. This completes the extensive programme of classifying algebras of unary partial functions under combinations of these operations. We look at the complexity of the equational theories and provide a nondeterministic polynomial upper bound. Finally we look at the problem of finite representability and show that finite algebras can be represented as a collection of unary functions over a finite base set provided that intersection is not in the signature. △ Less

Submitted 15 October, 2014; originally announced October 2014.

MSC Class: 20M20; 03G15; 08A02