Basil Fürer ; Andreas Lochbihler ; Joshua Schneider ; Dmitriy Traytel - Quotients of Bounded Natural Functors

lmcs:7354 - Logical Methods in Computer Science, February 1, 2022, Volume 18, Issue 1 - https://doi.org/10.46298/lmcs-18(1:23)2022
Quotients of Bounded Natural Functors

Authors: Basil Fürer ; Andreas Lochbihler ; Joshua Schneider ; Dmitriy Traytel

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.


Volume: Volume 18, Issue 1
Published on: February 1, 2022
Accepted on: October 28, 2021
Submitted on: April 13, 2021
Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages


Share

Consultation statistics

This page has been seen 340 times.
This article's PDF has been downloaded 461 times.