发表机构
Chennai Mathematical Institute; CNRS IRL ReLaX（钦奈数学研究所; 法国国家科学研究中心印度联合研究国际部 ReLaX）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出基于模式的树变换模型，证明其类型检查问题可判定，通过归约为交替树自动机空集问题实现，该模型表达能力强但等价性检查不可判定。
AI 中文摘要
我们引入并研究基于模式的树变换。作为示例，考虑源模式 $(x \cdot y) + (x \cdot z)$ 和目标模式 $x \cdot (y + z)$ 组成的一对。该源模式匹配任何形如 $(e_1 \cdot e_2) + (e_1 \cdot e_3)$ 的表达式 $e$（通过将 $x$ 替换为 $e_1$、$y$ 替换为 $e_2$、$z$ 替换为 $e_3$），该对会将其转换为目标模式指定的表达式 $e_1 \cdot (e_2 + e_3)$。需注意，此示例中匹配源模式的表达式集合并非正则树语言。我们提出一种树变换模型，该模型由有限个此类（源模式、目标模式）对的集合（可能为无限集）表示。该模型的表达能力以等价性检查的不可判定性为代价。不过，我们证明了基于模式的树变换模型的类型检查问题是可判定的。类型检查问题是指，将给定变换应用于具有给定正则属性（类型）的树时，是否会保留该属性。我们的判定过程通过归约为交替树自动机的空集问题实现。
英文摘要
We introduce and study pattern-based tree transformations. As an illustrating example, consider a source pattern $(x \cdot y) + (x \cdot z)$ and a target pattern $x \cdot (y + z)$ as a pair. This source pattern matches any expression $e$ of the form $(e_1 \cdot e_2) + (e_1 \cdot 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 \cdot (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.
Comments26 pages, 9 figures, full version of a preprint accepted at FSTTCS 2026
