利用域论证明强正规化
计算机科学中的逻辑
2015-07-01 v2 编程语言
摘要
Ulrich Berger 提出了一种利用域论证明强正规化的有力方法，特别是它显著简化了 Tait 关于 Spector 条递归强正规化的证明。本文的主要贡献在于表明，利用交类型和 Martin-Löf 类型论的域解释中的思想，可以进一步简化 U. Berger 的论证。我们为一个无类型编程语言构建了一个域模型，其中 U. Berger 仅对有类型项有解释，或者对无类型项有解释但需要额外条件来推导强正规化。作为一个主要应用，我们证明了扩展了 Spector 双重否定移位程序的 Martin-Löf 依赖类型理论。
引用
@article{arxiv.0709.1401,
title = {A proof of strong normalisation using domain theory},
author = {Thierry Coquand and Arnaud Spiwack},
journal= {arXiv preprint arXiv:0709.1401},
year = {2015}
}
评论
16 pages