Church's thesis is questioned by new calculation paradigm
丘奇的论文声称所有有效可计算的函数都是递归的。递归函数的各种定义的一个缺点在于，它不是一个语法检查的问题，以找出一个实体是否产生了一个函数。八个新的想法，一个精确的设置算术逻辑和它的元语言给出了适当的环境，建设一个特殊的计算机，ARBACUS计算机。计算机不需要停止;要求计算器以计算机为基础构建，使其总是停止，然后所有计算都有效。仲裁器被定义为具有两层计算的计算器。它允许计算所有原始递归函数，但多级仲裁也允许计算其他非原始递归的仲裁函数。新的计算范式没有上述缺点。教会的论文的捍卫者面临的挑战表明，异国情调的仲裁功能是递归的，并提出了一个递归功能，是不是仲裁。一个包含对角化的三层多级仲裁的构造导致了一个奢侈但可计算的Snark函数，它不是仲裁的。只要它不是表明，所有外来的仲裁功能，特别是Snark函数是算术表示的哥德尔的第一个不完全句是在地狱。
2006-10-07 cs.LO
Church's thesis and related axioms in Coq's type theory
“Church's thesis”（$\mathsf{CT}$）作为构造性逻辑中的一个公理指出，每个$\mathbb{N} \to \mathbb{N}$类型的全函数都是可计算的，即在计算模型中是可定义的。$\mathsf{CT}$在经典数学和布劳威尔的直觉主义中都是不一致的，因为它分别与弱柯尼希引理和扇形定理相矛盾。最近，$\mathsf{CT}$被证明是一致的（单价）建设性类型论。由于弱柯尼希引理和扇形定理都不是构造性逻辑中假设的逻辑公理或选择类公理的结果，所以$\mathsf{CT}$似乎只与经典逻辑和选择公理的组合不一致。我们研究的后果$\mathsf{CT}$和它的关系，几类公理在Coq的类型论，建设性的类型论与宇宙的命题，既不证明经典的逻辑公理，也不强选择公理。因此，我们对以下问题提供了部分答案：哪些公理可以保留类型论固有的计算直觉，哪些公理肯定不能。该文件也可以阅读作为一个广泛的调查公理在类型论，所有结果机械化的Coq证明助手。
2020-11-03 cs.LO
Game semantics of Martin-Löf type theory, part III: its consistency with Church's thesis
我们证明了内涵马丁-洛夫型理论（MLTT）与正式教会的论文（CT），这是开放至少15年的一致性。证明一致性的困难在于，一个标准的Kleene可实现性方法并不适用于一致性，尽管它验证了CT，因为它没有对MLTT建模;具体地说，可实现性并不验证MLTT在pi类型上的同余规则（称为$ξ$规则）。我们克服了这一点，并证明了新的可实现性à la游戏语义，这是作者以前的工作的基础上的一致性。
2020-07-28 cs.LO math.LO
The Formalization of two Computational Models in Dafny
Alexandru Ioan Cuza University of Ia s i, Romania
本研究在Dafny中完成图灵机与Lambda演算两种计算模型的形式化，并实现了图灵机终止性证明、丘奇编码证明及丘奇-罗瑟定理机械化证明等多项应用。
2026-09-28 cs.FL cs.LO cs.PL
Is Turing's Thesis the Consequence of a More General Physical Principle?
我们讨论了历史上试图制定一个物理假设，图灵的论文可能来自，也讨论了一些相关的尝试，以建立物理学中的数学模型的可计算性。我们表明，这些尝试都与一个单一的，统一的假设。
2012-04-02 cs.CC cs.LO math-ph
Parametric Church's Thesis: Synthetic Computability without Choice
在Richman、Bridges和Bauer开创的综合可计算性中，人们在没有明确计算模型的情况下发展了可计算性理论。这是通过假设一个公理等价于假定一个函数$ϕ$对于空间$\mathbb{N}\to\mathbb{N}$是泛在的（$\mathsf{CT}_ϕ$，构造主义公理$\mathsf{CT}$的一个推论），马尔可夫原理，以及至少可数选择公理。假设$\mathsf{CT}$和可数选择使排中律失效，从而也使可计算性教科书中流行的经典直觉失效。另一方面，像赖斯定理这样的结果在没有选择的情况下是不可证明的。与现有的工作相比，我们的调查建设性的类型论与一个单独的，不可预测的宇宙的命题可数的选择不成立，因此先验$\mathsf{CT}_ϕ$和法律的排中律似乎是一致的。我们引入各种参数的加强$\mathsf{CT}_ϕ$，这相当于假设$\mathsf{CT}_ϕ$和$S^m_n$运营商的$ϕ$一样，在$S^m_n$定理。加强公理允许发展合成可计算性理论没有选择，如赖斯定理的优雅的合成证明所示。此外，它们似乎与经典直觉并不冲突，因为它们是$\mathsf{CT}$的传统分析形式的结果。除了解释新的公理和赖斯定理的证明，我们贡献的Coq证明助手的所有结果的机器检查证明。
2021-12-22 cs.LO math.LO
Means-fit effectivity
从历史上看，有效算法的概念与丘奇-图灵命题密切相关。但有效性并不限制计算时间或任何其他资源;从这个意义上说，它与工程或物理学不相容。我们提出了一个自然的概括，意味着拟合的有效性，这是相对于（物理或抽象）的算法的基本机制的有效性。这种机制因算法的不同而不同。以尺子和罗盘算法、算术算法和Blum-Shub-Smale算法为例。我们相信，手段拟合的有效性是有意义的和有用的独立的丘奇-图灵命题。均值拟合的有效性是可以定义的，至少在抽象状态机（ASMs）理论中是这样。该定义也阐明了原始有效性。不假定熟悉ASM理论。我们试图使报纸自成一体。
2020-02-20 cs.LO math.LO
Basic interactive algorithms: Preview
University of Michigan（密歇根大学）
本文预览了基本交互式算法的公理化工作，回顾了基本算法的公理化及其在证明 Church-Turing 论题中的作用，并探讨了概率、非确定性和量子算法等扩展概念与预言机基本算法的关联。
2025-08-07 cs.CL cs.LO math.LO
A Game-Semantic Model of Computation
本文介绍了一种新的概念“（有效）可计算性”，称为生存能力，在游戏语义中的战略在一个内在的（即，不求助于标准的丘奇-图灵可计算性），非归纳和非公理化的方式，并显示，作为一个主要的技术成就，可行的策略是图灵完备的。因此，我们已经给出了与图灵机相同意义上的计算的数学基础，但超出了自然数的计算，例如，高阶计算，以一种更抽象的方式。作为直接推论，推广了可计算性理论中的一些著名定理，如smn定理和第一递归定理。值得注意的是，我们的游戏语义框架区分“高层次”的计算过程，直接操作的数学对象，如自然数（而不是他们的符号表示）和他们的“符号实现”，定义他们的“可计算性”，这揭示了新的光计算的概念。这项工作的目的是成为一个垫脚石走向一个新的数学基础的计算，直觉逻辑和建设性数学。
2018-06-26 cs.LO
A Hypercomputation in Brouwer's Constructivism
与其他建构主义学派不同的是，布劳威尔认为，“建构客体”的概念并不局限于以某种有限的符号字母表中的“词”来呈现，非预定的、未完成的客体的选择序列是合法的建构客体。这样，布劳威尔的建构主义超越了图灵可计算性。1999年，J. Copeland提出了超计算（hypercomputation）一词。超计算是指超越丘奇-图灵命题的计算模型。在本文中，我们提出了一个超计算称为持久进化图灵机的基础上布劳威尔的概念是建设性的。
2015-11-15 cs.FL cs.LO
Incomputability after Alan Turing
不可计算性作为一个数学概念，起源于阿兰·图灵和阿朗佐·丘奇在20世纪30年代的工作。就像图灵本人一样，它在数学领域之外吸引的注意力比它应得的要少。今天，我们在计算机科学、物理学、生物学、人工智能、经济学和人文科学方面的经验都表明了这一概念对于理解我们周围世界的重要性。这篇文章以图灵百年来的视角来审视可计算世界和不可计算世界之间的接口是如何形成图灵工作的中心主题的-从早期建立存储程序计算机的标准模型，到后期关于自然界形式出现的工作，以及理解和模拟人类智能的第一种方法。图灵的思想非常有先见之明，他的遗产仍然影响着我们的许多工作。不可计算的可能会成为遗产中特别重要的一部分，其后果是艾伦·图灵本人无法想象的。
2013-04-22 cs.CC cs.LO math.HO
A definable number which cannot be approximated algorithmically
图灵机（TM）和丘奇命题已经形式化了可计算数的概念，这允许显示不可计算数。本文定义了TM“可接近”数的概念，并证明了某些（如果不是全部）已知的不可计算数是TM可接近的。然后给出了一个TM不可达数的例子。
2010-03-01 cs.CC cs.LO
Hypercomputation: Towards an extension of the classical notion of Computability?
本文的目的是分析超计算的概念和一些超机。本文主要分为三个部分。我们在第一章中首先以图灵机和Church-Turing论文为主要参考，分析了经典可计算性的概念，然后在第二章中，我们继续分析超计算和一些超机。注意这些机器的可能的物理实现和它们的有用性。第三章对量子计算做了一个简单的介绍，并对量子超计算模型Tien D. Kieu的绝热量子计算。
2012-10-26 cs.CC cs.LO
Computing over the Reals: Foundations for Scientific Computing
我们给出了一个详细的治疗的“位模型”的可计算性和复杂性的实函数和子集的R^n，并认为这是一个很好的方式来形式化许多问题的科学计算。在引言中，我们还讨论了另一种Blum-Shub-Smale模型。在最后一节中，我们将讨论物理系统是否能够击败丘奇-图灵命题的问题。
2005-09-14 cs.CC cs.LO
Addressing Machines as models of lambda-calculus
本文提出可寻址机器作为λ演算模型，通过仅操作地址的简单机器及最左归约语义，并引入类似ω和ζ_β的规则，构建完整的无类型λ演算模型。
2022-07-28 cs.LO
On the completeness of quantum computation models
可计算性的概念在无限维向量空间上是稳定的（即独立于索引的选择），只要它们具有有限的“张量维数”。这种具有有限张量维数的向量空间允许定义量子计算模型的绝对完备性概念，并在量子理论的框架内为丘奇-图灵命题提供精确的含义。（额外的关键词：量子程序设计语言，指称语义，通用性。）
2010-04-07 cs.CC cs.LO quant-ph
Algorithmic Cost in "Exact Real Computation"
KAIST, School of Computing（韩国科学技术院计算机学院）；Kyoto University, Graduate School of Human and Environmental Studies（京都大学人类与环境学研究科）
该研究定量强化精确实数计算（ERC）的图灵完备性，为其操作原语分配位代价，证实多项式代价实函数与多项式时间图灵可计算性等价，且iRRAM C++库的运行时测量验证了理论预测。
2026-08-26 cs.LO cs.NA cs.PL
Evolving Algebras 1993: Lipari Guide
计算模型和规范方法似乎截然不同。关于抽象状态机（简称ASM，也称为演化代数）的项目开始时试图通过改进图灵的论文来弥合这一差距。我们寻求更通用的机器，能够逐步模拟其自然抽象层次上的任意算法。ASM论文断言ASM是如此多功能的机器。该指南提供了顺序、并行和分布式ASM的定义。
2018-08-19 cs.LO cs.SE math.LO
On the relation between representations and computability
可计算性的一个基本结果是存在无法计算的定义良好的函数。在本文中，我们研究的数据表示对可计算性的影响，我们表明，虽然每一种可能的方式表示数据存在不可计算的功能，一个特定的抽象函数的可计算性从来不是一个绝对的属性，但取决于用于功能域的表示。我们研究这种依赖关系的范围，并提供数学标准，有利于一些表示超过其他人。正如我们将要展示的，有很强的理由表明，计算可枚举性应该是计算模型的一个附加公理。我们分析的技术和代表性的变化和甲骨文机器的影响之间的联系，显示其层次结构之间的重要联系。最后，这些概念使我们能够获得一个新的洞察丘奇图灵命题：它的解释为计算是不变的基本代数结构。
2017-06-29 cs.CC cs.LO
Notes on kAExp(pol) problems for deterministic machines
一些逻辑的复杂性，如Presburger算术，依赖逻辑和环境逻辑，只能用交替的图灵机来描述。尽管很自然，交替的存在有时会导致整洁的想法在重型技术机器中被混淆。在这些笔记中，我们提出了两个确定性机器上的问题，可以用来证明计算类$k$ AExp $_{\text{pol}}$的下界，这是一类所有问题可解的交替图灵机运行在$k$指数时间和执行多项式量的交替，相对于输入大小。第一个问题称为$k$ AExp $_{\text{pol}}$ -prenex TM问题，是关于确定性图灵机的问题。第二个问题，称为$k$ -exp交替多平铺问题，类似于第一个，但平铺系统。这两个问题都是TM交替问题和交替多块问题的自然推广，L. Bozzelli，A. Molinari，A. Montanari和A. Peron in [Gandalf，pp. 31-45，2017]。在这些说明中提出的证据遵循优雅的阐述A。Molinari的博士论文将这些结果从$k = 1$的情形推广到任意$k$的情形。
2021-10-11 cs.CC cs.LO
