Seminars

Speaker: Sarah Winter — sarahwinter.net/

Title: A Regular and Complete Notion of Delay for Streaming String Transducers

Abstract:
The notion of delay between finite transducers is a core element of numerous fundamental results of transducer theory. The goal of this work is to provide a similar notion for more complex abstract machines: we introduce a new notion of delay tailored to measure the similarity between streaming string transducers (SST).

We show that our notion is regular: we design a finite automaton that can check whether the delay between any two SSTs executions is smaller than some given bound. As a consequence, our notion enjoys good decidability properties: in particular, while equivalence between non-deterministic SSTs is undecidable, we show that equivalence up to fixed delay is decidable. Moreover, we show that our notion has good completeness properties: we prove that two SSTs are equivalent if and only if they are equivalent up to some (computable) bounded delay.

Together with the regularity of our delay notion, it provides an alternative proof that SSTs equivalence is decidable. Finally, the definition of our delay notion is machine-independent, as it only depends on the origin semantics of SSTs. As a corollary, the completeness result also holds for equivalent machine models such as deterministic two-way transducers, or MSO transducers.

This is joint work with Emmanuel Filiot, Ismaël Jecker, and Christof Löding.

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.