Home

We present a generalisation of the theory of quantitative algebras of Mardare, Panangaden and Plotkin where (i) the carriers of quantitative algebras are not restricted to be metric spaces and can be arbitrary fuzzy relations or generalised metric spaces, and (ii) the interpretations of the algebraic operations are not required to be nonexpansive. Our main results include: a novel sound and complete proof system, the proof that free quantitative algebras always exist, the proof of strict monadicity of the induced Free-Forgetful adjunction, the result that all monads (on fuzzy relations) that lift finitary monads (on sets) admit a quantitative equational presentation.

---

Vertex Integrity is a graph measure which sits squarely between two more well-studied notions, namely vertex cover and tree-depth, and that has recently gained attention as a structural graph parameter. In this paper we investigate the algorithmic trade-offs involved with this parameter from the point of view of algorithmic meta-theorems for First-Order (FO) and Monadic Second Order (MSO) logic. Our positive results are the following: (i) given a graph $G$ of vertex integrity $k$ and an FO formula $\phi$ with $q$ quantifiers, deciding if $G$ satisfies $\phi$ can be done in time $2^{O(k^2q+q\log q)}+n^{O(1)}$; (ii) for MSO formulas with $q$ quantifiers, the same can be done in time $2^{2^{O(k^2+kq)}}+n^{O(1)}$. Both results are obtained using kernelization arguments, which pre-process the input to sizes $2^{O(k^2)}q$ and $2^{O(k^2+kq)}$ respectively. The complexities of our meta-theorems are significantly better than the corresponding meta-theorems for tree-depth, which involve towers of exponentials. However, they are worse than the roughly $2^{O(kq)}$ and $2^{2^{O(k+q)}}$ complexities known for corresponding meta-theorems for vertex cover. To explain this deterioration we present two formula constructions which lead to fine-grained complexity lower bounds and establish that the dependence of our meta-theorems on $k$ is the best possible. More precisely, we show that it is not possible to decide FO formulas with $q$ quantifiers in time $2^{o(k^2q)}$, and that there exists a […]

---

Algebraic effects & handlers have become a standard approach for side-effects in functional programming. Their modular composition with other effects and clean separation of syntax and semantics make them attractive to a wide audience. However, not all effects can be classified as algebraic; some need a more sophisticated handling. In particular, effects that have or create a delimited scope need special care, as their continuation consists of two parts-in and out of the scope-and their modular composition introduces additional complexity. These effects are called scoped and have gained attention by their growing applicability and adoption in popular libraries. While calculi have been designed with algebraic effects & handlers built in to facilitate their use, a calculus that supports scoped effects & handlers in a similar manner does not yet exist. This work fills this gap: we present $\lambda_{\mathit{sc}}$, a calculus with native support for both algebraic and scoped effects & handlers. It addresses the need for polymorphic handlers and explicit clauses for forwarding unknown scoped operations to other handlers. Our calculus is based on Eff, an existing calculus for algebraic effects, extended with Koka-style row polymorphism, and consists of a formal grammar, operational semantics, a (type-safe) type-and-effect system and type inference. We demonstrate $\lambda_{\mathit{sc}}$ on a range of examples.

---

The regular spanners (characterised by vset-automata) are closed under the algebraic operations of union, join and projection, and have desirable algorithmic properties. The core spanners (introduced by Fagin, Kimelfeld, Reiss, and Vansummeren (PODS 2013, JACM 2015) as a formalisation of the core functionality of the query language AQL used in IBM's SystemT) additionally need string-equality selections and it has been shown by Freydenberger and Holldack (ICDT 2016, Theory of Computing Systems 2018) that this leads to high complexity and even undecidability of the typical problems in static analysis and query evaluation. We propose an alternative approach to core spanners: by incorporating the string-equality selections directly into the regular language that represents the underlying regular spanner (instead of treating it as an algebraic operation on the table extracted by the regular spanner), we obtain a fragment of core spanners that, while having slightly weaker expressive power than the full class of core spanners, arguably still covers the intuitive applications of string-equality selections for information extraction and has much better upper complexity bounds of the typical problems in static analysis and query evaluation.

---

Can the $\lambda$-calculus be considered a reasonable computational model? Can we use it for measuring the time $\textit{and}$ space consumption of algorithms? While the literature contains positive answers about time, much less is known about space. This paper presents a new reasonable space cost model for the $\lambda$-calculus, based on a variant over the Krivine abstract machine. For the first time, this cost model is able to accommodate logarithmic space. Moreover, we study the time behavior of our machine and show how to transport our results to the call-by-value $\lambda$-calculus.

---