2024-03-29T11:58:04Zhttp://digital.csic.es/dspace-oai/requestoai:digital.csic.es:10261/1332702017-06-07T15:16:06Zcom_10261_60com_10261_4col_10261_439
DIGITAL.CSIC
author
Baumgartner, Alexander
author
Kutsia, Temur
author
Levy, Jordi
author
Villaret, Mateu
funder
Generalitat de Catalunya
funder
Ministerio de Economía y Competitividad (España)
2016-06-09T16:45:25Z
2016-06-09T16:45:25Z
2013-06-24
24th International Conference on Rewriting Techniques and Applications, RTA 2013; Eindhoven; Netherlands; 24 June 2013 through 26 June 2013. Leibniz International Proceedings in Informatics, LIPIcs, vol. 21, 2013, pp. 113-127
http://hdl.handle.net/10261/133270
10.4230/LIPIcs.RTA.2013.113
http://dx.doi.org/10.13039/501100002809http://dx.doi.org/10.13039/501100003329
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. © Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret; licensed under Creative Commons License CC-BY 24th International Conference on Rewriting Techniques and Applications (RTA'13).
eng
openAccess
Higher-order anti-unification
Higher-order patterns
A Variant of Higher-Order Anti-Unification
comunicación de congreso
TGljZW5jaWEgQ1NJQyAKClBhcmEgcXVlIGVsIHJlcG9zaXRvcmlvIERpZ2l0YWwuQ1NJQyBwdWVkYSBhbG1hY2VuYXIgeSBkaXN0cmlidWlyIGVsIG9iamV0byBkaWdpdGFsIGRlcG9zaXRhZG8sIAplcyBuZWNlc2FyaW8gcXVlIGxhIHBlcnNvbmEgcXVlIGhhZ2EgZWwgZGVww7NzaXRvIGxlYSB5IGFjZXB0ZSBsYXMgY29uZGljaW9uZXMgZXN0YWJsZWNpZGFzIGVuIAplc3RhIGxpY2VuY2lhOiAKCkVsL2xvcyBhdXRvci9lcyBvIHBvc2VlZG9yL2VzIGRlbCBjb3B5cmlnaHQgZGVsIHRyYWJham8gZGVwb3NpdGFkbyBvIGVuIHN1IGNhc28gbGEgcGVyc29uYSAKZGVsZWdhZGEgcGFyYSBoYWNlcmxvLCBnYXJhbnRpemEgYWwgQ1NJQyBlbCBkZXJlY2hvIG5vIGV4Y2x1c2l2byBwYXJhIGRpc3RyaWJ1aXIsIGFsbWFjZW5hciB5IApwcmVzZXJ2YXIgZW4gZm9ybWF0byBlbGVjdHLDs25pY28gZWwgb2JqZXRvIGRpZ2l0YWwgZGVwb3NpdGFkby4KCkVsIGRlcG9zaXRhbnRlLCBlbiBjYXNvIGRlIHVuYSBvYnJhIGNvbiBtw6FzIGRlIHVuIGF1dG9yLCBnYXJhbnRpemEgcXVlIGxvIGhhY2UgcmVzcG9uc2FibGVtZW50ZSAKZW4gbm9tYnJlIHkgY29uIGNvbnNlbnRpbWllbnRvIGRlIGxvcyBkZW3DoXMgY29hdXRvcmVzLgoKRGVjbGFyYSBxdWUgc2UgdHJhdGEgZGUgdW4gdHJhYmFqbyBvcmlnaW5hbCB5IG5vIGVzdGEgc3VqZXRvIGEgcmVzdHJpY2Npb25lcyBkZSBjb3B5cmlnaHQgY29uIAp0ZXJjZXJvcyBwYXJhIHBvZGVyIG90b3JnYXIgYWwgQ1NJQyBsb3MgZGVyZWNob3MgcmVxdWVyaWRvcyBlbiBlc3RhIGxpY2VuY2lhLgoKU2kgZWwgdHJhYmFqbyBkZXBvc2l0YWRvIGNvbnRpZW5lIG1hdGVyaWFsIGRlbCBxdWUgZWwgYXV0b3Igbm8gcG9zZWUgZWwgY29weXJpZ2h0LCBlbCBhdXRvciAKZGVjbGFyYSBxdWUgaGEgb2J0ZW5pZG8gZWwgcGVybWlzbyBuZWNlc2FyaW8gZGVsIHByb3BpZXRhcmlvIGRlbCBjb3B5cmlnaHQgcGFyYSBnYXJhbnRpemFyIGFsIApDU0lDIGxvcyBkZXJlY2hvcyBkZXNjcml0b3MgZW4gZXN0YSBsaWNlbmNpYSwgeSBxdWUgZWwgcG9zZWVkb3IgZGVsIGNvcHlyaWdodCBlc3TDoSBjbGFyYW1lbnRlIAppZGVudGlmaWNhZG8geSByZWNvbm9jaWRvIGVuIGVsIHRleHRvIG8gY29udGVuaWRvIGRlbCBhcmNoaXZvIGRlcG9zaXRhZG8uCgpFbCBhdXRvciBhY2VwdGEgcXVlIGVsIENTSUMgcHVlZGUsIHNpbiByZWFsaXphciBjYW1iaW9zIGVuIGVsIGNvbnRlbmlkbywgY29udmVydGlyIGVsIHRyYWJham8gYSAKY3VhbHF1aWVyIG1lZGlvIG8gZm9ybWF0byBjb24gb2JqZXRpdm9zIGRlIHByZXNlcnZhY2nDs24uCgpBc2ltaXNtbyBlbCBhdXRvciBhY2VwdGEgcXVlIGVsIENTSUMgcHVlZGUgY29uc2VydmFyIG3DoXMgZGUgdW5hIGNvcGlhIGRlIGVzdGUgdHJhYmFqbyBwYXJhIGdhcmFudGl6YXIgCmxhIHNlZ3VyaWRhZCB5IGxhIHByZXNlcnZhY2nDs24gZGUgbG9zIGFyY2hpdm9zLgoKRWwgQ1NJQyBwcmVzZXJ2YXLDoSB5IGRpZnVuZGlyw6EgZXN0ZSB0cmFiYWpvLiBFbiBlbCBjYXNvIGRlIHF1ZSBubyBwdWVkYSBjb250aW51YXIgbWFudGVuaWVuZG8gZWwgCmFyY2hpdm8gY29tbyBwYXJ0ZSBkZWwgcmVwb3NpdG9yaW8gaW5zdGl0dWNpb25hbCBzZSByZXNlcnZhIGVsIGRlcmVjaG8gZGUgZGV2b2x2ZXIgZWwgY29udGVuaWRvIGFsIApkZXBvc2l0YW50ZS4gU2kgZXN0byBubyBlcyBwb3NpYmxlIChwb3JxdWUgbGEgY29tdW5pZGFkLCBjb2xlY2Npw7NuIGV0Yy4geWEgbm8gZXhpc3RhIG8gZWwgYXV0b3Igbm8gCmVzdMOpIGxvY2FsaXphYmxlKSwgZWwgbWF0ZXJpYWwgcG9kcsOtYSBzZXIgYXJjaGl2YWRvIGNvbW8gcGFydGUgZGVsIGFyY2hpdm8gZGlnaXRhbCBkZSBsYSBpbnN0aXR1Y2nDs24uIAoKU2kgbGEgY29udHJpYnVjacOzbiBzZSBiYXNhIGVuIHRyYWJham9zIGZpbmFuY2lhZG9zIG8gcGF0cm9jaW5hZG9zIHBvciBvcmdhbml6YWNpb25lcyBkaXN0aW50YXMgYWwgCkNTSUMsIGRlY2xhcmEgaGFiZXIgY3VtcGxpZG8gY29uIGN1YWxxdWllciBkZXJlY2hvIHkgb2JsaWdhY2nDs24gZXhwcmVzYWRvcyBlbiBlbCBjb250cmF0byBvIGFjdWVyZG8gCmNvbiBkaWNoYXMgb3JnYW5pemFjaW9uZXMuIAoKRWwgbm9tYnJlIGRlbCBkZXBvc2l0YW50ZSBxdWVkYXLDoSBjbGFyYW1lbnRlIGlkZW50aWZpY2FkbyBwb3IgZWwgQ1NJQyBjb21vIGVsIGRlbCBhdXRvciBvIHByb3BpZXRhcmlvIApkZSBsYSBjb250cmlidWNpw7NuLCB5IGVsIENTSUMgbm8gcmVhbGl6YXLDoSBuaW5ndW5hIGFsdGVyYWNpw7NuIGRlIHN1IGNvbnRyaWJ1Y2nDs24sIGV4Y2VwdG8gbGFzIHJlZmVyaWRhcyAKYWwgZm9ybWF0bywgcGVybWl0aWRhcyBwb3IgZXN0YSBsaWNlbmNpYS4K
URL
https://digital.csic.es/bitstream/10261/133270/1/LIPIcs.v21.2013.113-27.pdf
File
MD5
4f30c3f141b531236f9af422700b96d0
500839
application/octet-stream
LIPIcs.v21.2013.113-27.pdf