一句话：证明在无穷关系模型中每个 λ 项都有非空指称，并用无穷交类型刻画其元数。
无穷类型与公式常表现出奇特且不可靠的行为：它们可以给自应用项 Ω 赋予类型，因而不能保证规范化或生产率；在多数无穷框架中还容易定义可赋给所有 λ 项的万能类型 R。然而，这并不说明无穷类型语法能提供什么，尤其难以判断给定项除 R 外还能获得哪些类型。本文先讨论不同无穷类型形式的表达力，随后利用顺序交类型（系统 S）的资源感知特性与 tracking，证明无穷类型能够刻画每个 λ 项的 arity，并证明在关系模型的无穷扩展中每个项都有“意义”，即非空指称。技术难点在于可类型化项完全不保证生产率，作者通过引入受一阶模型论启发的方法来处理。
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 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 guarantee of productivity for typable terms: we do so by importing methods inspired by first order model theory.
DOI 原文 ·
@inproceedings{paperbot4304,
title = {Every λ-Term is Meaningful for the Infinitary Relational Model},
author = {Pierre Vial},
booktitle = {LICS},
year = {2018},
doi = {10.1145/3209108.3209133}
}