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...
Main Authors: | , |
---|---|
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 |