基于 {\lambda}-项泰勒展开的强可规范化作为有限性结构
计算机科学中的逻辑
2016-03-24 v1
摘要
在线性逻辑的传统认知中，一种常见直觉是 Ehrhard 引入的有限性空间（finiteness spaces）结构在语义上反映了消去割的强规范化性质。我们在非确定性 {\lambda}-演算的背景下使这一直觉形式化，通过引入资源项上的有限性结构，使得一个 {\lambda}-项强可规范化当且仅当其泰勒展开的支持是有限（finitary）的。我们结果的一个应用是：任意强可规范化的非确定性 {\lambda}-项的泰勒展开存在范式。
引用
@article{arxiv.1603.07218,
title = {Strong Normalizability as a Finiteness Structure via the Taylor Expansion of {\lambda}-terms},
author = {Michele Pagani and Christine Tasson and Lionel Vaux},
journal= {arXiv preprint arXiv:1603.07218},
year = {2016}
}
备注
Presented at FoSSaCS 2016