On Transforming Narrowing Trees into Regular Tree Grammars Generating Ranges of Substitutions

Naoki Nishida
(Nagoya University)
Yuya Maeda
(Nagoya University)

The grammar representation of a narrowing tree for a syntactically deterministic conditional term rewriting system and a pair of terms is a regular tree grammar that generates expressions for substitutions obtained by all possible innermost-narrowing derivations that start with the pair and end with particular non-narrowable terms. In this paper, under a certain syntactic condition, we show a transformation of the grammar representation of a narrowing tree into another regular tree grammar that overapproximately generates the ranges of ground substitutions generated by the grammar representation. In our previous work, such a transformation is restricted to the ranges w.r.t. a given single variable, and thus, the usefulness is limited. We extend the previous transformation by representing the range of a ground substitution as a tuple of terms, which is obtained by the coding for finite trees. We show a precise definition of the transformation and prove that the language of the transformed regular tree grammar is an overapproximation of the ranges of ground substitutions generated by the grammar representation. We leave an experiment to evaluate the usefulness of the transformation as future work.

In Joachim Niehren and David Sabel: Proceedings Fifth International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2018), Oxford, England, 8th July 2018, Electronic Proceedings in Theoretical Computer Science 289, pp. 68–87.
Published: 22nd February 2019.

ArXived at: http://dx.doi.org/10.4204/EPTCS.289.5 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org