有限集定义的可计算性及其模型的有效性研究

可在www.sciencedirect.com在线获取理论计算机科学电子笔记324（2016）91-106www.elsevier.com/locate/entcs用有限集定义可计算性雨果·D. Macedoa，b，1aDTU丹麦计算技术大学2800 Kongens Lyngby丹麦Edward H. Haeusler2bDepartamentodeInform'atica-22451-900G'aveaRio deJaneiro巴西亚历克斯·加西亚3Instituto Militar de Engenharia小行星22290-270里约热内卢巴西摘要本文研究可计算性领域中的有效性问题。在有效性的模型理论方法的背景下，如果存在包含该函数的表示的模型，则该函数被认为是有效的，我们的定义依赖于由有限集之间的函数提供的模型，使用范畴论作为数学基础。该模型依赖于这样一个事实，即有限集合之间的每个函数都是可计算的，并且这些函数的有限组合也是可计算的。我们的方法是一种替代传统的模型理论为基础的工程依赖（ZFC）集理论作为数学基础，我们的方法也是新颖的相比，已经存在的工程使用范畴理论来接近可计算性的结果。此外，我们展示了如何在模型中编码图灵机计算，从而得出结论，该模型至少表达了所需的计算行为。我们还提供了关于模型的哪些实例确实可以由图灵机计算的细节。关键词：有效性，有限集，计算模型1电子邮件：hmacedo@inf.puc-rio.br2电子邮件：hermann@inf.puc-rio.br3电子邮件：garcia@ime.eb.brhttp://dx.doi.org/10.1016/j.entcs.2016.09.0091571-0661/© 2016作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。92H.D. Macedo等人/理论计算机科学电子笔记324（2016）911介绍随着先进计算机的到来，20世纪上半叶向我们提出了可计算性的概念。如今，关于这个问题的标准课程应该讨论计算的模型和结果，特别是Church-Turing论文，它等同于什么可以有效地计算，什么可以通过运行算法的机器计算。在下文中，术语算法将根据其当前含义来理解。另一方面，可计算性将根据其“可计算”的直观含义来定义尽管它在20世纪达到了顶峰，但在古代人类知识的许多领域都已经存在了。在我们的日常生活中，由于文化遗产，我们执行了一些常规，而其他人则在每一种文化中普遍存在并遇到。这种普遍存在的惯例可以被认为是我们生活中普遍或自然的方面。算术是这样一个普遍方面的一个例子，它存在于所有已知的文明中，并且（历史上）我们认知生活的很大一部分（曾经和）致力于学习和开发用于计算自然数和其他数字系统的基本运算的算法。除了算术之外，几何学领域也有它的算法领域。例如，命题一。1，在书我的欧几里得欧几里得《几何原本》中的许多命题对算法及其正确性伴随参数的描述。经典的问题，如平方圆或三等分一个角度使用有限数量的直尺和指南针操作可以理解为寻找一种方法来解决一个问题，通过一个专门的算法。这两个问题都被证明是不可能解决的，似乎只有在数学中，这种不可能的证明才以一种确定的形式出现。后来的研究表明，用直尺和圆规作图，再加上四种基本算术运算的常用算法，不足以代表这类问题的有效性。阿基米德因此，自古代古典时期以来，人们就知道，所选择的解决问题的方法中涉及的对象的性质决定了相应方法本身的如今，这种经验法则在计算机程序员决定和设计程序所操纵的数据库时的最佳实践手册中找到了自己的位置我们花了几千年的时间才意识到，有效性首先应该被认为是函数的一种属性，而且，函数应该被认为是4此外，灵长类动物、狮子和海豚也有算术能力[2]。H.D. Macedo等人/理论计算机科学电子笔记324（2016）9193被称为输入和输出之间的关系。上个世纪成功地描述了从一组输入A到一组输出B的函数是有效的。在它开始的几十年后，部分函数而不是全函数被承认在有效函数的领域。此外，认识到自然数的集合，作为一个数字系统，应该被认为是前面提到的子集A和B的宇宙，也是最近的发展。从历史上看，对效率的调查主要遵循两条非排他性的轨道。在模型理论方法中，提出了一个“实例M f表示f“的含义fM产生输出o，则f（i）= o必定为真。“提交”和“生产”的含义也在引入“模型”M时得到了定义，至少是非正式的定义。在证明论方法中，定义了一个逻辑理论T，并且f，一个从A<$N到B<$B的函数，被称为T-有效的当且仅当f∈ T。 当然T由一组公理和推理规则来表示，用于导出关于理论T的成员资格以及函数f和g之间的等价性的命题，即， 的形式g∈T和f∈g。模型理论方法的一个典型例子是基于图灵机的有效性定义，而哥德尔部分递归函数则是证明理论方法的一个例子。定义有效性的方法不完全是模型理论或证明理论。如果忽略由同一性关系提供的潜在评估模型，则可以将隐式演算视为纯证明理论的例子另一方面，如果关注λ-terms评估模型，我们可以将lambda演算视为模型理论方法Roger[10]一个非常有价值的讨论）。罗杰公理化是一种证明理论的尝试，以一种真正抽象的方式精确地表达有效性模型。程序是数字，模型是由前者索引的自然数值函数族据我们所知，除了它的相似之处，值得一提的是，几乎所有的模型理论方法的有效性在于ZFC6。范畴论（CT），虽然不是完全脱离ZFC和其他集合论方法的替代，但它提供了一个替代的本体论。在CT中，对象和态射的类形成一个范畴。 态射是由定义域和余定义域来分类的。为例如，设A和B是范畴C中的对象，f：A→B是C中的态射，f具有结构域A和共结构域B。图5强于一些具体模型提供的证据，如自图灵工作以来提出的那些模型。第6章策梅洛·弗兰克尔集合论与选择公理7哲学意义94H.D. Macedo等人/理论计算机科学电子笔记324（2016）91然而，元理论CT，除了它使用的ZFC包之外，并没有为C中的A=B形式的命题提供意义。这样的理论只在f和g是态射时才给f=g类型的断言提供意义。鉴于此，我们可以得出结论，在集合类（所有集合和它们之间的所有函数的类的原型范畴）中，只有函数上的恒等式具有精确的语义。此外，关于SETS的对象，即，集合本身，不能说任何两个集合相等或不相等。最多只能可以说，它们是同构的或不是9。这种观点的改变是非常有趣的，因为它提供了更多的方法来比较某些概念的模型，而不是在ZFC之上形式化概念。本文遵循模型理论的方法来定义有效性，通过提供一种替代方法来使用范畴理论来表示有效性函数。我们的建议是不同的有效的topos（[7]），并从一系列的文章中提出的工作教授。罗伯特·沃尔特斯（参见[16]关于这个主题的简短在下一节中，我们将讨论我们对有效性研究的替代方案的主要动机2E-选择性及其范畴模型高阶逻辑（HOL）通常用于表达和形式化计算机科学中的概念（[9，14，15]）。作为一种类型化语言，它非常适合于形式化规范和验证中无处不在的类型规则。与ZFC规范（通常是无类型的，使用一阶逻辑）相反，这种类型化规则比避免悖论的简单事实有更深层次的后果。由于篇幅有限，我们不能在此讨论。读者可以看到[5，8]的全面介绍。从模型论的对应物来看，高阶逻辑理论有特殊的范畴，称为Toposes，作为这些理论的抽象模型，就像Heyting代数作为直觉主义命题逻辑的代数模型一样。虽然有一个简单的定义，一个topos描述了整个数学宇宙的话语HOL理论。任何可证明的HOL公式在每个拓扑中都是真的，因此在集合中也是真的。另一方面，任何topos都有一个内部逻辑，如果HOL公式在这个topos中为真，那么这个公式在直觉逻辑中是可证明的。 范畴SETS是一个以经典HOL作为内部语言的topos，因为每个有效的经典HOL公式在SETS中都是真的。 另一方面，来自预序范畴ω=的函子范畴{0，1，2，n，.. . }转换为SETS只验证直观有效的HOL公式。在这篇文章中，从ω到SETS的有限值函子的子范畴是中心的。这个范畴用FinSetω表示。什么是有效性的适当话语范围？从技术上讲，我们想知道什么是研究有效性的适当主题。我们研究FinSetω的动机来自于这样一个结论：8.函数的重复性是一个已知问题9A同构于B，i ≠，存在f：A→B和g：B→A，使得f≠g=IdB和g≠f=IdAH.D. Macedo等人/理论计算机科学电子笔记324（2016）9195⎧⎨∃∧⎩topos满足排中律，只有可计算函数作为态射，并且有一个自然数对象。因此，有效性的论述领域必须放弃这三个属性中的至少一个，但让我们首先检查这样的结果。[ 13 ][14][15][16][17][18][19][首先，考虑强丘奇命题（SCT）考虑到一个函数是可计算的，当且仅当有一个程序来计算它，并且，任何程序都可以用它的代码来表示，而代码反过来可以被看作是一个自然数。因此，STC可以由以下一阶公式表示：<$f<$p<$n<$y·（T（p，n，y）<$Out（y）=f（n）），其中T（p，n，y）是Kleene利用Peano算术理论，我们可以得到T和Out分别作为原始因此，在任何带有自然数对象的topos中，T和Out也是原始递归的。因此，在类型化HOL语言中，SCT的形式是：fNN考虑一个具有自然数对象的任意topos，并具有经典逻辑作为内部逻辑，可以证明SCT与这种情况不一致，即在这个topos中SCT不能成立。利用经典逻辑满足排中律的事实，g的定义如下：m+1，如果jN（T（n，n，j）Out（j）=m）g（n）=0否则对于每个n，都可以证明是有定义的。 因此g是一个全函数，因此SCT有一个程序p。然而，任何实现g的程序p∈N使得g（p）=（g（p））+ 1，因为存在j，使得T（p，p，j）和Out（j）=m和（g（p））=m+ 1。这是不可能的，所以SCT与具有自然数对象的topos中让我们在定义拓扑时分析剩余的替代方案。拓扑可能具有以下属性：(i) 拓扑结构的内在逻辑是经典的;(ii) 拓扑中的每一个态射都是有效的，即，螺旋CT在地形中的应用(iii) Topos有一个自然数对象。我们如果我们用非经典的内部逻辑来定义一个topos，我们最终会重新审视研究得很好的有效topos。另一方面，如果我们去掉第二项，我们就得到了第一项和第三项，也是研究得很好的递归函数的经典理论最后一种选择是放弃自然数对象的存在。在一个朴素的设置中，i和ii一起包含有限集合和一阶有限域逻辑。在范畴论的背景下，FinSetω代表了我们声称值得更多研究的这种选择96H.D. Macedo等人/理论计算机科学电子笔记324（2016）91An3FinSet（FinSet）定义计算模型的第一步是澄清什么是一个有限的集合这样的努力避免了误解，在接下来的发展，由于其直观的特点，一个人通常会越过手续失去洞察力。有限集是用finite来定义的，这意味着有限的和数学上的：定义3.1空集是有限的。 一个非空集S是有限的，如果存在一个从S到自然数的一个前缀{1，···，n}<$N的双射。数n通常被称为集合的基数请注意，通过依赖自然数来定义有限集合，我们并没有在可计算性模型中引入自然数对象（NNO）。人们可以很容易地使用[6]中研究的其他替代品来定义有限性，然而N的使用简化了我们对有限集的表征定义3.2以有限集合为对象和所有这些集合之间的函数的范畴，记为FinSet，是集合的全子范畴，其中对象被限制为有限集合。我们对FinSet的定义筛选了集合之间的所有函数的范畴，并丢弃了每个具有无穷集的函数作为域或值域，下面的命题表明FinSet中剩余的函数是有限的。命题3.3一个函数f：A→B有一个有限域，即A是一个有限集合，是有限的，即集合{（a，f（a））的基数|a∈A}是有限的。证据设f是一个函数，其类型为f：A→B，其中A是一个有限集。 由于f是一个函数，对于每个a∈A，必须只有且只有一个元素b∈B使得b=f（a），因此f（a）的元素最多与a中的元素一样多。 因为A中元素的数量是有限的，所以元素的数量也是有限的。{（a，f（a））|a ∈ A}。Q作为推论，FinSet中的每个函数都是有限的。现在让我们来研究FinSet中的hom-集合的基数，即有限集合之间的函数命题3.4给定有限集合A={a1，· · ·，an}和B={b1，· · ·，bm}，函数空间B是具有m个元素的有限集合。我们现在可以证明以下几点：命题3.5对于有限集合A和B，每个函数f：A→B都是可计算的。证据假设A和B是有限集合，那么根据公式3.4，函数B的空间A是有限的。因此，让我们选择一个函数f：A→B。让我们证明它是可计算的。因为f是一个函数，对于每个a∈A，存在唯一的b∈Bs. t。f（a）=b.由于A被（3.1）式所限定，它具有某个基数n，并且存在一个双射，我们可以用它来断言A={a1，···，an}。现在可以将f应用于A的每个元素，得到H.D. Macedo等人/理论计算机科学电子笔记324（2016）9197输入x;输出y;并行如果x> r1，则t2;如果x> r2，则t2;：如果x> r3，则t1;endFig. 1. 程序计算K集合{f（a1），···，f（ann）}，f的像通常写为f（A）。因此，我们设计了一个程序P，将f计算为输入x的简单查表。Q由于在前面的证明中，表查找参数固有的模式匹配，因此需要研究元素对等式判定造成问题的情况，例如在有限集合或不可区分集合中。模式匹配具有不可区分元素的有限集合让我们从可能无法区分的元素开始。当定义一个有两个元素的有限集合A的函数时，我们假设元素是可区分的。这样的论证可以从同构对象被认为是相等的这一事实中推导出来，因此，因为每个有n个元素的有限集合A可以与集合{1，···，n}进行双射。在实践中，我们抽象出元素的性质，并使用自然数标签。在模式匹配过程中，在FinSet外部不可区分的元素e和eJ在内部也将不可区分 在任何情况下，给定集合没有重复元素的事实，也就是说如果a∈A那么{a}<$A = A，由两个不可区分元素{e，eJ}建立的集合不能是二元集合，因为它需要双射f：{e}→ {0，1}，但基数不同。模式匹配包含无限元素的有限集合命题3.5成立，即使A和B的元素属于一个非递归的递归可递归集。让我们也知道R中的差是递归可递归的。设A={r1，r2，r3}<$R，B={t1，t2}<$ R，K：A→B，使得K（r1）=K（r2）=t1，K（r3）=t2. 我们可以假设实数由计算它们的进程/程序表示。例如，π可以由任何程序表示，给定精度p，π扩展到该精度。等价地，我们可以把实数看作是列出它们的十进制展开式的程序。在最后一种情况下，π是任何打印3.141593的程序。永不停歇使用（可计算的）实数的最后一种表示，函数K由图1中的程 序计算。 其中命 令parallel： ;. ：;end 并行运行 所有 <的cmdi>，i= 1，n，并且每当某些停止时停止。parallel命令的输出是第一次停止的的输出。像这样的程序，需要这样一个事实，即有限集合之间的任何函数都是可计算的，即使在这种情况98H.D. Macedo等人/理论计算机科学电子笔记324（2016）91·↓01¸2¸···n域的元素属于非递归的递归可重复数据类型。既然我们解决了使用模式匹配所产生的问题，我们可以继续证明如何使用有限函数作为原子和可计算步骤来构建复杂行为。命题3.6设A、B和C是有限集合，f和g是有限函数，其类型为f：A→B和g：B→C。复合函数g·f是一个有限且可计算的函数。证据合成g·f是一个函数，具有A→C型。由于A和C是有限集合，命题3.4成立，这意味着gf是函数CA的有限集合的成员，作为一个函数，它必须将A的每个元素映射到C的一个元素，因为A中有有限元素，g·f映射至多有限元素，因此它是一个有限函数，因此通过命题3.5，复合g·f是可计算的。Q因此，扩展前面的论点，我们可以证明FinSet中的每个态射都是可计算的，因此有限函数的每个有限组合都是可计算的。为了使这样的陈述精确，让我们定义函数的有限合成。定义3.7设n∈N是一个固定数。从n中我们得到一个预序范畴，其对象为1到n，当a≤b时，所有态射a→b，记为↓n，并描述为：范畴↓n是一个有限线性预序。任何从↓n到FinSet的函子都可以作为有限函数的有限合成的表示。因此，通过命题3.6和固定n，函子范畴FinSet↓n是可计算函数的范畴。尽管如此，FinSet↓n的表现力不足以捕捉所有的计算，例如π的计算。为了捕捉无限行为，我们将研究n被ω取代的情况，从而将FinSetω作为计算模型进行研究。刚刚提到的极限以及ω允许捕获无限行为的原因将在下一节中阐明。4在FinSetω在本节中，我们定义了基本范畴FinSetω，我们证明了这样的范畴至少与通用图灵机计算模型一样具有表达能力，并且我们观察到FinSetω也包括不可计算的行为。这样的最终观察导致了关于应该对FinSetω施加什么限制以限制其对可计算函数的表达能力H.D. Macedo等人/理论计算机科学电子笔记324（2016）9199ω4.1在FinSetω中将计算编码为函子我们的标准计算模型是图灵机，它是一个自动机，具有非空的有限状态集Q，来自字母表Γ的有限读/写符号集，独特的空白符号b，描述机器行为的部分转移函数δ，对应于机器初始状态的独特状态qo和最终状态集FQ因此，元组M=（Q，r，b， r|b，δ，q0，F）对应于图灵机，通用计算模型为了完成计算模型，机器M通常与包含具有以下符号的单元的无界带耦合：更准确地说，在每个时刻，机器都可以访问一个单元格，并被允许移动到磁带中的左（-1）/右（1）单元格。这种运动由δ控制，如其类型所记录的δ：（Q\F）×Γ→Q× Γ× {− 1，1}当到达final（F）状态时，图灵机停止，因此δ的类型读作“对于每个定义的非final状态和机器状态改变的符号，一个新的对于每台机器M和磁带，机器的行为都有明确的定义，并用配置序列Ci表示，其中i是跟踪发生的转换次数的自然数。因此，机器M在给定磁带上的行为等价于一个无限序列的配置C0·C1·C2···，它编码了机器的逐步执行。这样的序列通常被称为计算。因此，让我们解释如何在我们的模型中编码计算。配置行为很容易在FinSetω中编码。 在正式解释为什么这是一个事实之前，让下面的图来说明无限配置序列。事实上，它提供了对刚才提到的序列的几何透视。C0C1C2Cn但是，012n图二. FinSet中的计算现在让我们使配置Ci具体化，从而使用FinSetω提供关于编码的严格状态。一个配置由一个包含状态q∈Q的有限集合组成，机器在其中，磁带中的当前位置（p）和一个包含磁带内容的有限字符串w∈Q因此，每个配置都是由自然数索引的有限集合，无需进一步定义T∈FinSet100H.D. Macedo等人/理论计算机科学电子笔记324（2016）91⎪⎨⎨如10：（一）T0（i）=Ci=（q，p，w）T1（i → i + 1）= λ（q，p，w）. （qJ，p+off，wJ）T1（i→j）=T1（（j−1）→j）·T1（i，（j−1））其中（qJ，γ，off）=δ（q，wp），wJ是w的副本，除了位置p中的内容是wpJ=γ因此，我们对有效性的定义可以用来证明SCT论文的一个应用，每个图灵机都有相应的有效计算模型。它对应于与机器执行相对应的动态系统的展开。因此，有趣的问题是蕴涵的反命题。FinSetω中对应于计算的元素是什么？e.图灵机在回答这个问题之前，让我们强调一下计算的函式表达式和关于可计算性的民间知识之间的一个有趣的连接点，该连接点表示可计算函数必须满足以下条件：这个陈述可以在（1）中T1注意它是如何陈述的，给定一个时间跨度（i→j），要观察输出的行为，只需要计算有限的量（实际上是应用T1的j−i+ 1步）。4.2FinSetω的哪个子范畴对应于计算？既然我们已经证明了一个结果，即有限集合之间的函数是可计算的，并且这些函数的合成也是可计算的，那么我们可以预期，给定图2中的计算框架是有限集合之间的逐步转换，给定框架是FinSetω，我们可以推测FinSetω的函子确实是可计算实体。但事实并非如此，原因是当用ω代替↓n时，有限函数复合再次成为有限函数的论点丢失了现在我们将给出一个反例，证明FinSetω的函子中必须存在更多的结构才能使其可计算。这个论点是基于以下推理。假设对于每一个i，我们都赋予一个包含真值T和的有限集合。我们还假设图灵机的枚举。对于每一个我都有一个函数，f（i）=如果第i台机器停止，否则，函数f是FinSetω的一个成员，但由于它解决了停机问题，10我们采用T=（T0，T1）函子符号，其中T0是对象映射，T1是态射映射H.D. Macedo等人/理论计算机科学电子笔记324（2016）91101¸η0zvr¸η1zvr不应该是可计算的。因此，应该向FinSetω添加更多要求为了使它对应于一类计算。值得注意的一点是，所描述的f可以被分成批次，预先计算或部分评估。例如，对于每个i，我们可以将第i台机器和第i+1台机器的结果存储在一个表中。此外，我们可以批处理（表）大量的f的结果，预计算并存储结果，但尽管如此，人们不能预计算整个函数。这就像运行算法的程序必须是无限的，才能计算出整个输入域的函数。记住这一点，我们将发展使用自然转换的概念。4.3将计算编码为自然变换另一种观点是在抽象上更高，并使用FinSetω函子之间的自然转换，因此元素η类型为η：FinSetω→FinSetω。设C和CJ是FinSetω中的函子，其中C对应于某个图灵机的计算，对于Cj的情况也类似。我们可以定义一个自然变换η：C→Cj，使得对于每个i∈ω，我们有ηi：C（i）→CJ（i）。以C为例，用图形表示：C0C1C2Cn但是 ，01和CJ用图形表示：0¸12012年12月2012年12月vzzvzvzvC0JC1JC2JCnj那么自然变换η：C→CJ被描述为：C0C1C）Cn¸¸0¸12012年12月η2vzrηnvzrC0JC1JC2JCnj将C的每个元素变换为满足自然性条件的CJ在深入研究自然性之前，让我们举一个简单的例子。选择C作为任意图灵机T的执行，CJ作为执行配置102H.D. Macedo等人/理论计算机科学电子笔记324（2016）91¸η1zvn+ 2在每个时间间隔执行两步T的图灵机C0C1C2Cn但是，012nη0zvη2zvηnzC2C3C4Cn+2η是一个自然变换的事实表达了一个已知的事实，即可以将计算分批分组为了实现这一点，只需在ω范畴中选择态射h：ω→ω，其中h（i）=i+2，它直观地将ω的连续元素分组，也就是说，它在离开ω的拓扑中创建覆盖，并且它被描绘为：012nh（0）c=2h（1）c=3h（2）c=4h（n）=cn+2由自然性产生的性质表明下面的图是可交换的：C0C1C2但是，0¸1H2012年12月2c4c6cη0vzη1zvη2zvηnzC2C3C4Cn+2并对这样的属性进行编码，该属性表示一个人能够计算任意数量的计算步骤，然后向前看两个状态。或者分批计算相同的任意数量的步骤。能够对可计算函数建模的必要条件背后的直觉是，执行计算所需的步骤数量应该是有限的。也就是说，产出的生产所包含的内在逻辑是有限的。这就相当于在一系列步骤中找到一个极限limηn =ηtn→ω这样的条件也是必要的，但并不充分，如果在图灵机的配置序列中理解，它表明在时间t的某个点上δ函数是完全定义的，并且可以存储为有限表。5FinSetω中哪些元素是可计算的？现在让我们从相反的方向来看：哪些函子确实可以计算，或者换句话说，哪些函子与图灵机相关联？H.D. Macedo等人/理论计算机科学电子笔记324（2016）91103我们的猜想是，这样的函子是存在由F在ω上诱导的拓扑的覆盖的函子。换句话说，只有紧的函子F才应该被认为是有效的。为了观察这种覆盖并分析FinSetω逐步演化（计算步骤）的拓扑，我们通过添加另一层ω来跟踪ω来增强模型，从而获得函子（FinSetω）ω=FinSetω×ω，如图所示。3 .第三章。按照惯例，我们假设垂直增长的ω编码逐步的机器执行，而水平增长的ω编码逐步的转换。使用这种编码，图灵机的转换是FinSetω函子之间的自然转换。因此，每个水平阶规定了Fi和Fi+1之间的态射η。、、，F0（m）<$F1（m） <$F2（m）<$Fn（m）<$、、m，F0（2）<$F1（2）<$F2（2）<$Fn（2）<$、、2，F0（1）<$F1（1）<$F2（1）<$Fn（1）<$、、1，F0（0）<$F1（0）<$F2（0）<$Fn（0）<$、、0¸12012年12月图三. FinSetω×ω模型。我们将增广模型刻画为一个流形，即计算流形，其中每个元素Fn∈FinSetω，每个（n−1）步计算迹是从满足相容性条件的整个流形（at- las）FinSetω×ω的投影（通常流形术语中的映射）.直观地说，这样的条件保证了在流形中描绘公共点的映射应该是相容的，也就是说，在这样的点的邻域中的映射的交集应该具有相同的形状。5我们将使用丛、筛和命题5.1范畴FinSetωω可以对应于一个在（ω×ω，FinSetω）上的层证据设T是图灵机，函子 FT：FinSetsω×ω定义如上。用Grothendieck拓扑来装备ω×ω。则FT满足相容条件，因此FT是层。Q正如所暗示的，存在每个图灵机T到FinSetω×ω的成员的内射映射，利用这样的T<$→FT内射映射，人们能够证明对象104H.D. Macedo等人/理论计算机科学电子笔记324（2016）91对于某个图灵机T，形式为FT的FinSet的ω×ω构成一个子范畴Tur。因此，问题是：FinSetω×ω中的可计算元素是什么？它们是什么？命题5.2（猜想/目标：）Tur是（FinSets ω）ω的相对子范畴吗？如果是，我们有每个计算层C本质上是FT，对于某个T. M。T.5.1E函数作为流形，程序作为投影在描述数学对象的局部/全局方法的传统中，其中• 拓扑流形是局部连续的对象，即，每个点具有其图表是连续函数的相邻点• Different（Ck）流形是局部（Ck）可微分的对象，即，它的每个点都有一个开邻居，其图是Ck。我们的计算模型是一个流形，其中对象是局部可计算的。6结论我们目前基于有限集合的有效性模型方法的状态仍在进行中，但作为结果，我们已经制定了一些重要步骤。我们展示了如何将图灵机行为编码为FinSetω中的函子。我们将函数性与必要条件联系起来，即为了产生有限数量的输入，图灵机必须只消耗有限数量的输入。我们将n步（批次）计算表示为自然变换，并使用批次的概念来设计FinSetω中确实可由图灵机计算的元素的限制。相关工作我们建立了一个模型，实现了使用CT的有效性的模型理论方法，该方法与有效性ToposE和[16]不同。 这是不同的 从E，topos出现从一个类别的集合配备了一个对称和传递关系和等价类的功能关系之间的这种集合，因为它确实使用了一个简单的直觉主义topos没有自然数对象（NNO），而E使用一个非经典的，并有一个NNO。它也不同于[16]描述的方法，因为它也使用NNO我们的框架在类别中没有我们认为这可以被视为一个优势[16]，它强烈依赖于自由对象，例如输入和输出数据的幺半群。这些输入/输出数据在我们的方法中不是必不可少的H.D. Macedo等人/理论计算机科学电子笔记324（2016）91105在[4]中，使用CT提供了递归性的分类表示。它以完全抽象的方式将能够定义原始递归态射的范畴axiomatizes。使用范畴的内部语言，可以精确地定义任何原始递归函数。这项工作非常有趣，因为它以一种非常和谐的方式将模型理论定义与证明理论定义结合起来。元理论中存在的同一性为一种在定义原始递归函数的故意不同的方法之间的平等理论提供了意义。除此之外，不需要提到一个更丰富的自然数定义的具体数值系统，但需要定义原始递归性。最近有人试图将Church-Turing的地位从一个不可证明的论点转变为一个正式的证明[3]。我们的目标不是证明这样一个巨大的结果，而是第一步进入有效性的定义。今后工作所提出的计算模型不模拟环境输入，输入磁带内容在计算开始时是固定的。即使磁带内容可能会因机器执行的动作而增长，也不能接受由另一台机器生成的无限输入，例如，一台机器正在产生π的无限十进制扩展，而另一台机器正在处理这样的输出作为输入。因此，未来的工作可以通过丰富模型或重新解释FinSetω×ω来解决这个问题。我们还设想了一个更好的和形式化的证明，证明图灵机与FinSetω×ω中的局部可计算层相等。进一步研究的另一个途径是对其他可计算性范式的比较和建模。例如，自然数序列上的递归函数。以及我们的拓扑结构如何与域理论研究中的拓扑结构相联系，例如：Scott拓扑确认目 前 的 工 作 得 到 了 CNPq ， ConselhoNacionaldeDesenvolvimentoCient′ficoeTecnol′ogico-Brasil引用[1] 阿基米德和T. L.希思，[2] Dehaene，S.，N.莫尔科湖Cohen和A. J. Wilson，Arithmetic and the Brain，Current opinion inneurobiology14（2004），pp. 218-224[3] Dershowitz，N.和Y. Gurevich，可计算性的自然公理化和Church论文的证明299-350[4] Eilenberg，S.和C.C. Elgot，[5] 戈德布拉特河，106H.D. Macedo等人/理论计算机科学电子笔记324（2016）91[6] Haeusler，E. H、在toposes中的精确性和计算，第11届计算模型发展国际研讨会的初步会议记录（DCM2015）http：//dcm-workshop。org. uk/2015（2015），p. 27岁。[7] Hyland ， J.M. E 、 《 逻 辑 与 数 学 基 础 研 究 》 （ Studies in Logic and the Foundations ofMathematics）110（1982），第110页。165-216[8] 约翰斯通，P.T.，《大象的素描：拓扑学理论纲要》（Sketches of anElephant：A Topos TheoryCompendium-Volume 1），彼得·约翰斯通（Peter T Johnstone）著，页100。562.彼得·约翰斯通的前 言 牛 津 大 学 出 版 社 ， 2002 年 11 月 。 ISBN-10 ： 0198534256 。 ISBN-13 ： 97801985342591（2002）。[9] Lambek，J.和P. Scott，[10] Machtey，M.和P. Young，; pp.[11] McLarty，C.，“Elementary categories, elementary toposes,” Oxford University Press,[12] 罗杰斯，H.，“Theory of Recursive Functions and Erective Computability”，MIT Press，1987，141-146页。[13] 夏皮罗，S.，Varieties of pluralism and relativism for logic，A companion to relativism（2011）. 526-552[14] 史密斯，D. R.，机械化软件开发，NATO ASI系列F计算机和系统科学173（1999），pp.251-292.[15] Srini vas，Y. V. 和R. Jullig，Specware：面向对象的软件设计，见：程序构造数学，Springer，1995，pp. 399-422.[16] 沃尔特斯河，巴西-地F. C.的方法，