DUGiDocsA Variant of Higher-Order Anti-Unification
dc.contributor.author
dc.date.accessioned
2013-10-03T10:16:11Z
dc.date.available
2013-10-03T10:16:11Z
dc.date.issued
2013
dc.identifier.issn
1868-8969
dc.identifier.uri
dc.description.abstract
We present a rule-based Huet’s style anti-unification algorithm for simply-typed lambda-terms in ɳ long β normal form, 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. The algorithm computes it in cubic time within linear space. It has been implemented and the code is freely available
dc.format.mimetype
application/pdf
dc.language.iso
eng
dc.publisher
Dagstuhl Publishing
dc.relation.isformatof
Reproducció digital del document publicat a: http://dx.doi.org/10.4230/LIPIcs.RTA.2013.113
dc.relation.ispartof
Leibniz International Proceedings in Informatics (LIPPICS) : 24th International Conference on Rewriting Techniques and Applications (RTA 2013) : RTA 2013 : June 24-26 2013 : Eindhoven, The Netherlands, vol. 21, p. 113-127
dc.relation.ispartofseries
Articles publicats (D-IMA)
dc.rights
Attribution 3.0 Spain
dc.rights.uri
dc.subject
dc.title
A Variant of Higher-Order Anti-Unification
dc.type
info:eu-repo/semantics/article
dc.rights.accessRights
info:eu-repo/semantics/openAccess
dc.embargo.terms
Cap
dc.type.version
info:eu-repo/semantics/publishedVersion
dc.identifier.doi