### Abstract

Bounded natural functors (BNFs) provide a modular framework for the construction of (co)datatypes in higher-order logic. Their functorial operations, the mapper and relator, are restricted to a subset of the parameters, namely those where recursion can take place. For certain applications, such as free theorems, data refinement, quotients, and generalised rewriting, it is desirable that these operations do not ignore the other parameters. In this article, we formalise the generalisation BNFCC that extends the mapper and relator to covariant and contravariant parameters. We show that

1. BNFCCs are closed under functor composition and least and greatest fixpoints,
2. subtypes inherit the BNFCC structure under conditions that generalise those for the BNF case, and
3. BNFCCs preserve quotients under mild conditions.

These proofs are carried out for abstract BNFCCs similar to the AFP entry BNF Operations. In addition, we apply the BNFCC theory to several concrete functors.

### License

BSD License

### Topics

- Computer science/Functional programming
- Tools

### Session BNF_CC

- Preliminaries
- Axiomatised_BNF_CC
- Composition
- Fixpoints
- Subtypes
- Quotient_Preservation
- Operation_Examples
- Concrete_Examples
- DDS

## Cite

×

BNF_CC-AFP

    @article{BNF_CC-AFP,
      author  = {Andreas Lochbihler and Joshua Schneider},
      title   = {Bounded Natural Functors with Covariance and Contravariance},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2018},
      note    = {\url{https://isa-afp.org/entries/BNF_CC.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Apr 25, 2018 : Isabelle2017