η-conversions of IPC implemented in atomic F
η-conversions of IPC implemented in atomic F
复制标题
以原子 F 实现的 IPC 的 eta 转换
DOI：
10.1093/jigpal/jzw035
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Gilda Ferreira
中科院分区：
文献类型：
--
作者：
Gilda Ferreira
已知完全直觉命题演算（IPC）的β-转换转化为原子多态演算Fat的βη-转换。由于Fat具有βη-转换的强正规化性质，因此可以导出考虑β-转换的IPC的强正规化的另一种证明。在本文中，我们通过分析后一个演算的η-转换到前一个系统的技术变体（原子多态演算Fat）的翻译，改进了以前的结果。事实上，从Fat的强规范化，我们可以推导出考虑所有标准（β和η）转换的全直觉命题演算的强规范化。
It is known that the β-conversions of the full intuitionistic propositional calculus (IPC) translate into βη-conversions of the atomic polymorphic calculus Fat. Since Fat enjoys the property of strong normalization for βη-conversions, an alternative proof of strong normalization for IPC considering β-conversions can be derived. In the present paper we improve the previous result by analyzing the translation of the η-conversions of the latter calculus into a technical variant of the former system (the atomic polymorphic calculus Fat). In fact, from the strong normalization of Fat we can derive the strong normalization of the full intuitionistic propositional calculus considering all the standard (β and η) conversions.
影响因子：
0.6
作者：
Ghani N
通讯作者：
Ghani N