Every λ-Term is Meaningful for the Infinitary Relational Model

Author: Pierre Vial

Paper Information

Title:Every λ-Term is Meaningful for the Infinitary Relational Model
Authors:Pierre Vial
Proceedings:LICS PDF files
Editors: Anuj Dawar and Erich Grädel
Keywords:lambda-calculus, coinduction, relational model, denotation, semantics, intersection types, sequential types, non-idempotency

ABSTRACT. 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.

Talk:Jul 09 17:20 (Session 51E)