On Continuous Normalization
On Continuous Normalization
复制标题
论连续标准化
DOI：
10.1007/3-540-45793-3_5
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
Felix Joachimski
中科院分区：
文献类型：
--
作者：
Klaus Aehlig;Felix Joachimski
这项工作的目的是解释连续规范化的句法性质，如在证明理论中引入的Mints，并进一步研究了Ruckert，布赫霍尔茨和Schwichtenberg。通过void构造函数的演算（所谓的重复规则），定义了原始递归规范化函数。与其他连续归一化公式相比，这个定义简单得多，因此适合于在共代数环境中进行分析。它被证明是连续的w.r.t.自然拓扑上的非良基项的单位作为模的连续性。重复规则的数量与达到标准形式所需的s-约简的数量（如玻姆树所表示的）以及出现在该标准形式中的应用程序的数量局部相关。
This work aims at explaining the syntactical properties of continuous normalization, as introduced in proof theory by Mints, and further studied by Ruckert, Buchholz and Schwichtenberg.In an extension of the untyped coinductive ?-calculus by void constructors (so-called repetition rules), a primitive recursive normalization function is defined. Compared with other formulations of continuous normalization, this definition is much simpler and therefore suitable for analysis in a coalgebraic setting. It is shown to be continuous w.r.t. the natural topology on non-wellfounded terms with the identity as modulus of continuity. The number of repetition rules is locally related to the number of s-reductions necessary to reach the normal form (as represented by the Bohm tree) and the number of applications appearing in this normal form.