Higher-Order Pattern Anti-Unification in Linear Time

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 [Formula: see text] -equivalence...

Descripción completa

Detalles Bibliográficos
Autores principales: Baumgartner, Alexander, Kutsia, Temur, Levy, Jordi, Villaret, Mateu
Formato: Online Artículo Texto
Lenguaje:English
Publicado: Springer Netherlands 2016
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC6109779/
https://www.ncbi.nlm.nih.gov/pubmed/30174364
http://dx.doi.org/10.1007/s10817-016-9383-3
_version_ 1783350377867902976
author Baumgartner, Alexander
Kutsia, Temur
Levy, Jordi
Villaret, Mateu
author_facet Baumgartner, Alexander
Kutsia, Temur
Levy, Jordi
Villaret, Mateu
author_sort Baumgartner, Alexander
collection PubMed
description 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 [Formula: see text] -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.
format Online
Article
Text
id pubmed-6109779
institution National Center for Biotechnology Information
language English
publishDate 2016
publisher Springer Netherlands
record_format MEDLINE/PubMed
spelling pubmed-61097792018-08-31 Higher-Order Pattern Anti-Unification in Linear Time Baumgartner, Alexander Kutsia, Temur Levy, Jordi Villaret, Mateu J Autom Reason Article 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 [Formula: see text] -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. Springer Netherlands 2016-07-27 2017 /pmc/articles/PMC6109779/ /pubmed/30174364 http://dx.doi.org/10.1007/s10817-016-9383-3 Text en © The Author(s) 2016 Open AccessThis article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.
spellingShingle Article
Baumgartner, Alexander
Kutsia, Temur
Levy, Jordi
Villaret, Mateu
Higher-Order Pattern Anti-Unification in Linear Time
title Higher-Order Pattern Anti-Unification in Linear Time
title_full Higher-Order Pattern Anti-Unification in Linear Time
title_fullStr Higher-Order Pattern Anti-Unification in Linear Time
title_full_unstemmed Higher-Order Pattern Anti-Unification in Linear Time
title_short Higher-Order Pattern Anti-Unification in Linear Time
title_sort higher-order pattern anti-unification in linear time
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC6109779/
https://www.ncbi.nlm.nih.gov/pubmed/30174364
http://dx.doi.org/10.1007/s10817-016-9383-3
work_keys_str_mv AT baumgartneralexander higherorderpatternantiunificationinlineartime
AT kutsiatemur higherorderpatternantiunificationinlineartime
AT levyjordi higherorderpatternantiunificationinlineartime
AT villaretmateu higherorderpatternantiunificationinlineartime

Ejemplares similares