2016/12/20 by Pierre Vial, Vial, Pierre
Computer Science · Business, Management and Accounting · #Advanced Database Systems and Queries #Business Process Modeling and Analysis #Service-Oriented Architecture and Web Services
paper · pdf · doi:10.48550/arxiv.1612.06740
Infinite types and formulas are known to have really curious and unsound behaviors. For instance, they allow to type Ω, the auto- autoapplication and they thus do not ensure any form of normalization/productivity. Moreover, in most infinitary frameworks, it is not difficult to define a type R that can be assigned to every λ-term. However, these observations do not say much about what coinductive (i.e. infinitary) type grammars are able to provide: it is for instance very difficult to know what types (besides R) can be assigned to a given term in this setting. We begin with a discussion on the expressivity of different forms of infinite types. Then, using the resource-awareness of sequential intersection types (system S) and tracking, we prove that infinite types are able to characterize the order (arity) of every λ-terms and that, in the infinitary extension of the relational model, every term has a "meaning" i.e. a non-empty denotation. From the technical point of view, we must deal with the total lack of productivity guarantee for typable terms: we do so by importing methods inspired by first order model theory.