PaperlayerView exact revision on arXiv

Source-linked AI summary

Type-Checking for Pattern-Based Tree Transformations

C. Aiswarya, Sahil Mhaskar, M. Praveen

arXiv:2610.11337v1cs.FLcs.CL

TL;DR

Pattern-based tree transformations can describe rewrites whose matching source trees need not form a regular language, while equivalence checking is undecidable. The paper finitely represents potentially infinite pattern-pair families and reduces type-checking to alternating-tree-automaton emptiness; it establishes that type-checking is decidable and in 3-EXPTime.

  • Problem

    The paper asks whether a transformation maps trees satisfying a regular source property into a regular target property, even when pattern matching has a nonregular domain.

    Source: §1 · p. 1, §5 · pp. 14–15

  • Method

    The model represents possibly infinite pattern-pair families with bimorphisms, and its type-checking procedure reduces the problem to alternating tree automata.

    Source: §1 · p. 2, §9 · p. 23

  • Results

    Type-checking is decidable and in 3-EXPTime, although equivalence checking for the model is undecidable.

    Source: §5 · p. 16, §9 · p. 23

  • Takeaways & Limitations

    The model's expressive power does not prevent decidable type-checking, which the paper establishes through an automata-theoretic algorithm.

    Source: §9 · p. 23

Abstract

from arXiv · show

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.

C. Aiswarya #

The front matter classifies the paper under tree languages and transducers and lists its focus on type-checking and pattern matching.

Classification

  • The ACM classification places the paper in tree languages and transducers.The listed classification year is 2012.Source: C. Aiswarya # · p. 1

Keywords

  • The listed keywords are tree transducers, type-checking, alternating tree automata, and pattern-matching.Source: C. Aiswarya # · p. 1

Related version

  • The paper is described as the full version of a preprint accepted at FSTTCS 2026.Source: C. Aiswarya # · p. 1

1 Introduction

The introduction presents pattern-based tree transformations as a finite way to describe potentially infinite families of rewrites, including cases with nonregular domains. It motivates type-checking for these transformations and outlines an automata-based decision procedure.

1 Introduction

  • Horner-style rewrites factor repeated products across an arbitrary number of summands, motivating transformations whose source domains need not be regular.The same subtree must occur in multiple positions, and the introduction notes that such source-tree sets need not be regular.Source: §1 · pp. 1–2
  • Bimorphisms finitely represent possibly infinite sets of source-target pattern pairs using a regular seed language and two tree homomorphisms.The distributivity example uses guards to constrain the subtrees substituted for placeholders.Source: §1 · p. 2
  • Type-checking asks whether regular source properties are preserved into a target property; counterexamples can be searched for with alternating tree automata over seed trees.The procedure reduces the question to emptiness checking for alternating tree automata.Source: §1 · p. 3
  • The single-pattern-pair type-checking problem is EXPTime-complete, while matching a tree to a pattern is NP-complete.The introduction relates the single-pair case to pattern-based word transformations [1].Source: §1 · p. 3

Related work

  • Pattern-based word transformations [1] use a single pattern pair; this paper extends the setting to trees and potentially infinite pattern-pair families.Source: Related work · p. 3
  • The model subsumes classical top-down and bottom-up tree transducers but is incomparable with streaming and macro tree transducers [2, 7].The paper attributes the contrast in part to its potentially nonregular domains and its inability to reverse a word.Source: Related work · p. 3
  • Compared with the pattern-based forest rewriting system [9], this work studies one-step rewriting on unrestricted trees and reports elementary-complexity algorithms.Source: Related work · p. 3

Paper organisation

  • The paper proceeds from the model and examples through the type-checking problem and automata-based intuition to the decidability proof.Some detailed proofs are moved to the appendix.Source: Paper organisation · p. 4

2 Illustrating Example

The example illustrates how a seed language and two morphisms encode distributivity rewrites. It then frames preservation of product-depth bounds as a type-checking question.

Distributivity transformation

  • The illustrated distributivity transformation preserves the shaded expression parts while regrouping products and sums.The figure caption identifies the expressions as arbitrary; the accompanying text describes the shaded portions as unchanged.Source: Figure 1 · p. 4, §2 · p. 4

Seed trees and morphisms

  • A seed tree and two morphisms generate each source-target pattern pair, with one seed for each operand choice and +-kernel shape.The seed-tree set is tree-regular: its root is a, each path has one b, and the segment between them contains only + nodes.Source: §2 · p. 4, Figure 2 · p. 5

Type-checking example

  • Preservation of k-bounded product-depth is posed as type-checking because k-pd-bounded expressions form a regular tree language.Product-depth is the maximum number of × operators on any branch.Source: §2 · pp. 4–5

3 Formal Model

The formal model builds tree transformations from patterns, substitutions, and guards, then represents a possibly infinite family of atomic transformations with a bimorphism. Its definitions rely on finite ranked trees and regular tree languages.

Sets and Relations

  • The paper works with finite ranked trees and regular tree languages recognized by tree automata.A ranked alphabet assigns an arity to each symbol, and trees satisfy that arity at every node.Source: Sets and Relations · p. 5
  • A bottom-up tree automaton accepts a tree when some compatible run ends in a final state.Its nondeterministic transition system assigns possible parent states to child-state tuples and a symbol.Source: Sets and Relations · p. 6
  • A context is a tree with designated holes, each occurring exactly once, where other trees can be appended.The paper restricts its attention to finite contexts.Source: Sets and Relations · p. 6

3.2 Tree Transformations

  • Tree homomorphisms map symbols to trees and extend recursively by replacing variables with the homomorphic images of child trees.The paper describes them as extensions of word homomorphisms to trees.Source: §3.2 · pp. 6–7
  • A pattern is a tree containing variables, and substitutions replace those variables with contexts of matching arity.The paper defines each variable's degree as one plus its arity.Source: §3.2 · p. 7
  • Guards restrict which tree languages may be substituted for variables; a match requires a guarded substitution that yields the tree.A tree may admit more than one matching substitution.Source: §3.2 · p. 7
  • An atomic transformation pairs source and target patterns with guards, applying a matching substitution to produce the output tree.The model allows a possibly infinite set of atomic transformations.Source: §3.2 · pp. 7–8
  • A transformation uses a seed language and two tree homomorphisms to generate source and target patterns, with guards governing substitutions.Each seed tree induces an atomic transformation; the collection is represented by the bimorphism-based model.Source: §3.2 · p. 8

4 Example - Code Snippet Translation

The example encodes bounded-for-loop programs as trees and uses a regular seed language to generate source and target patterns for converting for loops to while loops. The seed language restricts loop markers so the generated transformations are well-formed.

4 Example - Code Snippet Translation

  • The example represents programs as trees over an alphabet with for/5, while/3, null/0, and unary symbols from Σcore.The number of for loops is bounded by a fixed n.Source: §4 · p. 8
  • The regular seed language restricts each loopi/endLoopi pair to at most one occurrence and requires loops to be well-nested.The automata Ui enforce the pair-occurrence restriction, while a further automaton is introduced for nesting.Source: §4 · pp. 11, 13
  • Each binary loopi marker represents loop i, with its left child holding the loop body through endLoopi and its right child holding following code through null.The seed alphabet also contains the unary core symbols and null.Source: §4 · p. 11
  • For programs with at most n for loops, a seed tree generates source and target patterns that transform every for loop into a while loop.The same substitution is applied to the target pattern to produce the transformed code.Source: §4 · p. 13

5 Decision Problems for Tree Transformations

The section studies whether transformations can reach a regular target language from a regular source language, and establishes decidability and complexity bounds for related problems. In particular, type-checking is in 3-EXPTime.

5 Decision Problems for Tree Transformations

  • Matching a pattern against a tree with guarded substitutions is NP-complete.A polynomial-size substitution certificate can be verified in polynomial time, and hardness is shown by reduction from 1-in-3 SAT.Source: §5 · p. 14
  • Atomic Transformation Reachability is EXPTime-complete.The upper bound reduces the problem to finding a substitution satisfying both source- and target-language constraints; the lower bound reduces from intersection nonemptiness for deterministic tree automata.Source: §5 · pp. 14–15
  • Transformation Reachability is in 2-EXPTime, with a time bound 2^poly(|input|) where the polynomial degree is deg(T).The central question is whether a tree in a regular target language can be reached from a tree in a regular source language.Source: §5 · pp. 15–16
  • The Type-Checking Problem is in 3-EXPTime.The bound follows using closure of nondeterministic tree automata under complementation, with an exponential blow-up.Source: §5 · p. 16

6 Core Idea Behind the Automata Construction

The decision procedure simulates source-automaton runs while traversing a seed tree, tracking the state transformations induced by contexts and substitutions. Alternating tree automata can check the required constraints, including those imposed by repeated variables.

6 Core Idea Behind the Automata Construction

  • The automaton traverses the seed tree and simulates source-automaton state transformations for the corresponding source-tree contexts.At a seed node, it validates a tuple of child states against the resulting state.Source: Figure 7 · p. 16, §6 · p. 17
  • Instead of choosing an actual substitution tree, the construction tracks its effect on automaton states, which has only finitely many possibilities.Any substitution inducing the same state transformation can serve in its place.Source: §6 · p. 17
  • For a variable repeated in the source pattern, one substitution must satisfy the state transformations required at all its occurrences.The construction uses relational lifts to capture these simultaneous requirements, and alternating tree automata check the constraints on both source and target trees.Source: §6 · p. 17

7 Alternating Tree Automata and Relational Lifts

The section develops automata and relational tools for deciding whether a relation can be induced by a context. Relation realisability is EXPTime-complete, and the proof also yields a realizing context when one exists.

7 Alternating Tree Automata and Relational Lifts

  • An alternating top-down tree automaton uses positive Boolean combinations of state-and-child pairs to define transitions and accepts trees with a successful run from an initial state.Its recognized tree languages are regular tree languages.Source: §7 · pp. 17–18
  • An extended transition relation assigns each context the relation it induces on the states of a nondeterministic bottom-up tree transition system.For a context with holes, the tuple of states placed at those holes determines the possible resulting states.Source: §7 · p. 18
  • Relational lift composes relations through an operator, extending that operator from elements of a set to relations over the set.For tree contexts, it combines the relations induced by child contexts with the node’s transition relation.Source: §7 · p. 18
  • Relation Realisability is EXPTime-complete.The lower bound reduces Intersection Nonemptiness of DBTAs to realisability; the upper bound checks nonemptiness of a constructed automaton intersected with the given automaton.Source: §7 · pp. 19–20
  • Relation realisability reduces to nonemptiness by constructing an automaton whose states are relations and whose accepted contexts induce the requested relation.The construction also yields a realizing context in EXPTime whenever one exists.Source: §7 · pp. 19–20

8 Deciding Transformation Reachability

Transformation reachability is reduced to finding a seed tree whose source and target images, under one shared substitution, belong to their respective regular languages. The procedure checks automaton nonemptiness for choices of realizable relations and runs in 2^poly(|input|), with polynomial degree deg(T).

8 Deciding Transformation Reachability

  • Reachability asks whether a seed tree has source and target images that, under the same substitution, belong to their respective regular languages.The procedure represents successful seed trees as a union of languages recognized by constructed alternating tree automata.Source: §8 · p. 20
  • For variables shared by the source and target, the procedure computes pairs of relations simultaneously realizable by one context satisfying the guard.For variables appearing on only one side, it computes realizable relations for that side’s automaton.Source: §8 · pp. 20–21
  • For each pair of relation choices, an alternating tree automaton simulates the seed automaton and both transformed-language automata.The construction computes extended transition relations for source and target homomorphisms; its size is O(max(|Qsrc|, |Qtgt|)).Source: §8 · pp. 20–22
  • The destination function maps each input child position to the inorder-numbered holes in its homomorphic image.The sets of destinations for the child positions partition the image’s hole positions.Source: §8 · p. 21
  • 2^poly(|input|), with polynomial degree deg(T), bounds the transformation-reachability procedure’s running time.The procedure checks nonemptiness for each pair of source and target relation choices.Source: §8 · p. 23

9 Conclusion

The paper introduces a highly expressive model of tree transformations and gives an automata-theoretic algorithm placing type-checking in 3-EXPTime, despite equivalence checking being undecidable. A future direction is to study type-checking for variants generated by more general tree transducers.

  • Type-checking is in 3-EXPTime via an automata-theoretic algorithm, although equivalence checking is undecidable.Source: §9 · p. 23
  • The paper introduces a formal model of tree transformations described as highly expressive.Source: §9 · p. 23
  • Equivalence checking for the introduced tree transformations is undecidable.Source: §9 · p. 23
  • A future direction is to study type-checking for expressive transformation variants generated by more general tree transducers.Source: §9 · p. 23

A Comparison with k-Pebble Transducers

A 2-pebble tree transducer can reverse strings in the paper’s tree encoding, while the section establishes limits on representing reversal with homomorphism bimorphisms and the specified action model.

Loading 2610.11337v1…