计算机科学哲学（三）

4.3 程序及其与世界的关系

计算机程序是否是理论的问题与程序与外部世界的关系有关。如果程序是理论，它们就必须代表某种经验系统，并且程序与世界之间将直接建立语义关系。相反，一些人认为程序与自然系统之间的关系是由外部世界的模型介导的（Colburn 等人 1993 年，Smith 1985 年）。特别是，Smith（1985 年）认为模型是经验系统的抽象描述，在其中运行的计算系统具有充当模型模型的程序，即它们代表现实的抽象模型。在描述计算机科学中的正确性问题时，这种程序本体论的解释非常有用（见第 7 节）：如果将规范视为需要计算系统具有某些行为的模型，那么程序就可以看作满足规范的模型。

可以根据人们是否承认与世界的关系（RapaPort 2023，CH.16）给出了两个方案的两个观点。 根据第一个视图，程序是“宽”，“外部”和“语义”：它们授予直接引用对这些对象的经验系统和操作的对象。 根据第二种视图，程序是“窄”，“内部”和“句法”：它们仅参考实现计算的实施机器的原子操作。 RapaPort（2023）认为方案不需要“外部”和“语义”。 首先，计算本身不需要“外部”：图灵机通过使用在其磁带上写入的数据来执行其有限表中包含的指令，并在计算由计算产生的数据之后暂停。 数据不是，严格地讲，从中讲解和输出到外部用户。 此外，KNUTH（1973）所需的算法具有零或多个输入和输出（参见第3.1节）。 一个需要没有输入的计算机程序可以是一个程序，例如，从1开始输出所有素数; 而没有输出的程序可以是计算某个给定变量x的值的程序，而无需返回存储在x中的输出。 其次，程序不需要“外部”，目政，即目标。 这种观点反对文献中的其他已知位置。 Suber（1988）辩称，在不考虑目标和目的的情况下，不可能评估计算机程序是否正确，即如果它按预期行为。 并在§3.3中召回。，Hill（2016）规定了她的非正式定义，即算法在给定的规定下完成了“给定的目的” （山2016：48）。 对于这些观点来说，rapaport（2023，ch.16）回复，而目标，目的和程序员的意图对人类计算机来理解程序非常有用，但是人工计算机不需要进行程序执行计算的计算代码。 实际上，经典方法需要算法（参见第3.1节）所需的效果原则，以及其他属性，该算法在没有任何诉诸直觉的情况下执行该算法。 换句话说，执行用于添加自然数字的程序的机器不“理解”它正在添加; 与此同时，知道给定的程序执行添加可以帮助人类代理理解程序的代码。

根据这一观点，计算涉及符号，而不是含义。 图灵机成为符号操纵器，而不是单个但多种含义可以与其操作相关联。 然后，何时可以确定两个程序是相同的程序，如果不是他们的含义，也就是说，通过考虑它们执行的功能？ 一个答案来自Piccini对计算分析及其“内部语义”（Piccini 2008,2015 Ch.3）：通过分析它们的语法和程序在其符号上进行操作可以识别两个程序。 字符串操作操作的影响可以被认为是程序的内部语义。 通过隔离程序代码中的子程序或方法可以容易地确定后者，并且之后可以用于识别程序或建立两个程序是否相同，即当它们由同一子例程定义时。

然而，已经据说存在存在其中不可能确定两个程序是否相同而不参考外部语义。 Sprevak（2010年）建议考虑两个课程，这与一个人在阿拉伯语上运作的事实不同，罗马数字上的另一个。 这两个程序计算相同的功能，即添加，但不能始终通过将代码与子例程检查代码来建立; 必须通过将内容分配给输入/输出字符串，以将阿拉伯语和罗马数字解释为数字来确定。 在这方面，angius和Primiero（2018）强调了计算机程序的身份问题如何与自然类型的身份问题不同（Lowe 1998）和技术工件（Carrara等，2014）。 通过修复身份标准，即正式关系可以解决问题，任何两个程序都应该娱乐，以便定义相同。 angius和Primiero（2018）展示了如何使用两项机构在考试中实施的两项自动机之间的双层刺激的过程代数与这种身份标准。 Bisimulation允许建立实现相同功能的程序的匹配结构特性，以及在模拟方面提供副本的较弱标准。 这将讨论带回程序的概念作为实现。 我们现在转向分析后一种概念。

5.实施

这个词“实现”通常与计算系统的物理实现相关联，即执行计算机程序的机器。 特别是，根据§1.1中检查的计算系统的双本体学，在此检测中的实现减少到结构硬件，而不是功能软件。 相比之下，遵循抽象级别的方法（第1.2节），实现成为在定义计算系统的任何LOA之间的更广泛的关系，并且层次结构中较高的级别。 因此，算法是（集）规范的实现; 以高级编程语言表示的程序可以定义为算法的实现（参见§4）; 组装和机器代码说明可以看作是关于给定ISA的一组高级编程语言指令的实现; 最后，执行是这些机器代码指令的物理，可观察的实现。 通过相同的令牌，以高级语言制定的程序也是规范的实现，并且与双本体范例类似地认为，执行是高级编程语言指令的实现。 根据特纳（2018年），即使是规范也可以理解为称为意图的实施。

这里仍有待检查的是所定义的实现关系的性质。 分析这一关系对于定义正确性（§7）是必不可少的。 实际上，正确的程序达到了正确的算法的正确实现; 并且正确的计算系统是正确实现一组规范。 换句话说，在这种视图下，正确性的概念与任何LOA的实现配对：如果且仅当它是正确的实现时，则可以说，可以说出任何级别。

以下三个章节审查了在计算机科学文献哲学中提出的执行关系的三个主要定义。

5.1实施作为语义解释

通过RAPAPORT（1999,2005）提出了对计算机科学实施概念的第一哲学分析。 他将一个实施方式定义为在实现媒体中的句法或抽象域A的语义解释。如果实现被理解为在计算系统的分层本体中的给定LOA和任何上层之间的关系，则rapaport定义相应地扩展，因此任何LOA在上层的给定介质中提供了语义解释。 在此视图下，规范提供了对规范（正式）语言中的利益相关者表达的意图的语义解释，并且算法可以使用许多语言算法中的一种来提供规范的语义解释（自然语言，伪-code，逻辑语言，功能语言等）。 实施媒介可以是抽象或混凝土。 计算机程序是实现算法的实现，因为前者在高级编程语言中提供了后者的语法构造作为其实现媒介的语法解释。 程序的指令以编程语言解释算法的任务。 此外，执行LOA提供了通过物理机器结构特性给出的组装/机器代码操作的语义解释。 根据分析（RapaPort 1999,2005），实施是一种不对称关系：如果我是一个实施，A不能成为我的实施。但是，作者争辩说，任何LOA都可以是一个句法和语义级别，即它可以播放实现I和句法域A的角色。虽然通过高级语言表达的程序分配了语义解释的算法，但相同的算法为规范提供了语义解释。 遵循抽象实施关系对计算系统的功能结构关系对。

Primiero（2020）将后一种方面视为侏儒人（1999,2005）实施的一个主要限制：实施减少了句法水平与其语义解释之间的独特关系，并且它不会考虑分层本体的计算在§1.2中看到的系统。 为了将实现的实现定义扩展到所有LOA，必须每次作为句法或作为语义级别重新解释每个级别。 反过来，这是对第二个难度表征的反射，根据Primero（2020），作为语义解释的实现：一方面，这种方法没有考虑不正确的实现; 另一方面，对于给定的不正确实现，所定义的唯一关系可以将不正确的不正确与一个句法级别相关联，以排除所有其他级别作为潜在的错误位置。

Turner（2018）旨在表明，语义解释不仅不考虑不正确的实施，而且甚至无法纠正。 通过将一种语言实施进入另一个语言的第一示例：这里的实现语言不是提供所实现语言的语义解释，除非前者与为后者提供含义和正确性标准的语义相关联。 此类语义将保持在实施关系外部：而正确性与语义解释相关，但实施并不总是具有语义解释。 通过考虑由数组实现的抽象堆栈来给出第二个例子; 同样，阵列不提供堆栈的正确性标准。 相反，它是阵列指定其使用的任何实现的正确性标准的堆栈。

5.2 实现作为规范-工件关系

由于实现关系的正确性标准由抽象层提供，因此 Turner (2012, 2014, 2018) 将实现定义为规范-工件关系。如第 2 节所述，规范对工件具有正确性管辖权，即它们规定了工件的允许行为。还要记住，工件可以是抽象实体，也可以是具体实体，并且任何 LoA 都可以充当较低级别的规范。这相当于说，规范-工件关系能够定义跨计算系统分层本体的任何实现关系。

根据规范-工件关系的定义方式，Turner (2012) 区分了多达三种不同的实现概念。考虑物理机器实现给定抽象机器的情况。根据有意的实现概念，抽象机可作为物理机的规范，前提是它推进了物理机必须满足的所有功能要求，即它（原则上）指定了实现物理机的所有允许行为。根据外延的实现概念，当且仅当可以建立同构将后者的状态映射到前者的状态，并且抽象机中的转换对应于工件的实际执行（计算轨迹）时，物理机才是抽象机的正确实现。最后，经验的实现概念要求物理机显示与抽象机规定的计算相匹配的计算；也就是说，正确的实现必须通过测试进行经验评估。

Primiero (2020) 强调，虽然这种方法解决了正确性和错误计算的问题，因为它允许区分正确和不正确的实现，但它仍然确定了规范级别和工件级别之间的唯一实现关系。同样，如果允许此解释通过每次将任何 LoA 重新解释为规范或工件来涉及计算系统的分层本体，则 Turner 的解释会阻止人们同时将多个级别作为错误计算的原因：错误计算总是发生在这里，因为工件对规范的错误实现。通过将实现定义为跨所有 LoA 的关系，人们将能够识别出多个不直接引用抽象规范的错误实现。错误计算确实可能是由较低级别的错误实现引起的，然后一直继承到执行级别。

5.3 LoA 的实现

Primiero (2020) 提出了一种实现定义，它不是两个固定级别之间的关系，而是一个允许跨越任何 LoA 的关系。根据这种观点，实现 I 是 LoA 与抽象层次结构中任何其他更高级别的 LoA 之间的实例化关系。因此，物理计算机是汇编/机器代码操作的实现；通过传递性，它也可以被视为用高级编程语言指令表达的一组指令的实例。用高级语言表达的程序是算法的实现；但它也可以被视为一组规范的实例。

这种实现定义使 Primiero (2020) 能够提供正确性的一般定义：物理计算系统正确当且仅当它在任何 LoA 上具有正确的实现特征时才是正确的。因此，正确性和实现是耦合的，并在任何 LoA 上定义。功能正确性是计算系统的属性，它显示该系统规范所需的功能。程序正确性表征了显示所实现算法所预期功能的计算系统。执行正确性被定义为能够在其架构上正确执行程序的系统的属性。这些正确性形式的每一种也可以根据所满足的功能数量进行定量分类。功能高效的计算系统显示规范所需功能的最小子集；功能最优的系统能够显示这些功能的最大子集。同样，作者定义了程序和执行效率都很高且最优的计算系统。

5.4 物理计算

根据此定义，实现从一个级别转移到另一个级别：定义计算系统的一组算法被实现为某种形式语言中的程序、高级语言中的指令或低级编程语言中的操作。一个有趣的问题是，除了计算工件之外，实现此类程序的任何系统是否都有资格成为计算系统。换句话说，询问物理实现的性质就等于询问什么是计算系统。如果任何实现算法的系统都有资格成为计算系统，那么这种系统的类别可以扩展到生物系统，例如大脑或细胞；物理系统，包括宇宙或其中的某些部分；并最终扩展到任何系统，这一论点被称为泛计算主义（有关该主题的详尽概述，请参阅 Rapaport 2018）。

传统上，计算系统旨在作为一种机械制品，它接收输入数据，根据一组指令以算法方式对其进行阐述，并返回经过处理的数据作为输出。例如，冯·诺依曼（1945 年，第 1 页）指出：“自动计算系统是一种（通常高度复合的）设备，它可以执行指令来执行相当复杂程度的计算”。这种非正式且被广泛接受的定义留下了一些问题，包括计算系统是否必须是机器，它们是否必须以算法方式处理数据，以及计算是否必须是图灵完备的。

Rapaport（2018 年）对计算系统进行了更明确的描述，将其定义为“任何在逻辑上等同于通用图灵机的物理上可行的实现”。严格来说，个人计算机不是物理图灵机，但已知寄存器机是图灵等价的。要符合计算的条件，系统必须是其合理的实现，因为与物理机器相反，图灵机可以访问无限的内存空间，并且作为抽象机器，没有错误。根据 Rapaport (2018) 的定义，任何此类物理实现都是计算系统，包括自然系统。这就提出了一个问题，即哪一类自然系统能够实现图灵等效计算。Searle 曾提出，任何东西都可以是图灵机或逻辑等效模型的实现（Searle 1990）。他的论点利用了这样一个事实：图灵机是一种句法属性，因为它完全是关于操纵 0 和 1 的标记。根据 Searle 的说法，句法属性不是物理系统固有的，而是由观察者赋予的。换句话说，系统的物理状态本质上不是计算状态：必须有一个观察者或用户为该状态分配计算角色。因此，任何可以将其行为描述为 0 和 1 的句法操作的系统都是计算系统。

Hayes (1997) 反对 Searle (1990) 的观点，即如果一切都是计算系统，那么“作为计算系统”这一属性将变得毫无意义，因为所有实体都拥有它。相反，有些实体是计算系统，有些实体不是。计算系统是指那些接收的输入模式并保存到内存中能够自行改变的系统。换句话说，Hayes 提到了这样一个事实：存储的输入既可以是数据，也可以是指令，并且指令在执行时能够修改某些输入数据的值。“如果它是纸，它就是‘魔法纸’，上面的字迹可能会自发改变，或者出现新的字迹”（Hayes 1997，第 393 页）。只有能够充当“魔法纸”的系统才能被承认为计算系统。

Piccinini (2007, 2008) 在对物理计算进行机械分析时提出了另一种不同的方法（Piccinini 2015；另见条目“物理系统中的计算”）。物理计算系统是一种可以通过描述引起这些行为的计算机制来机械解释其行为的系统。机制可以定义为“实体和活动，这些实体和活动被组织起来，使得它们从开始或设置到结束或终止条件产生有规律的变化”（Machamer 等人 2000；参见条目“科学中的机制”）。计算作为物理过程，可以理解为“根据适用于所有输入字符串的一般规则从输入字符串生成输出字符串，并依赖于输入（有时是内部状态）”的机制（Piccinini 2007，第 108 页）。很容易识别计算过程的设置和终止条件。任何可以通过描述底层计算机制来解释的系统都被视为计算系统。对解释的关注有助于 Piccinini 避免得出任何系统都是计算系统的 Searlean 结论：即使人们原则上可以将任何给定的一组实体和活动解释为计算机制，但只需要用计算机制来解释某种观察到的现象，就可以将所考察的系统定义为计算系统。

为了避免得出 Searlean 结论，Curtis-Trudel，2021 年提出了一种实现概念，即相似关系，适用于人工和自然计算系统。根据这一概念，如果物理系统类似于计算架构，则它会实现计算。例如，图灵机的形式定义提供了任何物理图灵机的蓝图。物理系统是物理图灵机，前提是它类似于图灵机的计算架构。对于数字计算机的一般情况，定义其架构相当于指定其指令集架构 (ISA)。相似性可以用 Weisberg (2012) 的相似性概念来理解：对于给定的一组特征，评估计算架构与物理系统之间的相似性需要确定两个系统共享的特征数量以及每个系统相对于另一个系统缺少的特征数量。

6. 验证

验证是软件开发过程中的一个关键步骤。这包括评估给定计算系统是否符合其设计规范的过程。在计算机行业的早期，有效性和正确性检查方法包括几种设计和构造技术，例如（Arif 等人，2018 年）。如今，正确性评估方法大致可分为两大类：形式验证和测试。形式验证（Monin 和 Hinchey，2003 年）涉及使用数学工具证明正确性；软件测试（Ammann 和 Offutt，2008 年）则包括运行实施的程序以观察执行的执行是否符合高级规范。在许多实际情况下，会使用两种方法的组合（例如，参见 Callahan 等人，1996 年）。

6.1 模型和理论

形式化验证方法需要对被验证的软件进行表示。在定理证明中（参见 van Leeuwen，1990 年），程序以公理系统和一组推理规则表示，这些规则表示程序转换的先决条件和后置条件。然后通过从公理中推导出表达规范的公式来获得正确性证明。在模型检查中（Baier 和 Katoen，2008 年），程序以状态转换系统表示，其属性规范由时间逻辑公式形式化（Kröger 和 Merz，2008 年），正确性证明通过深度优先搜索算法实现，该算法检查这些公式是否适用于状态转换系统。

用于正确性评估的公理系统和状态转换系统可以理解为所表示工件的理论，因为它们用于预测和解释其未来行为。从方法论上讲，模型检查中的状态转换系统可以与经验科学中的科学模型进行比较（Angius 和 Tamburrini 2011）。例如，克里普克结构（参见 Clarke 等人 1999 年第 2 章）符合 Suppes（1960 年）对科学模型的定义，即建立与通过对目标经验系统进行实验收集的数据模型的适当映射关系的集合论结构（另请参阅科学中的模型条目）。形式化验证方法中使用的克里普克结构和其他状态转换系统通常称为系统规范。它们与通用规范（也称为属性规范）不同。后者指定了要编码的程序必须实例化的一些必需的行为属性，而前者（原则上）指定了已编码程序的所有潜在执行，从而允许对其踪迹进行算法检查（Clarke 等人，1999 年）。为了实现这一目标，系统规范被视为溯因结构，根据程序的代码和允许的状态转换假设目标计算系统的潜在执行集（Angius，2013b）。事实上，一旦检查了某个时间逻辑公式是否适用于建模的 Kripke 结构，就会根据与检查公式相对应的行为属性对所表示的程序进行实证测试，以评估模型假设是否是目标计算系统的充分表示。事实上，在进行验证之前，当程序的完整行为仍然未知时，系统规范可以被视为程序的假设（Turner，2020 年）。状态转换系统在模型检查中的描述性和溯因性是使状态转换系统与科学模型相提并论的附加且必不可少的特征。