Polyregular functions on unordered trees of bounded height
We consider first-order interpretations that input and output trees of bounded height. The corresponding functions have polynomial output size, since a first-order interpretation can use a k-tuple of input nodes to represent a single output node. We prove that the equivalence problem for such functions is decidable, i.e. given two such interpretations, one can decide whether, for every input tree, the two output trees are isomorphic.
We also give a calculus, based on prime functions and combinators, which derives all first-order interpretations for unordered trees of bounded height. The calculus is based on a type system, where the type constructors are products, co-products and a monad of multisets. Thanks to our results about tree-to-tree interpretations, the equivalence problem is decidable for this calculus.
As an application, we show that the equivalence problem is decidable for first-order interpretations between classes of graphs that have bounded tree-depth. In all cases studied in this paper, first-order logic and MSO have the same expressive power, and hence all results apply also to MSO interpretations.
Thu 18 JanDisplayed time zone: London change
15:30 - 16:50 | |||
15:30 20mTalk | Polyregular functions on unordered trees of bounded height POPL | ||
15:50 20mTalk | Solving Infinite-State Games via Acceleration POPL Philippe Heim CISPA Helmholtz Center for Information Security, Rayna Dimitrova CISPA Helmholtz Center for Information Security Pre-print | ||
16:10 20mTalk | Ramsey Quantifiers in Linear Arithmetics POPL Pascal Bergsträßer University of Kaiserslautern-Landau, Moses Ganardi MPI-SWS, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS, Georg Zetzsche MPI-SWS Pre-print | ||
16:30 20mTalk | Reachability in Continuous Pushdown VASS POPL A. R. Balasubramanian Technical University of Munich, Rupak Majumdar MPI-SWS, Ramanathan S. Thinniyam Uppsala University, Georg Zetzsche MPI-SWS Pre-print |