Pattern matching with associative and commutative operators

Question

Pattern matching (as found in e.g. Prolog, the ML family languages and various expert system shells) normally operates by matching a query against data element by element in strict order.

In domains like automated theorem proving, however, there is a requirement to take into account that some operators are associative and commutative. Suppose we have data

A or B or C

and query

C or $X

Going by surface syntax this doesn't match, but logically it should match with $X bound to A or B because or is associative and commutative.

Is there any existing system, in any language, that does this sort of thing?

Answer 1

Associative-Commutative pattern matching has been around since 1981 and earlier, and is still a hot topic today.

There are lots of systems that implement this idea and make it useful; it means you can avoid write complicated pattern matches when associtivity or commutativity could be used to make the pattern match. Yes, it can be expensive; better the pattern matcher do this automatically, than you do it badly by hand.

You can see an example in a rewrite system for algebra and simple calculus implemented using our program transformation system. In this example, the symbolic language to be processed is defined by grammar rules, and those rules that have A-C properties are marked. Rewrites on trees produced by parsing the symbolic language are automatically extended to match.