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

## TL;DR

This paper presents a new method to transform regular tree grammars representing narrowing trees into overapproximations of substitution ranges, extending previous work to tuples of terms for better analysis.

## Contribution

It introduces a novel transformation that overapproximates substitution ranges using tuples of terms, improving upon previous single-variable restrictions.

## Key findings

- The transformation overapproximates the ranges of ground substitutions.
- It extends previous work by representing substitution ranges as tuples.
- The language of the transformed grammar is proven to be an overapproximation.

## Abstract

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.