All the {\lambda}-Terms are Meaningful for the Infinitary Relational Model

TL;DR

This paper demonstrates that in an infinitary relational model, all lambda-terms are meaningful, and infinite types can characterize term arity, overcoming traditional issues with non-normalizing infinite types.

Contribution

It proves that every lambda-term has a non-empty denotation in the infinitary relational model using resource-aware intersection types and model-theoretic methods.

Findings

All lambda-terms have non-empty denotation in the infinitary relational model.

Infinite types can characterize the arity of every lambda-term.

Resource-awareness and tracking enable meaningful interpretation of all terms.

Abstract

Infinite types and formulas are known to have really curious and unsound behaviors. For instance, they allow to type {\Omega}, 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 {\lambda}-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 {\lambda}-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.