Speaker: Balder ten Cate
Date and Time: Thursday, December 5th 2024, 16:30-18:00
Venue: ILLC Seminar Room F1.15, Science Park 107.
Title: Preservation theorems for algebras of binary relations
Abstract. Several areas of computer science (databases, knowledge representation, program verification, reasoning about knowledge and actions) feature logical languages in which one can construct complex binary relations from basic ones, through a certain set of operations (e.g., composition, intersection, inverse, …). Examples include Kleene algebra with tests, propositional dynamic logics, Boolean modal logics, various query languages for graph databases, Tarksi’s relation algebra. Underlying each of these is a “binary relation algebra” , i.e., an algebraic signature consisting of finitely many operations on binary relations. The specific set of operators, in each of the aforementioned languages, is typically chosen as a compromise between computational complexity and expressive power and/or may be based on a requirement to respect certain natural structural invariances (e.g., bisimulation).
Preservation theorems link semantics properties of formulas to their syntactic shape. The most famous example is the Łoś-Tarski theorem, which states that a first-order formula is preserved under induced substructures (i.e., remains true if one passes from a structure to an induced substructure) if and only if it can be written without using any existential quantifiers (assuming negation normal form). Another famous example is the Van Benthem characterization theorem, which states that a first-order formula φ(x) is preserved by bisimulations if and only if it can be written as a modal formula.
In this talk, we will review some recent results (both positive and negative) about the existence of preservation theorems for algebras of binary relations. (Algebraically, the results I will present can be equivalently viewed as addressing the question whether certain clones admit a finite set of generators).
Specifically, I will discuss results from a joint paper with Bart Bogaerts, Brett McLean, and Jan van den Bussche (LMCS 2024) as well as from a joint paper with Tobias Kappe (POPL 2025).