We introduce Pure Recursive Calculi (PRC): finite, operator-only rewrite calculi with no variable binding, no external memory, no imported axioms, and an unrestricted step-duplicating recursor. We study KO7, a minimal witness system (7 constructors, 8 rules) designed to isolate the duplication barrier while remaining auditable. In the full relation, a non-local-join witness at eqW void void shows that unrestricted confluence is unavailable. We therefore define a guarded fragment, SafeStep, and prove strong normalization via a computable triple-lex measure (deltaFlag, kappa^M, tau). The proof is rule-by-rule and mechanized: rec-succ is discharged by a strict deltaFlag drop, rec-zero by a Dershowitz-Manna multiset decrease on kappa^M, and tie branches (including merge-cancel and guarded eqW cases) by tau. From this measure we derive a certified normalizer and prove totality and soundness. We then formalize a Newman engine for SafeStep, discharge the local-join hypothesis in the artifact, and obtain unconditional confluence and unique normal forms for the safe fragment. To characterize limits of internal termination proving under duplication, we report fourteen failed strategy families (twelve machine-checked, two meta-theoretical). These include additive and simple lexicographic counters, polynomial and weight-based interpretations, flag-only and depth-only rankings, naive multisets, local patch lemmas, and unrestricted recursion barriers; path-order methods are treated separately because they rely on imported subterm principles. We also connect safe-fragment normalization to fixed-target reachability via a normalize-and-compare decision pattern under confluence. These results motivate a conjecture: for PRCs with unrestricted step duplication, no internally definable method currently known proves full-calculus termination without importing external structural principles.

翻译：本文引入纯递归演算（PRC）：一种有限、仅含运算符的重写演算，其不含变量绑定、外部存储、外部公理，并具有不受限制的步复制递归子。我们研究KO7——一个最小见证系统（7个构造子，8条规则），旨在隔离复制障碍的同时保持可审计性。在全关系中，eqW void void处的非局部汇合见证表明不受限制的汇合性不可得。因此我们定义了一个受保护片段SafeStep，并通过可计算的三重字典序度量（deltaFlag, kappa^M, tau）证明了强范式化。该证明按规则逐条进行且已机械化：rec-succ通过deltaFlag的严格递减消解，rec-zero通过kappa^M上的Dershowitz-Manna多重集递减消解，而平局分支（包括merge-cancel及受保护的eqW情形）通过tau消解。基于此度量，我们推导出一个经过验证的范式化器，并证明了其完全性与可靠性。随后，我们为SafeStep形式化了一个Newman引擎，在验证件中消解了局部汇合假设，从而为该安全片段获得了无条件的汇合性与唯一范式。为刻画复制条件下内部终止性证明的极限，我们报告了十四类失败的策略族（其中十二类经机器检验，两类属元理论层面）。这些策略包括加法与简单字典序计数器、多项式与基于权重的解释、纯标志与纯深度排序、朴素多重集、局部修补引理以及无限制递归屏障；路径序方法因依赖外部子项原理而被单独讨论。我们还通过汇合性下的“范式化-比较”判定模式，将安全片段的范式化与固定目标可达性联系起来。这些结果引出一个猜想：对于具有不受限制步复制的PRC，目前已知的内部可定义方法均无法在不引入外部结构原理的情况下证明全演算的终止性。