Oberseminar (SoSe 2025)

Inquisitive first-order logic (InqFOL) extends classical first-order logic by inqusitive disjunction and inquisitive existential quantification which can be used to model questions, using sets of FO-models as semantics. Unfortunately, an existing natural deduction system by Ciardelli is not yet proven to be complete. Consequently, it is quite interesting to look at bounded InqFOL which restricts the number of models to a finite set, thus allowing for an extension of the natural deduction system which is sound and complete, but its definition depends on the signature. Contrary, a sequent calculus by Litak/Sano uses labels to capture this boundedness property, avoiding the signature-dependency.

In this talk, we give an introduction to (bounded) InqFOL and our formalization using the proof assistant Rocq which also implements a slightly adapted version of the sequent calculus by Litak/Sano.
We present various techniques used during the formalization process which might be useful in similar projects.

Nominal sets can be used to model data languages, which are languages over infinite alphabets. Regular nominal automata with name allocation (RNNA) first produce bar strings containing bound atoms that can be renamed under alpha-equivalence. Under local freshness semantics, the language generated by such automata contains all alpha-equivalent bar strings with the binders removed.

In this talk, we present a coalgebraic definition for the trace semantics of RNNA in the framework of graded semantics. First, we define a general syntax and semantics for nominal algebra which can be used to define graded algebraic theories over nominal sets. It can then be shown that every such graded theory induces a graded monad over the category of nominal sets. We proceed provide an explicit description of a graded theory that can be used to capture exactly the trace semantics under local freshness.

Gabbay and Pitts introduced nominal sets as „a new approach to syntax and variable binding“: a set-based semantics for algebras with names and binding operations such as the lambda calculus. Fiore, Turi and Plotkin showed slightly earlier how to also model the operational semantics of the lambda calculus (beta reduction) by combining the abstraction operator with a monoidal structure modelling substitution — something missing for nominal sets.

We fill this surprisingly long-standing gap by introducing a new simple right-closed substitution product on nominal sets. To compare it with the Turi-Fiore-Plotkin approach we first recall and compare various existing and new „nominal“ set-based models for sets with names with the (pre-)sheaf approach and present a uniform view as well as the relations between them. This allows us to develop a general view of name-based substitution: a monidal structure on presheaves over „context“-categories induces by the graded monad on presheafs naturally arising from Day-convolution-powers, instatiation to known instances (classic and „linear“ presheaves), but also „affine“ and „relevant“ presheaves and their nominal counterparts: classic, renaming, linear and relevant nominal sets with an additional strictness option for maps.

The paper „Sorting with Bialgebras and Distributive Laws“ by Hinze et al. uses the framework of bialgebraic semantics to define sorting algorithms. From distributive laws between functors they construct pairs of sorting algorithms using both folds and unfolds. Pairs of sorting algorithms arising this way include insertion/selection sort and quick/tree sort. We extend this work to define intrinsically correct variants in cubical Agda. Our key idea is to index our data types by multisets, which concisely captures that a sorting algorithm terminates with an ordered permutation of its input list. In particular, all coalgebras for the respective base functors are recursive. By lifting bialgebraic semantics to the indexed setting, we obtain the correctness of sorting algorithms purely from the distributive law.

Data languages, which are languages over an infinite alphabet, are essential for the sequential representation of data. Commonly, the same piece of data can have multiple equivalent representations that share the same structure but differ in the names they carry.

To specify these equivalences, binders have been introduced into these languages. Binders accompany letters and allow for their renaming. This concept is evident in various languages such as bar languages, dynamic sequences, and bracket algebra. In bar languages, binders have infinite scope to the right, deallocating letters implicitly. In contrast, dynamic sequences and bracket algebra use properly scoped binders with explicit deallocation through parentheses.

Following the introduction of deallocation languages, incorporating deallocating binders into bar-style languages, and the exploration of a novel automaton model for them, we present our next approach to bridge the gap between our languages, equivalence relations, automaton model, and coalgebraic representation. This approach introduces unknown letters and transitions to provide a concise and meaningful semantics.

In this talk, we will examine the issues with our preceding ideas that led to the development of this new approach. We will introduce our new semantics and discuss how we plan to use it to overcome the challenges we currently face in our constructions.

In preparation for IJCAI’25: Fuzzy description logics serve the representation of vague knowledge, typically letting concepts take truth degrees in the unit interval. Expressiveness, logical properties, and complexity vary strongly with the choice of propositional base. The Łukasiewicz propositional base is generally perceived to have preferable logical properties but often entails high complexity or even undecidability. Contrastingly, the less expressive Zadeh propositional base comes with low complexity but entails essentially no change in logical behaviour compared to the classical case. To strike a balance between these poles, we propose non-expansive fuzzy ALC, in which the Zadeh base is extended with Łukasiewicz connectives where one side is restricted to be a rational constant, that is, with constant shift operators. This allows, for instance, modelling dampened inheritance of properties along roles. We present an unlabelled tableau method for non-expansive fuzzy ALC, which allows reasoning over general TBoxes in ExpTime like in two-valued ALC.

In preparation for LICS’25: Behavioural conformances – e.g. behavioural equivalences, distances, preorders – on a wide range of system types (non-deterministic, probabilistic, weighted etc.) can be dealt with uniformly in the paradigm of universal coalgebra. One of the most commonly used constructions for defining behavioural distances on coalgebras arises as a generalization of the well-known Wasserstein metric. In this construction, couplings of probability distributions are replaced with couplings of more general objects, depending on the functor describing the system type. In many cases, however, the set of couplings of two functor elements is empty, which causes such elements to have infinite distance even in situations where this is not desirable. We propose an approach to defining behavioural distances and preorders based on a more liberal notion of coupling where the coupled elements are matched laxly rather than on-the-nose. We thereby substantially broaden the range of behavioural conformances expressible in terms of couplings, covering, e.g., refinement of modal transition systems and behavioural distance on metric labelled Markov chains.

In preparation for LICS’25: Formal languages over infinite alphabets serve as abstractions of structures and processes carrying data. Automata models over infinite alphabets, such as classical register automata or, equivalently, nominal orbit-finite automata, tend to have computationally hard or even undecidable reasoning problems unless stringent restrictions are imposed on either the power of control or the number of registers. This has been shown to be ameliorated in automata models with name allocation such as regular nondeterministic nominal automata, which allow for deciding language inclusion in elementary complexity even with unboundedly many registers while retaining a reasonable level of expressiveness. In the present work, we demonstrate that elementary complexity survives under extending the power of control to alternation: We introduce regular alternating nominal automata (RANAs), and show that their non-emptiness and inclusion problems have elementary complexity even when the number of registers is unbounded. Moreover, we show that RANAs allow for nearly complete de-alternation, specifically de-alternation up to a single deadlocked universal state. As a corollary to our results, we improve the complexity of model checking for a flavour of Bar-μTL, a fixed-point logic with name allocation over finite data words, by one exponential level.