 |
 |
Selected Papers of the 19th International Conference on Relational and Algebraic Methods in Computer Science (RAMICS 2021)
Editors: Luigi Santocanale, Uli Fahrenberg
1. Relational Models for the Lambek Calculus with Intersection and Constants
We consider relational semantics (R-models) for the Lambek calculus extended with intersection and explicit constants for zero and unit. For its variant without constants and a restriction which disallows empty antecedents, Andreka and Mikulas (1994) prove strong completeness. We show that it fails without this restriction, but, on the other hand, prove weak completeness for non-standard interpretation of constants. For the standard interpretation, even weak completeness fails. The weak completeness result extends to an infinitary setting, for so-called iterative divisions (Kleene star under division). We also prove strong completeness results for product-free fragments.
2. Deciding Equations in the Time Warp Algebra
Join-preserving maps on the discrete time scale $\omega^+$, referred to as time warps, have been proposed as graded modalities that can be used to quantify the growth of information in the course of program execution. The set of time warps forms a simple distributive involutive residuated lattice -- called the time warp algebra -- that is equipped with residual operations relevant to potential applications. In this paper, we show that although the time warp algebra generates a variety that lacks the finite model property, it nevertheless has a decidable equational theory. We also describe an implementation of a procedure for deciding equations in this algebra, written in the OCaml programming language, that makes use of the Z3 theorem prover.
3. Varieties of unary-determined distributive $\ell$-magmas and bunched implication algebras
A distributive lattice-ordered magma ($d\ell$-magma) $(A,\wedge,\vee,\cdot)$ is a distributive lattice with a binary operation $\cdot$ that preserves joins in both arguments, and when $\cdot$ is associative then $(A,\vee,\cdot)$ is an idempotent semiring. A $d\ell$-magma with a top $\top$ is unary-determined if $x{\cdot} y=(x{\cdot}\!\top\wedge y)$ $\vee(x\wedge \top\!{\cdot}y)$. These algebras are term-equivalent to a subvariety of distributive lattices with $\top$ and two join-preserving unary operations $\mathsf p,\mathsf q$. We obtain simple conditions on $\mathsf p,\mathsf q$ such that $x{\cdot} y=(\mathsf px\wedge y)\vee(x\wedge \mathsf qy)$ is associative, commutative, idempotent and/or has an identity element. This generalizes previous results on the structure of doubly idempotent semirings and, in the case when the distributive lattice is a Heyting algebra, it provides structural insight into unary-determined algebraic models of bunched implication logic. We also provide Kripke semantics for the algebras under consideration, which leads to more efficient algorithms for constructing finite models. We find all subdirectly irreducible algebras up to cardinality eight in which $\mathsf p=\mathsf q$ is a closure operator, as well as all finite unary-determined bunched implication chains and map out the poset of join-irreducible varieties generated by them.
4. On Tools for Completeness of Kleene Algebra with Hypotheses
In the literature on Kleene algebra, a number of variants have been proposed which impose additional structure specified by a theory, such as Kleene algebra with tests (KAT) and the recent Kleene algebra with observations (KAO), or make specific assumptions about certain constants, as for instance in NetKAT. Many of these variants fit within the unifying perspective offered by Kleene algebra with hypotheses, which comes with a canonical language model constructed from a given set of hypotheses. For the case of KAT, this model corresponds to the familiar interpretation of expressions as languages of guarded strings. A relevant question therefore is whether Kleene algebra together with a given set of hypotheses is complete with respect to its canonical language model. In this paper, we revisit, combine and extend existing results on this question to obtain tools for proving completeness in a modular way. We showcase these tools by giving new and modular proofs of completeness for KAT, KAO and NetKAT, and we prove completeness for new variants of KAT: KAT extended with a constant for the full relation, KAT extended with a converse operation, and a version of KAT where the collection of tests only forms a distributive lattice.
5. Isolated Suborders and their Application to Counting Closure Operators
In this paper we investigate the interplay between isolated suborders and closures. Isolated suborders are a special kind of suborders and can be used to diminish the number of elements of an ordered set by means of a quotient construction. The decisive point is that there are simple formulae establishing relationships between the number of closures in the original ordered set and the quotient thereof induced by isolated suborders. We show how these connections can be used to derive a recursive algorithm for counting closures, provided the ordered set under consideration contains suitable isolated suborders.