Homeomorphic Embedding modulo Combinations of Associativity and Commutativity Axioms

TL;DR

This paper extends the homeomorphic embedding relation to order-sorted rewrite theories with associativity and commutativity axioms, demonstrating its practical efficiency for symbolic program analysis.

Contribution

It generalizes homeomorphic embedding to handle complex equational axioms in symbolic execution, with systematic performance evaluation.

Findings

Most efficient formulation improves practical performance

Homeomorphic embedding applicable to theories with associativity and commutativity

Experimental results confirm efficiency gains

Abstract

The Homeomorphic Embedding relation has been amply used for defining termination criteria of symbolic methods for program analysis, transformation, and verification. However, homeomorphic embedding has never been investigated in the context of order-sorted rewrite theories that support symbolic execution methods modulo equational axioms. This paper generalizes the symbolic homeomorphic embedding relation to order-sorted rewrite theories that may contain various combinations of associativity and/or commutativity axioms for different binary operators. We systematically measure the performance of increasingly efficient formulations of the homeomorphic embedding relation modulo associativity and commutativity axioms. From our experimental results, we conclude that our most efficient version indeed pays off in practice.