paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Infinitary intersection types as sequences: A new answer to Klop's problem

作为序列的无穷交类型：Klop 问题的新答案
LICS 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2017匹配度 2/10 · 该论文属于纯类型论与λ演算理论，研究无穷交类型对弱规范化项的刻画并回答Klop问题，与用户关注的ML/Agent程序静态分析、LLM与静态分析/形式化验证交叉、浮点或贝叶斯程序分析均无直接交集。虽属PL与形式化方向，但并非当前研究问题的核心。引用 17 inbox
Pierre Vial
类型系统
crossref: 2026-09-12dblp: 2026-09-12

AI 速览

一句话：提出 System S，用序列化无穷交类型刻画弱规范化项，正面回答 Klop 问题。

本文在无穷 λ 演算中为弱规范化项给出类型论刻画，并正面回答 Klop 问题：是否存在类型系统刻画遗传头规范化（HHN）λ 项。作者将 λ 演算中标准的定量交类型（非幂等交）赋值系统推广到无穷演算。Tatsuta 在 2007 年表明 HHN 无法由有限类型系统刻画；本文证明，若在无穷类型系统中加入称为可逼近性（approximability）的有效性条件，则可以做到。关键观察是，当交类型用多重集表示时，可逼近性无法表达；因此作者用按整数索引的类型序列以余归纳方式替代多重集，定义 System S，从而获得 HHN/弱规范化的刻画。

问题
如何在无穷 λ 演算中类型论地刻画弱规范化项，特别是是否存在类型系统刻画 HHN λ 项，即 Klop 问题。
方法
将定量交类型赋值系统推广到无穷 λ 演算，引入可逼近性有效性条件，并将交的多重集表示改为整数索引的类型序列余归纳表示，定义 System S。
评估
通过理论证明表明 System S 可刻画 HHN/弱规范化项，从而正面回答 Klop 问题；同时说明多重集表示无法表达可逼近性。
原文摘要（Abstract）

We provide a type-theoretical characterization of weakly-normalizing terms in an infinitary lambda-calculus. We adapt for this purpose the standard quantitative (with non-idempotent intersections) type assignment system of the lambda-calculus to our infinite calculus. Our work provides a positive answer to a semi-open question known as Klop's Problem, namely, finding out if there is a type system characterizing the set of hereditary head-normalizing (HHN) lambda-terms. Tatsuta showed in 2007 that HHN could not be characterized by a finite type system. We prove that an infinitary type system endowed with a validity condition called approximability can achieve it. As it turns out, approximability cannot be expressed when intersection is represented by means of multisets. Multisets are then replaced coinductively by sequences of types indexed by integers, thus defining a type system called System S.

链接与引用

DOI 原文 · DBLP

BibTeX 
@inproceedings{Vial17,
  title = {Infinitary intersection types as sequences: A new answer to Klop's problem},
  author = {Pierre Vial},
  booktitle = {LICS},
  year = {2017},
  doi = {10.1109/lics.2017.8005103}
}