DUGiDocsHigher-Order Pattern Anti-Unification in Linear Time
dc.contributor.author
dc.date.accessioned
2017-11-24T07:37:50Z
dc.date.available
2017-11-24T07:37:50Z
dc.date.issued
2017-02-01
dc.identifier.issn
0168-7433
dc.identifier.uri
dc.description.abstract
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
dc.description.sponsorship
This research has been partially supported by the Austrian Science Fund (FWF) project SToUT (P 24087-N18), the Upper Austrian Government strategic program “Innovatives OÖ 2010plus”, the MINECO projects RASO (TIN2015-71799-C2-1-P) and HeLo (TIN2012-33042), the MINECO/FEDER UE project LoCoS (TIN2015-66293-R) and the UdG project MPCUdG2016/055
dc.format.mimetype
application/pdf
dc.language.iso
eng
dc.publisher
Springer Verlag
dc.relation
info:eu-repo/grantAgreement/MINECO//TIN2012-33042/ES/HERRAMIENTAS LOGICAS PARA PROBLEMAS COMBINATORIOS/
info:eu-repo/grantAgreement/MINECO//TIN2015-66293-R/ES/LOGICA PARA PROBLEMAS COMBINATORIOS/
dc.relation.isformatof
Reproducció digital del document publicat a: https://doi.org/10.1007/s10817-016-9383-3
dc.relation.ispartof
Journal of Automated Reasoning, 2017, vol. 58, núm. 2, p. 293-310
dc.relation.ispartofseries
Articles publicats (D-IMA)
dc.rights
Attribution 3.0 Spain
dc.rights.uri
dc.subject
dc.title
Higher-Order Pattern Anti-Unification in Linear Time
dc.type
info:eu-repo/semantics/article
dc.rights.accessRights
info:eu-repo/semantics/openAccess
dc.type.version
info:eu-repo/semantics/publishedVersion
dc.identifier.doi
dc.identifier.idgrec
026315
dc.contributor.funder
dc.relation.ProjectAcronym
dc.identifier.eissn
1573-0670