Seminars

TBA

Title: Search-Based Regular Expression Inference on a GPU

Abstract: Regular expression inference (REI) is a supervised machine
learning and program synthesis problem that takes a cost metric for regular
expressions, and positive and negative examples of strings as input. It
outputs a regular expression that is precise (i.e., accepts all positive
and rejects all negative examples), and minimal w.r.t. to the cost metric.
We present a novel algorithm for REI over arbitrary alphabets that is
enumerative and trades off time for space. Our main algorithmic idea is to
implement the search space of regular expressions succinctly as a
contiguous matrix of bitvectors. Collectively, the bitvectors represent, as
characteristic sequences, all sub-languages of the infix-closure of the
union of positive and negative examples. Mathematically, this is a semiring
of (a variant of) formal power series. Infix-closure enables bottom-up
compositional construction of larger from smaller regular expressions using
the operations of our semiring. This minimises data movement and
data-dependent branching, hence maximises data-parallelism. In addition,
the infix-closure remains unchanged during the search, hence search can be
staged: first pre-compute various expensive operations, and then run the
compute intensive search process. We provide two C++ implementations, one
for general purpose CPUs and one for Nvidia GPUs (using CUDA). We benchmark
both on Google Colab Pro: the GPU implementation is on average over 1000x
faster than the CPU implementation on the hardest benchmarks.

Joint work with Mojtaba Valizadeh

Download: martinfriedrichberger.net/pldi2023.html

Speaker: Lê Thành Dũng Nguyễn, aka “Tito” — nguyentito.eu/

Title: Polyregular functions: some recent developments

Abstract:
The class of polyregular functions is composed of the string-to-string functions computed by pebble transducers. While this machine model (which extends two-way finite transducers) is two decades old, several alternative characterizations of polyregular functions have been discovered recently [Bojańczyk 2018; Bojańczyk, Kiefer & Lhote 2019], demonstrating their canonicity. The name comes from the polynomial bound on the growth rate of these functions: |f(w)| = |w|^O(1) where |w| is the length of the string w.

In this talk, after recalling this context, I will present some subsequent developments in which I have been involved:
* the subclass of comparison-free polyregular (or “polyblind”) functions, definable through a natural restriction of pebble transducers, which Pierre Pradic and I actually discovered while studying a linear λ-calculus;
* some results that either relate the growth rate of a polyregular function (comparison-free or not) to the “resources” needed to compute it, or show that there is no such relationship.

Speaker: Rémi Morvan — www.morvan.xyz/

Titre: Approximation and Semantic Tree-width of Conjunctive Regular Path Queries

Abstract:
We show that the problem of whether a query is equivalent to a query of tree-width k is decidable, for the class of Unions of Conjunctive Regular Path Queries with two-way navigation (UC2RPQs). A previous result by Barceló, Romero, and Vardi has shown decidability for the case k=1, and here we show that decidability in fact holds for any arbitrary k>1. The algorithm is in 2ExpSpace, but we show that the complexity drops to the second level of the polynomial hierarchy for a restricted but practically relevant case of queries obtained by only allowing simple regular expressions.
We also investigate the related problem of approximating a UC2RPQ by queries of small tree-width. We exhibit an algorithm which, for any fixed number k, builds the maximal under-approximation of tree-width k of a UC2RPQ. The maximal under-approximation of tree-width k of a query q is a query q' of tree-width k which is contained in q in a maximal and unique way, that is, such that for every query q'' of tree-width k, if q'' is contained in q then q'' is also contained in q'. Joint work with Diego Figueira.

Speaker: Pierre Pradic — perso.ens-lyon.fr/pierre.pradic/

Title: Synthesizing Nested Relational Queries from Implicit Specifications

Abstract:
Derived datasets can be defined implicitly or explicitly. An implicit
definition (of dataset O in terms of datasets I⃗ ) is a logical specification
involving the source data I⃗ and the interface data O. It is a valid definition
of O in terms of I⃗ , if any two models of the specification agreeing on I⃗
agree on O. In contrast, an explicit definition is a query that produces O from
I⃗ . Variants of Beth's theorem state that one can convert implicit definitions
to explicit ones. Further, this conversion can be done effectively given a
proof witnessing implicit definability in a suitable proof system. In this
talk, I will discuss an analogous effective implicit-to-explicit result for
nested relations: implicit definitions, given in the natural logic for nested
relations, can be effectively converted to explicit definitions in the nested
relational calculus NRC.

I will first spend some time explaining what NRC is and what logic we use to
describe implicit definitions of nested queries. Then I will present the
results obtained in our papers, attempt to give some intuitions on the proof of
the main theorem and say a few words on in particular the proof-theoretic
techniques and concerns that come up (namely, cut-elimination and focussing)
and how this can impact the complexity of extracting explicit definitions from
proofs of implicit definability. Then if time allows I will discuss a more
general model-theoretic result that we first used to give a non-constructive
proof of our theorem, and some ideas that we have towards making it
constructive and bounding the complexity of extracting explicit definitions.

This is Joint work with Michael Benedikt and Christoph Wenhard. The main
results I will be discussing were written up in
arxiv.org/abs/2005.06503 and arxiv.org/abs/2209.08299.

Speaker : Luis Galárraga — luisgalarraga.de/about/

Title: Computing How-Provenance for SPARQL Queries via Query Rewriting

Abstract:
Over the past few years, we have witnessed the emergence of large knowledge graphs built by extracting and combining information from multiple sources. This has propelled many advances in query processing over knowledge graphs, however the aspect of providing provenance explanations for query results has so far been mostly neglected. In this talk I will present SPARQLprov, a method based on query rewriting, to compute how-provenance polynomials for SPARQL queries over knowledge graphs. Contrary to existing works, SPARQLprov is system-agnostic and can be applied to standard and already deployed SPARQL engines without the need of customized extensions. To do so, we rely on spm-semirings to compute polynomial annotations that respect the property of commutation with homomorphisms on monotonic and non-monotonic SPARQL queries without aggregate functions. An evaluation on real and synthetic data shows that SPARQLprov over standard engines competes with state-of-the-art solutions for how-provenance computation, while covering a larger fragment of the query language.

Title:The Regular Languages of First-Order Logic with One Alternation
Abstract: The regular languages with a neutral letter expressible in first-order logic with one alternation are characterized. Specifically, it is shown that if an arbitrary Σ2 formula defines a regular language with a neutral letter, then there is an equivalent Σ2 formula that only uses the order predicate. This shows that the so-called Central Conjecture of Straubing holds for Σ2 over languages with a neutral letter, the first progress on the Conjecture in more than 20 years. To show the characterization, lower bounds against polynomial-size depth-3 Boolean circuits with constant top fan-in are developed. The heart of the combinatorial argument resides in studying how positions within a language are determined from one another, a technique of independent interest.

Title:
Separator logic, expressive power and algorithmic applications
Abstract:
First-order logic (FO) can express many algorithmic problems on graphs,
but fails to express whether two vertices are connected. We define a
new logic (separator logic) by enriching FO with connectivity
predicates connk(x, y, z1, . . . , zk) that hold true in a graph if
there exists a path between x and y after deletion of z1, . . . , zk.
In this talk I will first present a study of the expressive power of
this new logic.
I will then present algorithmic results for this logic on graph classes
that exclude a topological minor.
These results were obtained in collaboration with Michał Pilipczuk,
Nicole Schirrmacher, Sebastian Siebertz, and Szymon Toruńczyk.

Title: Stackless Processing of Streamed Trees
Abstract:
Processing tree-structured data in the streaming model is a chal-lenge: capturing regular properties of streamed trees by means of astack is costly in memory, but falling back to finite-state automata drastically limits the computational power. We propose an intermediate stackless model based on register automata equipped with a single counter, used to maintain the current depth in the tree. We explore the power of this model to validate and query streamed trees. Our main result is an effective characterization of regular path queries (RPQs) that can be evaluated stacklessly—with and without registers. In particular, we confirm the conjectured characterization of tree languages defined by DTDs that are recognizable without registers, by Segoufin and Vianu (2002), in the special case of tree languages defined by means of an RPQ.

Link: paperman.name/data/pub.....0.pdf

Title: Knowledge graph generation and validation

Title:
Spanner Evaluation over SLP-Compressed Documents

Abstract:
We consider the problem of evaluating regular spanners over compressed documents, i.e., we wish to solve evaluation tasks directly on the compressed data, without decompression. As compressed forms of the documents we use straight-line programs (SLPs) -- a lossless compression scheme for textual data widely used in different areas of theoretical computer science and particularly well-suited for algorithmics on compressed data. In terms of data complexity, our results are as follows. For a regular spanner M and an SLP S that represents a document D, we can solve the tasks of model checking and of checking non-emptiness in time O(size(S)). Computing the set M(D) of all span-tuples extracted from D can be done in time O(size(S) size(M(D))), and enumeration of M(D) can be done with linear preprocessing O(size(S)) and a delay of O(depth(S)), where depth(S) is the depth of S's derivation tree. Note that size(S) can be exponentially smaller than the document's size |D|; and, due to known balancing results for SLPs, we can always assume that depth(S) = O(log(|D|)) independent of D's compressibility. Hence, our enumeration algorithm has a delay logarithmic in the size of the non- compressed data and a preprocessing time that is at best (i.e., in the case of highly compressible documents) also logarithmic, but at worst still linear. Therefore, in a big-data perspective, our enumeration algorithm for SLP-compressed documents may nevertheless beat the known linear preprocessing and constant delay algorithms for non-compressed documents.
[This is joint work with Markus Schmid, to be presented at PODS'21.]

Link to the paper: arxiv.org/pdf/2101.10890.pdf for the paper at least
Link to the ACM video: TBA

titre: Problèmes algorithmiques en théorie des groupes infinis
resumé:
Malgré le titre très général, il s'agira uniquement de problèmes concernant les sous-groupes de groupes infinis, et même juste les sous-groupes de groupes libres. Les résultats et méthodes que je présenterai sont issus de près de 40 ans de littérature et sont dûs à un grand nombre d'auteurs.

Je commencerai par poser le paysage, y compris pour ceux qui ne savent plus ce qu'est le groupe libre -- où l'on verra qu'on est, du point de vue algorithmique, dans une variante de la combinatoire des mots. Je présenterai ensuite l'outil central de la plupart des algorithmes efficaces sur les sous-groupes du groupe libre : la représentation de chaque sous-groupe finiment engendré par un graphe étiqueté et enraciné (disons : d'un automate :-)…) unique et facilement calculable à partir d'un ensemble de générateurs du sous-groupe considéré, qu'on appelle le graphe de Stallings.

Le jeu consiste ensuite à traduire les problèmes algorithmiques sur les sous-groupes en problèmes algorithmiques sur les graphes de Stallings, et à résoudre ces problèmes de la façon la plus efficace possible.

On considèrera notamment les problèmes suivants -- bon, juste le début de cette longue liste.
- Le problème du mot généralisé : étant donnés k+1 éléments du groupe libre (ce sont des mots), le dernier appartient-il au sous-groupe engendré par les k premiers ?
- Le problème de l'indice : étant donné un tuple d'éléments du groupe libre, le sous-groupe qu'ils engendrent est-il d'indice fini ?
- Le problème de la base : étant donné un tuple d'éléments du groupe libre, trouver le rang, et une base du sous-groupe qu'ils engendrent.
- Le problème de l'intersection : étant donnés deux tuples d'éléments du groupe libre, calculer l'intersection des sous-groupes qu'ils engendrent (ou calculer une base de cette intersection).
- Le problème de la conjugaison : étant donnés deux tuples d'éléments du groupe libre, engendrent-ils le même sous-groupe ? deux sous-groupes conjugués ?
- Et de nombreux autres problèmes (mots clés : minimalité de Whitehead, facteur libre, malnormalité, clôture par radical, clôture au sens de la topologie pro-p, etc…)


title: Algorithmic problems in the theory of infinite groups
abstract:
In spite of the very general title, we will talk only about problems on subgroups of infinite groups, and in fact, only on subgroups of free groups . The results and methods I will present have been obtained over the past 40 years and are due to many researchers.

I will start by setting the landscape, including for those who forgot what the free group is --- and we will see that we are dealing here, from the algorithmic point of view, with a variant of combinatorics on words. I will then present the tool that is central to most efficient algorithms on subgroups of free groups: the representation of each finitely generated subgroup by a labeled rooted graph (shall we say… an automaton?) which is unique and easily computable when a tuple of generators of the subgroup under consideration is given. This graph is called the Stallings graph.

The game consists, then, in translating algorithmic problems on subgroups into algorithmic problems on Stallings graphs, and in solving these problems as efficiently as possible.

We will discuss in particular the following problems (clearly: just the beginning of this long list).
- The generalized word problem: given k+1 elements of the free group (these are words), does the last one belong to the subgroup generated by the k first ones?
- The index problem: given a tuple of elements of the free group, does the subgroup they generate have finite index?
- The basis problem: given a tuple of elements of the free group, find the rank and a basis of the subgroup they generate.
- The intersection problem: given two tuples of elements of the free group, compute the intersection of the subgroups they generate (compute a basis of this intersection).
- The conjugacy problem: given two tuples of elements of the free group, are the subgroups they generate equal? conjugated?
- And many other problems (keywords: Whitehead minimality, free factors, malnormality, closure under radicals, closure in the sense of the pro-p topology, etc…)