Quotients of Bounded Natural Functors
Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › fagfællebedømt
Standard
Quotients of Bounded Natural Functors. / Fürer, Basil; Lochbihler, Andreas; Schneider, Joshua; Traytel, Dmitriy.
I: Logical Methods in Computer Science, Bind 18, Nr. 1, 23, 2022, s. 1-28.Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › fagfællebedømt
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - JOUR
T1 - Quotients of Bounded Natural Functors
AU - Fürer, Basil
AU - Lochbihler, Andreas
AU - Schneider, Joshua
AU - Traytel, Dmitriy
N1 - Publisher Copyright: © B. Fürer, A. Lochbihler, J. Schneider, and D. Traytel.
PY - 2022
Y1 - 2022
N2 - 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.
AB - 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.
KW - Functors
KW - Higher-order logic
KW - Inductive and coinductive datatypes
KW - Proof assistants
KW - Quotient types
UR - http://www.scopus.com/inward/record.url?scp=85124708144&partnerID=8YFLogxK
U2 - 10.46298/LMCS-18(1:23)2022
DO - 10.46298/LMCS-18(1:23)2022
M3 - Journal article
AN - SCOPUS:85124708144
VL - 18
SP - 1
EP - 28
JO - Logical Methods in Computer Science
JF - Logical Methods in Computer Science
SN - 1860-5974
IS - 1
M1 - 23
ER -
ID: 309119610