类型化语法与语义的初始性

本论文对简单类型化语言的语法和语义进行了代数刻画。更确切地说，我们通过一个泛性质，即作为某个范畴的初始对象，来刻画配备归约规则的简单类型化绑定语法。我们通过一个 2-签名 ($\Sigma$, A) 来指定一种语言，这是一个两层级的签名：语法层级 $\Sigma$ 指定语言的 sorts 和项，并为每个项关联一个 sort；语义层级 A 通过不等式指定语言项上的归约规则。对于任何给定的 2-签名 ($\Sigma$, A)，我们关联一个 ($\Sigma$, A) 的“模型”范畴。我们证明该范畴具有一个初始对象，它整合了由 $\Sigma$ 自由生成的项以及由 A 生成的（在这些项上的）归约关系。我们将此对象称为由 ($\Sigma$, A) 生成的编程语言。初始性提供了一个迭代原理，允许指定语法上的翻译，可能是翻译到具有不同 sorts 的语言。此外，通过迭代原理指定的翻译在构造上就是类型安全且关于归约忠实的。为了说明我们的结果，我们详细考虑了两个例子：首先，我们通过范畴论迭代原理指定了从经典命题逻辑到直觉主义命题逻辑的双重否定翻译；其次，我们指定了从 PCF 到无类型 lambda 演算的翻译，该翻译关于源语言和目标语言中的归约均是忠实的。在第二部分中，我们在证明助手 Coq 中形式化了部分初始性定理。该实现产生了一套机制，当给定一个 2-签名时，返回其相关抽象语法的实现，以及经认证的替换操作、迭代算子和由指定归约规则生成的归约关系。