计算机科学哲学

　　计算机科学哲学关注计算机科学学科内部以及软件开发实践及其商业和工业部署中出现的本体论和方法论问题。更具体地说，计算机科学哲学考虑了计算系统的本体论和认识论，重点关注与其规范、编程、实现、验证和测试相关的问题。计算机程序的复杂性确保了计算机科学哲学提出的许多概念性问题在数学哲学、经验科学哲学和技术哲学都有相关性。。我们将在第15集中对这些主题进行分析，以反映计算系统本体的分层性质；然后，我们将在第68集中讨论与他们的方法论相关的主题。1。计算系统1。1软件和硬件1。2抽象层次的方法2。意图和规格2。1意图2。2定义和规格2。3规格与功能3。算法3。1经典方法3。2正式方法3。3非正式途径4。程序4。1作为理论的程序4。2作为技术工件的程序4。3程序及其与世界的关系5。实施5。1作为语义解释的实现5。2作为关系规范工件的实现5。3LoA的实施5。4物理计算6。验证6。1模型与理论6。2测试和实验6。3说明7。正确性7。1数学正确性7。2物理正确性7。3错误计算8。计算机科学的认识论地位8。1作为数学学科的计算机科学8。2计算机科学作为一门工程学科8。3计算机科学作为一门科学学科1。计算系统
　　计算系统在日常生活中很普遍。它们的设计、开发和分析是计算机科学学科的适当研究对象。计算机科学哲学将它们视为理论分析的对象。它的第一个目标是定义这样的系统，即开发计算系统的本体。文献提供了关于该主题的两种主要方法。第一个理解由软件和硬件的不同本体定义的计算系统，通常被视为它们的基本组件。一种不同的方法将计算系统视为包括围绕软件硬件二分法的其他几个元素：在第二种观点下，计算系统是基于抽象层次的层次结构定义的，在这种层次结构的底部安排硬件级别，向上扩展到设计元素，向下扩展到包括用户。下面我们将介绍这两种方法。1。1软件和硬件
　　通常，计算系统被视为由两个本体论不同的实体组成：软件和硬件。算法、源代码和程序属于第一类抽象实体；微处理器、硬盘驱动器和计算机器是具体的物理实体。
　　Moore（1978）认为这种二元性是计算机科学的三个神话之一，因为软件硬件二分法具有实用意义，但不是本体论意义。计算机程序作为计算机可以执行的指令集，可以在符号级别作为编码指令进行检查，也可以在物理级别作为存储在物理介质中的指令集进行检查。摩尔强调，没有任何程序作为纯粹的抽象实体存在，即没有物理实现（闪存驱动器、服务器上的硬盘，甚至是一张纸）。早期的程序甚至是直接硬连线的，在计算机时代开始时，程序只包含物理杠杆的模式。通过软件硬件对立，人们通常将软件标识为程序的符号级别，和具有相应物理级别的硬件。然而，这种区别只能在实用性上证明是合理的，因为它划定了开发人员的不同任务。对于他们来说，软件可能由算法和实现它们的源代码提供，而硬件由机器代码和能够执行它的微处理器提供。相比之下，实现硬连线程序的工程师可能倾向于将软件称为计算机的许多物理部分。换句话说，对一个专业人士来说算作软件的东西，对于另一位专业人士来说可能算作硬件。而硬件由机器代码和能够执行它的微处理器给出。相比之下，实现硬连线程序的工程师可能倾向于将软件称为计算机的许多物理部分。换句话说，对于一个专业人士来说算作软件的东西，对于另一位专业人士来说可能算作硬件。而硬件由机器代码和能够执行它的微处理器给出。相比之下，实现硬连线程序的工程师可能倾向于将软件称为计算机的许多物理部分。换句话说，对于一个专业人士来说算作软件的东西，对于另一位专业人士来说可能算作硬件。
　　Suber（1988）更进一步，坚持认为硬件是一种软件。软件被定义为任何易于读取和执行的模式：一旦意识到所有物理对象都显示模式，人们就被迫接受硬件作为物理对象也是软件的结论。Suber将模式定义为任何确定的结构，而不是狭义的需要某种递归、规律性或对称性的结构（1988，90），并认为任何这样的结构确实可以被阅读和执行：对于任何确定的模式，意义是相关联的，总是有可能构思出赋予意义的句法和语义，从而使模式成为可执行程序。
　　Colburn（1999，2000）在将软件和硬件分开的同时，强调前者具有双重性质，它是一种既抽象又具体的具体抽象。在定义软件时，需要同时参考描述媒介，即用于表达算法的语言，以及执行媒介，即构成硬件的电路。虽然软件总是具体的，因为在某些物理介质中没有没有具体化的软件，但它仍然是抽象的，因为程序员在他们的活动中不考虑实现机器：他们宁愿开发可由任何机器执行的程序。这方面被Colburn（1999）称为内容的放大，它将计算机科学中的抽象定义为内容的抽象：内容被放大而不是被删除，
　　Irmak（2012）批评Colburn（1999，2000）提出的软件的双重性质。他将抽象实体理解为缺乏时空特性的实体，而具体意味着具有这些特性。因此，将软件定义为具体的抽象意味着软件具有相互矛盾的属性。软件确实具有时间属性：作为人类创造的对象，它一旦构思和实现就在某个时间开始存在；它可以在随后的某个时间不复存在。当所有副本都被销毁，他们的作者去世并且没有其他人记得各自的算法时，软件就不复存在了。作为人类创造的对象，软件是一种人工制品。然而，软件缺乏空间属性，因为它不能被识别为它的任何具体实现。如上所述，销毁给定软件的所有物理副本并不意味着特定软件不复存在，也不会出于同样的原因删除以某种高级语言实现软件算法的所有文本。因此，软件是一个具有时间属性的抽象实体。由于这些原因，Irmak（2010）将软件定义为抽象的神器。
　　Duncan（2011）指出，与涉及简单抽象具体二分法的本体论相比，区分软件与硬件需要更精细的本体论。Duncan（2017）的目标是通过专注于Turner（2011）的规范概念来提供这样一个本体论，即为程序提供正确性条件的表达式（参见2）。Duncan（2017）强调，程序还可以作为执行机器的规范，这意味着程序指定了机器需要执行的所有正确行为。如果机器的行为与程序不一致，则称该机器出现故障，同样，根据其规范不正确的程序被称为有缺陷或包含错误。定义区分软件硬件所必需的另一个本体论类别是人工制品，Duncan（2017）将其定义为一个物理的、时空的实体，该实体的构建是为了履行某些功能，因此有一个社区认可神器作为服务于该目的。那说，软件被定义为以某种编程语言编码的一组指令，作为能够读取这些指令的工件的规范；硬件被定义为一个工件，其功能是执行指定的计算。1。2抽象层次的方法
　　如上所示，软件和硬件之间的区别并不明显。计算系统的不同本体论方法依赖于抽象的作用。抽象是计算机科学中的一个关键元素，它有许多不同的形式。GoguenBurstall（1985）描述了这种变化中的一些，下面的例子就是其中的例子。通过命名文本和参数，可以在编程期间重复代码，这种做法称为过程抽象。该操作已在演算的抽象化运作正式的基础上（见的入门演算）并且它允许一种称为多态性的正式机制（Hankin2004）。另一个例子是类型化，这是函数式编程的典型特征，它为语言的句法构造函数提供了一个表达系统。或者，在面向对象的设计中，模式（Gamma等人，1994年）是从软件系统中常见的结构中抽象出来的，用作对象实现与其规范之间的接口。
　　所有这些例子在抽象层次（以下称为LoA）中共享一个基本方法，也用于数学（Mitchelmore和White2004）和哲学（Floridi2008）。数学中的抽象在对越来越抽象概念的永无止境的搜索中相互叠加。因此，抽象是自包含的：抽象的数学对象仅从定义它的系统中获取其意义，唯一的限制是新对象在一致的系统中相互关联，无需参考即可操作先前的或外在的意义。有些人认为，至少在这方面，计算机科学中的抽象与数学中的抽象有着根本的不同：计算抽象必须留下实现痕迹，这意味着信息被隐藏但不会被破坏（ColburnShute2007）。在一个LoA中被忽略的任何细节都不能被较低的LoA之一忽略：例如，程序员不必担心与特定变量关联的内存中的精确位置，但需要虚拟机来处理所有内存分配。这种对不同层次抽象的依赖反映在计算系统的属性上，即依赖于实现的存在：例如，即使类隐藏了它们方法的细节，它们也必须有实现。因此，计算抽象既保留了抽象的伪装，又保留了实现。在一个LoA中被忽略的任何细节都不能被较低的LoA之一忽略：例如，程序员不必担心与特定变量关联的内存中的精确位置，但需要虚拟机来处理所有内存分配。这种对不同层次抽象的依赖反映在计算系统的属性上，即依赖于实现的存在：例如，即使类隐藏了它们方法的细节，它们也必须有实现。因此，计算抽象既保留了抽象的伪装，又保留了实现。在一个LoA中被忽略的任何细节都不能被较低的LoA之一忽略：例如，程序员不必担心与特定变量关联的内存中的精确位置，但需要虚拟机来处理所有内存分配。这种对不同层次抽象的依赖反映在计算系统的属性上，即依赖于实现的存在：例如，即使类隐藏了它们方法的细节，它们也必须有实现。因此，计算抽象既保留了抽象的伪装，又保留了实现。这种对不同层次抽象的依赖反映在计算系统的属性上，即依赖于实现的存在：例如，即使类隐藏了它们方法的细节，它们也必须有实现。因此，计算抽象既保留了抽象的伪装，又保留了实现。这种对不同层次抽象的依赖反映在计算系统的属性上，即依赖于实现的存在：例如，即使类隐藏了它们方法的细节，它们也必须有实现。因此，计算抽象既保留了抽象伪装，又保留了实现。
　　Primiero（2016）设计了用于数字计算系统本体的LoA的完整公式，包括：意图规格算法高级编程语言指令汇编机器代码操作执行
　　意图是定义要解决的计算问题的认知行为：它制定了创建计算过程以执行特定任务的请求。此类请求通常由客户、用户和其他涉及给定软件开发项目的利益相关者提供。规范是解决手头计算问题所必需的一组需求的公式化：它涉及通过称为需求获取的过程对软件必须执行的操作的可能形式的确定。算法表示为所提出的计算问题提供解决方案的过程，该过程必须满足规范的要求。高级编程语言（如C、Java或Python）指令构成了所提出算法的语言实现，通常称为源代码，它们可以被训练有素的程序员理解，但不能由机器直接执行。用高级语言编码的指令被编译器编译，即翻译成汇编代码，然后在机器代码操作中组装，由处理器执行。最后，执行LoA是运行软件的物理层，即执行指令的计算机架构的物理层。
　　根据这种观点，孤立的LoA不能定义计算系统是什么，也不能确定如何区分软件和硬件。计算系统是由整个抽象层次结构定义的；每个LoA本身都表达了与实现相关的语义级别，无论是语言的还是物理的。2。意图和规格
　　意图是指计算系统之外的一种认知状态，它表达了要解决的计算问题的公式化。规范描述了要开发的计算系统必须完成的功能。虽然意图本身并没有在计算机科学哲学中引起具体的哲学争议，但出现了与规范是什么及其与意图的关系的定义相关的问题。2。1意图
　　意图阐明了确定计算系统是否合适（即正确，参见第7节）的标准，因此它被视为适合该问题的计算系统的第一个LoA。例如，客户和用户可能需要一款能够过滤来自呼叫中心的烦人电话的智能手机应用程序；此类请求构成了开发能够执行此类任务的计算系统的意向书。在非原始系统的软件开发过程中，意图通常是通过诸如头脑风暴、调查、原型设计甚至焦点小组（Clarke和Moreira1999）等技术来收集的，旨在定义各种利益相关者意图的结构化集合。在本LoA中，没有提及如何解决计算问题，但只是问题的描述是必须解决的问题是提供。
　　在当代文学中，至少自Anscombe（1963）以来，意图一直是哲学探究的对象。哲学家们已经研究了执行行为的意图（戴维森1963年）、未来做某事的意图（戴维森1978年）和有意的行为（Anscombe1963年、拜尔1970年、费雷罗2017年）。出现的问题涉及三种意图中的哪一种是主要的，它们如何连接，意图与信念之间的关系，意图是否是或预设特定的心理状态，以及意图是否作为行动的原因（见意图条目）。更正式的问题涉及具有不一致意图但被认为是理性的代理的机会（Bratman1987，Duijf等人，2019）。
　　作为计算系统本体中第一个LoA的角色，意图当然可以被认为是对未来的意图，因为它们表达了构建能够执行某些所需计算任务的系统的目标。如上所述，由于意图将自己局限于要解决的计算问题的定义，而不指定其计算解决方案，因此它们的本体论和认识论分析与哲学文献中提到的那些没有区别。换句话说，在定义计算系统的意图中没有什么特别的计算值得在计算机科学哲学中单独处理。这里重要的是意图和规范之间的关系，因为意图为规范提供了正确性标准；2。2定义和规格
　　再次考虑呼叫过滤应用程序的示例；规范可能要求创建与呼叫中心相关的电话号码黑名单；每n天更新一次列表；来电时查看号码是否在黑名单中；与呼叫管理系统通信，在肯定回答的情况下不允许来电，在否定回答的情况下允许呼叫。
　　后者是一个成熟的规范，虽然是用自然语言表达的。规范通常以自然语言提出，以更接近利益相关者的意图，然后才以适当的正式语言形式化。规范可以通过诸如UML（Fowler2003）之类的图形语言或诸如TPL（Turner2009a）和VDM（Jones1990）之类的更正式的语言来表达，使用谓词逻辑，或Z（WoodcockandDavies1996），侧重于集合论。例如，类型谓词逻辑（TPL）使用谓词逻辑公式来表达计算系统的要求，其中指定了量化变量的类型。变量类型的选择允许在更合适的抽象级别定义规范。规范是以非正式的还是正式的形式表达通常取决于所遵循的开发方法，在正式开发方法的上下文中通常首选正式的规范。此外，形式规范有助于验证计算系统的正确性（参见6）。
　　Turner（2018）询问模型和规范之间有什么区别，这两者都广泛用于计算机科学。不同之处在于Turner（2011）所说的有意立场：模型描述了一个要开发的预期系统，如果两者不匹配，模型将被改进；规范规定了如何构建系统以符合预期功能，如果不匹配，则需要改进系统。模型与系统之间的匹配反映的意图之间的对应关系描述什么和规范系统在计算问题的系统必须能够解决的方面来构造确定如何系统是被构造，在该组的必要解决计算问题的要求而言，举例说明于呼叫过滤应用。用Turner（2011）的话来说，当某物被赋予对人工制品的正确性管辖权时，它就是一个规范：规范为计算系统提供了正确性标准。因此，当计算系统符合它们的规范时，即当它们按照规范运行时，它们就是正确的。相反，它们提供了故障标准（7。3）：当计算系统的行为与其规格不一致时，它就会出现故障。Turner（2011）小心地注意到，这样的规格定义是一种理想化：规格本身在某些情况下会被修改，例如当指定的计算系统由于物理定律限制或成本限制而无法实现时，或者当结果证明高级规范不是客户和用户意图的正确形式化。
　　更一般地说，正确性问题不仅涉及规范，还涉及定义计算系统的任意两个LoA，下一小节将讨论。2。3规格与功能
　　完全实施和构建的计算系统是技术工件，即以实现特定功能为明确目标而设计和实施的人造系统（Kroes2012）。如此定义的技术制品包括桌子、螺丝刀、汽车、桥梁或电视，它们不同于非人造的自然物体（例如岩石、猫或一氧化二氢分子）和不满足要求的艺术品。职能。因此，计算系统的本体属于以二元性为特征的技术工件（Meijers2000），因为它们由功能和结构属性定义（Kroes2009，另见技术哲学条目）。功能属性指定工件需要执行的功能；结构特性表达了人工制品可以执行它们的物理特性。考虑一把螺丝刀：功能属性可能包括拧紧和松开的功能；结构特性可以参考一块能够插入螺钉头部的金属和一个允许顺时针和逆时针运动的塑料手柄。功能可以通过它们的结构对应物以多种方式实现。例如，螺丝刀的功能可以通过全金属螺丝刀来实现，也可以通过结构特性截然不同的电动螺丝刀来实现。
　　以许多不同LoAs为特征的计算系统的分层本体似乎扩展了定义技术工件的双重本体（Floridietal。2015）。Turner（2018）认为计算系统仍然是（Kroes2009，2012）意义上的人工制品，因为每个LoA是较低LoA的功能级别和较高LoA的结构级别：意图表达了系统必须实现并由规范实现的功能；规范起功能作用，详细说明软件必须实现的具体功能，它是通过算法实现的，它的结构层次；算法表示高级语言程序，其结构层次，必须实现的程序；高级语言中的指令定义了机器语言代码的功能特性，实现了它们；机器码，最后表达的是执行层实现的功能属性，即表达物理结构属性。
　　根据Turner（2018）的说法，结构层次不一定是物理层次，抽象工件的概念在计算机科学中成立。出于这个原因，Turner（2011）开始将高级语言程序本身定义为技术工件，因为它们构成了一个结构级别的实现规范作为它们的功能级别（参见第4。2节）。
　　第一结果是每个协议书表达什么函数来完成可以通过潜在的结构的水平表达多个来实现如何这些函数完成：一个预定的功能可以通过多种方式的规范来实现，由规范表达的计算问题具有多种不同算法的解决方案，这些算法对于某些重要属性可能有所不同，但都同样有效（参见第3节）；一个算法可以在不同的程序中实现，每个程序都用不同的高级编程语言编写，都表达相同的程序是否实现相同的算法（AngiusandPrimiero2019）；源代码可以用多种机器语言编译，采用不同的ISA（指令集架构）；可执行代码可以在多台机器上安装和运行（前提是这些机器共享相同的ISA）。
　　第二个结果是，作为功能级别的每个LoA都为较低级别提供了正确性标准（Primiero2020）。不仅仅是在实现级别，从规范到执行的任何LoA都需要正确性，并且故障的原因可能位于未正确实现其正确功能级别的任何LoA（参见7。3和Fresco，Primiero（2013））。根据Turner（2018）的说法，尽管难以验证其正确性，但可以说规范级别就意图而言是正确的或不正确的。任何非物理层的正确性都可以通过形式验证在数学上验证，执行物理层可以通过测试经验验证（6）。验证与客户意图相关的规范的正确性将需要访问相关代理的心理状态。
　　后一个问题涉及更普遍的问题，即确定工件如何拥有功能，以及结构属性与代理的意图相关的含义。这个问题在生物学哲学和认知科学中也是众所周知的，并且已经提出了两个主要理论作为解决方案。根据函数因果论（Cummins1975），功能是由人工制品的物理能力决定的：例如，心脏收缩和扩张的物理能力决定了它在循环系统中泵血的功能。然而，这个理论在应用于技术工件时面临着严重的问题。首先，它可以防止定义正确性和故障（Kroes2010）：假设我们智能手机上安装的呼叫过滤应用程序开始禁止来自我们手机通讯录中的联系人的呼叫；根据函数的因果理论，这将是应用程序的一个新功能。其次，该理论没有将预期功能与副作用区分开来（Turner2011）：如果长时间通话，我们的智能手机肯定会开始发热；但是，这不是客户或开发人员想要的功能。根据意向性功能理论（McLaughlin2001，Searle1995），由设计者或用户固定的功能是预期的工件之一，并且选择工件的结构特性以便能够实现它。该理论能够解释正确性和故障，并将副作用与预期功能区分开来。然而，它并没有说明函数实际驻留在何处，无论是在工件中还是在代理的头脑中。在前一种情况下，人们又回到了人工制品如何拥有功能的问题。在后一种情况下，需要进一步解释精神状态如何与人工制品的物理特性相关（Kroes2010）。Turner（2018）认为，函数的因果理论和意向理论背后的直觉对于理解计算系统中函数和结构之间的关系很有用，并建议将这两种理论合二为一。一方面，没有实现就没有功能；另一方面，没有客户、开发人员和用户就没有意图。3。算法
　　尽管自古以来就广为人知并被广泛使用，但定义算法是什么的问题仍然存在（Vardi2012）。算法一词源于9世纪波斯数学家AbJafarMuammadibnMsalKhwrizm的名字，谁提供了使用阿拉伯数字进行算术运算的规则。实际上，计算乘法或除法等基本算术运算所遵循的规则是算法的日常示例。其他著名的例子包括使用罗盘和直尺平分角度的规则，或用于计算最大公约数的欧几里德算法。直观地说，算法是一组允许完成给定任务的指令。尽管有这种古老的数学传统，但只有现代逻辑和哲学反思提出了为算法提供定义的任务，这与20世纪初数学的基础危机有关（参见数学哲学条目）。的概念有效的可计算性源于逻辑研究，它为算法的直观概念提供了一些形式上的对应物，并催生了计算理论。从那时起，算法的不同定义被提出，从正式到非正式的方法，如下一节所述。3。1经典方法
　　Markov（1954）首次将算法精确定义为确定的、适用的和有效的计算过程。如果所涉及的指令足够精确，不允许在其执行中进行任何任意选择，则确定计算过程。（人类或人工）计算机绝不能不确定下一步要执行的步骤。算法适用于马尔可夫，因为它们适用于输入类别（基本算术运算的自然数）而不是单个输入（特定自然数）。Markov（1954：1）定义有效性作为算法获得某个结果的趋势。换句话说，算法是有效的，因为它最终会产生计算问题的答案。
　　Kleene（1967）将有限性指定为一个更重要的特性：算法是一个过程，它可以通过一组有限的指令来描述，并且需要有限数量的步骤来提供计算问题的答案。作为一个反例，考虑一个由有限步数定义的while循环，但由于循环中的条件总是满足，它永远运行。说明也应符合机械要求执行，也就是说，机器不需要任何洞察力来跟随它们。遵循马尔可夫的可确定性和强化有效性，Kleene（1967）额外指定指令应该能够识别计算问题的解决方案已经实现，并停止计算。
　　Knuth（1973）回顾并深化了Markov（1954）和Kleene（1967）的分析，指出：除了仅仅是一组有限的规则，它给出了解决特定类型问题的一系列操作，算法还有五个重要的特征：
　　有限性。算法必须始终在有限步数后终止。〔〕确定性。算法的每一步都必须精确定义；必须为每个案件严格而明确地规定要采取的行动。〔〕输入。一个算法有零个或多个输入。〔〕输出。一个算法有零个或多个输出。〔〕效力。一个算法通常也被认为是有效的，因为它的操作都必须足够基本，原则上它们可以由使用铅笔和纸的人在有限的时间内准确地完成。（Knuth1973：46）〔〕
　　正如在Kleene（1967）中一样，有限性影响指令的数量和实现的计算步骤的数量。与马尔可夫的确定性一样，Knuth的确定性原则要求明确指定每个连续的计算步骤。此外，Knuth（1973）更明确地要求算法具有（可能为空的）输入和输出。对于没有输入或输出的算法，Knuth可能指的是使用内部存储的数据作为输入的算法或不将数据返回给外部用户的算法（Rapaport2019，第7章，其他互联网资源）。至于有效性，除了马尔可夫求得一定结果的倾向外，Knuth还要求在有限的时间内求得结果，并且指令是原子的，即，3。2正式方法
　　Gurevich（2011）认为，一方面，不可能提供算法的正式定义，因为这个概念随着时间的推移而不断发展：考虑古代数学中使用的顺序算法是如何被并行、模拟或当前计算机科学实践中的量子算法，以及如何在不久的将来设想新的算法。另一方面，如果仅关注经典顺序算法，则可以进行形式分析。特别是，Gurevich（2000）为此类算法提供了一个公理定义。
　　任何顺序算法都可以通过满足三个公理的顺序抽象状态机来模拟：的顺序时间假设关联的任何算法阿一组状态S（A），一组初始状态I（A）的子集S（A），和从地图S（A）到S（A）一种A的步变换。状态是运行算法的快照描述。的运行阿是状态的（可能是无限的）序列，从一些初始状态开始，使得存在从一个状态一步法转化到其在序列中的继任者。Gurevich的定义并不以终止为前提。一步转换不需要是原子的，但它们可以由一组有界的原子操作组成。根据抽象状态公设，S（A）中的状态是一阶结构，通常在数理逻辑中定义；换句话说，状态为一阶语句提供了语义。最后，有界探索假设指出，鉴于两国X和的一个总有一组牛逼的术语，例如，当X和重合在牛逼，一组更新的X相当于设定的更新。X和以上重合时，对于每一个术语吨在，评价吨中X相同的评价吨在。这允许算法A仅探索与T中的项相关的那些状态部分。
　　Moschovakis（2001）反对抽象机器没有完全捕捉到算法的直观概念。给定一个在自然数上定义的一般递归函数f：，通常有许多不同的算法来计算它；基本的、与实现无关的属性不是由抽象机器捕获的，而是由递归方程系统捕获的。考虑排序列表的算法归并排序；归并排序有许多不同的抽象机器，问题是选择哪一个作为归并排序算法。该归并算法是指定所涉及函数的递归方程系统，而归并排序过程的抽象机器是同一算法的不同实现。Moschovakis的形式化分析提出了两个问题：同一算法的不同实现应该是等价的实现，而算法实现之间的等价关系要形式化定义。此外，由递归方程系统形式化的算法的直观概念究竟是什么还有待澄清。
　　Primiero（2020）提出了在三个不同抽象层次上对算法本质的解读。在LoA非常高的情况下，算法可以从它们描述的过程中抽象出来定义，允许许多不同的状态和转换集。在这种情况下，LoA算法可以理解为非正式规范，即过程P的非正式描述。在较低的LoA中，算法指定解决给定计算问题所需的指令；换句话说，它们指定了一个程序。因此，算法可以定义为过程，或者用某种给定的形式语言L描述如何执行过程P。。算法的许多重要属性，包括与复杂性类和数据结构相关的属性，无法在程序LoA中确定，而是需要参考实现该程序的抽象机器。在底层LoA中，算法可以定义为可实现的抽象机器，即。作为对给定抽象机器M的程序P执行的形式语言L的规范。算法的三重定义允许Primiero（2020）根据模拟和互模拟的代数概念为算法提供等价关系的正式定义（Milner1973，另见Angius和Primero2018）。一种机器中号我执行程序P我实现一机多用相同的算法中号执行程序P当且仅当在抽象机解释中号我和中号处于互模拟关系。3。3非正式途径
　　Vardi（2012）强调，尽管有许多正式和非正式的定义，但对于什么是算法并没有普遍的共识。Gurevich（2000）和Moschovakis（2001）的方法甚至可以被证明在逻辑上是等效的，它们只为算法提供逻辑结构，而没有回答主要问题。Hill（2013）建议，考虑到人们对算法的直观理解，算法的非正式定义可能更有用，尤其是对于公共话语以及从业者与用户之间的交流。
　　Rapaport（2012，附录）试图总结上述算法的三个经典定义，指出：
　　一个算法（让执行者E完成目标G）是：一个过程，即语句（或规则或指令）的有限集（或序列），使得每个语句是：由有限字母表中有限数量的符号（或标记）组成并且对于E是明确的也就是说，E知道怎么做E可以做到它可以在有限的时间内完成并且，做完之后，E知道接下来要做什么哪个过程需要有限的时间（即停止），并以G完成结束。
　　Rapaport强调算法是一个过程，即采用规则或指令形式的有限语句序列。这里的有限性是通过要求指令包含来自有限字母表的有限数量的符号来表达的。
　　Hill（2016）旨在提供算法的非正式定义，从Rapaport（2012）开始：
　　算法是一种有限的、抽象的、有效的、复合的控制结构，在给定的规定下强制给定、完成给定的目的。（Hill2016：48）。
　　首先，算法是复合结构而不是原子对象，即它们由更小的单元组成，即计算步骤。正如Markov、Kleene和Knuth明确提到的，这些结构是有限且有效的。虽然这些作者没有明确提到抽象性，但Hill（2016）认为它隐含在他们的分析中。算法是抽象的，因为它们缺乏时空特性并且独立于它们的实例。它们提供控制，即带来某种从一种状态到另一种状态的变化的内容，以变量的值和随后的动作表示（第45页）。算法是强制给出的，因为它们命令状态转换以执行指定的操作。最后，算法在一些通常明确规定的条件或先决条件下运行以实现某些目的。从这个角度来看，作者认为，算法在指定特定资源下的目标时与规范不相上下。该定义允许将算法与其他复合控制结构区分开来。例如，食谱不是算法，因为它们无效；游戏也不是，它们不是强制给出的。4。程序
　　计算机程序的本体与计算系统的包含性质密切相关（参见1）。如果计算系统是基于软硬件二分法定义的，那么程序是解释前者的抽象实体，与硬件的具体性质相对。1。1中提供了此类解释的示例，包括Colburn（2000）的具体抽象定义、Irmak（2012）的抽象工件特征以及Duncan（2011）提出的作为机器规范的程序。相比之下，根据LoA层次结构对计算系统的解释，程序是算法的实现。我们参考5在这个意义上分析程序本体的实现。本节重点介绍在文献中具有重要相关性的程序的定义，即那些将程序视为理论或人工制品的观点，重点是程序与世界之间的关系问题。4。1作为理论的程序
　　程序是理论的观点可以追溯到认知科学的方法。在对人类认知过程进行模拟研究的所谓信息处理心理学（IPP）的背景下，Newell和Simon（1972）提出了模拟程序是经验理论的论点他们的模拟系统。Newell和Simon为计算机程序分配了模拟系统和模拟系统理论的作用，即运行程序的机器，以制定对模拟系统的预测。特别是，模拟程序的执行轨迹，给定要解决的特定问题，用于预测人类受试者在被要求完成相同任务时将执行的心理操作策略。如果执行轨迹与人类主体的操作策略的口头报告不匹配，则修改模拟程序提供的经验理论。根据Newell和Simon的说法，这种计算机程序的预测性使用是可比的，
　　Newell和Simon的程序即理论的观点得到了认知科学家Pylyshyn（1984）和JohnsonLaird（1988）的认同。两者都同意，与典型的理论相比，程序更擅长面对要建模的模拟过程的复杂性，迫使人们填写执行程序所需的所有细节。尽管在科学探究的某个阶段可能会提出不完整或不连贯的理论，但对于程序而言却并非如此。
　　另一方面，Moore（1978）认为程序即理论论文是计算机科学的另一个神话。由于程序只能模拟一些经验现象，它们最多只是扮演这些现象的计算模型的角色。Moore注意到，对于被承认为模型的程序，仍然需要语义函数来解释被模拟的经验系统。然而，程序是模型的观点不应被误认为程序是理论的定义：理论解释和预测模型模拟的经验现象，而程序模拟并没有提供这一点。
　　根据计算机科学家PaulThagard（1984）的说法，将程序理解为理论需要对理论有句法或语义观点（请参阅有关科学理论结构的条目）。但是程序不符合这两种观点中的任何一种。根据句法观点（Carnap1966，Hempel1970），理论是用某种定义的语言表达的句子集，能够描述目标经验系统；其中一些句子定义了理论的公理，而另一些则是表达这些系统规律性的类似定律的陈述。程序是用某种定义的编程语言编写的指令集，但是，它们不描述任何系统，只要它们是过程语言实体而不是声明性实体。为此，Rapaport（2020，参见其他互联网资源）反对过程编程语言通常可以被翻译成声明性语言，并且有一些语言，例如Prolog，可以以过程性和声明性方式进行解释。根据语义观点（Suppe1989，VanFraassen1980），理论是由一组模型引入的，定义为满足理论句子的集合论结构。然而，与Moore（1978）不同的是，Thagard（1984）否认程序模型的认识论地位：程序模拟物理系统而不满足理论定律和公理。相反，出于模拟目的，程序包括所用编程语言的实现细节，但不包括被模拟的目标系统的实现细节。程序在不满足理论定律和公理的情况下模拟物理系统。相反，出于模拟目的，程序包括所用编程语言的实现细节，但不包括被模拟的目标系统的实现细节。程序在不满足理论定律和公理的情况下模拟物理系统。相反，出于模拟目的，程序包括所用编程语言的实现细节，但不包括被模拟的目标系统的实现细节。
　　计算机科学家PeterNaur（1985）提出了一种解决程序是否是理论问题的不同方法。根据Naur的说法，编程是一个理论构建过程，并不是说程序就是理论，而是因为成功的程序的开发和生命周期要求程序员和开发人员拥有可用的程序理论。根据Ryle（2009），这里的理论被理解为科学界共享的关于某些经验现象的知识库，不一定以公理或形式表达。理论的程序在程序生命周期中是必要的，以便能够根据观察到的错误计算或对程序被要求解决的计算问题的不满意解决方案来管理程序修改请求。特别是，程序理论应该允许开发人员修改程序，以便为所涉问题提供新的解决方案。出于这个原因，Naur（1985）认为这些理论在软件开发中比文档和规范更基础。
　　对于Turner（2010，2018ch。10），编程语言是由形式语法和形式语义定义的数学对象。特别是，每个句法结构，例如赋值、条件或while循环，都由确定其句法的语法规则以及与意义相关联的语义规则定义。取决于是操作语义还是指称语义是优选的，分别根据抽象机器的操作或从状态集到状态集的数学部分函数的操作来给出意义。例如，简单的赋值语句X：乙x：E在操作语义下，与机器操作相关联你磷d一种吨电子（秒，X，v）update（s，x，v）分配变量vv解释为乙E变Xx在状态秒s。在操作语义和指称语义的情况下，程序都可以被理解为表达执行机器操作的数学理论。考虑操作语义：形式的句法规则磷，秒秒P，ss从语义上说明该程序磷P在状态下执行秒s结果是秒。s。根据Turner（2010，2018）的说法，具有操作语义的编程语言类似于操作的公理理论，其中规则为关系提供公理。4。2作为技术工件的程序
　　程序可以被理解为技术工件，因为与任何其他工件一样，编程语言是根据功能和结构属性定义的（Turner2014，2018ch。5）。（高级）编程语言的功能特性由与语言的每个句法构造相关联的语义提供。Turner（2014）指出，编程语言只有在其功能层面被隔离时，才能真正被理解为公理理论。另一方面，结构属性是根据语言的实现来指定的，但不与计算机的物理组件相关联：给定具有相关功能描述的语言的句法构造，它的结构属性由机器执行的物理操作决定，以实现手头构造的指令。例如，赋值构造X：乙x：E与表达式值的物理计算相关联乙E以及价值的放置乙E在物理位置Xx。
　　将编程语言视为技术工件的另一个要求是，它必须具备为语言实现提供正确性标准的语义。程序员通过使用语义对程序拥有正确性管辖权来证明程序的功能和结构属性。4。3程序及其与世界的关系
　　计算机程序是否是理论的问题与程序与外界的关系有关。如果程序是理论，它们就必须代表某种经验系统，程序与世界之间将直接建立语义关系。相比之下，有些人认为程序和自然系统之间的关系是由外部世界模型调节的（Colburnetal。1993，Smith1985）。特别是，Smith（1985）认为模型是对经验系统的抽象描述，在其中运行的计算系统具有充当模型模型的程序，即它们代表现实的抽象模型。在描述计算机科学中的正确性问题时，这种对程序本体的描述会派上用场（见7）：如果规范被视为需要计算系统的某些行为的模型，则程序可以被视为满足规范的模型。
　　根据一个人是否承认他们与世界的关系，可以给出两种对程序的看法（Rapaport2020，第17章，参见其他互联网资源）。根据第一种观点，程序是广泛的、外部的和语义的：它们授予对经验系统的对象和对这些对象的操作的直接引用。根据第二种观点，程序是狭义的、内部的和句法的：它们只涉及执行计算的实现机器的原子操作。Rapaport（2020，见其他互联网资源）认为程序不需要是外部的和语义的。首先，计算本身不需要是外部的：图灵机通过使用写入其磁带的数据来执行其有限表中包含的指令，并在计算产生的数据写入磁带后停止。严格来说，数据不是来自外部用户的输入和输出。此外，Knuth（1973）要求算法具有零个或多个输入和输出（参见3。1）。一个不需要输入的计算机程序可能是一个程序，例如，输出从1开始的所有质数；没有输出的程序可以是计算某个给定变量x的值而不返回存储在x中的值作为输出的程序。其次，程序不必是外部的、目的论的，即目标导向的。这种观点反对文献中的其他已知立场。Suber（1988）认为，如果不考虑目标和目的，就不可能评估计算机程序是否正确，即它是否按预期运行。正如3。3中所回忆的那样。，Hill（2016）在她的非正式定义中指出，算法可以实现在给定规定下的给定目的。（希尔2016：48）。对于这些观点，Rapaport（2020，ch。17，seeOtherInternetResource）回答说，虽然目标、目的和程序员的意图对于人类计算机理解程序可能非常有用，但它们对于人工计算机来说并不是必需的。执行程序代码指示的计算。事实上，经典方法要求算法的有效性原则（见3。1）要求，除其他属性外，算法的执行无需任何直觉。换句话说，执行自然数加法程序的机器并不理解它正在加法；同时，知道给定的程序执行加法可能有助于人类代理理解程序的代码。
　　根据这种观点，计算只涉及符号，而不涉及意义。图灵机变成了符号操纵器，它的操作不是单一的而是多种含义。如果不是通过它们的含义，即通过考虑它们执行的功能，那么如何识别两个程序是同一个程序？一个答案来自Piccini对计算及其内部语义的分析（Piccini2008，2015ch。3）：仅通过分析它们的语法和程序对其符号执行的操作，就可以将两个程序识别为相同。字符串操作的效果可以被认为是程序的内部语义。后者可以通过隔离程序代码中的子例程或方法来轻松确定，然后可用于识别程序或确定两个程序是否相同，即当它们由相同的子例程定义时。
　　然而，有人争论说，在不参考外部语义的情况下，不可能确定两个程序是否相同。Sprevak（2010）建议考虑两种加法程序，这两种程序不同于一个处理阿拉伯数字，另一个处理罗马数字的事实。这两个程序计算相同的函数，即加法，但这不能总是通过检查代码及其子程序来确定；它必须通过将内容分配给输入输出字符串，将阿拉伯数字和罗马数字解释为数字来确定。在这方面，Angius和Primiero（2018年）强调了计算机程序的身份问题与自然种类（Lowe1998）和技术工件（Carrara等人，2014年）的身份问题没有什么不同。这个问题可以通过固定一个身份标准来解决，即任何两个程序应该接受的形式关系，以便被定义为相同。Angius和Primiero（2018）展示了如何使用由两个正在检查的程序实现的两个自动机之间互模拟的过程代数关系作为这样的身份标准。互模拟允许建立实现相同功能的程序的匹配结构特性，并在模拟方面为副本提供较弱的标准。这将讨论带回到将程序作为实现的概念。我们现在转向分析后一个概念。Angius和Primiero（2018）展示了如何使用由两个正在检查的程序实现的两个自动机之间互模拟的过程代数关系作为这样的身份标准。互模拟允许建立实现相同功能的程序的匹配结构特性，并在模拟方面为副本提供较弱的标准。这将讨论带回到将程序作为实现的概念。我们现在转向分析后一个概念。Angius和Primiero（2018）展示了如何使用由两个正在检查的程序实现的两个自动机之间互模拟的过程代数关系作为这样的身份标准。互模拟允许建立实现相同功能的程序的匹配结构特性，并在模拟方面为副本提供较弱的标准。这将讨论带回到将程序作为实现的概念。我们现在转向分析后一个概念。5。实施
　　实现一词通常与计算系统的物理实现相关联，即与执行计算机程序的机器相关联。特别是，根据1。1中检查的计算系统的双重本体，在这个意义上的实现减少到结构硬件，而不是功能软件。相比之下，按照抽象级别的方法（第1。2节），实现成为定义计算系统的任何LoA与层次结构中更高级别之间的更广泛关系。因此，算法是（一组）规范的实现；用高级编程语言表达的程序可以定义为算法的实现（参见4）；汇编和机器代码指令可以看作是针对给定ISA的一组高级编程语言指令的实现；最后，执行是那些机器代码指令的物理、可观察的实现。同理，用高级语言编写的程序也是规范的实现，并且，正如双本体范式所论证的，执行是高级编程语言指令的实现。根据Turner（2018）的说法，即使是规范也可以理解为所谓意图的实现。
　　这里还有待研究的是如此定义的实现关系的性质。分析这种关系对于定义正确性的概念至关重要（第7节）。事实上，一个正确的程序就是一个算法的正确实现；正确的计算系统是一组规范的正确实现。换句话说，在这种观点下，正确性的概念与任何LoA的实现相结合：当且仅当它是其正确实现时，任何级别都可以被称为相对于上层是正确的。
　　以下三个小节检查了计算机科学文献哲学中提出的实现关系的三个主要定义。5。1作为语义解释的实现
　　Rapaport（1999，2005）提出了对计算机科学中实现概念的第一个哲学分析。他将实现I定义为在实现M的媒介中句法或抽象域A的语义解释。如果实现被理解为一个给定的LoA和计算系统的分层本体中的任何上层之间的关系，那么Rapaport的定义相应地扩展，以便任何LoA在给定的实现介质中为上层提供语义解释。水平。在这种观点下，规范提供了利益相关者在规范（正式）语言中表达的意图的语义解释，算法使用算法可以用多种语言（自然语言、伪代码、逻辑语言、函数式语言等）。实现的媒介可以是抽象的，也可以是具体的。计算机程序是算法的实现，因为前者在高级编程语言中提供了后者的句法结构的语义解释，作为其实现的媒介。程序的指令以编程语言解释算法的任务。此外，执行LoA将汇编机器代码操作的语义解释提供到由物理机器的结构属性给定的介质中。根据（Rapaport1999，2005）中的分析，执行是一种非对称关系：如果此外，执行LoA将汇编机器代码操作的语义解释提供到由物理机器的结构属性给定的介质中。根据（Rapaport1999，2005）中的分析，执行是一种非对称关系：如果此外，执行LoA将汇编机器代码操作的语义解释提供到由物理机器的结构属性给定的介质中。根据（Rapaport1999，2005）中的分析，执行是一种非对称关系：如果I是A的实现，A不能是I的实现。然而，作者认为，任何LoA既可以是句法级别，也可以是语义级别，也就是说，它可以同时扮演实现I和句法域A的角色。在高级语言中，相同的算法为规范提供语义解释。因此，抽象实现关系与计算系统的功能结构关系配对。
　　Primiero（2020）认为后一个方面是Rapaport（1999，2005）实现解释的一个主要限制：实现简化为句法级别与其语义解释之间的独特关系，并且它没有考虑所看到的计算系统的分层本体在1。2中。为了将实现的当前定义扩展到所有LoA，每次都必须将每个级别重新解释为句法或语义级别。反过来，这会对第二个困难产生影响，根据Primero（2020）的说法，作为语义解释的实施：一方面，这种方法没有考虑到不正确的实施；另一方面，对于给定的错误实现，如此定义的唯一关系只能将错误与一个句法级别相关联，排除所有其他级别作为潜在错误位置。
　　Turner（2018）旨在表明语义解释不仅不能解释错误的实现，甚至不能纠正错误的实现。第一个例子是通过将一种语言实现为另一种语言：这里的实现语言不提供已实现语言的语义解释，除非前者与为后者提供含义和正确性标准的语义相关联。这种语义将保持在实现关系的外部：虽然正确性与语义解释相关联，但实现并不总是伴随着语义解释。第二个例子是考虑一个由数组实现的抽象堆栈；同样，数组不提供堆栈的正确性标准。恰恰相反，5。2作为关系规范工件的实现
　　抽象层提供了实现关系的正确性标准这一事实促使Turner（2012，2014，2018）将实现定义为关系规范人工制品。正如第2节所述，规范对工件具有正确性管辖权，也就是说，它们规定了工件的允许行为。还记得工件既可以是抽象实体，也可以是具体实体，任何LoA都可以充当较低级别的规范角色。这相当于说规范人工制品关系能够定义跨计算系统的分层本体的任何实现关系。
　　根据规范工件关系的定义方式，Turner（2012）区分了多达三种不同的实现概念。考虑实现给定抽象机的物理机的情况。根据实现的有意概念，抽象机作为物理机的规范工作，前提是它提出了后者必须满足的所有功能要求，即它（原则上）指定了实现物理机的所有允许行为。根据扩展实现的概念，当且仅当可以建立同构将后者的状态映射到前者的状态，并且抽象机中的转换对应于实际执行（计算轨迹）时，物理机才是抽象机的正确实现。神器。最后，实现的经验概念要求物理机显示与抽象机规定的计算相匹配的计算；也就是说，正确的实施必须通过测试凭经验进行评估。
　　Primiero（2020）强调，虽然这种方法解决了正确性和错误计算的问题，因为它允许区分正确的和不正确的实现，但它仍然标识了规范级别和工件级别之间的唯一实现关系。再一次，如果允许这个帐户通过每次将任何LoA重新解释为规范或工件来涉及计算系统的分层本体，那么特纳的帐户就可以防止同时引用多个级别作为错误计算的原因：错误计算此处总是作为工件对规范的不正确实现而出现。通过将实现定义为跨所有LoA的关系，人们将能够识别多个不直接引用抽象规范的错误实现。5。3LoA的实施
　　Primiero（2020）提出的实施定义不是两个固定级别之间的关系，而是允许跨越任何LoA的级别。在这种观点下，实现I是LoA与抽象层次结构中更高的任何其他实例之间的实例化关系。因此，物理计算机是汇编机器代码操作的实现；通过传递性，它也可以被认为是用高级编程语言指令表达的一组指令的实例化。用高级语言表达的程序是算法的实现；但它也可以被视为一组规范的实例化。
　　这样的实现定义允许Primiero（2020）提供正确性的一般定义：一个物理计算系统是正确的，当且仅当它以任何LoA的正确实现为特征。因此，正确性和实施在任何LoA中都是耦合和定义的。功能正确性是计算系统的属性，它显示了该系统规范所需的功能。程序正确性表征了计算系统，显示了所实现的算法所预期的功能。和执行正确性被定义为能够在其体系结构上正确执行程序的系统的属性。这些形式的正确性中的每一种也可以根据满足的功能数量进行定量分类。功能高效的计算系统显示规范所需功能的最小子集；功能优化的系统能够显示这些功能的最大子集。同样，作者在程序上以及执行上都定义了高效和最优的计算系统。5。4物理计算
　　根据这个定义，实现从一个层次转移到另一个层次：一组定义计算系统的算法被实现为某种形式语言中的过程、高级语言中的指令或低级编程语言中的操作。一个有趣的问题是是否有系统，除了计算工件之外，实现这种类型的过程也被称为计算系统。换句话说，询问物理实现的性质就等于询问什么是计算系统。如果任何实现算法的系统都符合计算条件，则此类系统可以扩展到生物系统，例如大脑或细胞；物理系统，包括宇宙或其一部分；并最终适用于任何系统，称为泛计算主义的论文（有关该主题的详尽概述，请参阅Rapaport2018）。
　　传统上，计算系统旨在作为一种机械工件，它接受输入数据，根据一组指令在算法上详细说明它们，并将操纵的数据作为输出返回。例如，vonNeumann（1945，p。1）指出自动计算系统是一种（通常是高度复合的）设备，它可以执行指令来执行相当复杂的计算。这种非正式且广为接受的定义留下了一些悬而未决的问题，包括计算系统是否必须是机器，它们是否必须通过算法处理数据，以及因此计算是否必须是图灵完备的。
　　Rapaport（2018）提供了一个更明确的计算系统特征，定义为任何逻辑上等同于通用图灵机的任何物理上合理的实现。严格地说，个人计算机不是物理图灵机，但众所周知，寄存器机是图灵等价的。为了符合计算的要求，系统必须是其合理的实现，因为与物理机器相反，图灵机可以访问无限的内存空间，并且作为抽象机器，没有错误。根据Rapaport（2018）的定义，任何因此，这种物理实现是一个计算系统，包括自然系统。这就提出了什么样的自然系统能够实现图灵等效计算的问题。塞尔著名地认为，任何东西都可以是图灵机或逻辑等效模型的实现（Searle1990）。他的论点基于这样一个事实，即作为图灵机是一种句法属性，因为它完全是关于操纵0和1的标记。根据Searle的说法，句法属性不是物理系统固有的，而是由观察者分配给它们的。换句话说，系统的物理状态本质上不是计算状态：必须有观察者或用户为该状态分配计算角色。
　　Hayes（1997）反对Searle（1990）的说法，如果一切都是一个计算系统，那么作为一个计算系统的属性将变得空洞，因为所有实体都将拥有它。相反，有些实体是计算系统，有些实体不是。计算系统是那些作为输入接收并保存到内存中的模式能够自行改变的系统。换句话说，Hayes提到了这样一个事实，即存储的输入既可以是数据，也可以是指令，并且指令在执行时能够修改某些输入数据的值。如果它是纸，它就是‘神奇的纸’，上面的文字可能会自发地改变，或者新的文字出现（Hayes1997，第393页）。只有能够充当魔术纸的系统才能被认为是计算性的。
　　Piccinini（2007，2008）在他对物理计算的机械分析（Piccinini2015；另见物理系统中的计算条目）中提出了另一种不同的方法。物理计算系统是一种可以通过描述导致这些行为的计算机制来机械解释其行为的系统。机制可以通过组织起来的实体和活动来定义，以便它们从开始或设置到完成或终止条件产生定期变化（Machamer等人，2000年；参见科学中的机制条目）。计算，作为物理过程，可以理解为根据适用于所有输入字符串并依赖于输入（有时是内部状态）的一般规则从输入字符串生成输出字符串的机制（Piccinini2007，p。108）。很容易识别计算过程的设置和终止条件。任何可以通过描述底层计算机制来解释的系统都被认为是一个计算系统。对解释的关注帮助皮奇尼尼避免了塞尔林的结论，即任何系统都是一个计算系统：即使原则上可以将任何给定的实体和活动集解释为计算机制，也只需要用术语来解释某个观察到的现象计算机制的定义将被检查的系统定义为计算系统。6。验证
　　软件开发过程中的一个关键步骤是验证。这包括评估给定计算系统是否符合其设计规范的过程。在计算机行业的早期，有效性和正确性检查方法包括几种设计和构造技术，例如参见（Arif等。2018）。如今，正确性评估方法可以大致分为两大类：形式验证和测试。形式验证（MoninandHinchey2003）涉及使用数学工具证明正确性；软件测试（Ammann和Offutt2008）而是运行已实现的程序以观察执行的执行是否符合高级规范。在许多实际案例中，使用两种方法的组合（例如参见Callahan等人，1996年）。6。1模型与理论
　　正式的验证方法需要被验证的软件的表示。在定理证明中（参见vanLeeuwen1990），程序用公理系统和一组表示程序转换的前置和后置条件的推理规则来表示。然后通过从公理导出表示规范的公式来获得正确性的证明。在模型检查中（Baier和Katoen2008），程序用状态转换系统表示，其属性规范由时序逻辑公式形式化（Krger和Merz2008），并且通过深度优先实现正确性证明检查这些公式是否适用于状态转换系统的搜索算法。
　　用于正确性评估的公理系统和状态转换系统可以理解为表示工件的理论，因为它们用于预测和解释它们的未来行为。模型检查中的方法论状态转换系统可以与实证科学中的科学模型进行比较（Angius和Tamburrini2011）。例如，Kripke结构（参见Clarke等人，1999年第2章）符合Suppes（1960）将科学模型定义为集合论结构，该结构与通过目标实验收集的数据模型建立适当的映射关系经验系统（另见关于科学模型的条目）。形式验证方法中使用的Kripke结构和其他状态转换系统通常称为系统规范。它们区别于通用规范，也称为属性规范。后者指定要编码的程序必须实例化的一些必需的行为属性，而前者指定（原则上）已编码程序的所有潜在执行，从而允许对其踪迹进行算法检查（Clarke等人，1999年）。为了实现这一目标，系统规范被认为是溯因结构，假设基于程序代码和允许的状态转换的目标计算系统的潜在执行集（Angius2013b）。实际上，一旦检查了某个时间逻辑公式是否适用于建模的克里普克结构，就根据与检查公式对应的行为属性对所表示的程序进行经验测试，以评估模型假设是否是对模型假设的充分表示。目标计算系统。因此，属性规范和系统规范在其有意立场上也有所不同（Turner2011）：前者是对要编码的程序，后者是编码程序的（假设）描述。模型检查中状态转换系统的描述性和归纳性特征是将状态转换系统与科学模型相提并论的附加和基本特征。6。2测试和实验
　　测试是启动程序并观察其执行以评估它们是否符合提供的属性规范的更经验的过程。这种技术在软件开发过程中被广泛使用。哲学家和有哲学头脑的计算机科学家根据科学发现中的传统方法论方法考虑了软件测试（Snelting1998；Gagliardi2007；Northoveretal。2008；Angius2014）并质疑软件测试是否可以被认为是评估软件测试的科学实验程序的正确性（Schiaffonati和Verdicchio2014，Schiaffonati2015；Tedre2015）。
　　Dijkstra的著名格言程序测试可用于显示错误的存在，但永远不能显示错误的存在（Dijkstra1970，第7页），介绍了Popper（1959）的可证伪性原则进入计算机科学（Snelting1998）。在给定的时间间隔内根据高级属性规范测试程序可能会出现一些故障，但如果在观察正在运行的程序时没有发生故障，就不能断定该程序是正确的。在下一次系统运行时可能会观察到不正确的执行。原因是测试人员只能使用潜在程序输入集的有限子集启动程序，并且只能在有限的时间间隔内运行；因此，并非所有要测试的程序的潜在执行都可以凭经验观察到。出于这个原因，软件测试的目的是检测程序的错误，而不是保证它们不存在（Ammann和Offutt2008，第11页）。程序是可证伪的，因为测试可以揭示错误（Northover等人。2008）。因此，给定计算系统和属性规范，测试类似于科学实验，通过观察系统的行为，试图证伪程序相对于感兴趣的规范是正确的假设。
　　但是，软件测试不具有表征科学实验的其他方法论和认识论特征。第一个方法论上的区别可以被认识到，因为伪造测试会导致计算系统的修订，而不是假设的修订，就像在测试科学假设的情况下一样。这是由于科学中规范和经验假设的有意立场的差异（Turner2011）。规范是其违反要求程序修订的要求，直到程序成为规范的正确实例。
　　为此，除其他原因外，科学实验的传统概念需要延伸才能应用于软件测试活动（Schiaffonati2015）。理论驱动的实验，表征了大多数实验科学，在实际的计算机科学实践中找不到对应物。如果排除测试与形式方法相结合的情况，软件工程师进行的大多数实验都是相当具有探索性的，即旨在探索在缺乏适当理论或理论背景的情况下，与人工制品的功能及其与环境的相互作用有关的可能性领域（Schiaffonati2015：662）。软件测试人员通常无法对他们执行的实验进行理论控制；探索与用户和环境交互的计算系统的行为，而是允许测试人员对观察到的行为进行理论概括。计算机科学中的探索性实验的另一个特点是程序经常在类似真实的环境中进行测试，其中测试人员扮演用户的角色。然而，实验者不参与要进行的实验是理论驱动实验的一个基本特征。
　　因此，虽然一些软件测试活动更接近于人们在实证科学中发现的实验活动，但其他一些活动却定义了一种新的实验类型，结果证明它属于软件开发过程。在指定、实施和评估计算系统的过程中，可以区分五种类型的实验（Tedre2015）：进行可行性实验以评估系统是否执行用户和利益相关者指定的功能；在给定一些初始条件的情况下，进行试验实验以评估系统的隔离能力；现场实验是在真实环境中进行的，而不是在模拟环境中进行；比较实验测试类似的系统，以不同的方式实例化相同的功能，以评估哪种实例化在真实环境和真实环境中都能更好地执行所需的功能；最后，受控实验用于评估测试计算系统行为的高级假设，并且是唯一可与科学理论驱动的实验相提并论的实验，因为它们是在一些被评估的理论假设的基础上进行的。6。3说明
　　当检测到错误计算时，软件测试被认为是成功的（假设没有计算工件是100正确的）。后续步骤是找出导致执行不正确的原因，即追溯故障（更熟悉的名称错误），然后再进入调试阶段，然后再次测试系统。换句话说，需要对观察到的错误计算进行解释。
　　已经努力考虑与科学哲学中阐述的不同解释模型相关的计算机科学解释（Piccinini2007；Piccinini和Craver2011；Piccinini2015；Angius和Tamburrini2016）。特别是，计算解释可以被理解为一种特定的机械解释（Glennan1996；Machameretal。2000；BechtelandAbrahamsen2005），只要计算过程可以被分析为机制（Piccinini2007；2015；另见条目关于物理系统中的计算）。
　　考虑一个执行指令的处理器。所涉及的过程可以理解为一种机制，其组件是处理器中的状态和组合元素，实例化相关硬件规范（寄存器规范、算术逻辑单元规范等）规定的功能，以这样一种方式组织起来：能够执行观察到的执行。提供这种机制的描述算作推进对观察到的计算的机制解释，例如对操作故障的解释。
　　对于每种类型的错误计算（参见第7。3节），可以在适当的LoA和表征该LoA的规范集定义相应的机制解释。事实上，机制的抽象描述仍然以机制模式的形式提供机制解释，定义为一种机制的截断抽象描述，可以填充已知组件和活动的描述（Machameretal。2000，第。15）。例如，假设一种非常常见的情况，其中机器通过执行包含语法错误的程序来错误计算，称为滑动。计算机无法正确实现程序规范提供的功能需求。然而，出于解释的目的，通过推进硬件组件及其功能组织的详细描述，在硬件抽象级别提供对发生的滑动的解释将是多余的。在这种情况下，令人满意的解释可能在于表明程序代码不是所提供程序规范的正确实例（AngiusandTamburrini2016）。为了从机制上解释发生的错误计算，提供错误程序的描述可能就足够了，从其余的计算机制中抽象出来（Piccinini和Craver2011）。抽象不仅在软件开发和规范中是一种美德，而且在计算系统行为的解释中也是一种美德。7。正确性
　　上一节中检查的每种不同的软件验证方法都假设对软件的正确性有不同的理解。标准地，正确性被理解为抽象与其实现之间的关系，这样如果后者满足前者制定的属性，则它成立。一旦计算系统被描述为具有分层本体，就需要将正确性重新表述为任何结构级别与其功能级别相关的关系（Primiero，2020）。因此，在抽象层和功能层之间表述时，正确性仍然可以被认为是一种数学关系；而在功能和实施层面之间制定时，它可以被视为一种经验关系。等。1979年；Fetzer1988）确实围绕着这种区别。7。1数学正确性
　　形式验证方法授予对程序行为的先验分析，而不需要观察它们的任何实现或考虑它们的执行。特别地，定理证明允许人们推导出正在考虑的程序的任何潜在行为及其来自合适公理表示的行为属性。在模型检查的情况下，通过对给定集合论模型中有效的公式进行算法搜索，可以预先知道程序执行所显示的行为属性。这些考虑使Hoare（1969）得出结论，程序开发是一门精确的科学，其特征应该是正确性的数学证明，在认识论上与数学实践中的标准证明相提并论。
　　德米洛等人。（1979）质疑Hoare的论文：正确的数学证明通常是优雅和易于理解的，这意味着任何（专家）读者都可以看到结论来自前提（关于软件优雅的概念，另见Hill（2018））。通常被称为笛卡尔证明（Hacking2014）在正确性证明中没有对应物，通常冗长而繁琐，难以理解，并且无法解释为什么结论必然来自前提。然而，数学中的许多证明又长又复杂，但它们原则上是可调查的，多亏了引理、抽象和新概念的分析构造的使用，逐步引导到要证明的陈述。相反，正确性证明不涉及新概念的创建，也不涉及通常在数学证明中发现的模块化（Turner，2018）。然而，不可测量的证明不能被视为数学证明（Wittgenstein1956）。
　　关于计算机程序正确性证明的第二个理论困难涉及它们的复杂性和要验证的程序的复杂性。Hoare（1981）已经承认，虽然原则上总是可以验证正确性，但实际上很难实现。除了琐碎的情况，当代软件是模块化编码的，需要满足大量规范，并且开发它是为了与其他程序、系统、用户交互。嵌入式和反应式软件就是一个很好的例子。为了验证这种复杂的软件，自动进行正确性证明。因此，一方面，正确性问题从被检查的程序转移到执行验证的程序，例如定理证明器；另一方面，由于机器的机械错误，物理过程进行的校样可能会出错。Arkoudas和Bringsjord（2007）反对这种无限回归的论点，认为可以使用证明检查器，它是一个相对较小的程序，通常更容易验证。
　　最近，基于逻辑和统计分析相结合的形式化方法检查正确性给这个研究领域带来了新的刺激：分离逻辑（Reynolds，2002）提供计算物理内存逻辑行为表示的能力。系统，以及将输入的概率分布视为统计误差源的可能性，允许对Facebook平台等大型交互式系统进行正式的正确性检查（另见Pym等人，2019年）。7。2物理正确性
　　Fetzer（1988）反对演绎推理只能保证程序在其规范方面的正确性，而不能保证计算系统的正确性，这也说明了程序的物理实现。即使程序在任何相关的上层LoA（算法、规范、要求）方面都是正确的，但由于物理故障，其实施仍可能违反一个或多个预期规范。前一种正确性原则上可以用数学证明，但执行LoA的正确性需要经验评估。如第6。2节所述，软件测试只能在原则上显示计算系统的正确性。在实践中，非平凡系统的允许执行次数可能是无限的，并且无法在有限（或合理）的时间内彻底检查（Dijkstra1974）。大多数成功的测试方法宁可将形式验证和测试结合使用以达到令人满意的校正水平。
　　对数学正确性的理论可能性的另一个反对意见是，由于证明是由定理证明器（即物理机器）执行的，因此人们获得的有关计算系统的知识不是先验的，而是经验的（参见Turner2018ch。25）。然而，Burge（1988）认为，基于计算机的正确性证明仍然可以被视为先验的，因为即使它们的可能性取决于感官经验，他们的理由也不是（就像后验知识一样）。例如，红色是一种颜色的知识是先验的即使它需要有红色的感官体验；这是因为红色是一种颜色是真实的，独立于任何感官体验。有关在数学证明中使用计算机的性质的进一步讨论，请参见（Hales2008；Harrison2008；Tymoczko1979，1980）。
　　正确性问题最终归结为询问物理机器满足抽象需求意味着什么。根据简单映射帐户，计算系统S是规范SP的正确实现，仅当：可以建立从归属于S的状态到由SP定义的状态的态射，并且对于任何状态转换秒1秒2s1s2在S中有一个状态转换秒1秒2s1s2在SP之间的状态秒1s1映射到秒1s1和状态秒2s2映射到秒2s2。
　　简单映射帐户只需要S和SP的描述之间的扩展协议。这个帐户的弱点是很容易识别任何一对物理系统规范之间的扩展协议，为泛计算主义的观点留下空间。
　　泛计算主义的危险导致一些作者试图解释正确的实现，这以某种方式限制了可能解释的类别。特别是，的因果帐户（DJ查尔姆斯1996；科普兰1996）表明，该材料的条件（如果系统是在物理状态秒1s1）被一个反事实的代替。该语义账户认为，一个计算系统必须具有语义描述相关联，指定系统是实现什么（Sprevak2012）。例如，一个物理设备可以被解释为一个与门或一个或门，但如果没有设备的定义，就无法确定工件是什么。的句法帐户的是，可以被定义为唯一的句法物理状态可以映射到计算状态的要求。仍有待研究的是定义句法状态的内容（请参阅Piccinini2015或物理系统中的计算条目，以了解句法帐户的概述）该规范账户（特纳2012）维护不仅是抽象的和物理的计算过程必须是一致的，但也是抽象规范对系统有规范力。根据这种说法，计算是物理过程，其功能由抽象规范固定。这种关系比要求简单描述关系的语义说明和注重句法对象及其语义解释的句法说明都强。7。3错误计算
　　从目前所说的来看，所实施程序的正确性并不能自动建立计算系统的良好运行。图灵（1950年）已经区分了运作的失误和结论的错误。前者是由于执行错误导致无法执行某些高级语言程序的指令；结论错误是正确的抽象机器的特征，但它们仍然无法执行它们应该完成的任务。这可能发生在程序正确实例化某些规范的情况下，这些规范没有正确表达用户对此类程序的要求。在这两种情况下，执行正确程序的机器仍然可以说是计算错误。
　　图灵在功能错误和结论错误之间的区别已扩展为错误计算的完整分类法（Fresco和Primiero2013）。分类是在定义计算系统的不同LoA的基础上建立的。错误可能是：概念上的：它们违反了要求以命题合取范式表达的规范的一致性的有效性条件；材料：它们违反了程序关于其规范集的正确性要求；可执行的：它们出现时，物理约束被一些错误的硬件实现突破。
　　可执行错误显然只出现在执行层面，它们对应于图灵（1950）的功能错误，也称为操作故障。从意图级别到物理实现级别的任何抽象级别都可能出现概念和实质性错误。概念错误会导致错误，而材料错误会导致失败。。例如，意图级别的错误包含一组不一致的要求，而在物理实现级别，它可能对应于无效的硬件设计（例如在为真值功能连接词选择逻辑门时）。发生在规范级别的失败可能是由于设计被认为不符合一组所需的功能要求，而算法级别的失败发生在那些发现算法不满足要求的常见情况下规格。除了错误、故障和操作故障之外，滑倒是高级编程语言指令级别错误计算的来源：它们可能是由于程序中的句法或语义缺陷分别导致的概念或实质性错误。在所有违反高级语言语法规则的情况下，都会出现概念错误；材料单涉及违反编程语言的语义规则，例如使用变量但未初始化时。
　　必须进一步区分功能障碍和错误功能用于基于软件的计算系统（Floridi、Fresco和Primiero2015）。软件只会出现故障，但永远不会出现故障。如果其物理实现无法满足意图或规范，则软件令牌可能会出现功能障碍。功能障碍仅适用于单个令牌，因为一个令牌功能失调，因为它的行为与其他相同类型的令牌在实现的功能方面的表现不同。因此，功能障碍不适用于意图层面和规范层面。相反，软件类型和令牌都可能出现故障，因为故障并不取决于与相同类型的令牌是否能够执行某些已实现的功能的比较。代币的错误功能通常取决于某些其他组件的功能障碍，而类型的错误通常是由于设计不当造成的。软件令牌不会功能障碍，因为给定类型的所有令牌都实现了在意图和规范级别统一指定的功能。这些功能在执行级执行之前先在算法实现级实现；在正确实施的情况下，所有令牌将在执行级别正确运行（前提是没有发生操作故障）。出于同样的原因，软件令牌不会出现故障，因为它们是相同意图和规范的实现。只有软件类型才能在设计不佳的情况下出错；故障软件类型能够正确执行其功能，但也可能产生一些不希望的副作用。8。计算机科学的认识论地位
　　在1960年代和1970年代之间，计算机科学成为一门独立于其老兄弟数学和物理学的学科，随之而来的是定义其受数学、经验和工程方法影响的认识论地位的问题（TedreandSutien2008，Tedre2011、Tedre2015、Primiero2020）。关于计算机科学是否必须主要被视为一门数学学科、工程的一个分支或作为一门科学学科，今天仍然存在争论。8。1作为数学学科的计算机科学
　　计算机科学的任何认识论特征都基于本体论、方法论和认识论的承诺，即基于对计算系统性质的假设、指导软件开发过程的方法以及由此涉及的推理类型，无论是演绎的、归纳的还是推理的。两者的结合（伊甸园2007）。
　　作为数学概念的计算分析的起源臭名昭著地来自逻辑，希尔伯特关于谓词演算的可判定性的问题，被称为Entschiedungsproblem（HilbertandAckermann1950）：是否有一个机械程序来决定一个任意的逻辑句子是否可证明？为了解决这个问题，需要一个严格的逻辑和数学中有效或机械方法的非正式概念模型。这首先是数学上的努力：人们必须发展出非正式概念的数学模拟。计算机科学本质上是数学的观点的支持者假设计算机程序可以被视为这种数学实体的物理实现，并且可。。。