可推导的对象识别方法 Inferable Methods for Identifying Objects

Inferable Methods for Identifying Objects

可推导的对象识别方法

https://link.springer.com/book/10.1007/978-3-031-76516-2

摘要：

对象识别问题在不同背景下长期受到研究者关注。本文提出一种基于同伦理论的解决途径：假设各类识别方法可在某个适当范畴内被整合为单一对象，即代表所有可能方法的集合，从而实现将识别方法本身视为一阶对象加以考察。文中进一步探讨了定义于识别方法之上的函数构造方法，这些函数可为相应对象引入代数结构；函数定义采用递归技术，支持基于自反定义关系构建函数层次体系。所提技术可作为构建对象识别系统的基础，包括应用于 Web 环境中安全支持任务的场景。

关键词：对象识别 · 逻辑推理 · 类型论 · 依赖类型

1 引言

计算机信息处理方法在人类活动各领域的持续应用，使得保障信息处理安全的方法开发变得日益迫切。计算机病毒的广泛传播及各类电子欺诈行为，要求我们发展信息保护的理论基础与实用系统。其中一项关键任务便是对象识别问题。

文献中存在多种解决识别问题的途径。目前最具前景的方法之一基于类型论 [1,2,11]。该方法的吸引力在于：它能够统一用于描述对象类型的形式化手段（包括在实际编程系统中所用者）与描述“哪些对象在何种意义上相同”的手段 [3,4]。此类工具既足够精确，可刻画对象间的同一性；又足够强大，可揭示对象描述对观察视角的依赖性 [5,6]。

类型论中涉及两类判断：

• “ a : A ” 表示“对象 a a 具有类型 A ”；
• “ a ≡ b ” 表示“对象 a a 与 b 在判断中相等”或“依定义相等”。

后者是最强形式的相等性，任何与类型论一致的计算系统都必须满足它。更宽泛结构的相等性亦可能存在 [7]，而此类相等性的建立，被发现直接依赖于所采纳的同伦视角。在此视角下，类型可被视作拓扑空间，对象则可被视作该空间中的点或元素；进而可引入对象的“信息轨迹”概念 [8]——这些轨迹可解释为将一对象连续形变为另一对象的连续映射。

形式上，上述形变定义为从实轴线段 [ 0 , 1] 到对象拓扑空间的连续映射，即同伦（homotopy）的定义。凡可通过同伦相连的对象，彼此可被识别为同一。此性质定义了一种更宽泛的相等性——“命题相等”（propositional equality），记作 “ a = b
”。命题相等的对象实际上是“同伦意义上相等”的，即它们可相互形变或转换。

将公式解释为类型的命题为类型（propositions-as-types）原则，赋予该理论以构造性特质 [9]。理论的形式规则被设计成既能构造相应类型的对象，又能识别其计算行为（即，依定义可适用于该对象的归约规则）。前一情形给出公式的证明，后一情形则给出一种根据证明片段构造完整证明的操作 [10]。这一特性简化了基于类型论的应用计算系统的设计与实现。

本文结构如下：第 2 节简要讨论若干对象识别方法；第 3 节明确“界定对象识别方法”的任务；第 4 节阐述基于类型论的对象识别主要思路——需注意，由于该理论的构造性本质，这些对象可直接映射至足够高级的编程语言构造中；第 5 节总结简要结论。

2 相关工作
对象识别可有多种理解方式。其中一种最为常见的方法将识别视为获取对象的数学描述或构建其模型的过程 [12]。尽管该方法显然具有吸引力，但它显得过于宽泛，尤其需要对所得数学模型的本质作进一步澄清。

一种更为令人满意的识别定义是：识别是一种过程，其执行结果是为被识别对象生成一个标识符（identificator），该标识符可在信息系统中唯一地标识该对象 [13]。然而，识别问题的复杂性恰恰在于：在许多情况下，这样的标识符根本无法被唯一确定，或仅能模糊地确定。因此，发展更具灵活性的方法显得尤为可取。

基于范畴模型框架内追踪对象信息轨迹的识别方法已在文献 [14] 中展开研究。该文确定了追踪信息轨迹及应用相应识别方法所必需映射的总体结构，并提出了迁移映射与克隆映射，阐明了其主要性质。

本文致力于拓展上述通用方法，具体针对如下情形：类型可被视为拓扑空间，而识别方法可被视为具备自然连续性性质的映射等。在此设定下，得以充分运用类型论的整套工具——既可用于构造所需映射，又可利用与应用式计算系统相一致的手段对其进行操作。

3 对象识别方法推导问题的提出

对范畴模型框架下所提出的对象识别方法 [14,15] 进行分析，并将其与类型论所提供的手段进行比较，使我们可将对象识别方法的推导问题明确为：构建并支持具备以下能力的逻辑推导方法与工具的任务：

• 基于最简单的同伦（即对象间恒等路径）来判定对象间的相等性；
• 建立同伦上的基本运算及其运算性质；
• 揭示同伦与类型系统中新类型构造手段之间的关联；
• 确定所提工具的计算特性，并阐明其与参数化类型（包括依赖函数与非依赖函数）之间的联系；
• 设计将识别方法嵌入应用式计算环境的机制。

4 推导系统的基本构造
4.1 命题相等性

我们首先考察命题相等性（propositional equality）所适用的推导规则。

4.2 命题相等性的性质

5 结论

本文提出了一种类型论的变体，支持多种类型对象的构造及其识别。所发展的理论具有构造性特征，使得识别方法可嵌入应用式编程环境，并为自动化实现此类嵌入提供了工具定义的可能性。

1. 类型与对象通过基本类型论构造；定义了两种对象识别方式：判断相等性（equality in judgment）与命题相等性（propositional equality）。
2. 基于对象间相互转换，确定了追踪对象信息轨迹的方法；其形式化依托于同伦概念。
3. 由此构建了命题相等性的计算模型，其核心是将自反映射（reflexive maps）作为基础。
4. 确立了操作相等性的基本公式——依据“公式即类型”（formulas-as-types）原则，这些公式对应具体的操纵运算；而这些运算又可嵌入一个计算模型中，从而在应用式编程环境中得以实现。

原文链接：https://link.springer.com/book/10.1007/978-3-031-76516-2