一句话：提出商类型继承 BNF 结构的充分条件与更一般提升方案，并在 Isabelle/HOL 中自动化商类型的 BNF 注册。
在 HOL 中，有界自然函子（BNF）为归纳与余归纳数据类型提供模块化定义与证明原则，但商类型能否保持 BNF 结构尚不清楚。本文研究商类型对 BNF 结构的保持问题，给出使其从底层类型继承 BNF 的充分条件；指出按显然方式提升对某些商会失败，包括 Lean 中多项式函子的商。作者提出一个严格更一般的提升方案来覆盖这些有问题情形，并在 Isabelle/HOL 中实现自动化命令，将用户证明负担从验证全部 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.
@article{paperbot1731,
title = {Quotients of Bounded Natural Functors},
author = {Basil Fürer and Andreas Lochbihler and Joshua Schneider and Dmitriy Traytel},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 1},
year = {2022},
doi = {10.46298/lmcs-18(1:23)2022}
}