Cargando…
Quotients of Bounded Natural Functors
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,...
Autores principales: | , , , |
---|---|
Formato: | Online Artículo Texto |
Lenguaje: | English |
Publicado: |
2020
|
Materias: | |
Acceso en línea: | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324035/ http://dx.doi.org/10.1007/978-3-030-51054-1_4 |
_version_ | 1783551867946532864 |
---|---|
author | Fürer, Basil Lochbihler, Andreas Schneider, Joshua Traytel, Dmitriy |
author_facet | Fürer, Basil Lochbihler, Andreas Schneider, Joshua Traytel, Dmitriy |
author_sort | Fürer, Basil |
collection | PubMed |
description | 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 paper, 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. We extend the Isabelle proof assistant with a command that automates the registration of a quotient type as a BNF by lifting the underlying type’s BNF structure. We demonstrate the command’s usefulness through several case studies. |
format | Online Article Text |
id | pubmed-7324035 |
institution | National Center for Biotechnology Information |
language | English |
publishDate | 2020 |
record_format | MEDLINE/PubMed |
spelling | pubmed-73240352020-06-30 Quotients of Bounded Natural Functors Fürer, Basil Lochbihler, Andreas Schneider, Joshua Traytel, Dmitriy Automated Reasoning Article 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 paper, 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. We extend the Isabelle proof assistant with a command that automates the registration of a quotient type as a BNF by lifting the underlying type’s BNF structure. We demonstrate the command’s usefulness through several case studies. 2020-06-06 /pmc/articles/PMC7324035/ http://dx.doi.org/10.1007/978-3-030-51054-1_4 Text en © Springer Nature Switzerland AG 2020 This article is made available via the PMC Open Access Subset for unrestricted research re-use and secondary analysis in any form or by any means with acknowledgement of the original source. These permissions are granted for the duration of the World Health Organization (WHO) declaration of COVID-19 as a global pandemic. |
spellingShingle | Article Fürer, Basil Lochbihler, Andreas Schneider, Joshua Traytel, Dmitriy Quotients of Bounded Natural Functors |
title | Quotients of Bounded Natural Functors |
title_full | Quotients of Bounded Natural Functors |
title_fullStr | Quotients of Bounded Natural Functors |
title_full_unstemmed | Quotients of Bounded Natural Functors |
title_short | Quotients of Bounded Natural Functors |
title_sort | quotients of bounded natural functors |
topic | Article |
url | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324035/ http://dx.doi.org/10.1007/978-3-030-51054-1_4 |
work_keys_str_mv | AT furerbasil quotientsofboundednaturalfunctors AT lochbihlerandreas quotientsofboundednaturalfunctors AT schneiderjoshua quotientsofboundednaturalfunctors AT trayteldmitriy quotientsofboundednaturalfunctors |