Alonzo 中的幺半群理论：简单类型论中的小理论形式化

Alonzo 是一种面向实践的古典高阶谓词逻辑版本，它扩展了一阶逻辑并允许未定义表达式。为纪念 Alonzo Church，Alonzo 基于 Church 类型论，即 Church 提出的简单类型论。小理论方法是一种将数学知识形式化为理论图的方法，该理论图以理论为节点，以理论态射为有向边。某一数学主题的发展在理论图中具有最方便的抽象层级和最方便词汇的“小理论”中进行，随后，发展中产生的定义和定理根据需要，通过理论图中的理论态射传输至其他理论。本文旨在说明如何使用小理论方法在 Alonzo 中形式化一个数学知识体系。这是通过在 Alonzo 中形式化幺半群理论——关于幺半群的数学知识体系——来实现的。我们没有使用标准的形式化数学方法（即借助证明助手进行数学推演，所有细节均经过形式证明和机械检查），而是采用了一种替代方法，其中一切均在形式逻辑内完成，但不要求证明完全形式化。标准方法侧重于认证，而这种替代方法侧重于交流与可及性。