Lifting Term Rewriting Derivations in Constructor Systems by Using Generators

TL;DR

This paper introduces a generator-based transformation to lift term rewriting derivations from arbitrary instances in constructor systems, extending classic narrowing techniques with a Maude implementation.

Contribution

It adapts generator-based extra-variables-elimination to lift derivations from arbitrary instances, overcoming limitations of classic narrowing in constructor systems.

Findings

Successfully lifts derivations from arbitrary instances in constructor systems.

Implementation in Maude demonstrates practical applicability.

Limits to left-linear systems and ground expressions.

Abstract

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.