License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2016.19
URN: urn:nbn:de:0030-drops-59955
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/5995/
Go to the corresponding LIPIcs Volume Portal

Dudenhefner, Andrej ; Martens, Moritz ; Rehof, Jakob

The Intersection Type Unification Problem

pdf-format:
LIPIcs-FSCD-2016-19.pdf (0.5 MB)

Abstract

The intersection type unification problem is an important component in
proof search related to several natural decision problems in
intersection type systems. It is unknown and remains open whether the
unification problem is decidable. We give the first nontrivial lower
bound for the problem by showing (our main result) that it is
exponential time hard. Furthermore, we show that this holds even under
rank 1 solutions (substitutions whose codomains are restricted to
contain rank 1 types). In addition, we provide a fixed-parameter
intractability result for intersection type matching (one-sided
unification), which is known to be NP-complete.

We place the intersection type unification problem in the context of
unification theory. The equational theory of intersection types can
be presented as an algebraic theory with an ACI (associative,
commutative, and idempotent) operator (intersection type) combined
with distributivity properties with respect to a second operator
(function type). Although the problem is algebraically natural and
interesting, it appears to occupy a hitherto unstudied place in the
theory of unification, and our investigation of the problem suggests
that new methods are required to understand the problem. Thus, for the
lower bound proof, we were not able to reduce from known results in
ACI-unification theory and use game-theoretic methods for two-player
tiling games.

BibTeX - Entry

@InProceedings{dudenhefner_et_al:LIPIcs:2016:5995,
  author =	{Andrej Dudenhefner and Moritz Martens and Jakob Rehof},
  title =	{{The Intersection Type Unification Problem}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{19:1--19:16},
  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/5995},
  URN =		{urn:nbn:de:0030-drops-59955},
  doi =		{10.4230/LIPIcs.FSCD.2016.19},
  annote =	{Keywords: Intersection Type, Equational Theory, Unification, Tiling, Complexity}
}

Keywords: Intersection Type, Equational Theory, Unification, Tiling, Complexity
Collection: 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