通过非确定性选择实现 HA + EM1 的强规范化
计算机科学中的逻辑
2013-09-06 v1
摘要
我们研究了 HA + EM1（即在 Sigma01 公式上带有排中律的构造性 Heyting 算术）的新 Curry-Howard 对应关系的强规范化。HA + EM1 的证明项语言由 lambda 演算加上一个算子 ||_a 组成；从编程角度看，该算子代表具有 delimited 范围异常处理算子，而从逻辑角度看，它代表排中律的受限版本。我们基于一种“非确定性浸入”技术，给出了该系统的强规范化证明。
引用
@article{arxiv.1309.1254,
title = {Strong Normalization for HA + EM1 by Non-Deterministic Choice},
author = {Federico Aschieri},
journal= {arXiv preprint arXiv:1309.1254},
year = {2013}
}
备注
In Proceedings COS 2013, arXiv:1309.0924