文章基本信息

标题：Nominal Anti-Unification
本地全文：下载
作者：Alexander Baumgartner ; Temur Kutsia ; Jordi Levy 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2015
卷号：36
页码：57-73
DOI：10.4230/LIPIcs.RTA.2015.57
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：We study nominal anti-unification, which is concerned with computing least general generalizations for given terms-in-context. In general, the problem does not have a least general solution, but if the set of atoms permitted in generalizations is finite, then there exists a least general generalization which is unique modulo variable renaming and alpha-equivalence. We present an algorithm that computes it. The algorithm relies on a subalgorithm that constructively decides equivariance between two terms-in-context. We prove soundness and completeness properties of both algorithms and analyze their complexity. Nominal anti-unification can be applied to problems where generalization of first-order terms is needed (inductive learning, clone detection, etc.), but bindings are involved.
关键词：Nominal Anti-Unification; Term-in-context; Equivariance