有界自然函子的商
Quotients of Bounded Natural Functors
AI总结：
本文研究有界自然函子（BNF）在商操作下的保持性，提出更一般的提升方案并扩展Isabelle/HOL自动注册商类型为BNF，减轻用户证明负担。
摘要：
类型构造子的函子结构是高阶逻辑（HOL）中许多定义和证明原理的基础。例如，归纳和余归纳数据类型可以从有界自然函子（BNFs）模块化地构建，这是一类行为良好的类型构造子。已知组合、不动点以及在特定条件下的子类型可以保持BNF结构。在本文中，我们探讨商的保持问题，这是在HOL中引入新类型的最后一个重要原理。我们识别出商从其底层类型继承BNF结构的充分条件。令人惊讶的是，以显而易见的方式提升结构对某些商是失败的，这个问题也影响了Lean证明助手中使用的多项式函子的商。我们提供了一个严格更一般的提升方案，支持此类有问题的商。我们扩展了Isabelle/HOL证明助手，添加了一个命令，自动将商类型注册为BNF，将用户的证明负担从完整的BNF公理集减少到我们的继承条件。我们通过几个案例研究展示了该命令的实用性。
英文摘要：
The functorial structure of type constructors is the foundation for many definition and proof principles in higher-order logic (HOL). For example, inductive and coinductive datatypes can be built modularly from bounded natural functors (BNFs), a class of well-behaved type constructors. Composition, fixpoints, and, under certain conditions, subtypes are known to preserve the BNF structure. In this article, we tackle the preservation question for quotients, the last important principle for introducing new types in HOL. We identify sufficient conditions under which a quotient inherits the BNF structure from its underlying type. Surprisingly, lifting the structure in the obvious manner fails for some quotients, a problem that also affects the quotients of polynomial functors used in the Lean proof assistant. We provide a strictly more general lifting scheme that supports such problematic quotients. We extend the Isabelle/HOL proof assistant with a command that automates the registration of a quotient type as a BNF, reducing the proof burden on the user from the full set of BNF axioms to our inheritance conditions. We demonstrate the command's usefulness through several case studies.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
