Primitive Recursive Presentations of Automata and their Products
讨论了通过原始递归函数抽象指定Moore型状态机（传感器）和通过同时原始递归定义并行组合的方法。该方法主要是作为一种简洁方便的方式来处理计算机编程和工程中发现的复杂状态系统，但有一小部分表明与代数自动机理论和Krohn和Rhodes定理的联系。
2010-01-10 cs.FL cs.LO
Universal Individual-Sequence Prediction with a Primitive-Recursive Superpredictor
Faculty of Engineering, Bar-Ilan University（巴伊兰大学工程学院）
研究个体二进制序列顺序预测，构造可计算概率预测器，其相对于原始递归预测器有次线性遗憾界，证明PPM预测器是原始递归的，该预测器在特定源实现上达最优，还与其他预测器建立严格分离。
2026-07-29 cs.IT cs.LO math.IT
Intensional Kleene and Rice Theorems for Abstract Program Semantics
可计算性理论中的经典结果，特别是赖斯定理，集中于程序的扩展内容，即程序计算的部分递归函数。后来和最近的工作调查了这些结果的内涵概括，这些结果考虑到函数计算的方式，从而受到计算它们的特定程序的影响。在本文中，我们挑出一类新的程序语义的基础上抽象域的程序属性，能够捕捉非扩展方面的程序计算，如其渐近复杂性或逻辑不变，并允许我们概括一些基本的可计算性结果，如赖斯定理和Kleene的第二递归定理，这些语义。特别是，事实证明，对于这一类的抽象程序语义，任何非平凡的抽象属性是不可判定的，每一个可判定的过度近似必然包括一个无限的假阳性集，涵盖了语义抽象域的所有值。
2021-09-14 cs.FL cs.LO
Primitive Recursive Dependent Type Theory
本文通过限制 MLTT 中自然数消去规则并排除最低宇宙中的 Π-类型，构造子理论 Tpr，证明所有可定义函数均为原始递归，从而将原始递归性推广到一般类型。
2024-04-01 cs.LO math.LO
Higher-Order Recursion Abstraction: How to Make Ackermann, Knuth and Conway Look Like a Bunch of Primitives, Figuratively Speaking
Ackermann函数是自然数上著名的全递归二元函数。这是一个典型的例子，这样的一个函数，不是原始递归，在经典递归理论的意义。然而，在表面上矛盾，有广义的概念，总递归，阿克曼函数实际上是原始递归，并经常作为一个证人的特点，额外的权力所获得的推广。在这里，我们调查的技术，发现和分析复杂的递归函数的原始形式，即也克努特和康威的箭头符号，特别是递归抽象，在功能程序转换的框架。
2016-02-16 cs.LO cs.PL
Certifying algorithms and relevant properties of Reversible Primitive Permutations with Lean
可逆原始排列（RPP）是递归定义的函数，旨在模拟可逆计算。我们说明了一个证明，完全开发的证明助理精益，证明：“RPP可以编码每一个原始递归函数”。我们对该声明的原始证明的修改在概念上更简单，修复了一些错误，提出了一个新的更原始的RPP可逆迭代方案，并且为了保持形式化和半自动证明的简单性，我们确定了一个可以在RPP中生成一些有用的可逆算法的模式：Cantor配对，整数除法的商/提醒，截断平方根。我们的精益源代码可用于可逆计算的实验，其属性可以被认证。
2022-06-29 cs.LO
On the Notions of Rudimentarity, Primitive Recursivity and Representability of Functions and Relations
众所周知，Kurt Godel（1931）关于不完全性定理的开创性结果表明，基本关系（即，那些可由有界公式定义的）是原始递归的，原始递归函数可在足够强的算术理论中表示。我们也知道，虽然可能不像前一个那样广为人知，但有些原始的递归关系并不是基本的。本文的第一部分给出了这一事实的一个简单而初等的证明。在第二部分中，我们回顾了文献中研究的函数可表示性的一些可能的概念，并给出了在充分强数论中函数的弱可表示性与（强）可表示性等价的一个新的证明。我们的研究结果揭示了一些新的光的概念，基本的，原始的递归，和可表示的功能和关系，并澄清，希望在文献中的一些误解和混乱的错误。
2020-03-01 cs.LO math.LO
Ackermannian and Primitive-Recursive Bounds with Dickson's Lemma
Dickson引理是一个简单而强大的工具，广泛用于终止证明，特别是在处理计数器或相关的数据结构。然而，大多数计算机科学家不知道如何从这种终止证明中推导出复杂性上界，现有的文献在这些问题上没有很大的帮助。我们提出了一个新的分析的坏序列的长度（N^k，\leq），并解释如何可以得到复杂性的上限从终止证明。我们的上界改善了早期的结果，本质上是紧的。
2011-07-19 cs.CC cs.LO
Total Recursion over Lexicographical Orderings: Elementary Recursive Operators Beyond PR
在这项工作中，我们推广原始递归，以构建一个层次的终止总递归算子，我们称之为{ \em级原始递归顺序$i$ }（$\mathbf{PR}_{i}$）。原语递归等价于$1$（$\mathbf{PR}_{1}$）阶的分级原语递归。可从基本函数构造的函数构成$\mathbf{PR}_{0}$。有趣的是，我们发现$\mathbf{PR}_{2}$是$\mathbf{PR}_{1}$的保守扩展。然而，$\mathbf{PR}_{2}$之外的层次结构的成员，即$\mathbf{PR}_{i}$，其中$i\geq 3$，可以形式化Ackermann函数，因此比原始递归更具表达性。它仍然是一个悬而未决的问题，层次结构的成员比以前的成员更有表现力，哪些是保守的扩展。我们猜想，对于所有的$i\geq 1$ $\mathbf{PR}_{2i} \subset \mathbf{PR}_{2i+1}$。对进一步扩展的调查留待今后工作。
2018-01-03 cs.LO math.LO
Essential Incompleteness of Arithmetic Verified by Coq
利用Coq证明助手完成了Goedel-Rosser不完备性定理的构造性证明。形式化了任意语言上的经典一阶逻辑的某些理论。给出了本原递归函数的一个发展，并证明了所有本原递归函数在一个弱公理系统中都是可表示的。公式和证明被编码为自然数，并且在这些代码上操作的函数被证明是原始递归的。证明了弱公理系统本质上是不完备的。特别地，Peano算法在Coq的类型论中被证明是相容的，因此是不完备的.
2006-05-11 cs.LO
Godel's Incompleteness Phenomenon - Computationally
我们认为，哥德尔完备性定理等价于相容理论的完备性，哥德尔不完备性定理等价于这种完备性不是构造性的事实，即存在一些相容的和递归可证明的理论不能被推广到任何完备的、相容的和递归可证明的理论.任何相容的可判定的理论都可以扩展为完备的相容的可判定的理论。因此，演绎和一致性在逻辑中是不可判定的，而莱斯定理的一个类似定理对递归可判定的理论成立：这些理论的所有非平凡性质都是不可判定的。
2016-12-10 cs.LO math.LO
Comparing Computational Power
比较不同计算模型的计算能力是常见的做法。例如，递归函数严格来说比原始递归函数更强大，因为后者是前者的真子集（包括阿克曼函数）。与这种测量功率的“遏制”方法并行，使用基于“模拟”的方法是标准的。例如，有人说（无类型）λ演算在计算上与部分递归函数一样强大，因为λ演算可以通过将自然数编码为Church数来模拟所有部分递归函数。问题是，不受约束地使用这两种比较能力的方法可以表明，某些计算模型严格地比它们自己更强！我们认为，一个更好的定义是，模型A严格强于B，如果A可以模拟B通过某种编码，而B不能模拟A下的任何编码。然后，我们表明，递归函数是严格强在这个意义上比原始递归。我们还证明了递归函数，部分递归函数，和图灵机是“完整的”，在这个意义上，没有内射编码可以使它们等价于任何“超计算”模型。
2005-10-23 cs.LO
Monotone recursive types and recursive data representations in Cedille
本文在 Cedille 中基于 Tarski 不动点定理推导单调递归类型，并应用于 Parigot 和 Scott 编码，证明归纳性质并给出高效唯一的迭代与原始递归方案。
2021-05-14 cs.LO cs.PL
Church's thesis is questioned by new calculation paradigm
丘奇的论文声称所有有效可计算的函数都是递归的。递归函数的各种定义的一个缺点在于，它不是一个语法检查的问题，以找出一个实体是否产生了一个函数。八个新的想法，一个精确的设置算术逻辑和它的元语言给出了适当的环境，建设一个特殊的计算机，ARBACUS计算机。计算机不需要停止;要求计算器以计算机为基础构建，使其总是停止，然后所有计算都有效。仲裁器被定义为具有两层计算的计算器。它允许计算所有原始递归函数，但多级仲裁也允许计算其他非原始递归的仲裁函数。新的计算范式没有上述缺点。教会的论文的捍卫者面临的挑战表明，异国情调的仲裁功能是递归的，并提出了一个递归功能，是不是仲裁。一个包含对角化的三层多级仲裁的构造导致了一个奢侈但可计算的Snark函数，它不是仲裁的。只要它不是表明，所有外来的仲裁功能，特别是Snark函数是算术表示的哥德尔的第一个不完全句是在地狱。
2006-10-07 cs.LO
Towards an Analysis of Proofs in Arithmetic
本文研究证明模式的表达力，证明其能够模拟原始递归算术，并将算术证明到证明模式的翻译视为归纳证明分析的关键步骤。
2025-06-06 cs.LO
Refutability as Recursive as Provability
本文在原始递归框架下定义可反驳性谓词 Rf(x,v)，考察其与可证明性谓词 Pf(x,v) 的交互关系，从而为不完备性论证及相关概念编码提供新视角。
2024-04-05 cs.LO math.LO
Formalizing computability theory via partial recursive functions
我们提出了一个扩展的$\mathtt{mathlib}$图书馆的精益定理证明形式化的基础，可计算性理论。我们使用原始递归函数和部分递归函数作为主要的研究对象，我们使用建设性编码的部分功能，使他们可执行的程序时，有问题的可证明停止。主要定理包括构造一个通用的部分递归函数和证明停机问题的不可判定性。类型类推断提供了一种透明的方式来在需要的地方提供哥德尔编号并封装编码细节。
2019-07-18 cs.LO math.LO
Pointers in Recursion: Exploring the Tropics
我们将通常的部分/原始递归函数类转换为指针递归框架，通过指针读取单位成本函数访问实际输入值。这些指针递归函数类被证明等价于通常的部分/原始递归函数。从复杂性方面来说，这个框架以一种简化的方式捕获了大多数相关的子多项式类。使用Bellantoni和Cook的安全/正常分层规则的指针递归对应于多对数时间计算。我们引入了一种新的非大小递增分层规则，称为热带分层。Tropical分层和指针递归与一些最常见的递归方案一起使用，捕获类logspace、logspace/polylogtime、ptime和NC。最后，以一种让人想起安全递归函数的方式，热带分层直接在函数代数的语法中表达，产生热带递归函数代数。
2019-08-14 cs.CC cs.LO cs.PL
Extraction of Efficient Programs in $IΣ_1$-arithmetic
子句语言（CL）是我们在计算机科学教学中使用的一种声明式程序设计和验证系统。CL是我们称之为$\mathit{PR}{+}IΣ_1$范式（具有$IΣ_1$ -算术的原始递归函数）的实现。本文介绍了一种扩展的$IΣ_1$证明称为提取证明，其中可以提取证明的$Π_2$规范的原始递归程序的高效的手编码的。这是通过使编程构造与具有计算内容的证明规则完全对应来实现的。
2019-10-01 cs.LO math.LO
Axiomatic approach to the theory of algorithms and relativized computability
众所周知，递归论中的许多定理都可以“相对化”。这意味着，如果部分递归函数被相对于某个固定的Oracle集是部分递归的函数所替换，则它们仍然为真。乌斯彭斯基制定了三个“公理”，称为“计算记录公理”、“程序公理”和“算术性公理”。然后，使用这些公理（更确切地说，前两个），他证明了基本结果的递归论。这两个公理对于相对于某个固定的预言集是部分递归的函数类也是正确的。这个类在替换、原始递归式和最小化（$μ$ -运算符）下也是封闭的;这些（直观上显而易见的）封闭性也用于证明中。这一观察所作出的乌斯彭斯基解释了为什么许多定理的递归论可以相对化。事实证明，相反的陈述也是正确的：所有可相对化的结果都遵循前两个公理和封闭性。没错，就是\emph{every class of partial functions that is closed under substitution, primitive recursion and minimization that satisfies the first two axioms is the class of functions that are partial recursive relative to some oracle set $A$}。这是本文的主要结果。
2018-11-15 cs.LO math.LO
A recursion theoretic foundation of computation over real numbers
我们定义了一类可计算的功能在实数使用功能计划类似的类的原始和部分递归函数定义的哥德尔和克莱因。我们表明，这类功能也可以由主从机，这是图灵机一样的设备。特征的证明给出了Kleene式的范式定理。此外，这个特征是两个最有影响力的实数计算理论的自然组合，即第二类有效性理论（TTE）（参见Weihrauch）和Blum-Shub-Smale计算模型（BSS）。在可计算性的概念下，实数的递归（或可计算）子集是精确有效的$Δ^0_2$集。
2020-10-02 cs.LO
Decidable Models of Recursive Asynchronous Concurrency
异步通信下推系统（ACPS）满足空栈约束（下推进程只能在其栈为空时接收）是一种流行的可判定模型，用于具有异步原子过程调用的递归程序。我们研究放松空栈约束ACPS，允许并发和通信行动在任何堆栈高度，称为形栈约束，从而使更大的一类并发程序进行建模。我们建立了一个紧密的连接ACPS与形栈和一个新的扩展Petri网：网与嵌套着色令牌（NNCTs）。NNCT中的令牌有两种类型：简单和复杂。复杂标记携带任意数量的彩色标记。NNCT的规则可以同步复杂和简单的令牌，将彩色令牌注入复杂令牌，并将指定颜色集的所有令牌弹出到预定义的位置。我们证明了NNCT的可覆盖性问题是塔完全的。据我们所知，NNCT是Petri网的第一个扩展，在具有无限令牌类型集的网类中，具有原始递归可覆盖性。这一结果意味着塔完全覆盖ACPS与形状的堆栈。
2015-01-18 cs.CC cs.LO
A New Approach to Abstract Machines - Introduction to the Theory of Configuration Machines
抽象机器是一种理论模型，旨在执行严格的计算研究。这种模型通常由机器的配置、指令、程序、输入和输出组成。在本文中，我们正式这些概念作为一个非常简单的代数系统，称为配置机。如果一个抽象机被定义为一个配置机，它由原始递归函数组成，那么它所计算的函数总是递归的。构形机理论为研究通用机械提供了一种有效的工具。
2010-07-19 cs.FL cs.LO math.LO
On the definability of functionals in Gödel's theory T
哥德尔的理论T可以理解为一个简单类型的lambda演算理论，它被扩展为包括常数0、后继函数S和用于tau类型对象上的原始递归式的算子R_tau。已知该理论所能定义的从非负整数到非负整数的函数恰是非负整数的<ε_0-递归函数。作为这个结果的推广，我们证明了当定义域和上定义域被限制为纯闭规范形时，T中可定义的任意类型的泛函都可以编码为<ε_0-递归函数.
2014-10-10 cs.LO math.LO
Sub-computable Boundedness Randomness
本文对某些缺乏通用机的子可计算函数类定义了一个新的有界可计算随机性概念。特别是，我们定义这样的版本的原始递归函数和PSPACE函数的随机性。这些新概念是稳健的，因为在（1）马丁-洛夫检验，（2）柯尔莫哥洛夫复杂性和（3）鞅方面有等价的公式。我们证明了这些概念可以等价地定义为无前缀柯尔莫哥洛夫复杂度。我们证明了范Lambalgen的定理的一个方向成立的相对可计算性，但另一个方向失败。我们讨论这些随机性概念的统计特性。
2014-12-22 cs.LO
$ω$PAP Spaces: Reasoning Denotationally About Higher-Order, Recursive Probabilistic and Differentiable Programs
本文提出 ωPAP 空间范畴作为指称语义框架，以统一处理高阶递归概率与可微程序，并据此证明自动微分正确性及概率程序迹密度的几乎处处可微性。
2023-05-25 cs.LG cs.LO cs.PL
Abstract Compilation as Abstraction of Operator Semantics, applied to Cost Analysis
Universidad Politécnica de Madrid（马德里理工大学）；IMDEA Software Institute（IMDEA软件研究所）；Spanish Council for Scientific Research (CSIC)（西班牙国家研究委员会）；Computer Science Laboratory of Sorbonne University (LIP6)（索邦大学计算机科学实验室）；STMicroelectronics（意法半导体）
该研究提出算子语义与抽象编译框架，将其应用于静态代价分析，开发出支持通用函数未知量等的最优递归提取技术，提升了代价分析的可靠性与精确性。
2026-08-11 cs.LO cs.PL
Provability in BI's Sequent Calculus is Decidable
本文针对束蕴涵逻辑（BI）自问世以来缺乏有效证明搜索过程的问题，通过推广根岑的可判定性论证并结合戴克霍夫缩并消除论证的关键特征，证明可将任意相继式的证明搜索空间规约为原始递归集，从而得出BI相继式演算的可证明性是可判定的，但文中存在错误导致主定理证明无效。
2024-04-12 cs.LO cs.SC math.LO
