E-Generalization Using Grammars

Syntactical antiunification reflects these abstraction techniques in the theoretically elegant domain of term algebras. In this article, we propose an extension, called E-anti-unification or E-generalization, which also provides a way of coping with the well-known problem of representation change [O'H92,DIS97]. It allows us to perform abstraction while modeling equivalent representations using appropriate equations between terms. This means that all equivalent representations are considered simultaneously in the abstraction process. Abstraction becomes insensitive to representation changes. In 1970, Plotkin and Reynolds [Plo70,Plo71,Rey70] introduced the notion of (syntactical) anti-unification of terms as the dual operation to unification: while the latter computes the most general common specialization of the given 1 1. x 0 x 2. x s(y) s(x y) 3. x 0 0 4. x s(y) x y x 0