First-order tree-to-tree functions

We study tree-to-tree transformations that can be defined in first-order logic or monadic second-order logic. We prove a decomposition theorem, which shows that every transformation can be obtained from prime transformations, such as tree-to-tree homomorphisms or pre-order traversal, by using combinators such as function composition.

In an early version of this paper, Theorem 6.1 was stated without the restriction that 𝜆-terms to be normalized need to use a unique variable as a bound variable. This old version is not correct, as pointed to us by Lê Thành D ũng (Tito) Nguy ễn. His counter-example can be found in Example F.3.