Higher-Order Pattern Anti-Unification in Linear Time

详细信息    查看全文

• 作者：Alexander Baumgartner ; Temur Kutsia ; Jordi Levy…
• 关键词：Generalizations of lambda terms ; Anti ; unification ; Higher ; order patterns
• 刊名：Journal of Automated Reasoning
• 出版年：2017
• 出版时间：February 2017
• 年：2017
• 卷：58
• 期：2
• 页码：293-310
• 全文大小：531KB
• 刊物类别：Computer Science
• 刊物主题：Mathematical Logic and Formal Languages; Artificial Intelligence (incl. Robotics); Mathematical Logic and Foundations; Symbolic and Algebraic Manipulation;
• 出版者：Springer Netherlands
• ISSN：1573-0670
• 卷排序：58

文摘

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.