A Method to Simplify Expressions: Intuition and Preliminary Experimental Results

We present a method to simplify expressions in the context of a formal, axiomatically defined, the- ory. In this paper, equality axioms are typically used but the method is more generally applicable. The key idea of the method is to represent large, even infinite, sets of expressions1 by means of a special data structure that allows us to apply axioms to the sets as a whole, not to single individual expressions. We then propose a bottom-up algorithm to finitely compute theories with a finite number of equivalence classes of equal terms. In that case, expressions can be simplified (i.e., minimized) in linear time by “folding” them on the computed representation of the theory. We demonstrate the method for boolean expressions with a small number of variables. Finally, we propose a “goal oriented” algorithm that computes only small parts of the underlying theory, in order to simplify a given particular expression. We show that the algorithm is able to simplify boolean expressions with many more variables but optimality cannot be certified anymore.We present a method to simplify expressions in the context of a formal, axiomatically defined, the- ory. In this paper, equality axioms are typically used but the method is more generally applicable. The key idea of the method is to represent large, even infinite, sets of expressions1 by means of a special data structure that allows us to apply axioms to the sets as a whole, not to single individual expressions. We then propose a bottom-up algorithm to finitely compute theories with a finite number of equivalence classes of equal terms. In that case, expressions can be simplified (i.e., minimized) in linear time by “folding” them on the computed representation of the theory. We demonstrate the method for boolean expressions with a small number of variables. Finally, we propose a “goal oriented” algorithm that computes only small parts of the underlying theory, in order to simplify a given particular expression. We show that the algorithm is able to simplify boolean expressions with many more variables but optimality cannot be certified anymore