We introduce and study pattern-based tree transformations. As an illustrating example, consider a source pattern (x⋅y)+(x⋅z) and a target pattern x⋅(y+z) as a pair. This source pattern matches any expression e of the form (e1⋅e2)+(e1⋅e3) (by substituting x with e1, y with e2, and z with e3) and the pair transforms it into the expression e1⋅(e2+e3) 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.
Figures & tables
Figure 1: The transformation of an expression following distributivity. Here f , e1 , … e6 are arbitrary expressions. If f is a variable instead of an expression, we get a (source pattern, target pattern) pair that captures this transformation.
Figure 2: The seed tree and the morphisms generating the (source pattern, target pattern) pair capturing the transformation depicted in Figure 1 .
Source code
int[] A = new int[m];
for(int i=0;i<A.length;i++) {
A[i] = getInputFromUser();
}
for(int j=0;j<A.length;j++) {
int minIndex = j;
Figure 3: The source and target code snippets for Selection Sort, before and after transforming for loops to while loops.
Figure 4: Source and target code snippets from Fig 3 as trees.
Figure 5: The seed tree generating the source and target patterns in Figure 6 .
Figure 6: Source and target patterns. The source and target morphisms are identity everywhere, except for loopi and endLoopi , which are indicated by colors blue and red respectively.
Figure 7: The source tree is annotated with states of ALsrc . We want to simulate the effect of running ALsrc on the source tree in the seed tree itself. This means, when processing η , it should guess and validate the potential transformation of the tuple (q7,q8,q9) to q10 by a context (colored blue) in the source tree that matches ϕsrc(η) , and simultaneously make sure that there is a substitution for x that preserves the transformations (q1,q2) to q3 as well as (q4,q5) to q6 . An alternating tree automaton on the seed tree can achieve this.