|
Bounded
Natural
Functors
with
Covariance
and
Contravariance
Title: |
Bounded Natural Functors with Covariance and Contravariance |
Authors:
|
Andreas Lochbihler and
Joshua Schneider
|
Submission date: |
2018-04-24 |
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
- BNFCCs are closed under
functor composition and least and greatest fixpoints,
- subtypes inherit the BNFCC structure
under conditions that generalise those for the BNF case,
and
- 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. |
BibTeX: |
@article{BNF_CC-AFP,
author = {Andreas Lochbihler and Joshua Schneider},
title = {Bounded Natural Functors with Covariance and Contravariance},
journal = {Archive of Formal Proofs},
month = apr,
year = 2018,
note = {\url{https://isa-afp.org/entries/BNF_CC.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Status: [ok] |
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.
|
|