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.