Higher-Order Pattern Anti-Unification in Linear Time

Consultar RECERCAT

Para acceder a los documentos con el texto completo, por favor, siga el siguiente enlace: http://hdl.handle.net/10256/14604

Título:	Higher-Order Pattern Anti-Unification in Linear Time
Autor/a:	Baumgartner, Alexander; Kutsia, Temur; Levy, Jordi; Villaret i Ausellé, Mateu
Otros autores:	Ministerio de Economía y Competitividad (Espanya)
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
Abstract:	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
Materia(s):	-Algorismes computacionals -Computer algorithms -Lògica matemàtica -Logic, Symbolic and mathematical
Derechos:	Attribution 3.0 Spain http://creativecommons.org/licenses/by/3.0/es/
Tipo de documento:	Artículo Artículo - Versión publicada
Editor:	Springer Verlag
Compartir: