Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH scholarly article en Libal, Tomer; Miller, Dale https://www.dagstuhl.de/lipics License: Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-59810
URL:

;

Functions-as-Constructors Higher-Order Unification

pdf-format:


Abstract

Unification is a central operation in the construction of a range of computational logic systems based on first-order and higher-order logics. First-order unification has a number of properties that dominates the way it is incorporated within such systems. In particular, first-order unification is decidable, unary, and can be performed on untyped term structures. None of these three properties hold for full higher-order unification: unification is undecidable, unifiers can be incomparable, and term-level typing can dominate the search for unifiers. The so-called pattern subset of higher-order unification was designed to be a small extension to first-order unification that respected the basic laws governing lambda-binding (the equalities of alpha, beta, and eta-conversion) but which also satisfied those three properties. While the pattern fragment of higher-order unification has been popular in various implemented systems and in various theoretical considerations, it is too weak for a number of applications. In this paper, we define an extension of pattern unification that is motivated by some existing applications and which satisfies these three properties. The main idea behind this extension is that the arguments to a higher-order, free variable can be more than just distinct bound variables: they can also be terms constructed from (sufficient numbers of) such variables using term constructors and where no argument is a subterm of any other argument. We show that this extension to pattern unification satisfies the three properties mentioned above.

BibTeX - Entry

@InProceedings{libal_et_al:LIPIcs:2016:5981,
  author =	{Tomer Libal and Dale Miller},
  title =	{{Functions-as-Constructors Higher-Order Unification}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{26:1--26:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Delia Kesner and Brigitte Pientka},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/5981},
  URN =		{urn:nbn:de:0030-drops-59810},
  doi =		{10.4230/LIPIcs.FSCD.2016.26},
  annote =	{Keywords: higher-order unification, pattern unification}
}

Keywords: higher-order unification, pattern unification
Seminar: 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Issue date: 2016
Date of publication: 17.06.2016


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI