''From OnceAndOnlyOnce:''

''This appears to me to be a parameterized/paraphrased discussion from the RefactoringBrowserThesis. The RefactoringBrowser and thesis use FirstOrderPredicateLogic to prove various facts about refactorings. --ShaeErisson''

I think SetTheory, GroupTheory, CategoryTheory may be together useful backgrounds for building a code algebra. Those three sub-disciplines of mathematics were all founded with the idea that there are universal patterns in mathematics that can be extracted and matched. GraphTheory may also prove itself useful. The concept called "(homo)morphism" in CategoryTheory, GroupTheory, etc., is just a formal version of the concept of Analogy. And then if you can find strong analogies between different portions of code, then maybe you have a redundancy to eliminate there. -- MathieuBouchard