论归约候选作为强归约语义的完备性
计算机科学中的逻辑
2015-07-01 v2
摘要
本文为 Curry 风格最小演绎模理论定义了基于归约候选的可靠且完备的语义判定标准。通过使用 Curry 风格证明项，该标准得以建立在经典的前 Heyting 代数概念之上，并使其适用于所有以最小演绎模表达的理论。与使用 Church 风格证明项相比，该方法提供了更简单的标准定义及其完备性证明。
关键词
引用
@article{arxiv.1201.1705,
title = {On completeness of reducibility candidates as a semantics of strong normalization},
author = {Denis Cousineau},
journal= {arXiv preprint arXiv:1201.1705},
year = {2015}
}
备注
24 pages