The Intersection Type Unification Problem
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.
Intersection Type
Equational Theory
Unification
Tiling
Complexity
19:1-19:16
Regular Paper
Andrej
Dudenhefner
Andrej Dudenhefner
Moritz
Martens
Moritz Martens
Jakob
Rehof
Jakob Rehof
10.4230/LIPIcs.FSCD.2016.19
S. Anantharaman, P. Narendran, and M. Rusinowitch. Acid-unification is NEXPTIME-decidable. In Mathematical Foundations of Computer Science 2003, pages 169-178. Springer, 2003.
S. Anantharaman, P. Narendran, and M. Rusinowitch. Unification Modulo ACUI Plus Distributivity Axioms. Journal of Automated Reasoning, 33(1):1-28, 2004.
F. Baader and P. Narendran. Unification of Concept Terms in Description Logics. Journal of Symbolic Computation, 31:277-305, 2001.
H. Barendregt, M. Coppo, and M. Dezani-Ciancaglini. A Filter Lambda Model and the Completeness of Type Assignment. Journal of Symbolic Logic, 48(4):931-940, 1983. URL: http://dx.doi.org/10.2307/2273659.
http://dx.doi.org/10.2307/2273659
H. Barendregt, W. Dekkers, and R. Statman. Lambda Calculus with Types. Perspectives in Logic, Cambridge University Press, 2013.
G. Boudol and P. Zimmer. On type inference in the intersection type discipline. Electr. Notes Theor. Comput. Sci., 136:23-42, 2005. URL: http://dx.doi.org/10.1016/j.entcs.2005.06.016.
http://dx.doi.org/10.1016/j.entcs.2005.06.016
G. Castagna, K. Nguyen, Z. Xu, and P. Abate. Polymorphic functions with set-theoretic types: Part 2: Local type inference and type reconstruction. In Principles of Programming Languages POPL 2015, pages 289-302. ACM, 2015.
W. Charatonik and L. Pacholski. Set constraints with projections are in NEXPTIME. In 35th Annual Symposium on Foundations of Computer Science, pages 642-653. IEEE, 1994. URL: http://dx.doi.org/10.1109/SFCS.1994.365727.
http://dx.doi.org/10.1109/SFCS.1994.365727
B. S. Chlebus. Domino-tiling games. Journal of Computer and System Sciences, 32(3):374-392, 1986.
M. Coppo and P. Giannini. Principal types and unification for a simple intersection type system. Inf. Comput., 122(1):70-96, 1995. URL: http://dx.doi.org/10.1006/inco.1995.1141.
http://dx.doi.org/10.1006/inco.1995.1141
M. Dezani-Ciancaglini and J. R. Hindley. Intersection Types for Combinatory Logic. Theoretical Computer Science, 100(2):303-324, 1992.
B. Düdder, M. Martens, and J. Rehof. Intersection Type Matching with Subtyping. In Proceedings of TLCA'13, Springer LNCS, 2013.
B. Düdder, M. Martens, J. Rehof, and P. Urzyczyn. Bounded Combinatory Logic. In Proceedings of CSL'12, volume 16 of LIPIcs, pages 243-258, 2012.
J. R. Hindley. The Simple Semantics for Coppo-Dezani-Sallé Types. In International Symposium on Programming, volume 137 of LNCS, pages 212-226. Springer, 1982.
J. R. Hindley and J. P. Seldin. Lambda-calculus and Combinators, an Introduction. Cambridge University Press, 2008.
A. J. Kfoury. Beta-reduction as unification. Banach Center Publications, 46(1):137-158, 1999.
A. J. Kfoury and J. B. Wells. Principality and Type Inference for Intersection Types Using Expansion Variables. Theor. Comput. Sci., 311(1-3):1-70, 2004.
T. Kurata and M. Takahashi. Decidable properties of intersection type systems. In TLCA, volume 902 of LNCS, pages 297-311. Springer, 1995.
J. Rehof and P. Urzyczyn. Finite Combinatory Logic with Intersection Types. In Proceedings of TLCA'11, volume 6690 of LNCS, pages 169-183. Springer, 2011.
J. Rehof and P. Urzyczyn. The Complexity of Inhabitation with Explicit Intersection. In Kozen Festschrift, volume 7230 of LNCS, pages 256-270. Springer, 2012.
S. Ronchi Della Rocca. Principal Type Scheme and Unification for Intersection Type Discipline. Theor. Comput. Sci., 59:181-209, 1988.
R. Statman. A finite model property for intersection types. In Proceedings Seventh Workshop on Intersection Types and Related Systems, ITRS 2014, Vienna, Austria, 18 July 2014., pages 1-9, 2015. URL: http://dx.doi.org/10.4204/EPTCS.177.1.
http://dx.doi.org/10.4204/EPTCS.177.1
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode