基于类型论的逻辑—应用式计算

Logical-Applicative Computing Based on Type Theory

基于类型论的逻辑—应用式计算

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

摘要：

本文探讨了开发支持计算思维工具这一现实任务。研究将同伦类型论作为支撑计算思维的形式基础，构建了应用式环境中的基本对象，并着重关注其应用的技术手段。其中，应用操作（即函数作用于参数）被视为核心使用方式，而通过为参与应用的对象赋予类型，可保障应用的正确性。文中还探讨了一种对象参数化方法，该方法可引入各类行为相似（在应用过程中）的对象族。由此形成的对象集合，使得可在基础计算环境中定义并嵌入相应算子。

关键词：计算思维 · 类型论 · 依赖类型

1 引言

为计算模型构建新基础的任务，持续处于研究者关注的焦点。信息技术用户的群体不断扩大，这对软件开发与维护工具在概念清晰性与正确性方面提出了更高要求。事实上，为在降低对开发者资质要求的条件下支持开发工作，相关工具应承担一部分验证所开发程序正确性的任务。

尽管人们已在澄清各类信息系统开发方法方面付出了大量努力，但至今仍未达成完全清晰的认知 [1,2]。这激发了人们对理论基础的持续关注——实际的信息处理方法与技术正应建立于这些基础之上 [3–5]。尤其在大量具备强大计算能力的计算机网络不断发展的背景下 [6,7]，这一任务显得尤为紧迫；然而，这些网络的能力边界与局限性仍未得到充分界定。

其中一种较为传统的方法是采用程序类型化（program typing）来支持开发，它可在开发早期阶段识别出程序中某些语义错误 [8]。已发展的类型系统 [14] 允许将类型定义为值的集合及其上允许的操作，从而限定某些表达式可被使用的上下文范围。这些值可具有复杂结构，并可相互嵌套等。

本文探讨基于类型论构建计算基础的可能性。所采用的类型论形成于集合论与拓扑学分支——同伦论的交汇处。这使得我们能够研究对象识别的方法 [9,10]，而该问题在信息技术领域仍属开放性难题。

所讨论类型论的一个关键特征是能够定义所谓的“高阶归纳类型”（higher inductive types），从而对实际信息处理中大量出现的构造提供直接的逻辑刻画。归纳定义尤其涵盖结构正确的树形结构，每种树均由相应的“归纳原理”所刻画——该原理包含了绝大多数实际编程语言中所采用的数据结构。

特别地，该理论允许我们从统一视角出发，发展定义与使用高阶类型的技术，从而可在实际编程系统中对它们进行一致解释。

该理论的另一特征是其构造性（constructiveness）。构造性意味着：每当论及某个对象时，该对象即被实际构造出来并呈现于我们面前。这使得该理论非常适合构建实用的、基于证明的编程系统，如 Agda [14] 或 Coq [15]。尽管该性质限制了某些经典推理原则（如排中律）的使用，但在实践中，此类限制往往微不足道。

构造性还导致：在本理论中，类型与公式相对应，而类型的对象则与相应公式的证明相对应。此即著名的“公式即类型”（formulas-as-types）原则。据此，理论中逻辑上可靠的性质可直接表示为编程环境中的对象。

本文结构如下：第 2 节简要概述该理论的构建与应用方法；第 3 节提出基于类型论构建计算基础的问题陈述；第 4 节给出该理论的基本构造；结论部分简要总结本研究的主要发现。

2 相关工作

从历史上看，类型论最初产生于数学基础研究中，旨在保障所用构造的一致性 [11]。随后，基于类型的方法被用于定义 λ 演算的不同变体 [12]；类型论亦被应用于数理逻辑，其中尤以高阶逻辑（higher-order logics）的构建最为引人注目 [13]，但此类系统在实际应用中显得相当繁复笨重。

与此同时，类型概念亦在编程语言设计任务中被独立研究。最初，类型被理解为计算机中数据的不同表示方式；但人们很快意识到，这种理解严重限制了语言的表达能力，因而开始探索更广泛的类型定义。然而，许多研究对“类型”概念仅作启发式阐释，削弱了该方法的实际成效。

上述两种路径的融合发生在函数式语言 ML [16] 与 Haskell [17] 的设计过程中：研究者首次为特定编程语言提出了形式化的类型理论，并配套设计了理论上可靠的语言表达式类型检查算法。该方法旋即被拓展至更广泛的编程语言类，如今已成为语言设计的准标准工具。

当前，在实用信息系统开发中涌现出一系列新问题，亟需工具支持，例如：探究多样化的对象识别方式、追踪对象的“信息路径”（information route）、考虑对象状态的动态变化等。因此，有必要拓展计算的理论基础，以构建可被工具直接且可证明地支持的计算模型。

3 计算基础的构建问题

对计算的理论基础 [1] 及其开发所用方法与工具的研究，使我们可将计算基础的构建问题明确为：基于理论方法创建具备以下能力的计算模型的任务：

• 提供足够灵活的工具，用于定义基本对象类型，包括支持类型的参数化；
• 定义参数化类型的基本对象；
• 定义结构化类型及其相应对象；
• 支持指定类型对象的自动化构造；
• 协调类型与其对应对象的性质，确保能以计算环境中的对象形式构造性质的证明；
• 支持高阶归纳类型的构造，并确立相应的归纳原理。

4 计算基础的基本构造

我们视上下文（contexts）为变量到类型的赋值集合，并视宇宙（universes）为给定层级中所有类型的类型。形式化描述是直接的（straightforward）。

我们将采用结构化规则：Var 规则（见下文），用于从相应上下文中推导变量的类型；以及通常的弱化规则（weakening）与代换规则（substitution）。

判断相等性是一种等价关系，即满足通常的自反性、对称性与传递性条件。 此外，所有用于构造类型与对象的规则均允许：将其内部所含表达式替换为在判断中与之相等的表达式。

4.1 依赖函数

其他可视为多态的函数亦以类似方式处理。 多态性是一种函数参数化的方式，但并非普适；后续将探讨更为精细的参数化设定方法。

4.2 依赖对（Dependent Pairs） 下面我们考察适用于依赖对的规则。

例 2. 依赖对的递归与归纳。 依赖对的递归与归纳通过 Σ-ELIM 和 Σ-COMP 原则进行。下面我们考虑在此情形下出现的各种特殊情况。

2.1 依赖对的递归

我们考虑一般形式的依赖对，但假设其结果类型是固定的。因此，我们希望得到：

2.2 一般形式依赖对的归纳

我们考察最一般的情形：依赖对的两个分量以及结果类型均具有依赖性。我们希望得到：

5 结论

本文提出了一种类型论的构造方案，该方案支持计算基本构件的构建，并能以计算环境中相应对象的形式证明其性质。

1. 基于类型与值的使用，构建了类型与对象的计算模型；主要考察两类表达式：
   • a:A （“对象 a 具有类型 A”）
   • a≡b（“对象 a 与 b 在判断中相等”）。
2. 该计算模型基于同伦类型论构建，可由具备依赖类型的函数式编程语言予以支持。
3. 模型以上下文为参数，这些上下文包含自由变量；在对对象应用归纳原理时，这些变量被关联绑定。
4. 计算通过将函数作用于具有典范形式（canonical form）的对象来执行，随后将该典范形式对象代入相应变量位置完成替

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