Strong Normalization of Herbelin's Explicit Substitution Calculus with Substitution Propagation
Strong Normalization of Herbelin's Explicit Substitution Calculus with Substitution Propagation
复制标题
Herbelin 显式替代演算与替代传播的强归一化
DOI：
10.1093/logcom/13.5.689
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
Christian Urban
中科院分区：
文献类型：
--
作者：
R. Dyckhoff;Christian Urban
草林（在CSL'94）呈现了最小含义逻辑的简单序列，对完整的FirstTard Intuitionistic逻辑可扩展，具有完整的切割规则系统，既是汇合又有强烈的标准化。构建明确的替代的规则。可以添加规则，而无需打破强大的归一化。
Herbelin presented (at CSL’94) a simple sequent calculus for minimal implicational logic, extensible to full firstorder intuitionistic logic, with a complete system of cut-reduction rules which is both confluent and strongly normalizing. Some of the cut rules may be regarded as rules to construct explicit substitutions. He observed that the addition of a cut permutation rule, for propagation of such substitutions, breaks the proof of strong normalization; the implicit conjecture is that the rule may be added without breaking strong normalization. We prove this conjecture, thus showing how to model beta-reduction in his calculus (extended with rules to allow cut permutations).