## 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: | 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. |

Pages: | 10 |

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

Paper: |