2024-03-29T14:15:37Zhttp://digital.csic.es/dspace-oai/requestoai:digital.csic.es:10261/1551702021-12-28T16:31:03Zcom_10261_60com_10261_4col_10261_313
Higher-Order Pattern Anti-Unification in Linear Time
Baumgartner, Alexander
Kutsia, Temur
Levy, Jordi
Villaret, Mateu
Austrian Science Fund
Ministerio de Economía y Competitividad (España)
Universidad de Girona
Generalizations of lambda terms
Anti-unification
Higher-order patterns
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 α-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.
2017-09-15T13:02:18Z
2017-09-15T13:02:18Z
2017
2017-09-15T13:02:19Z
artículo
Journal of Automated Reasoning 58: 293- 310 (2017)
http://hdl.handle.net/10261/155170
10.1007/s10817-016-9383-3
http://dx.doi.org/10.13039/501100002428
http://dx.doi.org/10.13039/501100003329
http://dx.doi.org/10.13039/100008722
30174364
eng
Publisher's version
Sí
info:eu-repo/grantAgreement/MINECO/Plan Estatal de Investigación Científica y Técnica y de Innovación 2013-2016/TIN2015-66293-R
info:eu-repo/grantAgreement/MINECO/Plan Estatal de Investigación Científica y Técnica y de Innovación 2013-2016//TIN2015-71799-C2-1-P
http://creativecommons.org/licenses/by/4.0/
openAccess
Springer