Hier finden Sie wissenschaftliche Publikationen aus den Fraunhofer-Instituten.

Typability in bounded dimension

: Dudenhefner, A.; Rehof, J.

Aceto, L. ; Association for Computing Machinery -ACM-; Institute of Electrical and Electronics Engineers -IEEE-:
32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017 : 20-23 June 2017, Reykjavík, Iceland
Piscataway, NJ: IEEE, 2017
ISBN: 978-1-5090-3018-7
ISBN: 978-1-5090-3019-4
Art. 67, 12 pp.
Symposium on Logic in Computer Science (LICS) <32, 2017, Reykjavík>
Conference Paper
Fraunhofer ISST ()

Recently (authors, POPL 2017), a notion of dimensionality for intersection types was introduced, and it was shown that the bounded-dimensional inhabitation problem is decidable under a non-idempotent interpretation of intersection and undecidable in the standard set-theoretic model. In this paper we study the typability problem for bounded-dimensional intersection types and prove that the problem is decidable in both models. We establish a number of bounding principles depending on dimension. In particular, it is shown that dimensional bound on derivations gives rise to a bounded width property on types, which is related to a generalized subformula property for typings of arbitrary terms. Using the bounded width property we can construct a nondeterministic transformation of the typability problem to unification, and we prove that typability in the set-theoretic model is PSPACE-complete, whereas it is in NP in the multiset model.