对称 $\lambda \mu$-演算强规范化结果的算术证明
逻辑
2009-05-08 v1
摘要
对称 -演算是由 Parigot 引入的 -演算，其中添加了 的对称归约规则 。我们给出了该演算的一些强规范化结果的算术证明。我们证明了（这是一个新结果）对于无类型演算，-归约是强规范化的。我们还证明了对于类型演算，-归约的强规范化：这一结果此前已知，但之前的证明使用了可归约性候选者，其中类型的解释被定义为某个递增算子的不动点，因此高度非算术化。
引用
@article{arxiv.0905.1034,
title = {Arithmetical proofs of strong normalization results for the symmetric $\lambda \mu$-calculus},
author = {René David and Karim Nour},
journal= {arXiv preprint arXiv:0905.1034},
year = {2009}
}