Document

**Published in:** LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

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.

Andrej Dudenhefner, Moritz Martens, and Jakob Rehof. The Intersection Type Unification Problem. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 19:1-19:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{dudenhefner_et_al:LIPIcs.FSCD.2016.19, author = {Dudenhefner, Andrej and Martens, Moritz and Rehof, Jakob}, 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 = {Kesner, Delia and Pientka, Brigitte}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.19}, URN = {urn:nbn:de:0030-drops-59955}, doi = {10.4230/LIPIcs.FSCD.2016.19}, annote = {Keywords: Intersection Type, Equational Theory, Unification, Tiling, Complexity} }

Document

**Published in:** LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

In combinatory logic one usually assumes a fixed set of basic combinators (axiom schemes), usually K and S. In this setting the set of provable formulas (inhabited types) is PSPACE-complete in simple types and undecidable in intersection types. When arbitrary sets of axiom schemes are considered, the inhabitation problem is undecidable even in simple types (this is known as Linial-Post theorem).
k-bounded combinatory logic with intersection types arises from combinatory logic by imposing the bound k on the depth of types (formulae) which may be substituted for type variables in axiom schemes. We consider the inhabitation (provability) problem for k-bounded combinatory logic: Given an arbitrary set of typed combinators and a type tau, is there a combinatory term of type tau in k-bounded combinatory logic?
Our main result is that the problem is (k+2)-EXPTIME complete for k-bounded combinatory logic with intersection types, for every fixed k
(and hence non-elementary when k is a parameter). We also show that the problem is EXPTIME-complete for simple types, for all k.
Theoretically, our results give new insight into the expressive power of intersection types. From an application perspective, our results are useful as a foundation for composition synthesis based on combinatory logic.

Boris Düdder, Moritz Martens, Jakob Rehof, and Pawel Urzyczyn. Bounded Combinatory Logic. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 243-258, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{dudder_et_al:LIPIcs.CSL.2012.243, author = {D\"{u}dder, Boris and Martens, Moritz and Rehof, Jakob and Urzyczyn, Pawel}, title = {{Bounded Combinatory Logic}}, booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL}, pages = {243--258}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-42-2}, ISSN = {1868-8969}, year = {2012}, volume = {16}, editor = {C\'{e}gielski, Patrick and Durand, Arnaud}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.243}, URN = {urn:nbn:de:0030-drops-36763}, doi = {10.4230/LIPIcs.CSL.2012.243}, annote = {Keywords: Intersection types, Inhabitation, Composition synthesis} }