We introduce and study pattern-based tree transformations. Consider (+(.(x, y), .(x, z)), .(x, +(y, z))), a pair of a source pattern and a target pattern. This source pattern matches any expression e of the form +(.(e1 , e2 ), .(e1 , e3 )), by substituting e1 for x, e2 for y and e3 for z. Note that the set of such matching expressions is not a regular tree language, since the same expression must appear in two locations where x appears in the source pattern. This pair transforms the expression e into the expression .(e1 , +(e2 , e3 )) (obtained by applying the same substitution to the target pattern). Our model finitely represents 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. The type-checking problem checks whether applying a given transformation to trees having a given regular property (type) preserves the property. We show that this problem is decidable for pattern-based tree transformations. Our decision procedure is by a reduction to the emptiness problem of alternating tree automata.
This is joint work with C. Aiswarya and Sahil Mhaskar from Chennai Mathematical Institute.
Short Bio:
Praveen is an associate professor at Chennai Mathematical Institute. He finished PhD at the Institute of Mathematical Institute, Chennai. He was a postdoc at LSV, ENS Cachan and LaBRI, University of Bordeaux before he joined CMI in 2014. His research interests and logic and automata theory for formal verification.
