Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP article: Bounded Natural Functors with...


view this post on Zulip Email Gateway (Aug 22 2022 at 17:07):

From: Tobias Nipkow <nipkow@in.tum.de>
Bounded Natural Functors with Covariance and Contravariance
Andreas Lochbihler and Joshua Schneider

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 BNF_CC that extends the mapper and relator to covariant and
contravariant parameters. We show that

  1. BNF_CCs are closed under functor composition and least and greatest fixpoints,
  2. subtypes inherit the BNF_CC structure under conditions that generalise those
    for the BNF case, and

  3. BNF_CCs preserve quotients under mild conditions.

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

https://www.isa-afp.org/entries/BNF_CC.html

Enjoy!
smime.p7s

view this post on Zulip Email Gateway (Aug 22 2022 at 17:07):

From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Tobias Nipkow wrote:

Bounded Natural Functors with Covariance and Contravariance
Andreas Lochbihler and Joshua Schneider
[...]

I'm not sure if I understand this correctly. Could this bring us closer
to obtaining a map function for 'a set, and hence for datatypes
involving sets?

datatype 'a foo = foo "('a × 'a) set"

(* no map_foo is provided since none of the arguments admit recursion *)

(The argument of set is special in that it admits both a contravariant
view (by viewing sets as predicates) and a covariant view with the
f ` X being corresponding map function -- it's the latter that I would
like to have as a map function...)

Cheers,

Bertram

view this post on Zulip Email Gateway (Aug 22 2022 at 17:07):

From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Dear Bertram,

You are right. This entry provides exactly the theory for getting such a map function (and
also a relator). For your example, you would precisely get the covariant map (but you
still cannot do (co)datatype recursion through such non-live covariant arguments). You can
also go crazy as in

datatype ('a, 'b) bar = Bar "(('a * 'a) set => 'b) => 'a list"

The construction gives you a map function that is covariant in 'a and contravariant in 'b.

The entry formalises the constructions for an abstract functor and for a few examples.
There's no automation yet, so you have to intelligently copy-n-paste. I have used these
constructions and proofs for quite complicated (co)datatypes. Joshua and I have a paper on
the theory at ITP this year. A preliminary draft is available on my homepage:

http://www.andreas-lochbihler.de/pub/lochbihlerschneider2018.pdf

Best,
Andreas


Last updated: Mar 29 2024 at 12:28 UTC