有限部分函数上的 Spector 杠递归

我们秉承 Berardi-Bezem-Coquand 泛函的精神，引入一种新的、需求驱动的 Spector 杠递归变体。该递归作用于有限部分函数 $u$，其中控制参数 $\varphi$（在 Spector 杠递归中用于在满足 $\varphi(\hat{s})<|s|$ 的序列 $s$ 处终止计算）现在充当一个向导，用于精确决定在何处进行杠递归更新，每当 $\varphi(\hat{u})\in\mbox{dom}(u)$ 时终止计算。我们首先探索这种新递归形式的理论方面，然后在论文的主要部分，我们证明需求驱动的杠递归可直接用于给出经典可数选择公理的一种替代函数解释。我们提供一个简短的案例研究作为说明，其中我们从不存在从 $\mathbb{N}\to\mathbb{N}$ 到 $\mathbb{N}$ 的单射这一证明中提取出一个新的杠递归程序，并将其与使用 Spector 原始变体所获得的程序进行比较。最后，我们正式证明我们的新杠递归器与原始 Spector 杠递归是原始递归等价的，因此当添加到 Gödel 系统 $\sf T$ 中时定义了相同的泛函类。