Algebraic generalization
Stephen M. Watt · ACM SIGSAM Bulletin · 2005
We explore the notion of generalization in the setting of symbolic mathematical computing. By "generalization" we mean the process of taking a number of instances of mathematical expressions and producing new expressions that may be specialized to all the instances. We identify a number of ways in which generalization may be useful in the setting of computer algebra. We formalize this generalization as an antiunification problem.The process of antiunification is the dual of unification. It takes two expressions E 1 , E 2 ∈ E (Σ, V ) and produces E 3 ∈ E (Σ, V ) such that there exist substitutions σ 1 and σ 2 such that σ 1 ( E 3 ) = E 1 and σ 2 ( E 3 ) = E 2 . We call the pair of substitutions an antiunifier and the resulting expression a generalization of the expressions. An antiunifier always exists, but is not necessarily unique. There is, however, a unique most specific antiunifier that places the most restrictions on the variables. This gives the most specific generalization , which is unique up to renaming of variables.