Lazy AC-Pattern Matching for Rewriting

TL;DR

This paper introduces a lazy pattern-matching mechanism for rewriting systems that handles associativity and commutativity, enabling efficient computation of solutions through lazy evaluation.

Contribution

It presents a novel lazy AC-matching approach integrated into a strategy language for improved rewriting process efficiency.

Findings

Lazy AC-matching solutions are stored in a lazy list structure.

The approach allows rewriting rules to produce lazy lists of terms.

Integration with strategy language enhances rewriting flexibility.

Abstract

We define a lazy pattern-matching mechanism modulo associativity and commutativity. The solutions of a pattern-matching problem are stored in a lazy list composed of a first substitution at the head and a non-evaluated object that encodes the remaining computations. We integrate the lazy AC-matching in a strategy language: rewriting rule and strategy application produce a lazy list of terms.