双胞胎程序（Twin procedures）、两种变量绑定方式以及两种计算方法

《Annals of Pure and Applied Logic》：Twin procedures, two kinds of variable binding, and two kinds of computation

本文针对透明意向逻辑（TIL）中变量绑定与替换的技术问题，提出修订基础定义，引入TIL 2025版本，解决Trivialization与Double Execution协作失败导致的变量状态异常问题，确保λ-转换规则有效性，并扩展至其他高表达式语言。

　　

玛丽·杜日|比约恩·耶斯佩尔森

计算机科学系，FEI，奥斯特拉瓦技术大学（V?B），11月15日，708 33奥斯特拉瓦，捷克共和国

摘要

我们探讨并解决了一些在透明意图逻辑（Transparent Intentional Logic）中出现的技术问题，该逻辑将超意图（hyperintensions）与算法结构化的程序相对应。这些问题涉及变量绑定和替换。一对名为“简化”（Trivialization）和“双重执行”（Double Execution）的程序在大多数情况下配合得很好。但在某些情况下，它们会失效。“简化”如果应用于另一个程序，会使对该程序本身的操作成为可能，而不是对其生成的结果进行操作。程序内部的任何变量实例都会被“简化”所绑定。“简化”绑定比λ绑定更强。当“双重执行”应用于另一个程序时，它的类型和结构首先用于获得该程序的结果，其次是在该结果本身也是一个程序的条件下获得其结果。“双重执行”可以将一些被“简化”绑定的变量实例转换为自由变量实例，并且还可以生成新的变量实例。这些情况削弱了我们对替换的定义，从而危及了λ转换规则的有效性。所需的限制是通过修订基本定义来实现的。我们解决的问题不仅限于透明意图逻辑，任何具有高度表达能力的逻辑或编程语言（尤其是基于λ演算的语言），其中程序可以作为操作数出现，都可能遇到类似的问题。

引言

任何形式语义学都不希望其变量在无意中从绑定状态变为自由状态，或者相反。然而，在程序语义学中，这种情况确实可能发生，原因仅仅是一个程序被执行了。这种不希望出现的变化表明程序之间的协调性不足，从而揭示了相关理论基础中的缺陷。这一缺陷又使得至少某些基于这些基础的应用的可靠性受到质疑。本文探讨并解决了一组此类问题，其中程序的执行导致变量实例从绑定状态变为自由状态，或者出现新的自由变量实例。

我们将在帕维尔·蒂奇（Pavel Tichy）在20世纪60年代开发的透明意图逻辑（Transparent Intentional Logic，简称TIL）框架内进行研究。TIL是最具概念性和技术复杂性的超意图理论之一。TIL的超意图实体被称为“程序”（procedures）。TIL属于结构化意义的范式，因为其各种程序都被结构化为通用算法。每个程序都是一个具有明确组成部分的结构化整体。每种类型的程序都可以作为一个整体来执行，最多产生一个结果，而且每种类型的程序本身也可以作为一个单元，其他程序可以对其进行操作。程序不能简化为其组成部分的集合论集合。即使这些组成部分按顺序排列，它们之间也缺乏直接联系。正是这种直接联系使得某些东西成为整体的一部分，而不仅仅是列表中的项目。结构化程序的适当部分论是非经典的，因为扩展性和幂等性原则在这里不适用。接下来需要关注两点：首先，程序本身可以是另一个程序的结果。我们说这样产生的程序以“显示”（displayed）模式出现，而不是“执行”（executed）模式。这使得显示的程序可以作为操作数，即函数的参数。其次，作为整体嵌入的程序本身也可以被显示并对其进行操作，这在替换和转换方面尤为重要。

从形式上讲，TIL是一种高阶的、部分的、超意图的λ演算，配备了程序语义学。意义是一个抽象的程序，包含一个或多个步骤，通过其类型和结构来指定对哪些操作数应用哪些操作以获得某种逻辑类型的产物（如果有的话）。典型的产物包括扩展实体（如集合、个体和真值），或意图实体（即来自可能世界的函数），所有这些都在一个简单的类型理论中组织起来。当一个程序的结果是另一个程序时，后者属于较低阶。这些程序在一个分层的类型层次结构中组织。

在本文中，我们解决了TIL中变量绑定方面的一个技术问题。解决方案排除了我们不希望保留的某些极端情况。一对特定的程序在自然语言应用中配合得很好，但在某些技术上可能的限制情况下它们会失效。“简化”如果应用于另一个程序，会使对该程序本身的操作成为可能，而不是对其生成的结果进行操作。程序内部的任何变量实例都会被“简化”所绑定。另一个程序“双重执行”如果应用于另一个程序，它的类型和结构首先用于获得该程序的结果，其次是在该结果本身也是一个程序的条件下获得其结果。不幸的是，在某些情况下，被“0绑定”的变量实例会变为自由变量实例，或者出现新的自由变量实例。这些情况削弱了我们对替换的定义，从而危及了λ转换规则的有效性，尤其是β转换规则。

本文的技术成果是对替换定义的调整，引入了所需的限制。此外，我们认为不能通过放弃“简化”或“双重执行”中的任何一个来解决这个问题，因为两者都是不可或缺的，因此必须确保它们在本文研究的那些虽然不太自然但在技术上仍然可能的情况下也能正常工作。这样做的必要性在于，我们必须证明——而不仅仅是基于有限的应用范围来假设——将变量从绑定状态转换为自由状态或生成新变量在技术上是不可能的。否则，我们就不能声称我们所基于的基础是完全有原则的，而不是临时拼凑的。

我们解决的问题不仅限于TIL。任何具有高度表达能力的逻辑或编程语言（特别是基于λ演算的语言），其中程序也可以作为操作数出现，都可能遇到类似的变量绑定和替换问题。我们将在下文将这个问题放在更广泛的背景下讨论。现在，这里有一个例子来说明这一点。所谓的条件语句在计算机科学中经常使用。这类语句的一般模式是：如果P（为真）那么（执行）C，否则（执行）D。这些语句指定了根据布尔条件P的值来执行不同的计算。为此，许多编程语言使用了if-then-else结构。

在自然语言中，有些句子带有预设。这些句子的真值评估也可以通过条件语句来指定：如果（预设）P（为真）那么（评估）S（为真或假），否则S没有真值。

问题出现了：‘if-then-else’的含义是什么？在计算机科学中，它通常被描述为一个“违反组合性原则的非严格函数”。曼纳（Manna）[36]指出，这种指令的语义无法在经典命题逻辑中指定。在本文中，我们引入了所谓的“严格”版本的‘if-then-else’函数定义。我们展示了由‘If P then C else $D^{\prime }表示的函数可以通过两阶段$程序来定义。首先，根据条件P在C和D之间进行选择。为此，我们必须通过“简化”将这两个程序都显示为可选的对象。然后执行选定的程序；因此实现了“双重执行”：第一次执行取消了“简化”的效果，将选定的程序的显示模式转换为执行模式，而第二次执行则执行选定的程序。这个例子表明，总是确定哪些程序实例处于显示模式哪些处于执行模式是有问题的，这反过来又阻碍了变量自由/绑定状态的确定。在第一阶段，C和D都被显示出来，其中出现的所有变量都被“0绑定”。在第二阶段，其中一个程序进入执行模式，使其变量看起来是自由的。关键点是，应该仅通过语法分析来确定哪些实例是自由的；它们的状态不能通过额外的逻辑评估（即通过P中变量的赋值）来改变。从逻辑角度来看，C和D中出现的所有变量都应该保持“0绑定”状态。然而，TIL（2010）对自由变量的定义过于宽松，允许替换到选定的执行程序中，从而导致由于“双重执行”而产生的不一致性。本文提出的限制旨在阻止这种情况并保持语法一致性。

本文的其余部分组织如下：第2节为问题奠定了基础。第3节根据2010年的版本介绍了TIL的基础，并总结了相关的缺陷。第4节通过解决问题将TIL 2010更新为TIL 2025。

章节片段

初步介绍

在这里，我们描述了TIL的相关特性。表达式E的广义语义图如图1所示，其中w和t分别表示可能世界和时间的变量，v是一个赋值函数：

一旦给出了一个术语或表达式的意义对应的程序，就可以推断出该程序产生什么（如果有的话），从而确定E的指称是什么。除非指称是一个平凡的（即常量的）意图（从可能世界到...的映射）

TIL 2010的基础

正如刚刚解释的，TIL与普通的λ演算不同，它不仅处理函数及其值，还处理产生函数的程序本身。当一个程序作为函数参数出现时，我们可以说该程序是“超意图”出现的。只有当一个程序由另一个程序产生时，它才能作为参数出现。

迈向TIL 2025

在本节中，我们提出了对Du?í等人[18]中提出的原始定义的调整。新定义的编号与Du?í等人[18]的编号不同。调整的部分用粗体标出。类型的分层层次结构的定义（即Du?í等人[18]中的定义1.1和1.7）保持不变。为了正确定义程序的两种基本出现模式，这里需要新的²⁰-正规形式定义。

结论

我们引入了改进版的TIL，称为TIL 2025，在其中解决了由“简化”和“双重执行”这两个程序之间的相互作用引发的各种问题。在TIL 2010中，这些问题源于对变量自由出现的定义过于宽松，从而导致替换定义有误。为了推广Tichy [45]中的相关定义，Du?í等人[18]走得太远了。作者将某些情况定义为自由...

致谢

这项研究得到了SGS资助，项目编号为SP2025/091，由V?B - 奥斯特拉瓦技术大学（捷克共和国）资助，项目名为“形式方法在知识建模和软件工程中的应用VIII”。本文的部分内容由玛丽·杜日（Marie Du?í）于2025年6月26日在荷兰乌得勒支大学的哲学与宗教研究系进行了宣读，以及比约恩·耶斯佩尔森（Bj?rn Jespersen）在2023年6月18日至22日在捷克共和国特普拉的Premonstratensian修道院举行的LOGICA 2023会议上进行了宣读。我们感谢两位匿名...