Date(s) - 07/06/2018
11 h 00 min - 12 h 30 min
An intersection type system with given features (strict or not, idempotent or not, relevant or not, rigid or not…) characterizing, e.g., a notion of normalization can be presented in various ways. Recent works by Asada, Ong and Tsukada have championed a rigid description of resources. Whereas in non-rigid paradigms (e.g., standard Taylor expansion or non-idempotent intersection types), bags of resources are multisets and invariant under permutation, in the rigid ones, permutations must be processed explicitly and can be allowed or disallowed. Rigidity enables a fine-grained control of reduction paths and their effects on, e.g., typing derivations. We previously introduced system S, featuring a sequential intersection: a sequence is a family of types indexed by a set of integers. However, one may wonder in what extent the absence of permutations causes a loss of expressivity w.r.t. reduction paths, compared to a usual multiset framework or a rigid one with permutations. Our main contribution is to prove that not only every non-idempotent derivation can be represented by a rigid, permutation-free derivation, but also that any dynamic behavior may be captured in this way. In other words, we prove that system S (sequential intersection) has full expressive power over multiset/ permutation-inclusive intersection. We do so in the most general setting, i.e. by considering coinductive type grammars, so that this work also applies in the study of the infinitary relational model.