Polyregular functions on unordered trees of bounded height
summary
Proves that equivalence of injective first‑order interpretations (polyregular functions) on unordered trees of fixed height is decidable by normalizing to a quantifier-free normal form and then checking syntactic equality of codes; builds a typed calculus with products, coproducts and a multiset monad that exactly captures these functions; shows FO = MSO on these inputs so MSO interpretations collapse to FO; yields the first nontrivial decidability result for transformations producing isomorphic graphs (e.g. bounded tree‑depth) and gives an algorithm whose complexity depends on representation.
AI-written summary · about
chapters (6)
- 0:00Introduction
- 4:33Bounded height unordered trees
- 8:06Polyregular functions
- 13:45Equivalence decidability
- 15:54Graph transformation corollaries
- 16:15Q&A
related talks
31mFibred Categories of Tree Automata
16mInterpolation and Quantifiers in Ortholattices
14mAdequacy for Algebraic Effects Revisited
49mCompiling FO Sentences to Circuits: Upper Bounds and Lower Bounds on the Size of the Circuit
32mTyped Program Analysis Without Encodings
30mComputation-Tree Semantics: An Algorithmic Approach to Structurally Defined Relations
32mVerifying Haskell's Rewrite Rules based on Polymorphic Rewriting Theory
49mSemantic Foundations for Probabilistic Programming