无置换表示置换，或序列类型的表达能力
计算机科学中的逻辑
2018-01-25 v2
摘要
Asada、Ong 和 Tsukada 近期的研究倡导一种严格的资源描述方式。在非严格范式（例如标准 Taylor 展开或非幂等交类型）中，资源包是多重集且在置换下不变；而在严格范式中，置换必须被显式处理，并且可以被允许或禁止。严格性能够对归约路径及其对（例如）类型推导的影响进行细粒度控制。我们先前引入了一个约束性很强的余归纳类型系统（系统 S），其中置换被完全禁止。人们可能会好奇，与通常的多重集框架或允许置换的严格框架相比，置换的缺失在多大程度上导致了关于归约路径的表达能力损失。我们在最一般的情况下，即无有效性条件的余归纳类型文法中，回答了这个问题。我们的主要贡献是证明了不仅每一个非幂等推导都可以由一个严格的、无置换的推导表示，而且任何动态行为都可以通过这种方式捕获。换言之，我们证明了系统 S 相对于多重集/置换包含的交集具有完全的表达能力。
引用
@article{arxiv.1610.06399,
title = {Representing permutations without permutations, or the expressive power of sequence types},
author = {Pierre Vial},
journal= {arXiv preprint arXiv:1610.06399},
year = {2018}
}
备注
15 pages