Search

We present a rule-based Huet's style anti-unification algorithm for simply typed lambda-terms, which computes a least general higher-order pattern generalization. For a pair of arbitrary terms of the same type, such a generalization always exists and is unique modulo $$\alpha $$ -equivalence and variable renaming. With a minor modification, the algorithm works for untyped lambda-terms as well. The time complexity of both algorithms is linear. [ABSTRACT FROM AUTHOR]

We study anti-unification for unranked terms and hedges that may contain term and hedge variables. The anti-unification problem of two hedges ${\tilde{s}}_1$ and ${\tilde{s}}_2$ is concerned with finding their generalization, a hedge ${\tilde{q}}$ such that both ${\tilde{s}}_1$ and ${\tilde{s}}_2$ are instances of ${\tilde{q}}$ under some substitutions. Hedge variables help to fill in gaps in generalizations, while term variables abstract single (sub)terms with different top function symbols. First, we design a complete and minimal algorithm to compute least general generalizations. Then, we improve the efficiency of the algorithm by restricting possible alternatives permitted in the generalizations. The restrictions are imposed with the help of a rigidity function, which is a parameter in the improved algorithm and selects certain common subsequences from the hedges to be generalized. The obtained rigid anti-unification algorithm is further made more precise by permitting combination of hedge and term variables in generalizations. Finally, we indicate a possible application of the algorithm in software engineering. [ABSTRACT FROM AUTHOR]