Polyregular functions on unordered trees of bounded height

We consider injective 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 s...

Full description

Bibliographic Details
Main Authors: Bojańczyk, M, Klin, B
Format: Conference item
Language:English
Published: Association for Computing Machinery 2024
_version_ 1797112730321158144
author Bojańczyk, M
Klin, B
author_facet Bojańczyk, M
Klin, B
author_sort Bojańczyk, M
collection OXFORD
description We consider injective 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. <br> We also give a calculus of typed functions and combinators which derives exactly injective first-order interpretations for unordered trees of bounded height. The calculus is based on a type system, where the type constructors are products, coproducts and a monad of multisets. Thanks to our results about tree-to-tree interpretations, the equivalence problem is decidable for this calculus. <br> 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.
first_indexed 2024-03-07T08:29:34Z
format Conference item
id oxford-uuid:abb3e67c-52ca-4c65-bcea-736dd6104918
institution University of Oxford
language English
last_indexed 2024-03-07T08:29:34Z
publishDate 2024
publisher Association for Computing Machinery
record_format dspace
spelling oxford-uuid:abb3e67c-52ca-4c65-bcea-736dd61049182024-03-01T10:06:31ZPolyregular functions on unordered trees of bounded heightConference itemhttp://purl.org/coar/resource_type/c_5794uuid:abb3e67c-52ca-4c65-bcea-736dd6104918EnglishSymplectic ElementsAssociation for Computing Machinery2024Bojańczyk, MKlin, BWe consider injective 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. <br> We also give a calculus of typed functions and combinators which derives exactly injective first-order interpretations for unordered trees of bounded height. The calculus is based on a type system, where the type constructors are products, coproducts and a monad of multisets. Thanks to our results about tree-to-tree interpretations, the equivalence problem is decidable for this calculus. <br> 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.
spellingShingle Bojańczyk, M
Klin, B
Polyregular functions on unordered trees of bounded height
title Polyregular functions on unordered trees of bounded height
title_full Polyregular functions on unordered trees of bounded height
title_fullStr Polyregular functions on unordered trees of bounded height
title_full_unstemmed Polyregular functions on unordered trees of bounded height
title_short Polyregular functions on unordered trees of bounded height
title_sort polyregular functions on unordered trees of bounded height
work_keys_str_mv AT bojanczykm polyregularfunctionsonunorderedtreesofboundedheight
AT klinb polyregularfunctionsonunorderedtreesofboundedheight