Seminars

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.