有限计算代理的共归纳模型：集合论和代数扩展的表达性研究

URL：http://www.elsevier.nl/locate/entcs/volume 19. html21页s有限计算主体的共归纳模型彼得·韦格纳布朗大学Providence，RI美国迪娜·戈尔丁美国马萨诸塞州波士顿，马萨诸塞州，美国摘要本文探讨了共同归纳方法在有限交互计算代理建模中的作用。计算代理从算法到交互的计算扩展与集合论和代数从归纳模型到共归纳模型的数学扩展相平行。最大固定点在观察模型中扮演着一个角色，与归纳数学中的最小固定点相似。互动（共归纳）模型的影响教会最后一节表明，实际的软件系统是交互式的，而不是算法的。随着计算机应用程序变得越来越具有交互性，共归纳模型在软件技术中可能变得与归纳模型一样重要。1表现力的扩展图灵机、lambda演算和递归可重复集的鲁棒等价性因为研究者假设有限计算代理的表现力问题已经一劳永逸地解决了，他们没有探索可计算性的替代模型，而是专注于算法的复杂性，性能和设计交互式有限计算代理比算法更具表达力的假设开辟了一个被认为是封闭的研究领域，并需要重新审视有关计算模型的基本假设。我们已经证明了[We1，WG]，随着时间的推移提供服务的交互机器比计算函数的图灵机更具表达力1999年由ElsevierScienceB. V. 操作访问和C CB Y-NC-ND许可证。2→→从算法到交互的表达性的扩展是由集合论和代数的最近扩展形式化的[Ac，BM，JR]。非良基集合理论通过形式化流的语义来对顺序交互进行建模[BM]：计算表现力的扩展：算法交互集合论表现力的扩展：良基集合非良基集合代数表示性的扩张：代数→余代数交互作用的模型，就像算法模型一样，可以用集合和代数以互补的方式描述。非良基集是图灵机的递归可重复集的交互式模拟，而余代数则扮演着lambda演算的角色余归纳是非良基集合论、余代数和交互作用的基础，是定义、推理和建模的抽象原则共诱导与溯因有关，溯因从观察到的行为中推断出内部系统的属性[We3]。数学表现力的扩展：归纳模型→演绎（溯因）模型TM、算法、可计算函数和形式系统的等价表达能力主要是由于它们共同使用归纳法作为系统规范的基础。丘奇-图灵命题的形式是它将算法计算的直观概念等同于从整数到整数的图灵可计算函数的形式概念Church-Turing Thesis：算法的直观概念由图灵机正式表达。X =算法，Y =图灵机在第5节中，我们通过扩展计算的直观概念X和相关的形式概念Y，将丘奇-图灵命题从算法扩展到顺序和多智能体交互：E1：顺序交互作用的直观概念由非良基集正式表示X =顺序（单流）交互，Y =非良基集E2：一般的交互式计算是用余归纳模型（余代数）来形式化表达的。X =一般（多流）相互作用，Y =余归纳模型（余代数）丘奇-图灵命题的扩展E1、 E2为相互作用模型提供了数学上的合理性非良基集合论和coal-gebras是归纳形式计算模型的共归纳扩展，表达了直观算法计算模型的扩展第2节介绍了作为流处理代理的交互机，3观察等价性（互模拟）作为交互式表达性的度量。第3节介绍了非良基集合论和余代数，并指出它们是如何建模流和标记转移系统的。第四节表明，消除初始性和用极大性代替极小性说明了共归纳比归纳更强的表达性。第五节考察了计算的元数学含义，包括Church论文的扩展第6节考察了软件工程，表明交互式模型为面向对象和面向代理的编程提供了一个统一的框架。2从图灵到交互机图灵机（Turing Machine，TM）是一种有限的代理，它通过一系列动作将输入非交互地转换为输出字符串给定输入的TM计算是历史独立的和可再现的，因为TM总是在相同的初始状态开始，并在计算期间关闭世界图灵机：TM是状态转换机M=（S，T，s0，F），具有有限组状态S和磁带符号T，起始状态s0，以及状态转换关系F：S×T→S×T。TM通过有限的计算步骤序列将有限的输入字符串x∈T转换为输出y=M（x），这些计算步骤从磁带中读取符号i，执行状态转换（s，i）→（sJ，o），写入符号o，和/或将读取头向右或向左移动一个位置[Tu 1]。交互机（IM）在模拟有限交互代理中发挥作用，与算法的TM相当。顺序交互机（SIM）模拟顺序交互，将输入转换为输出流。顺序交互机：SIM是状态转换机M=（S，A，m），其中S是一组可重复的状态，A是一组可重复的动态绑定动作（流元素），转换映射m：S×A→S将状态-动作对映射到新的状态。输入的动态绑定通过将m重写为从状态到动作-状态对的映射S → P（A ×S）来明确表示，该映射表示动作A的输入不确定性。有限主体的表达性由观察等价性来指定，并通过观察者区分主体行为的能力来衡量[WG]。TM行为由输入-输出对的集合组成，而SIM行为由观测序列的集合给定两个有限个体M1，M2，如果异或B（M1）<$B（M2）非空，则它们的异或B（M1），B（M2）相对于一类观察者（测试者）是可区分的 这个集合中的成员称为可验证性证书。有限代理是等价的，如果他们不能杰出的两个SIM的等价性可以通过有限的可区分性证明（观察序列）来证伪，但不能被无限地验证，这说明了波普尔的观点，即物理学的经验定律可以凭经验证伪，但不能被验证[Po]。用互模拟[Mi]表示的交互等价比邻线等价具有更强的区分能力.4∈× →×TM和可计算函数的输入在计算开始时完全指定可计算函数f：X→Y有一个输入字符串（整数）的域X，并且对每个x X确定唯一的y=f（x）。交互行为不能指定为从域X到范围Y的转换，因为流是动态生成的。交互流具有（a1，o1），（a2，o2），... . 其中，输出ok是从操作ak输入的，但是在操作ak+1中在s和c之前。 这种输入输出耦合违反了域和域的分离，导致了dy-输入对先前输出的动力学依赖，是交互式问答、对话和控制过程的特征。交互式输入的延迟（惰性）绑定（输入非确定性）比早期（静态）绑定更有表现力，不是因为交互具有更大的函数转换能力，而是因为更丰富的输入域不能由字符串归纳指定持久图灵机（PTM）是一个规范的模型，顺序交互，是尽可能直接的扩展TM [GW]。持久图灵机：PTM是一个多带TM，它有一个持久的工作带，其内容在交互之间保留。PTM的单个交互对应于TM计算，但其持久状态允许其语义扩展到定义SIM行为。PTM确定SIM（S，A，f），其中S是持久工作带的状态（内容）集合，A是输入集合（对应于初始TM输入）。转换函数f是由底层TM计算的映射f：A S S OS和A的元素在任何给定的时间都是有限的，但无界。为了理解SIM卡相对于TM的额外能力，考虑TM相对于有限查找表（FLT）的额外能力是有帮助的，当给定相应的键时，FLT返回一个值TM计算的单步转换包括执行新TM状态的查表和基于当前状态和磁带字符的磁带动作除了查表之外，TM在每个步骤中执行的唯一额外工作包括FLT可以被认为是原始的有限计算代理，其表达性是命题演算。由一系列FLT查找组成的TM计算比FLT计算更具表达力，因为它的行为不再是有限的。类似地，图灵可计算单步转换是SIM计算的原始计算步骤SIM计算比TM计算更有表现力，因为动态提供（外部控制）TM计算步骤的序列允许有限代理表现出不可预测的可能行为。SIM卡不能用算法表达的非正式论点非常简单，因为它只依赖于流元素是动态提供的概念命题：SIM的计算不可由或可约表示5到TM的计算。非正式证明：TM不能用有限输入表示，因为任何有限输入总是可以交互扩展的。流的转换不能通过字符串的转换来建模流没有最后一个元素，可以被不可预测的对手动态扩展，并且可以使用以前的输出来确定下一个输入。TM输入字符串有一个预定的有限长度，一旦计算开始就不能改变一个更精细的论证表明，对于有限计算，SIM比TM更有表现力设k为交互式计算的长度（交互步骤的数量），设Bk为可以进行k次或更少交互的观察者可以观察到的行为类别。我们可以证明，对于所有k>0，Bk<$Bk+1，而TM的行为对应于B1[工作组]。计算对于k+1交互作用比k交互作用更有表现力在这个意义上，它们可以进行更精细的观察区分。互模拟[Mi]捕获了k+1对k个输入的更大的观测区分能力。包含前k个交互输出的SIM可以通过k+ 1区分，但不能通过k个交互区分。交互式提问者（Ken Starr）通过k+1比通过k个后续问题可以引出更多关于被提问者（Clinton）的信息20个问题的游戏进一步说明了后续问题在获取信息方面的力量。TM具有k = 1的PTM的表现力：它们的行为仅限于回答单个问题（或预定的非交互式问题序列）。顺序交互的表现力已经在[WG]中进行了更详细的研究，包括问答和图灵测试[Tu2]。多流交互机（MIMs）是与多个自治代理交互的有限代理，如航空公司预订系统或为多个自治客户端提供服务的分布式数据库与多带TM并不比单带TM更有表现力的事实形成对比的是，MIM可移植性不是SIMs可表达的[WG]流的输入-输出耦合在合并时无法保留。我们证明了[WG]，输入输出耦合（可串行化）不能被保留为子任务的委托和其他形式的不可串行化行为，证明了MIM比SIM更具表达性：自治流的输入-输出耦合在合并时无法保持MIMs表达的是SIMs无法表达的不可序列化行为MIMs对可序列化行为的限制，就像SIM对非交互行为的限制一样，以问题解决能力为代价实现了易处理性。将自主流（观察通道）添加到有限智能体中可以增加表达能力，而添加非交互式磁带只会增加预定输入的结构复杂性，而不会6∈∈出色的表达能力MIM比SIM更具表现力，而多带和单带TM同样具有表现力串行化多个线程（流）的结果限制了有限代理解决问题的能力。不可序列化行为是集群的一个特征，它将处理与多个下属交互的高级管理人员与单个流交互的装配线工人区分开来[WG]。协作、协调和管理由MIM建模，而不是SIM或PTMMIM的行为比SIM的行为更难形式化，并且MIM比SIM更大的表达性比SIMs比TM更大的表达性更难证明。MIM支持不可序列化事务和真正的并发性[Pr]，而SIM只支持可序列化事务和交错并发。可验证性（观察不等价性）的度量确定了顺序交互的表现力层次结构和MIM比SIM更大的表现力。3非良基集与余代数虽然表达性的问题可以完全用基于机器的概念来表述和证明，但用非良基集合论和余代数来重新表述可以为交互式模型提供数学上的合法性。集合S上的二元关系R是非良基的，如果存在无限序列ebIS，其中i=0，1，2， . 。 . . 因此，对于所有I，都有bi+1Rbi，否则是有根据的。集合的良基性是根据集合成员关系的良基性来定义的;如果集合结构上的集合成员关系是良基的，则集合是良基的，否则是非良基的。良基集只有有限的集成员链，而非良基集合可以有无限集合成员链。在传统的集合论中，集合可以通过并、交、补和叉积构造器从原子元素中归纳构造，这些构造器构造具有原子元素的集合。 powerset构造函数构造集合，集合的元素也是集合。Zermelo-Frankel集合论提供了集合论的一个公理化的具体化ZFC-，它可以被基础公理补充以获得归纳可具体化的集合ZFC。foundation axiom（FA）：所有集合都是有根据的（可归纳定义）。FA不包括非良基集合，这些集合由可解集方程系统定义。一组可解集方程：可解集方程的系统具有（S，A，m）的形式，其中S是一组变量（状态），A是一组常数（动作，观察），m：S→P（A<$S）是一个映射，它指定每个s∈S一个集合7→→×--A中的常数和S中的变量。一个非良基集合可以定义为一个集合，它是一个可解的集合方程组的解形式m的方程：SP（A）S），其右边是有序对的集合，可以通过变换（a，b）→ a，a，b [BM]表示为可解方程。例如：集合方程s=（0，s），（1，s）的解是无限二进制字符串的集合，说明非良基集合可能是不可枚举的。非良基集合论利用反基准则（AFA）对ZFC-进行扩充，得到ZFA。[BM]AFA的特殊性在于所有的可解方程组都有唯一的解。反基础公理（AFA）：每个非线性方程组都有唯一解（ZFC- + AFA =ZFA）。ZFA是相容的，如果ZFC-是相容的，并且比ZFC允许更大类的集合（模型更大类的系统）集合方程s={（0，s），（1，s）}的解不满足FA，不能归纳生成。它不是ZFC的成员，说明类ZFA严格大于ZFC。非良基集可以对标记迁移系统（LTS）进行建模。具有n个状态的LTS可以由n个联立集合方程（S，A，m）的系统指定，其中m：S → P（A × S）将状态映射到动作-状态对的子集。例如，具有标记为a到s1、b到s2和c到s3由映射s→ {（a，s1），（b，s2），（c，s3）}表示。非线性方程组的映射函数m是余代数的。余代数是一种交互式计算的模型，它与代数类似，是算法的建模框架。代数计算步骤指定增量表达式评估，其目标是计算值，而联合计算步骤指定增量系统观察，其目标是确定系统行为。代数是结构A=（S，m：F（S）S），其中S是载体集，F是确定A的签名的函子。我们通常将S解释为一个值的集合，而m：F（S）rightarrowS是从语法上指定的表达式集合到值集合的保值同态。代数确定从语法指定表达式的归纳定义的初始代数到确定值集的商代数的归约过程（映射）余代数是结构CA=（S，m：S→Γ（S）），其中S是载体集，Γ是决定CA的签名的函子。我们通常将S解释为观测系统的一组状态，m：S→Γ（S）解释为从具有未知状态的观测系统到展开的行为集（观测序列）的行为保持同态。映射是一对一的余代数称为最终余代数。 最终余代数的状态表示展开的系统行为，并由非良基集指定。8→ ××→×初始代数是归纳指定的表达式集合，而最终余代数是共归纳指定的非良基集合。非良基集合相对于良基集合的更大的丰富性转化为余代数相对于代数的更大的计算能力。将系统映射到其行为的余代数同态比将表达式映射到值的代数同态更强，因为具有相同行为的系统的等价类（例如，计算相同函数的程序）是不可枚举的，而具有相同值的表达式的类是可枚举的。指定非良基集和模型序列相互作用的余代数具有形式m：S→P（A<$S）的映射，对应于AFA。文[BM]证明了LTS的映射m：S P（A S）或映射m：S OP（A）S）可表示为可解的方程组。然而，共代数映射可以更复杂，并模拟某些形式的多流相互作用。形式为S→Γ（S）的余代数映射是形式为ΓJ（S）→Γ（S）的非马尔可夫映射可以模拟一些下一个状态依赖于前几个状态的事务系统（MIMs）我们推测-具有持续时间或多代理交互的重叠操作的动作可能需要更复杂的映射。此外，我们相信，集合论的一致扩展，允许比非良基集合更大的集合是可能的，对应于非序列和多流有限代理[WG]。原则上，任何有限主体都可以通过集合论的一致扩展来建模，该集合论表达了主体可计算的行为类别，并且可能具有比非良基集合更复杂的共代数映射函数。多流交互的形式化是未来研究的主题，超出了本文的范围4从归纳到共归纳归纳法确定了定义、推理和建模的构造范式，其特征在于初始条件，允许从初始元素构造（导出）新元素的迭代条件，以及只有这样构造的元素才是可定义的最小条件归纳定义：初始（基）条件，构造性迭代条件，极小条件构造范式：从基本元素归纳生成结构归纳法是定义字符串、语言、形式系统和可计算函数的基础。例如，字母表A上的所有字符串的集合A由迭代拼接规则归纳定义：9∈ ∈∈→{∈|}String：（1）空字符串eA;（2）如果x一把斧头A;（3）A不包含其他元素。文法G借助非终结符N将终结符T上的语言L（G）定义为通过生成规则（产生式）P从初始非终结符S∈N归纳生成的字符串集合：T上的语言L（G）是集合L（G）=XTSx，其中G =（N，T，S，P）是具有非终结符N，终结符T，初始符号S∈N和产生式P的文法.导子关系是由P定义的单步导子关系的多步传递闭包。形式系统的定理是通过推理规则从公理归纳得出一个形式系统FS=（AX，TH，RI）是一个定理集合TH的归纳具体化，其中（1）公理AX是定理;（2）由推理规则RI从定理导出的公式是定理;（3）没有其他公式是定理。形式系统在两个不同的层次上是归纳的。形式良好的公式和公理由静态归纳法定义，而证明过程则由动态归纳法定义。可证明定理的集合是由归纳定义的公理归纳导出的公式定义的归纳定义域（静态）：域X是归纳定义的归纳定义的计算（动力学）：计算过程是归纳定义的可计算函数f：X Y同样使用两个层次的归纳定义。他们通过归纳定义的计算过程将归纳定义的域X映射到范围Y[Tu1]。TM通过归纳定义的状态转换步骤来转换归纳定义的字符串这个条件是充分的，也是必要的：可计算函数可以定义为在归纳定义域上的归纳计算。共归纳法决定了一种解构范式，它将复合结构解构为渐进的更原始的结构。非良基集合是通过逐步分解成子集的过程来定义的，该过程对于良基（归纳）集合是无限终止的。共归纳颠倒了相关归纳过程的迭代方向，用最终性代替初始性。非良基集合通过消除有限终止性引入了更大的集合类，从而消除了对偶归纳过程的初始性共归纳模型的观察过程。有限终结的消除对应于这样一个事实，即观察过程可以继续无限期地揭示关于被观察对象的新知识：隐藏的信息被不终止的过程逐步逼近余归纳法反转了迭代的方向，消除了初始/最终条件，并用极大条件代替了极小条件10∈×共归纳定义：解构迭代条件，极大性条件观察范式：观察和分析已经存在的构造元素A上的流是有序对s=（a，t），其中a A和t是另一个流。A上所有流的集合S是方程S=A×S的极大解（极大不动点）。在传统的集合论中，流方程的解是平凡空集，而递归流方程的解是集合。的最小不动点方程S=A S是空集，而最大不动点是S上所有流的集合。通过用更原始的概念来表达归纳和共归纳，我们可以分别考虑在定义和推理过程中逆迭代、消除初始性和用极大性代替极小性的效果有限共归纳终止，像初始性，是一个封闭系统的要求，其消除模型开放系统。初始性的消除与将图灵机扩展为交互机时的初始状态（和最终状态）要求的脱落有关。它消除了在计算开始之前对完整环境规范的要求。极小性，由最小不动点建模，是计算和构造性数学的构造性过程的属性由最大不动点建模，是经验观察范式的属性，用于描述在已经构造（已经存在）的世界中观察到的行为行为的最小化与行为约束的最大化相关联，而行为的最大化与约束的最小化相关联。最大不动点（最小约束）为经验范式提供了一个理论框架，即任何与观察一致的行为（可能世界）都是可接受的。允许任何可能的世界与一个规范一致的规范是最大不动点（对行为的最小约束）。Kripke [Kr]的可能世界语义学和trans-martel模型理论之间的区别正是极大性与极小性的区别限制性社会组织与放任性社会组织之间的差异，例如极权社会与民主社会之间的差异，是由最小化与最大化所塑造的。最小化模型集中控制结构，而最大化允许分布式控制：最小原则就是极权主义：一切不被允许的东西都被最大化原则是民主：凡是不被禁止的都是允许的非良基集合论扩展了传统的集合论，集合是递归集合方程的解它为形式化具有共归纳（非良基）结构的集合提供了一个框架11扩展了集合可以形式化的模型类，以包括交互式计算模型共归纳扩展了有限计算代理的定义和推理能力，因此它们可以对由流定义的不可重复集合进行数学指称语义是通过对确定可计算函数的最小固定点的格结构近似来指定的[Sc]，而传统的操作语义则表示算法执行步骤的状态转换结构。非良基集合比良基集合表达更丰富的非良基集合论为流提供了指称语义，而余代数为作为流转换器的 交 互 机 的 操 作 语 义 提 供 了 框 架 [WG]。5共归纳的元数学丘奇和图灵在20世纪30年代早期的观点受到20世纪早期关于数学基础的激烈辩论的强烈影响，而康德早期对数学的必然真理和物理学的偶然真理之间的区别的分析又反过来影响了这一观点丘奇共归纳模型需要重新审视共归纳思维可以被看作是一种新的范式，它以质的新的推理形式取代了直觉主义和形式主义我们更愿意把它看作是直觉主义和形式主义的加强，它们表达了更强的意向性形式和更强的（交互的）图灵检验形式[We3]。共归纳模型比传统的直觉主义或形式主义模型更强的有限主体行为，因为它对数学对象的存在有更强的本体论承诺。在本节中，我们将考察丘奇论文中计算的直观概念和形式概念之间的关系5.1从形式模型到直观概念理解形式主义和直观概念之间的关系被形式化是哥德尔关于完备性/不完备性的工作和丘奇论文的中心目标将直观模型与计算的形式模型联系起来的论文，其动机既可以是希望将给定的直观模型形式化，12→→或通过为给定的形式概念提供直观的Church他认识到这些问题的答案是不可定义的，但可计算性的替代形式主义的等价表达似乎为丘奇-图灵命题提供了强有力的证据Church-Turing命题：lambda演算（Church）或TM（Turing）的形式有效可计算性表达了函数（对正整数）的有效可计算性的直观概念Church-Turing命题回答了“TM所表达的计算的直观概念是什么？"的问题而不是“什么是表达计算的直观概念的形式化模型"的问题在计算的早期，计算的直观概念被认为是算法，上面两个问题被认为有相同的答案。随着技术变得越来越交互，人们意识到算法无法表达交互，计算的直观概念继续被TM形式化，因为除了TM或良好的集合论之外，没有任何形式化的模型可用。非良基集理论和SIM提供了定义良好的数学和机器模型，超越了算法，允许论文扩展。我们并不反对丘奇共归纳模型一致地扩展了机器、代数和集合论的表达能力共归纳为定义、推理和建模提供了一种更具表达力的心理工具，表明图灵机是受归纳限制的弱表达模型当有效计算的直观概念被扩展到包括交互作用时，可计算性的形式概念必须相应地被扩展到非良基集的共归纳规范。序贯交互的论文：非良基集、SIM或PTM的形式具体性对应于序贯（单流）交互的有效可计算性的直观概念丘奇-图灵命题是用从整数到整数的可计算函数f：X Y来形式化的。整数的域X对有效图灵可计算性进行建模，但不包括其域不可归纳定义的交互流（第2节）将定义域表示为整数需要在计算开始之前完全指定参数，以及定义域和范围的可分离性：Church和Turing假设的条件，但流违反了这些条件。流映射f：流流当然不是从整数到整数的函数：无论它们是被分类为不可计算函数（在非归纳域上）还是可计算非函数（因为在非归纳域上的映射不被认为是函数）13这是一个定义的问题非归纳域上的可计算映射是否是函数的问题，据作者所知，还没有丘奇-图灵命题是关于算法计算的限制性概念的猜想，而不是关于计算的更广泛的直观概念。关于顺序交互作用的论文同样是关于计算的一个限制性概念的猜想，即非良基集合不是相容集合论模型中最具表现力的一类，更强大的相容模型是公理化的。通过用一个指定更大类集合的一致公理来取代AFA，可以定义更有表现力的计算机制类。 我们进一步推测，不存在公理可定义的相容集的定义良好的最大类，也不存在定义良好的最大有效可计算性的形式概念。这表明，有效可计算性的任何形式概念都是相对的而不是绝对的，只能相对于关于交互形式的假设来定义。5.2重新解读哥德尔不完全性哥德尔完备性结果证明了句法形式体系对于语义概念的完备表达的充分性。Church哥德尔不完备性定理可以看作是关于包含整数运算的客观数学系统的归纳推理的弱性（不完备性）的一个结果。然而，图灵的计算模型在其计算概念的归纳（构造）模型中是“前哥德尔”的。TM完全表达直观可计算性的立场可以等同于希尔伯特哥德尔利用可计算函数是归纳可指定的这一事实，使用哥德尔编号来枚举TM。一阶逻辑只能对可证明的语义域建模，因为它的定理数量是可证明的，这很容易证明。证明一个特定的语义域是不可枚举的，因此是归纳不完全的可能是困难的，但对角化是证明不可枚举性的一个有用的工具，康托和哥德尔都用对角化来证明实数的不可枚举性，证明整数算术的真断言的哥德尔14一阶逻辑只能对归纳（递归）可解释的语义域进行要证明任何整环的哥德尔不完全性，证明它不是归纳可归纳的对角化是一种用于显示特定域不可归纳的交互机器具有不可预测的可能行为，因此是哥德尔不完全的。良基集是可判定的，而非良基集则不是。序贯交互作用的不完备性可以通过证明非良基集不能表示为良基集来直接证明哥德尔交互模型的不完备性比算术的不完备性更容易证明，因为交互模型比递归可积集更强的不可积。线性逻辑[Gi]为二人游戏[Ab]提供了一种基于双模拟的交互语义，比可计算函数更细粒度在[Ab]中，它被描述为交互的但事实上，它通过在函数的指称语义之上构建“二阶”操作语义而超越了传统语义 我们猜想，线性逻辑是完整的顺序相互作用的意义上说，它可以表示任何SIM的行为，并提供了一个模型，非良基集理论。然而，探索线性逻辑和非良基集合论之间的联系超出了本文的范围。我们进一步推测，MIM的多流行为不能用非良基集合或线性逻辑来表达，并且对于每个MIM，都有一个一致的集合论的共归纳公理化规范来表达它的行为。这表明了丘奇-图灵命题对一般交互行为的以下扩展。共归纳丘奇-图灵命题：公理集合论可表达的共归纳可具体化的概念对应于有限计算代理可表达的计算的直观概念在[We3]中，MIM行为与量子理论的非确定性有关，并且共归纳规范被扩展到“隐藏变量”之外，以隐藏导致非确定性行为的活动接口。然而，进一步elab-oration的共归纳丘奇-图灵命题超出了本文的范围。这篇论文可以表述为一个关于共归纳计算的完备性论文。我们的三个教会式论文中的每一个都可以被看作是关于通过计算的形式概念表征直觉的完备性结果，而逐渐增强的论文的层次结构决定了较弱论文的不完备性结果，作为形式或概念的表达15更强命题的直观语义。哥德尔把他在数学上的成功归功于他在大学早期就形成的对数学对象独立实在性的柏拉图式信念。他证明整数的算术不能形式化的动机是他对“哲学实在论”的信仰但哥德尔隐藏了他的柏拉图主义（现实主义）信仰，使用柏拉图主义原则作为研究的基础，而不是作为分析的主题5.3从共归纳到实在论本体论非良基集合可以比良基集合建模更大类的对象、情形和计算问题，因为ZFA的公理比ZFC的公理承认更大类集合的数学范式的存在性（逻辑上）力量决定了其模型的表达性.数学存在的问题是罗素试图将数学还原为逻辑、布劳威尔的直觉主义、希尔伯特的形式主义和哥德尔的不完备结果的核心逻辑学家不愿意接受基于循环推理的共归纳模型，因为他们无法区分循环推理的不一致和一致形式，追随罗素对集合论悖论的过度反应[BM]。另一个将合归纳思维排除在主流数学之外的原因是，以布劳威尔的直觉主义和希尔伯特的形式主义为代表的构造性数学对逻辑的限制虽然希尔伯特原则上接受柏拉图的立场，即（形式主义的）一致性意味着（模型的）存在，但他将形式主义限制在归纳定义和推理上，排除了循环推理的一致和不一致形式。当哥德尔通过对角化证明算术的不完备性时，算术的真实断言不能被归纳定义，主流数学界接受不完备性是形式主义数学的绝对不可能结果，而不是归纳推理的弱点的相对结果。芬斯勒在芬斯勒受康托实数模型的影响，得出了这样一个逻辑结论：概念的存在独立于表达它们的形式主义。 他超越了希尔伯特的形式主义在应用的原则“一致性意味着存在”，接受- ing存在的一致的概念集独立于他们是否正式。在20世纪20年代的基础性讨论之后的60年，非良基集合论对交互式计算建模的发现证实了这样一种观点，即概念上一致的可能世界独立于它们的可形式化性或可构造性而16→→→我们称这种观点为实在论的数学本体论。现实主义传统上指的是这样一种模型，即模型对象的存在与它们是否被感知无关[EB]。以此类推，正如我们所定义的那样，数学实在论给予对象一种独立于它们是否被形式化的存在数学中的实在论和物理学和计算中的唯象主义都赋予被建模的对象独立的存在性，为经验计算机科学提供了基础，也为唯象主义的跨学科方法论提供了基础。直觉主义、归纳形式主义和实在论可以根据它们对数学对象的存在的承诺程度来分类，体现了越来越强的本体论承诺形式，可以逐步模拟更大类的应用。直觉主义（布劳威尔）：存在需要（归纳）可建构性（最小本体论）归纳形式主义（希尔伯特）：（归纳）形式系统的一致性意味着模型现实主义（康托尔，芬斯勒）：一致性（具体化）意味着存在（最大本体论）有限主体的共归纳模型是实在论的，因为它们既可以模拟不可量化的实数域，也可以模拟像真实世界一样的物理域。他们将数学和物理意义的术语“真正的它们决定了本体论范式从建构主义到现实主义的转变由最小固定点指定的构造性归纳定义的本体论比由最大固定点指定的实在论共归纳定义的本体论弱最大固定点允许有限主体的交互和时间依赖行为：它们为现实主义本体论提供了希尔伯特的矛盾声称接受现实主义原则“consis- tency意味着存在”（CE），但限制其应用于归纳形式主义是哥德尔不完全性的主要原因。费弗曼[Fe]没有充分解释哥德尔令人惊讶地反对（C → E）的理由。我们的分析表明，这可能源于这样一个事实，即C→E与哥德尔对客观数学的信仰和他对数学的接受是不相容的他的老师希尔伯特的归纳形式主义。哥德尔令C E、归纳形式主义和客观数学不可能同时为真。C E、归纳模型和客观数学是数学世界观的三个不同的起点，它们是不相容的。希尔伯特，哥德尔，康托（芬斯勒）每个接受两个和拒绝其中之一17→→→→→→原则希尔伯特：CE+归纳形式主义;与客观数学不一致-哥德尔哥德尔：客观数学+归纳形式主义;解释哥德尔康托，芬斯勒：CE+客观数学;意味着拒绝归纳形式主义希尔伯特现实主义，共归纳范式的数学对应康托和芬斯勒的信念，在CE和客观的哥德尔如果哥德尔接受C→E，并与芬斯勒一起认识到这意味着接受共归纳推理，归纳推理的不完全性结果将成为共归纳推理的完全性结果，逻辑的演化可能是非常不同的。6交互式软件技术计算机体系结构从大型机到个人计算机和网络，软件工程从面向过程到面向对象和基于组件的系统，以及人工智能从基于逻辑到面向代理和分布式系统的演变都遵循着并行的路径[We1]。根据下面的胶囊历史，20世纪50年代到70年代关注于大型机算法技术的开发和改进，顺序交互成为20世纪80年代的主导技术，而分布式交互成为20世纪90年代的主导技术：20世纪5020世纪7020世纪8020世纪90从机器语言到面向过程的语言的转变仅仅涉及动作粒度的变化，而从过程语言到对象语言的转变则更为根本，涉及算法的定性扩展18随时间服务（QoS）面向对象编程结构化面向对象程序设计大规模涌现行为编程面向Agent的（分布式）人工智能开放系统经验计算机科学输入输出转换面向过程的编程结构化编程组合行为小程序设计AI封闭系统中的逻辑和搜索算法计算机科学互动概念Fig. 1. 从算法到交互的to interaction互动.从顺序交互扩展到分布式交互，需要计算模型的进一步基本范式转变SIM表示从算法到顺序交互架构的转变，而 MIM表示进一步向分布式交互的转变。图1展示了从算法到交互的扩展，涉及多个维度。左栏中的每一个算法概念都被右栏中更具表现力的交互概念所此外，每个右手概念都有一个单智能体（顺序）和一个多智能体（分布式）形式，其表现力由SIM和MIM指定。SIM和MIM的领域独立通用性既有利于提供统一的建模框架，也有缺点，即通用模型对特定领域的应用程序几乎没有指导从计算主要关注输入输出转换的观点到计算系统随时间提供服务的观点的转变出现在许多不同的上下文中随着时间的推移，服务由交互模型来具体化，而这些交互模型不能被简化为出租或TM，也不能用出租或TM来表达。算法是交互系统生命周期中与时间无关的（瞬时）事件。算法复杂度的一维定量性能度量逐渐转变为服务质量（QoS）的多维定性性能度量，这是数据库和人机交互领域日益关注的焦点。过程和对象都决定了资源的提供者和客户端之间的契约，但对象为客户端提供了更丰富的服务，这些服务无法通过算法指定的过程来表达算法就像销售合同，保证每一个输入都有一个输出，而对象就像婚姻合同，描述随着时间的推移正在进行的服务合同一个对象与它的客户的契约规定了它在对象的生命周期（直到死亡将我们分开）中所有偶然的相互作用（疾病和健康）的行为。婚姻合同不能简化为买卖合同的民间智慧，在计算上是通过不能简化为算法的交互来表达的虽然基于对象的编程已经成为一种主导技术，但它的基础仍然不稳固。每个人都在谈论它，但没有人知道它是什么。“Knowing what it is” hasproved elusive because of the implicit19“它是什么”必须用算法来定义。交互式模型具有解放性的效果，它提供了一个比算法更广泛的框架来定义基于对象的软件技术甚至比基于对象的技术更不成熟：它是基于互操作性、协调模型、模式理论和万维网的技术了解它是什么反过来又需要从顺序的基于对象的模型中解放出来结构化编程[Di]被证明作为程序结构的模型太弱了，因为向面向对象编程的过渡使得基于组合算法和while语句的过程式结构化编程对象的行为不能用其组件的行为动作（动词）的结构化编程可以通过函数组合进行形式定义，而对象（名词）的结构化编程则通过没有组合形式规范的设计模式进行建模[GHJV]。因此，研究构件组装的设计模式方法是一门艺术而不是一门科学。组合性是程序形式易处理性的一个理想属性，这导致了函数和逻辑编程作为计算基础的倡导。但它限制了表现力，因为它要求整体作为其部分的总和来表达。实际的面向对象程序和计算机网络表现出非组合的涌现行为。在形式化和可表达性之间存在着内在的权衡，这显然是由组合性的表达限制所带来的在20世纪60年代，gotos被认为对形式化有害的论点大规模编程（PIL）不是由大小决定的，因为由一百万条加法指令组成的程序不是PIL。PIL是交互式编程的同义词，它与小型编程有着质的区别，就像交互式程序与算法有着质的区别一样。随着时间的推移提供服务的嵌入式和反应式系统是PIL，而非交互式问题解决不是PIL，即使算法很复杂，程序很大。人工智能从逻辑和搜索到面向代理的编程的演变与软件工程的演变非常相似这种范式转变在对智能体[Ag]、交互式规划和控制[DW]的研究中以及在根据智能体[RN]系统地重新制定人工智能人工智能比软件工程更清楚地表明，推理是建模的不充分基础。虽然逻辑是计算的一种形式，但计算不能完全归结为逻辑。20世纪80年代的第五代计算项目旨在为通用计算提供一个基于逻辑的框架，其目标在原则上是无法实现的20开放系统可以精确地定义为交互系统：交互模型提供了一种工具，用于对开放形式进行分类，并分析开放系统的行为。 经验计算机科学同样可以被精确地定义为对交互系统的研究[We3]。引用[Ab]萨姆森·艾布拉姆斯基互动的语义Semantics and Logic ofComputation，ed.A. Pitts和P.Dibyer，Cambridge，1997.[Ac]彼得·阿采尔。非良基集。CSLI讲座笔记#14，斯坦福，1988年。[Ag]菲尔·阿格雷互动和代理的计算研究。公司简介情报局，1995年1月。[BM]乔恩·巴怀斯和劳伦斯·莫斯恶性循环CSLI Lecture Notes #60，CambridgeUniversity Press，1996.[CW]卢卡卡尔代利彼得·韦格纳关于理解类型、数据抽象和多态性。计算机调查，1985年12月。[De]迈克尔·德特勒夫森 20世纪的数学哲学在20世纪S. Shanker，1996年。[Di]Edsger Dijkstra 程序设计的学科，Prentice-Hall，1976年。[DW]托马斯 院长 和迈克尔·韦尔曼《规划与控制》，MorganKaufman，1991。[EB]大英百科全书，关于现实主义的文章。[Fe]所罗门·费弗曼库尔特·哥德尔《信念与谨慎》在哥德尔[Fi]保罗·芬斯勒Finsler Set Theory：Platonism and Circularity，Eds. David Booth和Renatus Ziegler，Birkhauser，1996年。[GHJV]Er ichGamm a，Ric h ardHelm，RalphJ ohns on，andJ ohnVliss id es.DesignPatterns ： Elements of Reusable Object-Oriented Software ， Addison-Wesley，1994。[Gi]