Polyregular Functions on Unordered Trees of Bounded Height

Explore a 20-minute conference talk from POPL 2024 examining polyregular functions on unordered trees of bounded height. Delve into the research by Mikołaj Bojańczyk and Bartek Klin, which investigates injective first-order interpretations for input and output trees with limited height. Learn about their proof of decidability for the equivalence problem of such functions and discover a calculus of typed functions and combinators that precisely derives injective first-order interpretations for unordered trees of bounded height. Understand the implications of their findings, including the application to decidability of the equivalence problem for first-order interpretations between graph classes with bounded tree-depth. Gain insights into the expressive power equivalence between first-order logic and MSO in the studied cases, extending the results to MSO interpretations as well.