Go to page
 

Bibliographic Metadata

Title
Higher-Order Pattern Anti-Unification in Linear Time
AuthorBaumgartner, Alexander ; Kutsia, Temur ; Levy, Jordi ; Villaret, Mateu
Published in
Journal of Automated Reasoning, 2016, Vol. 58, Issue 2, page 293-310
PublishedSpringer, 2016
LanguageEnglish
Document typeJournal Article
Keywords (EN)Generalizations of lambda terms / Anti-unification / Higher-order patterns
Project-/ReportnumberP 24087-N18
Project-/ReportnumberTIN2015-71799-C2-1-P
Project-/ReportnumberTIN2012-33042
Project-/ReportnumberTIN2015-66293-R
Project-/ReportnumberMPCUdG2016/055
ISSN1573-0670
URNurn:nbn:at:at-ubl:3-1247 Persistent Identifier (URN)
DOI10.1007/s10817-016-9383-3 
Restriction-Information
 The work is publicly available
Files
Higher-Order Pattern Anti-Unification in Linear Time [0.51 mb]
Links
Reference
Classification
Abstract (English)

We present a rule-based Huets 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.

Stats
The PDF-Document has been downloaded 3 times.
License
CC-BY-License (4.0)Creative Commons Attribution 4.0 International License