Lazy AC-Pattern Matching for Rewriting

Abstract

Extended version of hal-00642515 written in 2012International audienceWe 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 term