Lifting Term Rewriting Derivations in Constructor Systems by Using Generators

• Main Authors: Adrián Riesco, Juan Rodríguez-Hortalá
• Format: Article
• Language: English
• Published: Open Publishing Association 2015-01-01
• Series: Electronic Proceedings in Theoretical Computer Science
• Online Access: http://arxiv.org/pdf/1501.02035v1

Narrowing is a procedure that was first studied in the context of equational E-unification and that has been used in a wide range of applications. The classic completeness result due to Hullot states that any term rewriting derivation starting from an instance of an expression can be "lifted" to a narrowing derivation, whenever the substitution employed is normalized. In this paper we adapt the generator- based extra-variables-elimination transformation used in functional-logic programming to overcome that limitation, so we are able to lift term rewriting derivations starting from arbitrary instances of expressions. The proposed technique is limited to left-linear constructor systems and to derivations reaching a ground expression. We also present a Maude-based implementation of the technique, using natural rewriting for the on-demand evaluation strategy.