The graph planarity testing problem asks whether we can draw an input graph in the plane in such a way that it is actually crossing-free (or embedded). In a seminal paper from 1974, Hopcroft and Tarjan gave a linear-time algorithm for this problem, initiating a long series of variations and generalizations. One of them is to make the target space more general, namely, to consider embeddings not into the plane, but into a more general surface. It is known that the problem of deciding the embeddability of a graph into a surface is NP-hard, but Mohar (1999) and Kawarabayashi, Mohar, and Reed (2008) gave algorithms that are linear in the size of the graph (and exponential in the genus of the surface).

In this talk, we consider an even more general case, in which the target space is a 2-dimensional simplicial complex (a topological space obtained from a graph by attaching a solid triangle to some of its 3-cycles). It turns out that this generalization encompasses some other well known problems, such as the crossing number problem and the planarity number problem (and their generalizations to surfaces). We give an algorithm that is quadratic in the size of the input graph (and exponential in the size of the input complex), independent from the previous algorithms to embed graphs into surfaces. The techniques mix graph theory (branchwidth, excluded grid theorem, dynamic programming) with topology (combinatorial maps of graphs on surfaces).

This is joint work with Thomas Magnard.

Preservation Theorems in first-order logic are a collection of results derived from classical Model Theory. These results establish a direct correspondence between the semantic properties of formulas and the syntactic constraints imposed on the language used to express them. However, studying these theorems becomes notably challenging when focusing on finite models, which is unfortunate given that the field of Finite Model Theory is better equipped to describe phenomena occurring in Computer Science. This thesis presents a systematic approach to investigating Preservation Theorems within the realm of Finite Model Theory. The traditional ad-hoc proofs are replaced with a theoretical framework that generalizes techniques based on locality, and introduces a topological presentation of preservation theorems called logically presented pre-spectral spaces. Introducing these topological spaces enables the development of a compositional theory for preservation theorems. Additionally, this thesis takes an initial stride towards systematically examining preservation theorems across inductively defined classes of finite structures. It accomplishes this by proving a generic fixed point theorem for a topological extension of logically presented pre-spectral spaces, specifically Noetherian spaces.

Details can be found here: https://www.irif.fr/~alopez/posts/2023-08-23.html

In this joint talk we will explore proof-theoretic methods to prove Craig and uniform interpolation in modal logics. Iris will start with an introduction of Craig and uniform interpolation in modal logics. Ian will continue with the presentation of existing proofs of Craig and uniform interpolation via sequent calculi for the modal logic K, as well as their mechanisation in Coq. While they are accessible, the understanding of these proofs will allow us to expand on the topic of Bílková’s pen-and-paper proof of uniform interpolation, which has been resisting mechanisation this far. The issues on the porting of the proof for K to GL will be explained. Finally, Iris will discuss the difficulties of adopting the sequent-style proof of uniform interpolation to hypersequent-style calculi. We will discuss joint work with Raheleh Jalali and Roman Kuznets in which uniform interpolation is proved for extensions of modal logic K5 via hypersequent-like calculi.

Hierarchical clustering is a popular technique for organizing data as a rooted tree structure that simultaneously clusters data at multiple levels of granularity. A well-studied recent objective function views the input as a weighted graph with edges indicating similarity between the data points, and focuses on finding a tree that minimizes the cost of hierarchical partitioning. The resulting optimization problem is NP-hard, and previous algorithms for approximating this objective require at least linear time/space. In this talk, we will consider algorithms for hierarchical clustering that use sublinear resources (space, time, and communication). 

Specifically, we will present sublinear algorithms for hierarchical clustering in the streaming model (space), in the query model (time), and in the MPC model (communication). At the core of our algorithmic results is a connection between hierarchical clustering and a suitably relaxed notion of cut sparsifiers of graphs that lends itself to efficient sublinear algorithms. We complement our algorithmic results by establishing nearly matching lower bounds that rule out algorithms with better performance guarantees in each of these models.

This is joint work with Arpit Agarwal, Huan Li, and Prathamesh Patil.

Ferenczi and Mauduit showed in 1997 that a number represented over an integer base by a Sturmian sequence of digits is transcendental. In this talk we generalise this result to hold for all algebraic number base b of absolute value strictly greater than one. More generally, for a given base b and given irrational number θ, we prove rational linear independence of the set comprising 1 together with all numbers of the above form whose associated digit sequences have slope θ.

We give an application of our main result to the theory of dynamical systems. We show that for a Cantor set C arising as the set of limit points of a contracted rotation f on the unit interval, where f is assumed to have an algebraic slope, all elements of C except its endpoints 0 and 1 are transcendental.

This is joint work with Florian Luca and Joel Ouaknine.

Abstract:

Applications of graph transformation (GT) systems often require control structures that can be used to direct GT processes. Most existing GT tools follow a stateful computational model, where a single graph is repeatedly modified “in-place” when GT rules are applied. The implementation of control structures in such tools is not trivial. Common challenges include dealing with the non-determinism inherent to rule application and transactional constraints when executing compositions of GTs, in particular atomicity and isolation. The complexity of associated transaction mechanisms and rule application search algorithms (e.g., backtracking) complicates the definition of a formal foundation for these control structures. Compared to these stateful approaches, functional graph rewriting presents a simpler (stateless) computational model, which simplifies the definition of a formal basis for (functional) GT control structures. In this talk, I will discuss the “Graph Transformation control Algebra” (GTA) as a foundation for functional graph rewriting and its application in the tool GrapeVine.

Zoom meeting registration link

YouTube live stream