Item


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 α-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

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

Springer Verlag

Manager: Ministerio de Economía y Competitividad (Espanya)
Author: Baumgartner, Alexander
Kutsia, Temur
Levy, Jordi
Villaret i Ausellé, Mateu
Date: 2017 February 1
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
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
Format: application/pdf
Document access: http://hdl.handle.net/10256/14604
Language: eng
Publisher: Springer Verlag
Collection: info:eu-repo/semantics/altIdentifier/doi/10.1007/s10817-016-9383-3
info:eu-repo/semantics/altIdentifier/issn/0168-7433
info:eu-repo/semantics/altIdentifier/eissn/1573-0670
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/
Rights: Attribution 3.0 Spain
Rights URI: http://creativecommons.org/licenses/by/3.0/es/
Subject: Algorismes computacionals
Computer algorithms
Lògica matemàtica
Logic, Symbolic and mathematical
Title: Higher-Order Pattern Anti-Unification in Linear Time
Type: info:eu-repo/semantics/article
Repository: DUGiDocs

Subjects

Authors