Symbolic evaluation with structural recursive symbolic constants (Q1101205)

Symbolic evaluation is a technique used for many termination of associative commutative (AC in short) rewriting systems. This ordering is based on a transformation of the terms by a rewriting system with rules similar to distributivity. We show this is a reduction ordering which works in the AC case since it is AC-commuting, and which provides an automatizable termination tool, since it is stable by instantiation. Thereafter, we show cases where this ordering fails, and propose an extension of this method to other transformation rules such as endomorphism.