Links' Seminars and Public Events |
Fri, December 11, 2020 10:00 am 11:30 am | Alexandre Vigny Title: Elimination Distance to Bounded Degree on Planar Graphs Link to the zoominar: univ-lille-fr.zoom.us/j/95419000064 Abstract: What does it mean for a graph to almost be planar? Or to almost have bounded degree? On such simple graphs classes, some difficult algorithmic problems become tractable. Ideally, one would like to use (or adapt) existing algorithms for graphs that are "almost" in such a simple class. In this talk, I will discuss the notion of elimination distance to a class C, a notion introduced by Bulian and Dawar (2016). The goals of the talk are: 1) Define this notion, and discuss why it is relevant by presenting some existing results. 2) Show that we can compute the elimination distance of a given planar graph to the class of graph of degree at most d. I.e. answer the question: "Is this graph close to a graph of bounded degree?" The second part is the result of a collaboration with Alexandre Lindermayer and Sebastian Siebertz. |
Fri, December 4, 2020 10:00 am 11:00 am | Seminar: Pierre Pradic Title: Extracting nested relational queries from implicit definitions Abstract: arxiv.org/pdf/2005.06503.pdf In this talk, I will present results obtained jointly with Michael Benedikt establishing a connection between the Nested Relational Calculus (NRC) and sets implicitly definable using Δ₀ formulas. Call a formula φ(I,O) an implicit definition of the relation O(x,...) in terms of I(y,...) if O is functionally determined by I: for every I, O, O', if both φ(I,O) and φ(I,O') hold, then we have O ≡ O'. When φ is first-order and I and O are relations over base sorts, then Beth's definability theorem states that there is a first-order formula ψ(I,x,...) corresponding to O whenever φ(I,O) holds. Further, this explicit definition ψ can be effectively be computed from a sequent calculus proof witnessing that φ is functional. This allows for practical use of implicit definitions in the context of database programming, as there is a well-established link between fragments of explicitly FO definable relations and relational calculi. NRC is a conservative extension of relational calculi from database theory with limited powerset types in addition to tupling and anonymous base types. NRC expressions thus not only encompass flat relations over primitive datatypes like SQL but also nested collections, while remaining useful in practice. We extend the above correspondence between first-order logic and flat relational queries to NRC and implicit definitions using set-theoretical Δ₀ formulas over (typed) nested collection. Our proof of the equivalence goes through a notion of Δ₀-interpretation and a generalization of Beth definability for multi-sorted structures. This proof is non-constructive and thus does not yield any useful algorithm for converting implicit definitions into NRC terms. Using an approach more closely related to proof-theoretic interpolation, we give a constructive proof of the result restricted to intuitionistic provability, i.e, when the input functionality proof π of φ(I,O) is carried out in intuitionistic logic. Further, if π is cut-free, this can be done efficiently. Whether or not there exists a polynomial-time procedure working with classical proofs of functionality is still an open problem. I will focus on the effective result for the talk, and if time allows, discuss the difficulties with extending it to classical logic. I will not assume any background in either database or model theory. |