Tags:Anti-Unification, Functional Programming, Generalization, Nominal Techniques and Recursive Let
Abstract:
This paper describes anti-unification algorithms for computing least general generalizations of two expressions in a functional programming language with recursive let. First, by exploring a semantic approach to the problem, we argue for an improvement of the technique used in previous papers which avoids infinite chains of less general generalizations. Second, we present a (non-deterministic) nominal general anti-unification algorithm applicable to general expressions, which is complete, terminating and requires polynomial time. Third, we propose a specialized anti-unification algorithm applicable to two or more garbage-free ground expressions that produces a single least general generalization in polynomial time, and which can also exploit further semantically correct equivalences. Our results have potential applications in finding clones in functional programs.
Towards Fast Nominal anti-Unification of Letrec-Expressions