Home

We focus on formulae $\exists X.\, φ(\vec{Y}, X)$ of monadic second-order logic over the full binary tree, such that the witness $X$ is a well-founded set. The ordinal rank $\mathrm{rank}(X) < ω_1$ of such a set $X$ measures its depth and branching structure. We search for the least upper bound for these ranks, and discover the following dichotomy depending on the formula $φ$. Let $\mathrm{rank}(φ)$ be the minimal ordinal such that, whenever an instance $\vec{Y}$ satisfies the formula, there is a witness $X$ with $\mathrm{rank}(X) \leq \mathrm{rank}(φ)$. Then $\mathrm{rank}(φ)$ is either strictly smaller than $ω^2$ or it reaches the maximal possible value $ω_1$. Moreover, it is decidable which of the cases holds. The result has potential for applications in a variety of ordinal-related problems, in particular it entails a result about the closure ordinal of a fixed-point formula.

---

Many-valued models generalise the structures from classical model theory by defining truth values for a model with an arbitrary algebra. Just as algebraic varieties provide semantics for many non-classical propositional logics, models defined over algebras in a variety provide the semantics for the corresponding non-classical predicate logics. In particular, models defined over varieties of residuated lattices represent the model theory for first-order substructural logics. In this paper we study the extent to which the classical locality theorems from Hanf and Gaifman hold true in the residuated lattice setting. We demonstrate that the answer is sensitive both to how locality is understood in the generalised context and the behaviour of the truth-defining algebra. In the case of Hanf's theorem, we will show that the theorem fails for the natural understanding of local neighbourhoods, but is recoverable with an alternative understanding for well-connected residuated lattices. For Gaifman's theorem, rather than consider Gaifman normal forms directly we focus on the main lemma of the theorem from textbook proofs - that models which satisfy the same basic local sentences are elementarily equivalent. We prove that for a number of different understandings of locality, provided the algebra is well-behaved enough to express locality in its syntax, this main lemma can be recovered. In each case we will see the importance of an order-interpreting connective which creates a link […]

---

Modal separability for modal fixpoint formulae is the problem to decide for two given modal fixpoint formulae $φ,φ'$ whether there is a modal formula $ψ$ that separates them, in the sense that $φ\modelsψ$ and $ψ\models\negφ'$. We study modal separability and its special case modal definability over various classes of models, such as arbitrary models, finite models, trees, and models of bounded outdegree. Our main results are that modal separability is PSpace-complete over words, that is, models of outdegree $\leq 1$, ExpTime-complete over unrestricted and over binary models, and TwoExpTime-complete over models of outdegree bounded by some $d\geq 3$. Interestingly, this latter case behaves fundamentally different from the other cases also in that modal logic does not enjoy the Craig interpolation property over this class. Motivated by this we study also the induced interpolant existence problem as a special case of modal separability, and show that it is coNExpTime-complete and thus harder than validity in the logic. Besides deciding separability, we also provide algorithms for the effective construction of separators. Finally, we consider in a case study the extension of modal fixpoint formulae by graded modalities and investigate separability by modal formulae and graded modal formulae.

---

We study the question of which visibly pushdown languages (VPLs) are in the complexity class $\mathsf{AC}^0$ and how to effectively decide this question. Our contribution is to introduce a particular subclass of one-turn VPLs, called intermediate VPLs, for which the raised question is entirely unclear: to the best of our knowledge our research community is unaware of containment or non-containment in $\mathsf{AC}^0$ for any language in our newly introduced class. Our main result states that there is an algorithm that, given a visibly pushdown automaton, correctly outputs exactly one of the following: that its language $L$ is in $\mathsf{AC}^0$, some $m\geq 2$ such that $L$ is $\mathsf{ACC}^0(m)$-hard (implying that $L$ is not in $\mathsf{AC}^0$), or a finite disjoint union of intermediate VPLs that $L$ is constant-depth equivalent to. In the latter of the three cases one can moreover effectively compute $k,l\in\mathbb{N}_{>0}$ with $k\not=l$ such that the concrete intermediate VPL $L(S\rightarrow \varepsilon\mid a c^{k-1} S b_1\mid ac^{l-1}Sb_2)$ is constant-depth reducible to the language $L$. Due to their particular nature we conjecture that either all intermediate VPLs are in $\mathsf{AC}^0$ or all are not. As a corollary of our main result we obtain that in case the input language is a visibly counter language our algorithm can effectively determine if it is in $\mathsf{AC}^0$ - hence our main result generalizes a result by Krebs et al. stating that it is decidable if […]

---

Call-by-need evaluation for the lambda-calculus can be seen as merging the best of call-by-name and call-by-value, namely the wise erasing behaviour of the former and the wise duplicating behaviour of the latter. To better understand how duplication and erasure can be combined, we design a degenerated calculus, dubbed call-by-silly, that is symmetric to call-by-need in that it merges the worst of call-by-name and call-by-value, namely silly duplications by-name and silly erasures by-value. We validate the design of the call-by-silly calculus via rewriting properties and multi types. In particular, we mirror the main theorem about call-by-need -- that is, its operational equivalence with call-by-name -- showing that call-by-silly and call-by-value induce the same contextual equivalence. This fact shows the blindness with respect to efficiency of call-by-value contextual equivalence. We also define a call-by-silly strategy and a call-by-silly abstract machine implementing the strategy. Moreover, we measure the number of steps taken by the strategy via tight multi types. Lastly, we prove that the call-by-silly strategy computes evaluation sequences of maximal length in the calculus.

---