Every -term is meaningful for the infinitary relational model
From MaRDI portal
Publication:5145369
DOI10.1145/3209108.3209133zbMATH Open1453.03011arXiv1612.06740OpenAlexW2799073568MaRDI QIDQ5145369FDOQ5145369
Authors: Pierre Vial 
Publication date: 20 January 2021
Published in: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/1612.06740
Recommendations
Cited In (1)
This page was built for publication: Every \(\lambda \)-term is meaningful for the infinitary relational model
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5145369)
