Fraunhofer-Gesellschaft

Publica

Hier finden Sie wissenschaftliche Publikationen aus den Fraunhofer-Instituten.

Intersection type calculi of bounded dimension

 
: Dudenhefner, A.; Rehof, J.

:

Castagna, G. ; Association for Computing Machinery -ACM-; Association for Computing Machinery -ACM-, Special Interest Group on Programming Languages -SIGPLAN-; Association for Computing Machinery -ACM-, Special Interest Group on Algorithms and Computation Theory -SIGACT-:
POPL 2017, 44th ACM SIGPLAN Symposium on Principles of Programming Languages. Proceedings : Paris, France, January 15-21, 2017
New York: ACM, 2017
ISBN: 978-1-4503-4660-3
pp.653-665
Symposium on Principles of Programming Languages (POPL) <44, 2017, Paris>
English
Conference Paper
Fraunhofer ISST ()

Abstract
A notion of dimension in intersection typed λ-calculi is presented. The dimension of a typed λ-term is given by the minimal norm of an elaboration (a proof theoretic decoration) necessary for typing the term at its type, and, intuitively, measures intersection introduction as a resource. Bounded-dimensional intersection type calculi are shown to enjoy subject reduction, since terms can be elaborated in non-increasing norm under β-reduction. We prove that a multiset interpretation (corresponding to a non-idempotent and non-linear interpretation of intersection) of dimensionality corresponds to the number of simultaneous constraints required during search for inhabitants. As a consequence, the inhabitation problem is decidable in bounded multiset dimension, and it is proven to be EXPSPACE-complete. This result is a substantial generalization of inhabitation for the rank 2-fragment, yielding a calculus with decidable inhabitation which is independent of rank. Our results give rise to a new criterion (dimensional bound) for subclasses of intersection type calculi with a decidable inhabitation problem, which is orthogonal to previously known criteria, and which should have immediate applications in synthesis. Additionally, we give examples of dimensional analysis of fragments of the intersection type system, including conservativity over simple types, rank 2-types, and normal form typings, and we provide some observations towards dimensional analysis of other systems. It is suggested (for future work) that our notion of dimension may have semantic interpretations in terms of of reduction complexity.

: http://publica.fraunhofer.de/documents/N-589659.html