Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems

Authors: Naoki Nishida and Yuya Maeda

Paper Information

Title:Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems
Authors:Naoki Nishida and Yuya Maeda
Proceedings:FSCD Presented Papers
Editor: Helene Kirchner
Keywords:conditional term rewriting, innermost conditional narrowing, regular tree grammar, program transformation

ABSTRACT. Given a constructor term rewriting system, a narrowing tree for a pair of terms is a finite representation for the space of all possible innermost-narrowing derivations that start with the pair and end with non-narrowable terms. Narrowing trees have grammar representations that can be considered regular tree grammars. Innermost narrowing is a counterpart of constructor-based rewriting, and thus, narrowing trees can be used in analyzing constructor-based rewriting to normal forms. In this paper, using grammar representations, we extend narrowing trees to syntactically deterministic conditional term rewriting systems (SDCTRS) that are constructor systems. We do not directly extend narrowing trees to conditional systems, but we convert a constructor SDCTRS to an equivalent unconditional constructor system that may have extra variables. Narrowing trees for the converted constructor system can work for the original SDCTRS. As an application of narrowing trees, we show that narrowing trees are useful to prove two properties of a normal CTRS: (1) infeasibility of conditional critical pairs and (2) quasi-reductivity.

Talk:Jul 11 11:00 (Session 64B: Rewriting)