Type-Checking for Pattern-Based Tree Transformations

arXiv:2610.11337v1 Announce Type: cross Abstract: We introduce and study pattern-based tree transformations. As an illustrating example, consider a source pattern (x dot y) + (x dot z) and a target pattern x dot (y + z) as a pair. This source pattern matches any expression e of the form (e_1 dot e_2) + (e_1 dot e_3) (by substituting x with e_1, y with e_2, and z with e_3) and the pair transforms it into the expression e_1 dot (e_2 + e_3) as dictated by the target pattern. Note that in this example, the set of expressions that match the source pattern is not a regular tree language. We propose a model of tree transformations given by a finite representation of a (possibly infinite) set of such (source pattern, target pattern) pairs. The expressive power of this model comes at the cost of undecidability of checking equivalence. Nevertheless, we show that the type-checking problem is decidable for our model of pattern-based tree transformations. The type-checking problem asks whether applying a given transformation to trees having a given regular property (type) preserves the property. Our decision procedure is by a reduction to the emptiness problem of alternating tree automata.

Source: arXiv cs.CL | 2026-10-09